Adequacy and complete axiomatization for Timed Modal Logic

Samy Jaziri*, Kim G. Larsen, Radu Mardare, Bingtian Xue

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

5 Citations (Scopus)
12 Downloads (Pure)


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.

Original languageEnglish
Pages (from-to)183-210
Number of pages28
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 29 Oct 2014


  • complete axiomatization
  • non-compact modal logics
  • timed modal logic


Dive into the research topics of 'Adequacy and complete axiomatization for Timed Modal Logic'. Together they form a unique fingerprint.

Cite this