Adequacy and complete axiomatization for Timed Modal Logic
Jaziri, Samy and Larsen, Kim G. and Mardare, Radu and Xue, Bingtian (2014) Adequacy and complete axiomatization for Timed Modal Logic. Electronic Notes in Theoretical Computer Science, 308. pp. 183-210. ISSN 1571-0661 (https://doi.org/10.1016/j.entcs.2014.10.011)
Preview |
Text.
Filename: Jaziri_etal_ENTCS_2014_Adequacy_and_complete_axiomatization_for_Timed_Modal_Logic.pdf
Final Published Version License: Download (376kB)| Preview |
Abstract
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.
-
-
Item type: Article ID code: 70429 Dates: DateEvent29 October 2014PublishedSubjects: Science > Mathematics > Electronic computers. Computer science Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 05 Nov 2019 14:32 Last modified: 04 Sep 2024 01:04 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/70429