@inbook{4590,
  abstract     = {We introduce a temporal logic for the specification of real-time systems. Our logic, TPTL, employs a novel quantifier construct for referencing time: the "freeze" quantifier binds a variable to the time of the local temporal context. TPTL is both a natural language for specification and a suitable formalism for verification. We present a tableau-based decision procedure and a model-checking algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.},
  author       = {Alur, Rajeev and Henzinger, Thomas A},
  booktitle    = {Theories and Experiences for Real-Time System Development},
  editor       = {Rus, Teodor and Rattray, Charles},
  isbn         = { 9789810219239},
  keywords     = {real-time systems, clock variables},
  pages        = {1 -- 29},
  publisher    = {World Scientific Publishing},
  title        = {{Real-time system = discrete system + clock variables}},
  doi          = {10.1142/9789812831583_0001},
  volume       = {2},
  year         = {1994},
}