[{"date_published":"2002-09-01T00:00:00Z","publication":"Journal of the ACM","citation":{"chicago":"Alur, Rajeev, Thomas A Henzinger, and Orna Kupferman. “Alternating-Time Temporal Logic.” Journal of the ACM. ACM, 2002. https://doi.org/10.1145/585265.585270.","short":"R. Alur, T.A. Henzinger, O. Kupferman, Journal of the ACM 49 (2002) 672–713.","mla":"Alur, Rajeev, et al. “Alternating-Time Temporal Logic.” Journal of the ACM, vol. 49, no. 5, ACM, 2002, pp. 672–713, doi:10.1145/585265.585270.","apa":"Alur, R., Henzinger, T. A., & Kupferman, O. (2002). Alternating-time temporal logic. Journal of the ACM. ACM. https://doi.org/10.1145/585265.585270","ieee":"R. Alur, T. A. Henzinger, and O. Kupferman, “Alternating-time temporal logic,” Journal of the ACM, vol. 49, no. 5. ACM, pp. 672–713, 2002.","ista":"Alur R, Henzinger TA, Kupferman O. 2002. Alternating-time temporal logic. Journal of the ACM. 49(5), 672–713.","ama":"Alur R, Henzinger TA, Kupferman O. Alternating-time temporal logic. Journal of the ACM. 2002;49(5):672-713. doi:10.1145/585265.585270"},"article_type":"original","page":"672 - 713","day":"01","article_processing_charge":"No","scopus_import":"1","oa_version":"None","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4595","status":"public","title":"Alternating-time temporal logic","intvolume":" 49","abstract":[{"text":"Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by the execution of a system; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator "eventually" with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. The problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas. Depending on whether or not we admit arbitrary nesting of selective path quantifiers and temporal operators, we obtain the two alternating-time temporal logics ATL and ATL*.ATL and ATL* are interpreted over concurrent game structures. Every state transition of a concurrent game structure results from a choice of moves, one for each player. The players represent individual components and the environment of an open system. Concurrent game structures can capture various forms of synchronous composition for open systems, and if augmented with fairness constraints, also asynchronous composition. Over structures without fairness constraints, the model-checking complexity of ATL is linear in the size of the game structure and length of the formula, and the symbolic model-checking algorithm for CTL extends with few modifications to ATL. Over structures with weak-fairness constraints, ATL model checking requires the solution of 1-pair Rabin games, and can be done in polynomial time. Over structures with strong-fairness constraints, ATL model checking requires the solution of games with Boolean combinations of Büchi conditions, and can be done in PSPACE. In the case of ATL*, the model-checking problem is closely related to the synthesis problem for linear-time formulas, and requires doubly exponential time.","lang":"eng"}],"issue":"5","type":"journal_article","doi":"10.1145/585265.585270","language":[{"iso":"eng"}],"quality_controlled":"1","month":"09","publication_identifier":{"issn":["0004-5411"]},"author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"},{"full_name":"Kupferman, Orna","last_name":"Kupferman","first_name":"Orna"}],"date_created":"2018-12-11T12:09:40Z","date_updated":"2023-06-02T10:07:22Z","volume":49,"acknowledgement":"We thank Luca de Alfaro, Kousha Etessami, Salvatore La Torre, P. Madhusudan, Amir Pnueli, Moshe Vardi, Thomas Wilke, and Mihalis Yannakakis for helpful discussions. We also thank Freddy Mang for comments on a draft of this manuscript.","year":"2002","publication_status":"published","publisher":"ACM","publist_id":"110","extern":"1"},{"publisher":"Springer","publication_status":"published","year":"2002","acknowledgement":"This research was supported in part by the SRC contract 99-TJ-683.003, the DARPA contract NAG2-1214, and the NSF grant CCR-9988172.","volume":2380,"date_created":"2018-12-11T12:09:01Z","date_updated":"2023-06-05T08:05:13Z","author":[{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Krishnan, Sriram","first_name":"Sriram","last_name":"Krishnan"},{"full_name":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"},{"last_name":"Mang","first_name":"Freddy","full_name":"Mang, Freddy"}],"extern":"1","publist_id":"257","quality_controlled":"1","language":[{"iso":"eng"}],"doi":"10.1007/3-540-45465-9_55","conference":{"start_date":"2002-07-08","location":"Malaga, Spain","end_date":"2002-07-13","name":"ICALP: Automata, Languages and Programming"},"publication_identifier":{"isbn":["9783540438649"]},"month":"06","intvolume":" 2380","status":"public","title":"Synthesis of uninitialized systems","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4471","oa_version":"None","alternative_title":["LNCS"],"type":"conference","abstract":[{"lang":"eng","text":"The sequential synthesis problem, which is closely related to Church’s solvability problem, asks, given a specification in the form of a binary relation between input and output streams, for the construction of a finite-state stream transducer that converts inputs to appropriate outputs. For efficiency reasons, practical sequential hardware is often designed to operate without prior initialization. Such hardware designs can be modeled by uninitialized state machines, which are required to satisfy their specification if started from any state. In this paper we solve the sequential synthesis problem for uninitialized systems, that is, we construct uninitialized finite-state stream transducers. We consider specifications given by LTL formulas, deterministic, nondeterministic, universal, and alternating Büchi automata. We solve this uninitialized synthesis problem by reducing it to the well-understood initialized synthesis problem. While our solution is straightforward, it leads, for some specification formalisms, to upper bounds that are exponentially worse than the complexity of the corresponding initialized problems. However, we prove lower bounds to show that our simple solutions are optimal for all considered specification formalisms. We also study the problem of deciding whether a given specification is uninitialized, that is, if its uninitialized and initialized synthesis problems coincide. We show that this problem has, for each specification formalism, the same complexity as the equivalence problem."}],"page":"644 - 656","citation":{"ama":"Henzinger TA, Krishnan S, Kupferman O, Mang F. Synthesis of uninitialized systems. In: Proceedings of the 29th International Colloquium on Automata, Languages and Programming. Vol 2380. Springer; 2002:644-656. doi:10.1007/3-540-45465-9_55","ieee":"T. A. Henzinger, S. Krishnan, O. Kupferman, and F. Mang, “Synthesis of uninitialized systems,” in Proceedings of the 29th International Colloquium on Automata, Languages and Programming, Malaga, Spain, 2002, vol. 2380, pp. 644–656.","apa":"Henzinger, T. A., Krishnan, S., Kupferman, O., & Mang, F. (2002). Synthesis of uninitialized systems. In Proceedings of the 29th International Colloquium on Automata, Languages and Programming (Vol. 2380, pp. 644–656). Malaga, Spain: Springer. https://doi.org/10.1007/3-540-45465-9_55","ista":"Henzinger TA, Krishnan S, Kupferman O, Mang F. 2002. Synthesis of uninitialized systems. Proceedings of the 29th International Colloquium on Automata, Languages and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 2380, 644–656.","short":"T.A. Henzinger, S. Krishnan, O. Kupferman, F. Mang, in:, Proceedings of the 29th International Colloquium on Automata, Languages and Programming, Springer, 2002, pp. 644–656.","mla":"Henzinger, Thomas A., et al. “Synthesis of Uninitialized Systems.” Proceedings of the 29th International Colloquium on Automata, Languages and Programming, vol. 2380, Springer, 2002, pp. 644–56, doi:10.1007/3-540-45465-9_55.","chicago":"Henzinger, Thomas A, Sriram Krishnan, Orna Kupferman, and Freddy Mang. “Synthesis of Uninitialized Systems.” In Proceedings of the 29th International Colloquium on Automata, Languages and Programming, 2380:644–56. Springer, 2002. https://doi.org/10.1007/3-540-45465-9_55."},"publication":"Proceedings of the 29th International Colloquium on Automata, Languages and Programming","date_published":"2002-06-26T00:00:00Z","scopus_import":"1","article_processing_charge":"No","day":"26"},{"oa":1,"main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/S0890540101930858?via%3Dihub","open_access":"1"}],"quality_controlled":"1","doi":"10.1006/inco.2001.3085","language":[{"iso":"eng"}],"month":"02","publication_identifier":{"issn":["0890-5401"]},"acknowledgement":"We thank Ramin Hojati, Doron Bustan, and the anonymous reviewers for their comments on this paper.","year":"2002","publication_status":"published","publisher":"Elsevier","author":[{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Orna","last_name":"Kupferman","full_name":"Kupferman, Orna"},{"full_name":"Rajamani, Sriram","first_name":"Sriram","last_name":"Rajamani"}],"date_created":"2018-12-11T12:09:02Z","date_updated":"2023-06-05T07:53:27Z","volume":173,"publist_id":"255","extern":"1","publication":"Information and Computation","citation":{"short":"T.A. Henzinger, O. Kupferman, S. Rajamani, Information and Computation 173 (2002) 64–81.","mla":"Henzinger, Thomas A., et al. “Fair Simulation.” Information and Computation, vol. 173, no. 1, Elsevier, 2002, pp. 64–81, doi:10.1006/inco.2001.3085.","chicago":"Henzinger, Thomas A, Orna Kupferman, and Sriram Rajamani. “Fair Simulation.” Information and Computation. Elsevier, 2002. https://doi.org/10.1006/inco.2001.3085.","ama":"Henzinger TA, Kupferman O, Rajamani S. Fair simulation. Information and Computation. 2002;173(1):64-81. doi:10.1006/inco.2001.3085","apa":"Henzinger, T. A., Kupferman, O., & Rajamani, S. (2002). Fair simulation. Information and Computation. Elsevier. https://doi.org/10.1006/inco.2001.3085","ieee":"T. A. Henzinger, O. Kupferman, and S. Rajamani, “Fair simulation,” Information and Computation, vol. 173, no. 1. Elsevier, pp. 64–81, 2002.","ista":"Henzinger TA, Kupferman O, Rajamani S. 2002. Fair simulation. Information and Computation. 173(1), 64–81."},"article_type":"original","page":"64 - 81","date_published":"2002-02-25T00:00:00Z","scopus_import":"1","day":"25","article_processing_charge":"No","_id":"4474","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","title":"Fair simulation","status":"public","intvolume":" 173","oa_version":"Published Version","type":"journal_article","abstract":[{"lang":"eng","text":"The simulation preorder for labeled transition systems is defined locally, and operationally, as a game that relates states with their immediate successor states. Simulation enjoys many appealing properties. First, simulation has a denotational characterization: system S simulates system I iff every computation tree embedded in the unrolling of I can be embedded also in the unrolling of S. Second, simulation has a logical characterization: S simulates I iff every universal branching-time formula satisfied by S is satisfied also by I. It follows that simulation is a suitable notion of implementation, and it is the coarsest abstraction of a system that preserves universal branching-time properties. Third, based on its local definition, simulation between finite-state systems can be checked in polynomial time. Finally, simulation implies trace containment, which cannot be defined locally and requires polynomial space for verification. Hence simulation is widely used both in manual and in automatic verification. Liveness assumptions about transition systems are typically modeled using fairness constraints. Existing notions of simulation for fair transition systems, however, are not local, and as a result, many appealing properties of the simulation preorder are lost. We propose a new view of fair simulation by extending the local definition of simulation to account for fairness: system View the MathML sourcefairly simulates system View the MathML source iff in the simulation game, there is a strategy that matches with each fair computation of View the MathML source a fair computation of View the MathML source. Our definition enjoys a denotational characterization and has a logical characterization: View the MathML source fairly simulates View the MathML source iff every fair computation tree (whose infinite paths are fair) embedded in the unrolling of View the MathML source can be embedded also in the unrolling of View the MathML source or, equivalently, iff every Fair-∀AFMC formula satisfied by View the MathML source is satisfied also by View the MathML source (∀AFMC is the universal fragment of the alternation-free μ-calculus). The locality of the definition leads us to a polynomial-time algorithm for checking fair simulation for finite-state systems with weak and strong fairness constraints. Finally, fair simulation implies fair trace containment and is therefore useful as an efficiently computable local criterion for proving linear-time abstraction hierarchies of fair systems."}],"issue":"1"},{"type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"We present a formal methodology and tool for uncovering errors in the interaction of software modules. Our methodology consists of a suite of languages for defining software interfaces, and algorithms for checking interface compatibility. We focus on interfaces that explain the method-call dependencies between software modules. Such an interface makes assumptions about the environment in the form of call and availability constraints. A call constraint restricts the accessibility of local methods to certain external methods. An availability constraint restricts the accessibility of local methods to certain states of the module. For example, the interface for a file server with local methods open and read may assert that a file cannot be read without having been opened. Checking interface compatibility requires the solution of games, and in the presence of availability constraints, of pushdown games. Based on this methodology, we have implemented a tool that has uncovered incompatibilities in TinyOS, a small operating system for sensor nodes in adhoc networks."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4563","intvolume":" 2404","title":"Interface compatibility checking for software modules","status":"public","oa_version":"None","scopus_import":"1","article_processing_charge":"No","day":"19","citation":{"short":"A. Chakrabarti, L. De Alfaro, T.A. Henzinger, M. Jurdziński, F. Mang, in:, Proceedings of the 14th International Conference on Computer Aided Verification, Springer, 2002, pp. 428–441.","mla":"Chakrabarti, Arindam, et al. “Interface Compatibility Checking for Software Modules.” Proceedings of the 14th International Conference on Computer Aided Verification, vol. 2404, Springer, 2002, pp. 428–41, doi:10.1007/3-540-45657-0_35.","chicago":"Chakrabarti, Arindam, Luca De Alfaro, Thomas A Henzinger, Marcin Jurdziński, and Freddy Mang. “Interface Compatibility Checking for Software Modules.” In Proceedings of the 14th International Conference on Computer Aided Verification, 2404:428–41. Springer, 2002. https://doi.org/10.1007/3-540-45657-0_35.","ama":"Chakrabarti A, De Alfaro L, Henzinger TA, Jurdziński M, Mang F. Interface compatibility checking for software modules. In: Proceedings of the 14th International Conference on Computer Aided Verification. Vol 2404. Springer; 2002:428-441. doi:10.1007/3-540-45657-0_35","ieee":"A. Chakrabarti, L. De Alfaro, T. A. Henzinger, M. Jurdziński, and F. Mang, “Interface compatibility checking for software modules,” in Proceedings of the 14th International Conference on Computer Aided Verification, Copenhagen, Denmark, 2002, vol. 2404, pp. 428–441.","apa":"Chakrabarti, A., De Alfaro, L., Henzinger, T. A., Jurdziński, M., & Mang, F. (2002). Interface compatibility checking for software modules. In Proceedings of the 14th International Conference on Computer Aided Verification (Vol. 2404, pp. 428–441). Copenhagen, Denmark: Springer. https://doi.org/10.1007/3-540-45657-0_35","ista":"Chakrabarti A, De Alfaro L, Henzinger TA, Jurdziński M, Mang F. 2002. Interface compatibility checking for software modules. Proceedings of the 14th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2404, 428–441."},"publication":"Proceedings of the 14th International Conference on Computer Aided Verification","page":"428 - 441","date_published":"2002-06-19T00:00:00Z","publist_id":"147","extern":"1","acknowledgement":"This research was supported in part by the AFOSR grant F49620-00-1-0327, the DARPA grant F33615-00-C-1693, the MARCO grant 98-DT-660, the NSF grants CCR-9988172, CCR-0085949, CCR-0132780, the SRC grant 99-TJ-683, and the Polish KBN grant 7-T11C-027-20.","year":"2002","publisher":"Springer","publication_status":"published","author":[{"full_name":"Chakrabarti, Arindam","last_name":"Chakrabarti","first_name":"Arindam"},{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Jurdziński, Marcin","first_name":"Marcin","last_name":"Jurdziński"},{"full_name":"Mang, Freddy","last_name":"Mang","first_name":"Freddy"}],"volume":2404,"date_updated":"2023-06-05T07:38:10Z","date_created":"2018-12-11T12:09:30Z","publication_identifier":{"isbn":[" 9783540439974"]},"month":"06","quality_controlled":"1","doi":"10.1007/3-540-45657-0_35","conference":{"name":"CAV: Computer Aided Verification","start_date":"2002-07-27","location":"Copenhagen, Denmark","end_date":"2002-07-31"},"language":[{"iso":"eng"}]},{"scopus_import":"1","article_processing_charge":"No","day":"19","citation":{"ista":"Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. 2002. Temporal safety proofs for systems code. Proceedings of the 14th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2404, 526–538.","apa":"Henzinger, T. A., Necula, G., Jhala, R., Sutre, G., Majumdar, R., & Weimer, W. (2002). Temporal safety proofs for systems code. In Proceedings of the 14th International Conference on Computer Aided Verification (Vol. 2404, pp. 526–538). Copenhagen, Denmark: Springer. https://doi.org/10.1007/3-540-45657-0_45","ieee":"T. A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, and W. Weimer, “Temporal safety proofs for systems code,” in Proceedings of the 14th International Conference on Computer Aided Verification, Copenhagen, Denmark, 2002, vol. 2404, pp. 526–538.","ama":"Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. Temporal safety proofs for systems code. In: Proceedings of the 14th International Conference on Computer Aided Verification. Vol 2404. Springer; 2002:526-538. doi:10.1007/3-540-45657-0_45","chicago":"Henzinger, Thomas A, George Necula, Ranjit Jhala, Grégoire Sutre, Ritankar Majumdar, and Westley Weimer. “Temporal Safety Proofs for Systems Code.” In Proceedings of the 14th International Conference on Computer Aided Verification, 2404:526–38. Springer, 2002. https://doi.org/10.1007/3-540-45657-0_45.","mla":"Henzinger, Thomas A., et al. “Temporal Safety Proofs for Systems Code.” Proceedings of the 14th International Conference on Computer Aided Verification, vol. 2404, Springer, 2002, pp. 526–38, doi:10.1007/3-540-45657-0_45.","short":"T.A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, W. Weimer, in:, Proceedings of the 14th International Conference on Computer Aided Verification, Springer, 2002, pp. 526–538."},"publication":"Proceedings of the 14th International Conference on Computer Aided Verification","page":"526 - 538","date_published":"2002-06-19T00:00:00Z","type":"conference","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"We present a methodology and tool for verifying and certifying systems code. The verification is based on the lazy-abstraction paradigm for intertwining the following three logical steps: construct a predicate abstraction from the code, model check the abstraction, and automatically refine the abstraction based on counterexample analysis. The certification is based on the proof-carrying code paradigm. Lazy abstraction enables the automatic construction of small proof certificates. The methodology is implemented in Blast, the Berkeley Lazy Abstraction Software verification Tool. We describe our experience applying Blast to Linux and Windows device drivers. Given the C code for a driver and for a temporal-safety monitor, Blast automatically generates an easily checkable correctness certificate if the driver satisfies the specification, and an error trace otherwise."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4472","intvolume":" 2404","title":"Temporal safety proofs for systems code","status":"public","oa_version":"None","publication_identifier":{"isbn":["9783540439974"]},"month":"06","quality_controlled":"1","doi":"10.1007/3-540-45657-0_45","conference":{"end_date":"2002-07-31","start_date":"2002-07-27","location":"Copenhagen, Denmark","name":"CAV: Computer Aided Verification"},"language":[{"iso":"eng"}],"publist_id":"258","extern":"1","acknowledgement":"This work was supported in part by the NSF ITR grants CCR-0085949, CCR-0081588, the NSF Career grant CCR-9875171, the DARPA PCES grant F33615-00-C-1693, the MARCO GSRC grant 98-DT-660, the SRC contract 99-TJ-683, a Microsoft fellowship, and gifts from AT&T Research and Microsoft Research.","year":"2002","publisher":"Springer","publication_status":"published","author":[{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Necula, George","first_name":"George","last_name":"Necula"},{"full_name":"Jhala, Ranjit","first_name":"Ranjit","last_name":"Jhala"},{"full_name":"Sutre, Grégoire","first_name":"Grégoire","last_name":"Sutre"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"},{"full_name":"Weimer, Westley","last_name":"Weimer","first_name":"Westley"}],"volume":2404,"date_created":"2018-12-11T12:09:01Z","date_updated":"2023-06-05T08:11:32Z"}]