[{"month":"04","day":"24","conference":{"name":"RTAS: Real-time and Embedded Technology and Applications Symposium"},"doi":"10.1109/RTAS.2006.11","date_published":"2006-04-24T00:00:00Z","citation":{"chicago":"Henzinger, Thomas A, and Slobodan Matic. “An Interface Algebra for Real-Time Components,” 253–66. IEEE, 2006. https://doi.org/10.1109/RTAS.2006.11.","short":"T.A. Henzinger, S. Matic, in:, IEEE, 2006, pp. 253–266.","mla":"Henzinger, Thomas A., and Slobodan Matic. An Interface Algebra for Real-Time Components. IEEE, 2006, pp. 253–66, doi:10.1109/RTAS.2006.11.","apa":"Henzinger, T. A., & Matic, S. (2006). An interface algebra for real-time components (pp. 253–266). Presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, IEEE. https://doi.org/10.1109/RTAS.2006.11","ieee":"T. A. Henzinger and S. Matic, “An interface algebra for real-time components,” presented at the RTAS: Real-time and Embedded Technology and Applications Symposium, 2006, pp. 253–266.","ista":"Henzinger TA, Matic S. 2006. An interface algebra for real-time components. RTAS: Real-time and Embedded Technology and Applications Symposium, 253–266.","ama":"Henzinger TA, Matic S. An interface algebra for real-time components. In: IEEE; 2006:253-266. doi:10.1109/RTAS.2006.11"},"quality_controlled":0,"page":"253 - 266","abstract":[{"text":"We present an assume-guarantee interface algebra for real-time components. In our formalism a component implements a set of task sequences that share a resource. A component interface consists of an arrival rate function and a latency for each task sequence, and a capacity function for the shared resource. The interface specifies that the component guarantees certain task latencies depending on assumptions about task arrival rates and allocated resource capacities. Our algebra defines compatibility and refinement relations on interfaces. Interface compatibility can be checked on partial designs, even when some component interfaces are yet unknown. In this case interface composition computes as new assumptions the weakest constraints on the unknown components that are necessary to satisfy the specified guarantees. Interface refinement is defined in a way that ensures that compatible interfaces can be refined and implemented independently. Our algebra thus formalizes an interface-based design methodology that supports both the incremental addition of new components and the independent stepwise refinement of existing components. We demonstrate the flexibility and efficiency of the framework through simulation experiments.","lang":"eng"}],"publist_id":"294","extern":1,"type":"conference","author":[{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Thomas Henzinger"},{"full_name":"Matic, Slobodan","last_name":"Matic","first_name":"Slobodan"}],"date_updated":"2021-01-12T07:56:57Z","date_created":"2018-12-11T12:08:50Z","_id":"4436","year":"2006","title":"An interface algebra for real-time components","publication_status":"published","status":"public","publisher":"IEEE"},{"day":"19","month":"09","doi":"10.1007/11867340_1","date_published":"2006-09-19T00:00:00Z","conference":{"name":"FORMATS: Formal Modeling and Analysis of Timed Systems"},"citation":{"ista":"Henzinger TA, Prabhu V. 2006. Timed alternating-time temporal logic. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 4202, 1–17.","ieee":"T. A. Henzinger and V. Prabhu, “Timed alternating-time temporal logic,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, 2006, vol. 4202, pp. 1–17.","apa":"Henzinger, T. A., & Prabhu, V. (2006). Timed alternating-time temporal logic (Vol. 4202, pp. 1–17). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Springer. https://doi.org/10.1007/11867340_1","ama":"Henzinger TA, Prabhu V. Timed alternating-time temporal logic. In: Vol 4202. Springer; 2006:1-17. doi:10.1007/11867340_1","chicago":"Henzinger, Thomas A, and Vinayak Prabhu. “Timed Alternating-Time Temporal Logic,” 4202:1–17. Springer, 2006. https://doi.org/10.1007/11867340_1.","mla":"Henzinger, Thomas A., and Vinayak Prabhu. Timed Alternating-Time Temporal Logic. Vol. 4202, Springer, 2006, pp. 1–17, doi:10.1007/11867340_1.","short":"T.A. Henzinger, V. Prabhu, in:, Springer, 2006, pp. 1–17."},"page":"1 - 17","quality_controlled":0,"publist_id":"296","abstract":[{"text":"We add freeze quantifiers to the game logic ATL in order to specify real-time objectives for games played on timed structures. We define the semantics of the resulting logic TATL by restricting the players to physically meaningful strategies, which do not prevent time from diverging. We show that TATL can be model checked over timed automaton games. We also specify timed optimization problems for physically meaningful strategies, and we show that for timed automaton games, the optimal answers can be approximated to within any degree of precision.","lang":"eng"}],"extern":1,"type":"conference","alternative_title":["LNCS"],"author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Thomas Henzinger"},{"first_name":"Vinayak","last_name":"Prabhu","full_name":"Prabhu, Vinayak S"}],"volume":4202,"date_updated":"2021-01-12T07:56:56Z","date_created":"2018-12-11T12:08:49Z","acknowledgement":"This research was supported in part by the NSF grants CCR-0208875, CCR-0225610, and CCR-0234690.","_id":"4432","year":"2006","publisher":"Springer","intvolume":" 4202","publication_status":"published","title":"Timed alternating-time temporal logic","status":"public"},{"quality_controlled":0,"page":"1 - 15","citation":{"ama":"Henzinger TA, Sifakis J. The embedded systems design challenge. In: Vol 4085. Springer; 2006:1-15. doi:10.1007/11813040_1","ista":"Henzinger TA, Sifakis J. 2006. The embedded systems design challenge. FM: Formal Methods, LNCS, vol. 4085, 1–15.","apa":"Henzinger, T. A., & Sifakis, J. (2006). The embedded systems design challenge (Vol. 4085, pp. 1–15). Presented at the FM: Formal Methods, Springer. https://doi.org/10.1007/11813040_1","ieee":"T. A. Henzinger and J. Sifakis, “The embedded systems design challenge,” presented at the FM: Formal Methods, 2006, vol. 4085, pp. 1–15.","mla":"Henzinger, Thomas A., and Joseph Sifakis. The Embedded Systems Design Challenge. Vol. 4085, Springer, 2006, pp. 1–15, doi:10.1007/11813040_1.","short":"T.A. Henzinger, J. Sifakis, in:, Springer, 2006, pp. 1–15.","chicago":"Henzinger, Thomas A, and Joseph Sifakis. “The Embedded Systems Design Challenge,” 4085:1–15. Springer, 2006. https://doi.org/10.1007/11813040_1."},"conference":{"name":"FM: Formal Methods"},"doi":"10.1007/11813040_1","date_published":"2006-08-10T00:00:00Z","day":"10","month":"08","publication_status":"published","status":"public","title":"The embedded systems design challenge","intvolume":" 4085","publisher":"Springer","_id":"4431","year":"2006","acknowledgement":"Supported in part by the ARTIST2 European Network of Excellence on Embedded Systems Design, by the NSF ITR Center on Hybrid and Embedded Software Systems (CHESS), and by the SNSF NCCR on Mobile Information and Communication Systems (MICS).","date_updated":"2021-01-12T07:56:55Z","date_created":"2018-12-11T12:08:49Z","volume":4085,"author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Thomas Henzinger"},{"full_name":"Sifakis, Joseph","last_name":"Sifakis","first_name":"Joseph"}],"alternative_title":["LNCS"],"type":"conference","extern":1,"abstract":[{"lang":"eng","text":"We summarize some current trends in embedded systems design and point out some of their characteristics, such as the chasm between analytical and computational models, and the gap between safety-critical and best-effort engineering practices. We call for a coherent scientific foundation for embedded systems design, and we discuss a few key demands on such a foundation: the need for encompassing several manifestations of heterogeneity, and the need for constructivity in design. We believe that the development of a satisfactory Embedded Systems Design Science provides a timely challenge and opportunity for reinvigorating computer science."}],"publist_id":"301"},{"abstract":[{"lang":"eng","text":"One source of complexity in the μ-calculus is its ability to specify an unbounded number of switches between universal (AX) and existential (EX) branching modes. We therefore study the problems of satisfiability, validity, model checking, and implication for the universal and existential fragments of the μ-calculus, in which only one branching mode is allowed. The universal fragment is rich enough to express most specifications of interest, and therefore improved algorithms are of practical importance. We show that while the satisfiability and validity problems become indeed simpler for the existential and universal fragments, this is, unfortunately, not the case for model checking and implication. We also show the corresponding results for the alternation-free fragment of the μ-calculus, where no alternations between least and greatest fixed points are allowed. Our results imply that efforts to find a polynomial-time model-checking algorithm for the μ-calculus can be replaced by efforts to find such an algorithm for the universal or existential fragment."}],"publist_id":"276","issue":"2","extern":1,"type":"journal_article","author":[{"full_name":"Thomas Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"},{"full_name":"Majumdar, Ritankar S","last_name":"Majumdar","first_name":"Ritankar"}],"date_created":"2018-12-11T12:08:55Z","date_updated":"2021-01-12T07:57:04Z","volume":354,"year":"2006","_id":"4451","status":"public","publication_status":"published","title":"On the universal and existential fragments of the mu-calculus","publisher":"Elsevier","intvolume":" 354","day":"28","month":"03","date_published":"2006-03-28T00:00:00Z","doi":"10.1016/j.tcs.2005.11.015","publication":"Theoretical Computer Science","citation":{"chicago":"Henzinger, Thomas A, Orna Kupferman, and Ritankar Majumdar. “On the Universal and Existential Fragments of the Mu-Calculus.” Theoretical Computer Science. Elsevier, 2006. https://doi.org/10.1016/j.tcs.2005.11.015.","mla":"Henzinger, Thomas A., et al. “On the Universal and Existential Fragments of the Mu-Calculus.” Theoretical Computer Science, vol. 354, no. 2, Elsevier, 2006, pp. 173–86, doi:10.1016/j.tcs.2005.11.015.","short":"T.A. Henzinger, O. Kupferman, R. Majumdar, Theoretical Computer Science 354 (2006) 173–186.","ista":"Henzinger TA, Kupferman O, Majumdar R. 2006. On the universal and existential fragments of the mu-calculus. Theoretical Computer Science. 354(2), 173–186.","apa":"Henzinger, T. A., Kupferman, O., & Majumdar, R. (2006). On the universal and existential fragments of the mu-calculus. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2005.11.015","ieee":"T. A. Henzinger, O. Kupferman, and R. Majumdar, “On the universal and existential fragments of the mu-calculus,” Theoretical Computer Science, vol. 354, no. 2. Elsevier, pp. 173–186, 2006.","ama":"Henzinger TA, Kupferman O, Majumdar R. On the universal and existential fragments of the mu-calculus. Theoretical Computer Science. 2006;354(2):173-186. doi:10.1016/j.tcs.2005.11.015"},"quality_controlled":0,"page":"173 - 186"},{"title":"Synergy: A new algorithm for property checking","publication_status":"published","status":"public","publisher":"ACM","year":"2006","_id":"4523","date_created":"2018-12-11T12:09:18Z","date_updated":"2021-01-12T07:59:26Z","author":[{"full_name":"Gulavani, Bhargav S","last_name":"Gulavani","first_name":"Bhargav"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Thomas Henzinger"},{"full_name":"Kannan, Yamini","first_name":"Yamini","last_name":"Kannan"},{"first_name":"Aditya","last_name":"Nori","full_name":"Nori, Aditya V"},{"full_name":"Rajamani, Sriram K","last_name":"Rajamani","first_name":"Sriram"}],"type":"conference","extern":1,"abstract":[{"lang":"eng","text":"We consider the problem if a given program satisfies a specified safety property. Interesting programs have infinite state spaces, with inputs ranging over infinite domains, and for these programs the property checking problem is undecidable. Two broad approaches to property checking are testing and verification. Testing tries to find inputs and executions which demonstrate violations of the property. Verification tries to construct a formal proof which shows that all executions of the program satisfy the property. Testing works best when errors are easy to find, but it is often difficult to achieve sufficient coverage for correct programs. On the other hand, verification methods are most successful when proofs are easy to find, but they are often inefficient at discovering errors. We propose a new algorithm, Synergy, which combines testing and verification. Synergy unifies several ideas from the literature, including counterexample-guided model checking, directed testing, and partition refinement.This paper presents a description of the Synergy algorithm, its theoretical properties, a comparison with related algorithms, and a prototype implementation called Yogi."}],"publist_id":"206","quality_controlled":0,"page":"117 - 127","citation":{"ista":"Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. 2006. Synergy: A new algorithm for property checking. FSE: Foundations of Software Engineering, 117–127.","apa":"Gulavani, B., Henzinger, T. A., Kannan, Y., Nori, A., & Rajamani, S. (2006). Synergy: A new algorithm for property checking (pp. 117–127). Presented at the FSE: Foundations of Software Engineering, ACM. https://doi.org/10.1145/1181775.1181790","ieee":"B. Gulavani, T. A. Henzinger, Y. Kannan, A. Nori, and S. Rajamani, “Synergy: A new algorithm for property checking,” presented at the FSE: Foundations of Software Engineering, 2006, pp. 117–127.","ama":"Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. Synergy: A new algorithm for property checking. In: ACM; 2006:117-127. doi:10.1145/1181775.1181790","chicago":"Gulavani, Bhargav, Thomas A Henzinger, Yamini Kannan, Aditya Nori, and Sriram Rajamani. “Synergy: A New Algorithm for Property Checking,” 117–27. ACM, 2006. https://doi.org/10.1145/1181775.1181790.","mla":"Gulavani, Bhargav, et al. Synergy: A New Algorithm for Property Checking. ACM, 2006, pp. 117–27, doi:10.1145/1181775.1181790.","short":"B. Gulavani, T.A. Henzinger, Y. Kannan, A. Nori, S. Rajamani, in:, ACM, 2006, pp. 117–127."},"conference":{"name":"FSE: Foundations of Software Engineering"},"doi":"10.1145/1181775.1181790","date_published":"2006-01-01T00:00:00Z","month":"01","day":"01"}]