Adequacy and Complete Axiomatization for Timed Modal Logic

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

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

5 Citationer (Scopus)

Resumé

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.
OriginalsprogEngelsk
TitelElectronic Notes in Theoretical Computer Science : Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX)
RedaktørerBart Jacobs, Alexandra Silva, Sam Staton
Antal sider28
Vol/bind308
Udgivelses stedIthaca, New York
ForlagElsevier
Publikationsdato2014
Sider183-210
DOI
StatusUdgivet - 2014
Begivenhed Mathematical Foundations of Programming Semantics - Cornell University, Ithaca, New York, USA
Varighed: 12 jun. 201415 jun. 2014
Konferencens nummer: 30

Konference

Konference Mathematical Foundations of Programming Semantics
Nummer30
LokationCornell University
LandUSA
ByIthaca, New York
Periode12/06/201415/06/2014
NavnElectronic Notes in Theoretical Computer Science
Vol/bind308
ISSN1571-0661

Citer dette

Jaziri, S., Larsen, K. G., Mardare, R. I., & Xue, B. (2014). Adequacy and Complete Axiomatization for Timed Modal Logic. I B. Jacobs, A. Silva, & S. Staton (red.), Electronic Notes in Theoretical Computer Science: Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX) (Bind 308, s. 183-210). Ithaca, New York: Elsevier. Electronic Notes in Theoretical Computer Science, Bind. 308 https://doi.org/10.1016/j.entcs.2014.10.011
Jaziri, Samy ; Larsen, Kim Guldstrand ; Mardare, Radu Iulian ; Xue, Bingtian. / 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). red. / Bart Jacobs ; Alexandra Silva ; Sam Staton. Bind 308 Ithaca, New York : Elsevier, 2014. s. 183-210 (Electronic Notes in Theoretical Computer Science, Bind 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",

}

Jaziri, S, Larsen, KG, Mardare, RI & Xue, B 2014, Adequacy and Complete Axiomatization for Timed Modal Logic. i B Jacobs, A Silva & S Staton (red), Electronic Notes in Theoretical Computer Science: Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX). bind 308, Elsevier, Ithaca, New York, Electronic Notes in Theoretical Computer Science, bind 308, s. 183-210, Ithaca, New York, USA, 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; Xue, Bingtian.

Electronic Notes in Theoretical Computer Science: Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX). red. / Bart Jacobs; Alexandra Silva; Sam Staton. Bind 308 Ithaca, New York : Elsevier, 2014. s. 183-210 (Electronic Notes in Theoretical Computer Science, Bind 308).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer 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

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

ER -

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