A REALLY TEMPORAL LOGIC

Authors
ALUR R HENZINGER TA
Citation
R. Alur et Ta. Henzinger, A REALLY TEMPORAL LOGIC, Journal of the Association for Computing Machinery, 41(1), 1994, pp. 181-204
Citations number
32
Categorie Soggetti
Computer Sciences","Computer Science Hardware & Architecture
Journal title
Journal of the Association for Computing Machinery
ISSN journal
00045411 → ACNP
Volume
41
Issue
1
Year of publication
1994
Pages
181 - 204
Database
ISI
SICI code
Abstract
We introduce a temporal logic for the specification of real-time syste ms. Our logic, TPTL, employs a novel quantifier construct for referenc ing time: the freeze quantifier binds a variable to the time of the lo cal temporal context. TPTL is both a natural language for specificatio n and a suitable formalism for verification. We present a tableau-base d decision procedure and a model-checking algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.