Adequacy and complete axiomatization for Timed Modal Logic

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

Research output: Contribution to journalArticle

5 Citations (Scopus)

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.

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

Fingerprint

Axiomatization
Modal Logic
Proof System
Stone Space
Transition Systems
Countable
Lemma
Open Problems
Logic
Series

Keywords

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

Cite this

Jaziri, Samy ; Larsen, Kim G. ; Mardare, Radu ; Xue, Bingtian. / Adequacy and complete axiomatization for Timed Modal Logic. In: Electronic Notes in Theoretical Computer Science. 2014 ; Vol. 308. pp. 183-210.
@article{45097182863d4378be4559610d012257,
title = "Adequacy and complete axiomatization for Timed Modal Logic",
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.",
keywords = "complete axiomatization, non-compact modal logics, timed modal logic",
author = "Samy Jaziri and Larsen, {Kim G.} and Radu Mardare and Bingtian Xue",
year = "2014",
month = "10",
day = "29",
doi = "10.1016/j.entcs.2014.10.011",
language = "English",
volume = "308",
pages = "183--210",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",

}

Adequacy and complete axiomatization for Timed Modal Logic. / Jaziri, Samy; Larsen, Kim G.; Mardare, Radu; Xue, Bingtian.

In: Electronic Notes in Theoretical Computer Science, Vol. 308, 29.10.2014, p. 183-210.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Adequacy and complete axiomatization for Timed Modal Logic

AU - Jaziri, Samy

AU - Larsen, Kim G.

AU - Mardare, Radu

AU - Xue, Bingtian

PY - 2014/10/29

Y1 - 2014/10/29

N2 - 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.

AB - 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.

KW - complete axiomatization

KW - non-compact modal logics

KW - timed modal logic

UR - http://www.scopus.com/inward/record.url?scp=84908389448&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2014.10.011

DO - 10.1016/j.entcs.2014.10.011

M3 - Article

VL - 308

SP - 183

EP - 210

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -