Jaziri, Samy6; Larsen, Kim Guldstrand3; Mardare, Radu Iulian1; Xue, Bingtian7
Bart Jacobs, Alexandra Silva, Sam Staton
1 Department of Computer Science, The Faculty of Engineering and Science (ENG), Aalborg University, VBN2 The Faculty of Engineering and Science (TECH), Aalborg University, VBN3 CISS - Center for Embedded Software Systems, The Faculty of Engineering and Science (ENG), Aalborg University, VBN4 Distributed Systems and Semantics, The Faculty of Engineering and Science (ENG), Aalborg University, VBN5 Aalborg U Robotics, The Faculty of Humanities, Aalborg University, VBN6 ENS, Lab Specificat & Verificat, F-94235 Cachan7 Distributed, Embedded and Intelligent Systems, The Faculty of Engineering and Science (ENG), Aalborg University, VBN
In this paper we develop the metatheory for Timed Modal Logic (TML), which is the modal logic used for the analysis of timed transition systems (TTSs). We solve a series of long-standing open problems related to TML. Firstly, we prove that TML enjoys the Hennessy-Milner property and solve one of the open questions in the field. Secondly, we prove that the set of validities are not recursively enumerable. Nevertheless, we develop a strongly-complete proof system for TML. Since the logic is not compact, the proof system contains infinitary rules, but only with countable sets of instances. Thus, we can involve topological results regarding Stone spaces, such as the Rasiowa-Sikorski lemma, to complete the proofs.
Electronic Notes in Theoretical Computer Science: Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (mfps Xxx), 2014, p. 183-210