Axioms for Real-Time Logics

Jean-Francois Raskin, Pierre-Yves Schobbens, Thomas Henzinger

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

Résumé

This paper presents a complete axiomatization of fully decidable propositional real-time linear temporal logics with past: the Event Clock Logic (ECL) and the Metric Interval Temporal Logic with past (MITL). The completeness proof consists of an effective proof building procedure for ECL. From this result we obtain a complete axiomatization of MITL by providing axioms that allows the translation of MITL formulae into ECL formulae, the two logics being equally expressive. Our proof is structured to yield a similar axiomatization and procedure for interesting fragments of this logic: the linear temporal logic of the real numbers (LTR), the fragment with only past clocks.
langue originaleAnglais
titreCONCUR'98
Sous-titre9th International Conference on Concurrency Theory
rédacteurs en chefD Sangiorgi, R de
EditeurSpringer Verlag
Volume1466
Etat de la publicationPublié - 1998

Empreinte digitale

Examiner les sujets de recherche de « Axioms for Real-Time Logics ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation