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

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

5 Citationer (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.

Originalsprog	Engelsk
Titel	Electronic Notes in Theoretical Computer Science : Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX)
Redaktører	Bart Jacobs, Alexandra Silva, Sam Staton
Antal sider	28
Vol/bind	308
Udgivelsessted	Ithaca, New York
Forlag	Elsevier
Publikationsdato	2014
Sider	183-210
DOI	https://doi.org/10.1016/j.entcs.2014.10.011
Status	Udgivet - 2014
Begivenhed	Mathematical Foundations of Programming Semantics - Cornell University, Ithaca, New York, USA Varighed: 12 jun. 2014 → 15 jun. 2014 Konferencens nummer: 30

Konference

Konference	Mathematical Foundations of Programming Semantics
Nummer	30
Lokation	Cornell University
Land/Område	USA
By	Ithaca, New York
Periode	12/06/2014 → 15/06/2014

Navn	Electronic Notes in Theoretical Computer Science
Vol/bind	308
ISSN	1571-0661

Adgang til dokumentet

10.1016/j.entcs.2014.10.011

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

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
Projekter: Projekt › Forskning

Citationsformater

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). 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). 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",

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. 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, Mathematical Foundations of Programming Semantics, 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 et al.
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 proceeding › Konferenceartikel i proceeding › Forskning › 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. 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). doi: 10.1016/j.entcs.2014.10.011

Adequacy and Complete Axiomatization for Timed Modal Logic

Abstract

Konference

Adgang til dokumentet

AUB Link

Fingeraftryk

Projekter

IDEA4CPS: Foundations for Cyber-Physical Sytems

Citationsformater