State clock logic: A decidable real-time logic

Jean François Raskin, Pierre Yves Schobbens

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é

In this paper we define a real-time logic called SC logic. This logic is defined in the framework of State Clock automata, the state variant of the Event Clock automata of Alur et al [6]. Unlike timed automata [4], they are complementable and thus language inclusion becomes decidable. SC automata and SC logic are less expressive than timed automata and MITL but seem expressive enough in practice. A procedure to translate each SC formula into a SC automaton is presented. The main contribution of this paper is to complete the framework of this class of determinizable automata with a temporal logic and to introduce the notion of event clock in the domain of temporal logic.

langue originaleAnglais
titreHybrid and Real-Time Systems - International Workshop, HART 1997, Proceedings
EditeurSpringer Verlag
Pages33-47
Nombre de pages15
ISBN (imprimé)354062600X, 9783540626008
Les DOIs
Etat de la publicationPublié - 1 janv. 1997
EvénementInternational Workshop on Hybrid And Real-Time Systems, HART 1997 - Grenoble, France
Durée: 26 mars 199728 mars 1997

Série de publications

NomLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1201
ISSN (imprimé)0302-9743
ISSN (Electronique)1611-3349

Une conférence

Une conférenceInternational Workshop on Hybrid And Real-Time Systems, HART 1997
Pays/TerritoireFrance
La villeGrenoble
période26/03/9728/03/97

Empreinte digitale

Examiner les sujets de recherche de « State clock logic: A decidable real-time logic ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation