El valor de la verificación de sistemas ciberfísicos depende de la relación entre el estado del software y el estado del sistema físico. Esta relación puede ser compleja debido a la naturaleza en tiempo real y a las diferentes líneas temporales de la planta física, los sensores y actuadores, y el software que casi siempre es concurrente y distribuido. En este documento, estudiamos diferentes formas de construir un modelo de sistema de transición para los componentes de software distribuidos y concurrentes de un CPS. El propósito del modelo de sistema de transición es permitir la verificación del modelo, una técnica de verificación establecida y ampliamente utilizada. Describimos un modelo de sistema de transición basado en tiempo lógico, que se utiliza comúnmente para verificar programas escritos en lenguajes síncronos, y derivamos las condiciones bajo las cuales dicho modelo refleja fielmente los estados físicos. Cuando estas condiciones no se cumplen (una situación común), puede ser necesario un modelo de sistema de transición basado en eventos más detallado. Proponemos un enfoque para la verificación formal de sistemas ciberfísicos utilizando Lingua Franca, un lenguaje diseñado para programar sistemas ciberfísicos, y Rebeca, un lenguaje basado en actores diseñado para verificar modelos de sistemas distribuidos basados en eventos. Nos enfocamos en la parte cibernética y modelamos una interfaz fiel a la parte física. Nuestro método se basa en la suposición de que la alineación de diferentes líneas temporales durante la ejecución del sistema es responsabilidad de las plataformas subyacentes. Hacemos esas suposiciones explícitas y claras.