2025/09/08 by Ziran Wang, Jie An, Wang, Ziran +7
Biochemistry, Genetics and Molecular Biology · Computer Science · #Algorithms and Data Compression #Artificial Intelligence (cs.AI) #DNA and Biological Computing #Evolutionary Algorithms and Applications #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL)
paper · pdf · doi:10.48550/arxiv.2509.06262
openalex publication_date 2025/09/08 · openalex created_date 2025/10/11 · openalex updated_date 2026/07/28
Timed regular expressions serve as a formalism for specifying real-time behaviors of Cyber-Physical Systems. In this paper, we consider the synthesis of timed regular expressions, focusing on generating a timed regular expression consistent with a given set of system behaviors including positive and negative examples, i.e., accepting all positive examples and rejecting all negative examples. We first prove the decidability of the synthesis problem through an exploration of simple timed regular expressions. Subsequently, we propose our method of generating a consistent timed regular expression with minimal length, which unfolds in two steps. The first step is to enumerate and prune candidate parametric timed regular expressions. In the second step, we encode the requirement that a candidate generated by the first step is consistent with the given set into a Satisfiability Modulo Theories (SMT) formula, which is consequently solved to determine a solution to parametric time constraints. Finally, we evaluate our approach on benchmarks, including randomly generated behaviors from target timed models and a case study.