[{"day":"01","doi":"10.1007/BFb0014712","abstract":[{"lang":"eng","text":"In temporal-logic model checking, we verify the correctness of a program with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal-logic formula that specifies the behavior. The model-checking problem for the branching-time temporal logic CTL can be solved in linear running time, and model-checking tools for CTL are used successfully in industrial applications. The development of programs that must meet rigid real-time constraints has brought with it a need for real-time temporal logics that enable quantitative reference to time. Early research on real-time temporal logics uses the discrete domain of the integers to model time. Present research on real-time temporal logics focuses on continuous time and uses the dense domain of the reals to model time. There, model checking becomes significantly more complicated. For example, the model-checking problem for TCTL, a continuous-time extension of the logic CTL, is PSPACE-complete.\r\nIn this paper we suggest a reduction from TCTL model checking to CTL model checking. The contribution of such a reduction is twofold. Theoretically, while it has long been known that model-checking methods for untimed temporal logics can be extended quite easily to handle discrete time, it was not clear whether and how untimed methods can handle the reset quantifier of TCTL, which resets a realvalued clock. Practically, our reduction enables anyone who has a tool for CTL model checking to use it for TCTL model checking. The TCTL model-checking algorithm that follows from our reduction is in PSPACE, matching the known bound for this problem. In addition, it enjoys the wide distribution of CTL model-checking tools and the extensive and fruitful research efforts and heuristics that have been put into these tools."}],"year":"1997","citation":{"ama":"Henzinger TA, Kupferman O. From quantity to quality. In: <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>. Vol 1201. Springer; 1997:48-62. doi:<a href=\"https://doi.org/10.1007/BFb0014712\">10.1007/BFb0014712</a>","apa":"Henzinger, T. A., &#38; Kupferman, O. (1997). From quantity to quality. In <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i> (Vol. 1201, pp. 48–62). Grenoble, France: Springer. <a href=\"https://doi.org/10.1007/BFb0014712\">https://doi.org/10.1007/BFb0014712</a>","ieee":"T. A. Henzinger and O. Kupferman, “From quantity to quality,” in <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>, Grenoble, France, 1997, vol. 1201, pp. 48–62.","chicago":"Henzinger, Thomas A, and Orna Kupferman. “From Quantity to Quality.” In <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>, 1201:48–62. Springer, 1997. <a href=\"https://doi.org/10.1007/BFb0014712\">https://doi.org/10.1007/BFb0014712</a>.","mla":"Henzinger, Thomas A., and Orna Kupferman. “From Quantity to Quality.” <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>, vol. 1201, Springer, 1997, pp. 48–62, doi:<a href=\"https://doi.org/10.1007/BFb0014712\">10.1007/BFb0014712</a>.","short":"T.A. Henzinger, O. Kupferman, in:, Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems, Springer, 1997, pp. 48–62.","ista":"Henzinger TA, Kupferman O. 1997. From quantity to quality. Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems. HART: Hybrid and Real-Time Systems, LNCS, vol. 1201, 48–62."},"date_updated":"2022-08-17T12:29:48Z","acknowledgement":"This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 95-DC-324.036.","volume":1201,"extern":"1","article_processing_charge":"No","date_created":"2018-12-11T12:08:51Z","publication_status":"published","intvolume":"      1201","alternative_title":["LNCS"],"title":"From quantity to quality","scopus_import":"1","_id":"4438","author":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"}],"publisher":"Springer","quality_controlled":"1","page":"48 - 62","publication_identifier":{"isbn":["9783540626008"]},"publist_id":"291","type":"conference","date_published":"1997-01-01T00:00:00Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","oa_version":"None","month":"01","publication":"Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems","conference":{"end_date":"1997-03-28","location":"Grenoble, France","start_date":"1997-03-26","name":"HART: Hybrid and Real-Time Systems"},"language":[{"iso":"eng"}]},{"publisher":"Springer","page":"331 - 345","quality_controlled":"1","alternative_title":["LNCS"],"title":"Robust timed automata","intvolume":"      1201","publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:09:17Z","author":[{"last_name":"Gupta","first_name":"Vineet","full_name":"Gupta, Vineet"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jagadeesan, Radha","last_name":"Jagadeesan","first_name":"Radha"}],"_id":"4520","scopus_import":"1","extern":"1","volume":1201,"acknowledgement":"The first and third author were supported in part by grants from ARPA and ONR. The second author was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 95-DC-324.036. The third author was also supported by the NSF.","abstract":[{"text":"We define robust timed automata, which are timed automata that accept all trajectories robustly: if a robust timed automaton accepts a trajectory, then it must accept neighboring trajectories also; and if a robust timed automaton rejects a trajectory, then it must reject neighboring trajectories also. We show that the emptiness problem for robust timed automata is still decidable, by modifying the region construction for timed automata. We then show that, like timed automata, robust timed automata cannot be determinized. This result is somewhat unexpected, given that in temporal logic, the removal of realtime equality constraints is known to lead to a decidable theory that is closed under all boolean operations.","lang":"eng"}],"doi":"10.1007/BFb0014736","day":"01","date_updated":"2022-08-17T09:04:39Z","year":"1997","citation":{"ista":"Gupta V, Henzinger TA, Jagadeesan R. 1997. Robust timed automata. Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems. HART: Hybrid and Real-Time Systems, LNCS, vol. 1201, 331–345.","mla":"Gupta, Vineet, et al. “Robust Timed Automata.” <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>, vol. 1201, Springer, 1997, pp. 331–45, doi:<a href=\"https://doi.org/10.1007/BFb0014736\">10.1007/BFb0014736</a>.","short":"V. Gupta, T.A. Henzinger, R. Jagadeesan, in:, Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems, Springer, 1997, pp. 331–345.","ieee":"V. Gupta, T. A. Henzinger, and R. Jagadeesan, “Robust timed automata,” in <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>, Grenoble, France, 1997, vol. 1201, pp. 331–345.","chicago":"Gupta, Vineet, Thomas A Henzinger, and Radha Jagadeesan. “Robust Timed Automata.” In <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>, 1201:331–45. Springer, 1997. <a href=\"https://doi.org/10.1007/BFb0014736\">https://doi.org/10.1007/BFb0014736</a>.","apa":"Gupta, V., Henzinger, T. A., &#38; Jagadeesan, R. (1997). Robust timed automata. In <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i> (Vol. 1201, pp. 331–345). Grenoble, France: Springer. <a href=\"https://doi.org/10.1007/BFb0014736\">https://doi.org/10.1007/BFb0014736</a>","ama":"Gupta V, Henzinger TA, Jagadeesan R. Robust timed automata. In: <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>. Vol 1201. Springer; 1997:331-345. doi:<a href=\"https://doi.org/10.1007/BFb0014736\">10.1007/BFb0014736</a>"},"conference":{"end_date":"1997-03-28","location":"Grenoble, France","start_date":"1997-03-26","name":"HART: Hybrid and Real-Time Systems"},"language":[{"iso":"eng"}],"month":"01","oa_version":"None","publication":"Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems","status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"207","publication_identifier":{"isbn":["9783540626008"]},"date_published":"1997-01-01T00:00:00Z","type":"conference"}]