@inproceedings{6556258e117640d195cecce55b03d06b,
title = "State clock logic: A decidable real-time logic",
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.",
author = "Raskin, {Jean Fran{\c c}ois} and Schobbens, {Pierre Yves}",
year = "1997",
month = jan,
day = "1",
doi = "10.1007/BFb0014711",
language = "English",
isbn = "354062600X",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "33--47",
booktitle = "Hybrid and Real-Time Systems - International Workshop, HART 1997, Proceedings",
address = "Germany",
note = "International Workshop on Hybrid And Real-Time Systems, HART 1997 ; Conference date: 26-03-1997 Through 28-03-1997",
}