Este artículo aborda el problema de sintetizar expresiones regulares temporizadas (Timed Regular Expressions), un formato para especificar el comportamiento en tiempo real de sistemas ciberfísicos. Se centra en la generación de expresiones regulares temporizadas que coincidan con un conjunto dado de comportamientos del sistema, incluyendo ejemplos tanto positivos como negativos. Demostramos la decidibilidad del problema de síntesis explorando expresiones regulares temporizadas simples y proponemos un método para generar expresiones regulares temporizadas coincidentes con una longitud mínima. Este método consiste en enumerar y podar expresiones regulares temporizadas paramétricas candidatas, y luego codificar los requisitos que las candidatas generadas coinciden con el conjunto dado en una fórmula de teorías de módulo de satisfacibilidad (SMT) para determinar soluciones a las restricciones temporizadas paramétricas. Finalmente, evaluamos el método propuesto en puntos de referencia que incluyen comportamientos generados aleatoriamente a partir de un modelo de temporización objetivo y un caso práctico.
