A Really Temporal Logic

Alur, Rajeev; Henzinger, Thomas A.

dc.contributor.author	Alur, Rajeev	en_US
dc.contributor.author	Henzinger, Thomas A.	en_US
dc.date.accessioned	2007-04-23T16:27:12Z
dc.date.available	2007-04-23T16:27:12Z
dc.date.issued	1992-11	en_US
dc.identifier.citation	http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR92-1310	en_US
dc.identifier.uri	https://hdl.handle.net/1813/6088
dc.description.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.	en_US
dc.format.extent	2697653 bytes
dc.format.extent	840912 bytes
dc.format.mimetype	application/pdf
dc.format.mimetype	application/postscript
dc.language.iso	en_US	en_US
dc.publisher	Cornell University	en_US
dc.subject	computer science	en_US
dc.subject	technical report	en_US
dc.title	A Really Temporal Logic	en_US
dc.type	technical report	en_US