State clock logic: A decidable real-time logic

Jean François Raskin, Pierre Yves Schobbens

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationHybrid and Real-Time Systems - International Workshop, HART 1997, Proceedings
PublisherSpringer Verlag
Pages33-47
Number of pages15
ISBN (Print)354062600X, 9783540626008
DOIs
Publication statusPublished - 1 Jan 1997
EventInternational Workshop on Hybrid And Real-Time Systems, HART 1997 - Grenoble, France
Duration: 26 Mar 199728 Mar 1997

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1201
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Workshop on Hybrid And Real-Time Systems, HART 1997
CountryFrance
CityGrenoble
Period26/03/9728/03/97

Fingerprint

Dive into the research topics of 'State clock logic: A decidable real-time logic'. Together they form a unique fingerprint.

Cite this