Adequacy and Complete Axiomatization for Timed Modal Logic

Samy Jaziri; Kim Guldstrand Larsen; Radu Iulian Mardare; Bingtian Xue

doi:10.1016/j.entcs.2014.10.011

Adequacy and Complete Axiomatization for Timed Modal Logic

Samy Jaziri, Kim Guldstrand Larsen, Radu Iulian Mardare, Bingtian Xue

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

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 language	English
Title of host publication	Electronic Notes in Theoretical Computer Science : Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX)
Editors	Bart Jacobs, Alexandra Silva, Sam Staton
Number of pages	28
Volume	308
Place of Publication	Ithaca, New York
Publisher	Elsevier
Publication date	2014
Pages	183-210
DOIs	https://doi.org/10.1016/j.entcs.2014.10.011
Publication status	Published - 2014
Event	Mathematical Foundations of Programming Semantics - Cornell University, Ithaca, New York, United States Duration: 12 Jun 2014 → 15 Jun 2014 Conference number: 30

Conference

Conference	Mathematical Foundations of Programming Semantics
Number	30
Location	Cornell University
Country/Territory	United States
City	Ithaca, New York
Period	12/06/2014 → 15/06/2014

Series	Electronic Notes in Theoretical Computer Science
Volume	308
ISSN	1571-0661

Keywords

Non-compact modal logics
, complete axiomatization
timed modal logic

Access to Document

10.1016/j.entcs.2014.10.011

AUB Link

Search for the material in Aalborg University Library's search engine

IDEA4CPS: Foundations for Cyber-Physical Sytems
Larsen, K. G., Skou, A., Nielsen, B., Bulychev, P., Ravn, A. P. & Poulsen, D. B.
01/04/2011 → 30/04/2015
Project: Research

Cite this

Jaziri, S., Larsen, K. G., Mardare, R. I., & Xue, B. (2014). Adequacy and Complete Axiomatization for Timed Modal Logic. In B. Jacobs, A. Silva, & S. Staton (Eds.), Electronic Notes in Theoretical Computer Science: Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX) (Vol. 308, pp. 183-210). Elsevier. https://doi.org/10.1016/j.entcs.2014.10.011

Jaziri, Samy ; Larsen, Kim Guldstrand ; Mardare, Radu Iulian et al. / Adequacy and Complete Axiomatization for Timed Modal Logic. Electronic Notes in Theoretical Computer Science: Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX). editor / Bart Jacobs ; Alexandra Silva ; Sam Staton. Vol. 308 Ithaca, New York : Elsevier, 2014. pp. 183-210 (Electronic Notes in Theoretical Computer Science, Vol. 308).

@inproceedings{27800d8c174d49c0aab61b6e21fb6c01,

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 = "Non-compact modal logics, , complete axiomatization, timed modal logic",

author = "Samy Jaziri and Larsen, {Kim Guldstrand} and Mardare, {Radu Iulian} and Bingtian Xue",

year = "2014",

doi = "10.1016/j.entcs.2014.10.011",

language = "English",

volume = "308",

series = "Electronic Notes in Theoretical Computer Science",

publisher = "Elsevier",

pages = "183--210",

editor = "Bart Jacobs and Alexandra Silva and Sam Staton",

booktitle = "Electronic Notes in Theoretical Computer Science",

address = "United Kingdom",

note = " Mathematical Foundations of Programming Semantics, MFPS ; Conference date: 12-06-2014 Through 15-06-2014",

}

Jaziri, S, Larsen, KG, Mardare, RI & Xue, B 2014, Adequacy and Complete Axiomatization for Timed Modal Logic. in B Jacobs, A Silva & S Staton (eds), Electronic Notes in Theoretical Computer Science: Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX). vol. 308, Elsevier, Ithaca, New York, Electronic Notes in Theoretical Computer Science, vol. 308, pp. 183-210, Mathematical Foundations of Programming Semantics, Ithaca, New York, United States, 12/06/2014. https://doi.org/10.1016/j.entcs.2014.10.011

Adequacy and Complete Axiomatization for Timed Modal Logic. / Jaziri, Samy; Larsen, Kim Guldstrand; Mardare, Radu Iulian et al.
Electronic Notes in Theoretical Computer Science: Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX). ed. / Bart Jacobs; Alexandra Silva; Sam Staton. Vol. 308 Ithaca, New York: Elsevier, 2014. p. 183-210 (Electronic Notes in Theoretical Computer Science, Vol. 308).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

TY - GEN

T1 - Adequacy and Complete Axiomatization for Timed Modal Logic

AU - Jaziri, Samy

AU - Larsen, Kim Guldstrand

AU - Mardare, Radu Iulian

AU - Xue, Bingtian

N1 - Conference code: 30

PY - 2014

Y1 - 2014

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 - Non-compact modal logics

KW - , complete axiomatization

KW - timed modal logic

U2 - 10.1016/j.entcs.2014.10.011

DO - 10.1016/j.entcs.2014.10.011

M3 - Article in proceeding

VL - 308

T3 - Electronic Notes in Theoretical Computer Science

SP - 183

EP - 210

BT - Electronic Notes in Theoretical Computer Science

A2 - Jacobs, Bart

A2 - Silva, Alexandra

A2 - Staton, Sam

PB - Elsevier

CY - Ithaca, New York

T2 - Mathematical Foundations of Programming Semantics

Y2 - 12 June 2014 through 15 June 2014

ER -

Jaziri S, Larsen KG, Mardare RI, Xue B. Adequacy and Complete Axiomatization for Timed Modal Logic. In Jacobs B, Silva A, Staton S, editors, Electronic Notes in Theoretical Computer Science: Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX). Vol. 308. Ithaca, New York: Elsevier. 2014. p. 183-210. (Electronic Notes in Theoretical Computer Science, Vol. 308). doi: 10.1016/j.entcs.2014.10.011

Adequacy and Complete Axiomatization for Timed Modal Logic

Abstract

Conference

Keywords

Access to Document

AUB Link

Fingerprint

Projects

IDEA4CPS: Foundations for Cyber-Physical Sytems

Cite this