---
_id: '4490'
abstract:
- lang: eng
text: "A specification formalism for reactive systems defines a class of Ω-languages.
We call a specification formalism fully decidable if it is constructively closed
under boolean operations and has a decidable satisfiability (nonemptiness) problem.
There are two important, robust classes of Ω-languages that are definable by fully
decidable formalisms. The Ω -reqular languages are definable by finite automata,
or equivalcntly, by the Sequential Calculus. The counter-free Ω-regular languages
are definable by temporal logic, or equivalcntly, by the first-order fragment
of the Sequential Calculus. The gap between both classes can be closed by finite
counting (using automata connectives), or equivalently, by projection (existential
second-order quantification over letters).\r\nA specification formalism for real-time
systems defines a class of timed Ω-langnages, whose letters have real-numbered
time stamps. Two popular ways of specifying timing constraints rely on the use
of clocks, and on the use of time bounds for temporal operators. However, temporal
logics with clocks or time bounds have undecidable satisfiability problems, and
finite automata with clocks (so-called timed automata) are not closed under complement.
Therefore, two fully decidable restrictions of these formalisms have been proposed.
In the first case, clocks are restricted to event clocks, which measure distances
to immediately preceding or succeeding events only. In the second case, time bounds
are restricted to nonsingular intervals, which cannot specify the exact punctuality
of events. We show that the resulting classes of timed Ω-languages are robust,
and we explain their relationship.\r\nFirst, we show that temporal logic with
event clocks defines the same class of timed Ω-languages as temporal logic with
nonsingular time bounds, and we identify a first-order monadic theory that also
defines this class. Second, we show that if the ability of finite counting is
added to these formalisms, we obtain the class of timed Ω-languages that are definable
by finite automata with event clocks, or equivalently, by a restricted second-order
extension of the monadic theory. Third, we show that if projection is added, we
obtain the class of timed Ω-languages that are definable by timed automata, or
equivalently, by a richer second-order extension of the monadic theory. These
results identify three robust classes of timed Ω-languages, of which the third,
while popular, is not definable by a, fully decidable formalism. By contrast,
the first two classes are definable by fully decidable formalisms from temporal
logic, from automata theory, and from monadic logic. Since the gap between these
two classes can be closed by finite counting, we dub them the timed Ω-regular
languages and the timed counter-free Ω-rcgular languages, respectively."
acknowledgement: This work is supported in part by the ONR YIP award N00014-95-1-0520,
the NSF CAREER award CCR-9501708, the NSF grant CCR-9504469, the ARO MURI grant
DAAH-04-96-1-0341, the SRC contract 97-DC-324.041, the Belgian National Fund for
Scientific Research (FNRS), the European Commission under WGs Aspire and Fireworks,
the Portuguese FCT, and by Belgacom.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Jean
full_name: Raskin, Jean
last_name: Raskin
- first_name: Pierre
full_name: Schobbens, Pierre
last_name: Schobbens
citation:
ama: 'Henzinger TA, Raskin J, Schobbens P. The regular real-time languages. In:
Proceedings of the 25th International Colloqium on Automata, Languages and
Programming. Vol 1443. Springer; 1998:580-591. doi:10.1007/BFb0055086'
apa: 'Henzinger, T. A., Raskin, J., & Schobbens, P. (1998). The regular real-time
languages. In Proceedings of the 25th International Colloqium on Automata,
Languages and Programming (Vol. 1443, pp. 580–591). Aalborg, Denmark: Springer.
https://doi.org/10.1007/BFb0055086'
chicago: Henzinger, Thomas A, Jean Raskin, and Pierre Schobbens. “The Regular Real-Time
Languages.” In Proceedings of the 25th International Colloqium on Automata,
Languages and Programming, 1443:580–91. Springer, 1998. https://doi.org/10.1007/BFb0055086.
ieee: T. A. Henzinger, J. Raskin, and P. Schobbens, “The regular real-time languages,”
in Proceedings of the 25th International Colloqium on Automata, Languages and
Programming, Aalborg, Denmark, 1998, vol. 1443, pp. 580–591.
ista: 'Henzinger TA, Raskin J, Schobbens P. 1998. The regular real-time languages.
Proceedings of the 25th International Colloqium on Automata, Languages and Programming.
ICALP: Automata, Languages and Programming, LNCS, vol. 1443, 580–591.'
mla: Henzinger, Thomas A., et al. “The Regular Real-Time Languages.” Proceedings
of the 25th International Colloqium on Automata, Languages and Programming,
vol. 1443, Springer, 1998, pp. 580–91, doi:10.1007/BFb0055086.
short: T.A. Henzinger, J. Raskin, P. Schobbens, in:, Proceedings of the 25th International
Colloqium on Automata, Languages and Programming, Springer, 1998, pp. 580–591.
conference:
end_date: 1998-07-17
location: Aalborg, Denmark
name: 'ICALP: Automata, Languages and Programming'
start_date: 1998-07-13
date_created: 2018-12-11T12:09:07Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-24T09:30:11Z
day: '01'
doi: 10.1007/BFb0055086
extern: '1'
intvolume: ' 1443'
language:
- iso: eng
month: '01'
oa_version: None
page: 580 - 591
publication: Proceedings of the 25th International Colloqium on Automata, Languages
and Programming
publication_identifier:
isbn:
- '9783540647812'
publication_status: published
publisher: Springer
publist_id: '241'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The regular real-time languages
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1443
year: '1998'
...