[{"date_updated":"2022-06-02T09:35:58Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","scopus_import":"1","publist_id":"287","year":"1994","oa_version":"None","volume":863,"publication_status":"published","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-58468-4_173"}],"abstract":[{"lang":"eng","text":"We present a methodology for proving temporal properties of the divergent runs of reactive systems with real-valued clocks. A run diverges if time advances beyond any bound. Since the divergent runs of a system may satisfy liveness properties that are not satisfied by some convergent runs, the standard proof rules are incomplete if only divergent runs are considered. First, we develop a sound and complete proof calculus for divergence, which is based on translating clock systems into discrete systems. Then, we show that simpler proofs can be obtained for stronger divergence assumptions, such as unknown -divergence, which requires that all delays have a minimum duration of some unknown constant . We classify all real-time systems into an infinite hierarchy, according to how well they admit the translation of eventuality properties into equivalent safety properties."}],"_id":"4440","date_published":"1994-01-01T00:00:00Z","article_processing_charge":"No","language":[{"iso":"eng"}],"doi":"10.1007/3-540-58468-4_173","acknowledgement":"Supported in part by the National Science Foundation under grant CCR-9200794, by the United States Air Force Office of Scientific Research under contract F49620- 93-1-0056, and by the Defense Advanced Research Projects Agency under grant NAG2-892.","day":"01","alternative_title":["LNCS"],"type":"conference","author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"full_name":"Kopke, Peter","first_name":"Peter","last_name":"Kopke"}],"citation":{"short":"T.A. Henzinger, P. Kopke, in:, 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Springer, 1994, pp. 351–372.","ama":"Henzinger TA, Kopke P. Verification methods for the divergent runs of clock systems. In: <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>. Vol 863. Springer; 1994:351-372. doi:<a href=\"https://doi.org/10.1007/3-540-58468-4_173\">10.1007/3-540-58468-4_173</a>","apa":"Henzinger, T. A., &#38; Kopke, P. (1994). Verification methods for the divergent runs of clock systems. In <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i> (Vol. 863, pp. 351–372). Lübeck, Gernany: Springer. <a href=\"https://doi.org/10.1007/3-540-58468-4_173\">https://doi.org/10.1007/3-540-58468-4_173</a>","chicago":"Henzinger, Thomas A, and Peter Kopke. “Verification Methods for the Divergent Runs of Clock Systems.” In <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, 863:351–72. Springer, 1994. <a href=\"https://doi.org/10.1007/3-540-58468-4_173\">https://doi.org/10.1007/3-540-58468-4_173</a>.","ista":"Henzinger TA, Kopke P. 1994. Verification methods for the divergent runs of clock systems. 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS, vol. 863, 351–372.","ieee":"T. A. Henzinger and P. Kopke, “Verification methods for the divergent runs of clock systems,” in <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, Lübeck, Gernany, 1994, vol. 863, pp. 351–372.","mla":"Henzinger, Thomas A., and Peter Kopke. “Verification Methods for the Divergent Runs of Clock Systems.” <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, vol. 863, Springer, 1994, pp. 351–72, doi:<a href=\"https://doi.org/10.1007/3-540-58468-4_173\">10.1007/3-540-58468-4_173</a>."},"conference":{"end_date":"1994-09-23","start_date":"1994-09-19","name":"FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems","location":"Lübeck, Gernany"},"title":"Verification methods for the divergent runs of clock systems","quality_controlled":"1","publication":"3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems","status":"public","intvolume":"       863","publisher":"Springer","extern":"1","month":"01","date_created":"2018-12-11T12:08:52Z","page":"351 - 372"},{"quality_controlled":"1","publication":"Information and Computation","status":"public","intvolume":"       112","publisher":"Elsevier","extern":"1","month":"08","date_created":"2018-12-11T12:09:10Z","page":"273 - 337","language":[{"iso":"eng"}],"doi":"10.1006/inco.1994.1060","acknowledgement":"This research was supported in part by an IBM graduate fellowship, by the National Science Foundation under Grants CCR-9223226 and CCR-9200794. by the Defense Advanced Research Projects Agency under Contract N00039-84-C-0211. by the United States Air Force OMee of Scientific Research under Contracts F49620-93-141139 and F4962043-1-0056. and by the European Community ESPRIT Basic Research Action Project 6021 (REACT). A preliminary version of Part 1 of this paper appeared in the proceedings of the 1991 REX Workshop on Real Time Theory In Prate [HMP92a I a preliminary version of Part II appeared in the proceedings of the 1991 ACM Symposium on Principles of Programming Languages RIMP911. ","day":"01","author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Zohar","full_name":"Manna, Zohar","last_name":"Manna"},{"last_name":"Pnueli","first_name":"Amir","full_name":"Pnueli, Amir"}],"type":"journal_article","citation":{"ama":"Henzinger TA, Manna Z, Pnueli A. Temporal proof methodologies for timed transition systems. <i>Information and Computation</i>. 1994;112(2):273-337. doi:<a href=\"https://doi.org/10.1006/inco.1994.1060\">10.1006/inco.1994.1060</a>","apa":"Henzinger, T. A., Manna, Z., &#38; Pnueli, A. (1994). Temporal proof methodologies for timed transition systems. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1006/inco.1994.1060\">https://doi.org/10.1006/inco.1994.1060</a>","short":"T.A. Henzinger, Z. Manna, A. Pnueli, Information and Computation 112 (1994) 273–337.","mla":"Henzinger, Thomas A., et al. “Temporal Proof Methodologies for Timed Transition Systems.” <i>Information and Computation</i>, vol. 112, no. 2, Elsevier, 1994, pp. 273–337, doi:<a href=\"https://doi.org/10.1006/inco.1994.1060\">10.1006/inco.1994.1060</a>.","chicago":"Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “Temporal Proof Methodologies for Timed Transition Systems.” <i>Information and Computation</i>. Elsevier, 1994. <a href=\"https://doi.org/10.1006/inco.1994.1060\">https://doi.org/10.1006/inco.1994.1060</a>.","ieee":"T. A. Henzinger, Z. Manna, and A. Pnueli, “Temporal proof methodologies for timed transition systems,” <i>Information and Computation</i>, vol. 112, no. 2. Elsevier, pp. 273–337, 1994.","ista":"Henzinger TA, Manna Z, Pnueli A. 1994. Temporal proof methodologies for timed transition systems. Information and Computation. 112(2), 273–337."},"title":"Temporal proof methodologies for timed transition systems","volume":112,"publication_status":"published","main_file_link":[{"open_access":"1","url":"https://www.sciencedirect.com/science/article/pii/S0890540184710601?via%3Dihub"}],"oa":1,"abstract":[{"lang":"eng","text":"We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-;time properties of reactive systems. The abstract notion of timed transition systems generalizes traditional transition systems conservatively: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upper-bound timing constraints on transitions. This framework can model real-time systems that communicate either through shared variables or by message passing and real-time issues such as timeouts, process priorities (interrupts), and process scheduling. We exhibit two styles for the specification of real-time systems. While the first approach uses time-bounded versions of the temporal operators, the second approach allows explicit references to time through a special clock variable. Corresponding to the two styles of specification, we present and compare two different proof methodologies for the verification of timing requirements that are expressed in these styles. For the bounded-operator style, we provide a set of proof rules for establishing bounded-invariance and bounded-responce properties of timed transition systems. This approach generalizes the standard temporal proof rules for verifying invariance and response properties conservatively. For the explicit-clock style, we exploit the observation that every time-bounded property is a safety property and use the standard temporal proof rules for establishing safety properties."}],"_id":"4501","date_published":"1994-08-01T00:00:00Z","issue":"2","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2022-06-02T09:24:58Z","scopus_import":"1","publication_identifier":{"issn":["0890-5401"]},"publist_id":"227","article_type":"original","year":"1994","oa_version":"None"},{"citation":{"short":"T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Information and Computation 111 (1994) 193–244.","apa":"Henzinger, T. A., Nicollin, X., Sifakis, J., &#38; Yovine, S. (1994). Symbolic model checking for real-time systems. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1006/inco.1994.1045\">https://doi.org/10.1006/inco.1994.1045</a>","ama":"Henzinger TA, Nicollin X, Sifakis J, Yovine S. Symbolic model checking for real-time systems. <i>Information and Computation</i>. 1994;111(2):193-244. doi:<a href=\"https://doi.org/10.1006/inco.1994.1045\">10.1006/inco.1994.1045</a>","ieee":"T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic model checking for real-time systems,” <i>Information and Computation</i>, vol. 111, no. 2. Elsevier, pp. 193–244, 1994.","ista":"Henzinger TA, Nicollin X, Sifakis J, Yovine S. 1994. Symbolic model checking for real-time systems. Information and Computation. 111(2), 193–244.","chicago":"Henzinger, Thomas A, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. “Symbolic Model Checking for Real-Time Systems.” <i>Information and Computation</i>. Elsevier, 1994. <a href=\"https://doi.org/10.1006/inco.1994.1045\">https://doi.org/10.1006/inco.1994.1045</a>.","mla":"Henzinger, Thomas A., et al. “Symbolic Model Checking for Real-Time Systems.” <i>Information and Computation</i>, vol. 111, no. 2, Elsevier, 1994, pp. 193–244, doi:<a href=\"https://doi.org/10.1006/inco.1994.1045\">10.1006/inco.1994.1045</a>."},"title":"Symbolic model checking for real-time systems","day":"01","type":"journal_article","author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Xavier","full_name":"Nicollin, Xavier","last_name":"Nicollin"},{"last_name":"Sifakis","first_name":"Joseph","full_name":"Sifakis, Joseph"},{"last_name":"Yovine","full_name":"Yovine, Sergio","first_name":"Sergio"}],"acknowledgement":"We thank Peter Kopke for a careful reading.","language":[{"iso":"eng"}],"doi":"10.1006/inco.1994.1045","page":"193 - 244","extern":"1","month":"06","date_created":"2018-12-11T12:09:11Z","publisher":"Elsevier","quality_controlled":"1","publication":"Information and Computation","intvolume":"       111","status":"public","publist_id":"226","article_type":"original","oa_version":"None","year":"1994","date_updated":"2022-06-02T09:02:02Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","scopus_import":"1","publication_identifier":{"issn":["0890-5401"]},"issue":"2","article_processing_charge":"No","date_published":"1994-06-01T00:00:00Z","_id":"4503","abstract":[{"text":"We describe finite-state programs over real-numbered time in a guarded-command language with real-valued clocks or, equivalently, as finite automata with real-valued clocks. Model checking answers the question which states of a real-time program satisfy a branching-time specification (given in an extension of CTL with clock variables). We develop an algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered time. Unfortunately, many standard program properties, such as response for all nonzeno execution sequences (during which time diverges), cannot be characterized by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this result does not impair the symbolic verification of &quot;implementable&quot; real-time programs-those whose safety constraints are machine-closed with respect to diverging time and whose fairness constraints are restricted to finite upper bounds on clock values. All timed CTL properties of such programs are shown to be computable as finitely approximable fixpoints in a simple decidable theory.","lang":"eng"}],"publication_status":"published","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/S0890540184710455?via%3Dihub"}],"volume":111}]