Synthia swMATH ID: 12933 Software Authors: Peter, H.-J., Ehlers, R., Mattmüller, R. Description: Synthia: Verification and synthesis for timed automata. Synthia is the first certifying model checker for open real-time systems modeled as networks of timed automata. The key innovation of Synthia is its ability to justify why a given system is correct by providing a correctness certificate to the user. Such certificates are easy-to-validate deductive proofs that only reflect the specification-critical properties of the system. Synthia can also handle partially implemented systems, in which case it certifies their realizability by synthesizing reference implementations for the unimplemented parts. In the analysis of timed automata, the main technical challenge is to efficiently represent the arising infinite state space. Synthia’s analysis algorithm is based on a novel abstraction refinement technique that enables a clean combination of binary decision diagrams with difference bound matrices for a symbolic representation of both the discrete control-related and the continuous part of the state space. Homepage: https://www.react.uni-saarland.de/tools/synthia/ Related Software: UPPAAL TIGA; Uppaal; PRISM; REDLIB; CMC; Kronos; ROS; NuSMV; PuRSUE; LTLMoP; GitHub; PRISM-games; Modechart; TINA; LOTOS; TAPAAL; Romeo; Tempo; CoVer; McAiT Cited in: 7 Publications all top 5 Cited by 16 Authors 3 Dingel, Juergen 3 Rudie, Karen 3 Waez, Md Tawhid Bin 2 Wąsowski, Andrzej 1 Bersani, Marcello Maria 1 Cleaveland, Rance 1 Finkbeiner, Bernd 1 Fontana, Peter 1 Jensen, Peter Gjøl 1 Larsen, Kim Guldstrand 1 Menghi, Claudio 1 Pelliccione, Patrizio 1 Peter, Hans-Jörg 1 Rossi, Matteo A. C. 1 Soldo, Matteo 1 Srba, Jiří Cited in 3 Serials 1 Formal Aspects of Computing 1 Discrete Event Dynamic Systems 1 Computer Science Review Cited in 3 Fields 6 Computer science (68-XX) 3 Systems theory; control (93-XX) 1 Dynamical systems and ergodic theory (37-XX) Citations by Year