@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}, }