[{"quality_controlled":"1","oa_version":"None","language":[{"iso":"eng"}],"month":"01","doi":"10.1142/9789812831583_0001","day":"01","publication_status":"published","acknowledgement":"The authors thank Rance Cleaveland, Limor Fix, David Karr, Peter Kopke, Fred Schneider, and Bernhard Steffen for helpful comments.","main_file_link":[{"url":"https://link.springer.com/article/10.1007/s100090050007"}],"status":"public","citation":{"chicago":"Alur, Rajeev, and Thomas A Henzinger. “Real-Time System = Discrete System + Clock Variables.” In <i>Theories and Experiences for Real-Time System Development</i>, edited by Teodor Rus and Charles Rattray, 2:1–29. AMAST Series in Computing. World Scientific Publishing, 1994. <a href=\"https://doi.org/10.1142/9789812831583_0001\">https://doi.org/10.1142/9789812831583_0001</a>.","mla":"Alur, Rajeev, and Thomas A. Henzinger. “Real-Time System = Discrete System + Clock Variables.” <i>Theories and Experiences for Real-Time System Development</i>, edited by Teodor Rus and Charles Rattray, vol. 2, World Scientific Publishing, 1994, pp. 1–29, doi:<a href=\"https://doi.org/10.1142/9789812831583_0001\">10.1142/9789812831583_0001</a>.","short":"R. Alur, T.A. Henzinger, in:, T. Rus, C. Rattray (Eds.), Theories and Experiences for Real-Time System Development, World Scientific Publishing, 1994, pp. 1–29.","ista":"Alur R, Henzinger TA. 1994.Real-time system = discrete system + clock variables. In: Theories and Experiences for Real-Time System Development. AMAST Series in Computing, vol. 2, 1–29.","ieee":"R. Alur and T. A. Henzinger, “Real-time system = discrete system + clock variables,” in <i>Theories and Experiences for Real-Time System Development</i>, vol. 2, T. Rus and C. Rattray, Eds. World Scientific Publishing, 1994, pp. 1–29.","apa":"Alur, R., &#38; Henzinger, T. A. (1994). Real-time system = discrete system + clock variables. In T. Rus &#38; C. Rattray (Eds.), <i>Theories and Experiences for Real-Time System Development</i> (Vol. 2, pp. 1–29). World Scientific Publishing. <a href=\"https://doi.org/10.1142/9789812831583_0001\">https://doi.org/10.1142/9789812831583_0001</a>","ama":"Alur R, Henzinger TA. Real-time system = discrete system + clock variables. In: Rus T, Rattray C, eds. <i>Theories and Experiences for Real-Time System Development</i>. Vol 2. AMAST Series in Computing. World Scientific Publishing; 1994:1-29. doi:<a href=\"https://doi.org/10.1142/9789812831583_0001\">10.1142/9789812831583_0001</a>"},"keyword":["real-time systems","clock variables"],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","title":"Real-time system = discrete system + clock variables","date_updated":"2022-06-02T08:07:57Z","type":"book_chapter","abstract":[{"lang":"eng","text":"We introduce a temporal logic for the specification of real-time systems. Our logic, TPTL, employs a novel quantifier construct for referencing time: the &quot;freeze&quot; 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."}],"series_title":"AMAST Series in Computing","publication_identifier":{"isbn":[" 9789810219239"]},"date_created":"2018-12-11T12:09:38Z","publication":"Theories and Experiences for Real-Time System Development","article_processing_charge":"No","page":"1 - 29","date_published":"1994-01-01T00:00:00Z","editor":[{"first_name":"Teodor","last_name":"Rus","full_name":"Rus, Teodor"},{"first_name":"Charles","full_name":"Rattray, Charles","last_name":"Rattray"}],"year":"1994","publisher":"World Scientific Publishing","author":[{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A"}],"extern":"1","_id":"4590","alternative_title":["AMAST Series in Computing"],"volume":2,"intvolume":"         2","publist_id":"117"}]