The Automata and Applications team of LRE participated in the ANR-funded TiCKTaC project (2019–2023), which aimed to improve formal verification and synthesis of real-time systems using the timed automata formalism. The project focused on developing novel algorithms, alternative data structures, and richer specification techniques to enhance scalability and expressiveness in verifying systems with quantitative features such as execution time and energy consumption.
The project produced an open-source model checker, TChecker, implementing these advances and enabling systematic comparison of tools and algorithms. TiCKTaC applied its methods to practical case studies, including robotics planning and performance verification in train networks, validating the new algorithms and demonstrating their effectiveness on large-scale, real-world systems.
TiCKTaC was strongly committed to open science: all tools and software developed during the project were released under open-source licenses, facilitating reuse and further development by the research community.
Partners
Related Publications
[1]
Emily Clement • Nicolas Perrin-Gilbert • Philipp Schlehuber-Caissier. "Layered Controller Synthesis for Dynamic Multi-Agent Systems". Proceedings of the 21st International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'23). 2023. https://doi.org/10.1007/978-3-031-42626-1_4.
[2]
Sven Dziadek • Uli Fahrenberg • Philipp Schlehuber-Caissier. "Energy Problems in Finite and Timed Automata with Büchi Conditions". International Symposium on Formal Methods (FM). 2023. https://doi.org/10.1007/978-3-031-27481-7_14.