@article{4599, abstract = {State-space explosion is a fundamental obstacle in the formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reduction and symbolic state-space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.}, author = {Alur, Rajeev and Brayton, Robert and Henzinger, Thomas A and Qadeer, Shaz and Rajamani, Sriram}, issn = {0925-9856}, journal = {Formal Methods in System Design}, number = {2}, pages = {97 -- 116}, publisher = {Springer}, title = {{Partial-order reduction in symbolic state-space exploration}}, doi = {10.1023/A:1008767206905}, volume = {18}, year = {2001}, } @inproceedings{4600, abstract = {Model checking is a practical tool for automated debugging of embedded software. In model checking, a high-level description of a system is compared against a logical correctness requirement to discover inconsistencies. Since model checking is based on exhaustive state-space exploration and the size of the state space of a design grows exponentially with the size of the description, scalability remains a challenge. We have thus developed techniques for exploiting modular design structure during model checking, and the model checker jMocha (Java MOdel-CHecking Algorithm) is based on this theme. Instead of manipulating unstructured state-transition graphs, it supports the hierarchical modeling framework of reactive modules. jMocha is a growing interactive software environment for specification, simulation and verification, and is intended as a vehicle for the development of new verification algorithms and approaches. It is written in Java and uses native C-code BDD libraries from VIS. jMocha offers: (1) a GUI that looks familiar to Windows/Java users; (2) a simulator that displays traces in a message sequence chart fashion; (3) requirements verification both by symbolic and enumerative model checking; (4) implementation verification by checking trace containment; (5) a proof manager that aids compositional and assume-guarantee reasoning; and (6) SLANG (Scripting LANGuage) for the rapid and structured development of new verification algorithms. jMocha is available publicly at ; it is a successor and extension of the original Mocha tool that was entirely written in C.}, author = {Alur, Rajeev and De Alfaro, Luca and Grosu, Radu and Henzinger, Thomas A and Kang, Myong and Kirsch, Christoph and Majumdar, Ritankar and Mang, Freddy and Wang, Bow}, booktitle = {Proceedings of the 23rd International Conference on Software Engineering}, isbn = {0769510507}, pages = {835 -- 836}, publisher = {IEEE}, title = {{jMocha: A model-checking tool that exploits design structure}}, doi = {10.1109/ICSE.2001.919196}, year = {2001}, } @inproceedings{4622, abstract = {Conventional type systems specify interfaces in terms of values and domains. We present a light-weight formalism that captures the temporal aspects of software component interfaces. Specifically, we use an automata-based language to capture both input assumptions about the order in which the methods of a component are called, and output guarantees about the order in which the component calls external methods. The formalism supports automatic compatability checks between interface models, and thus constitutes a type system for component interaction. Unlike traditional uses of automata, our formalism is based on an optimistic approach to composition, and on an alternating approach to design refinement. According to the optimistic approach, two components are compatible if there is some environment that can make them work together. According to the alternating approach, one interface refines another if it has weaker input assumptions, and stronger output guarantees. We show that these notions have game-theoretic foundations that lead to efficient algorithms for checking compatibility and refinement.}, author = {De Alfaro, Luca and Henzinger, Thomas A}, booktitle = {Proceedings of the 8th European software engineering conference}, isbn = {9781581133905}, location = {Vienna, Austria}, pages = {109 -- 120}, publisher = {ACM}, title = {{Interface automata}}, doi = {10.1145/503209.503226}, year = {2001}, } @inproceedings{4623, abstract = {We classify component-based models of computation into component models and interface models. A component model specifies for each component howthe component behaves in an arbitrary environment; an interface model specifies for each component what the component expects from the environment. Component models support compositional abstraction, and therefore component-based verification. Interface models support compositional refinement, and therefore componentbased design. Many aspects of interface models, such as compatibility and refinement checking between interfaces, are properly viewed in a gametheoretic setting, where the input and output values of an interface are chosen by different players.}, author = {De Alfaro, Luca and Henzinger, Thomas A}, booktitle = {Proceedings of the 1st International Workshop on Embedded Software}, isbn = {9783540426738}, location = {Tahoe City, CA, USA}, pages = {148 -- 165}, publisher = {ACM}, title = {{Interface theories for component-based design}}, doi = {10.1007/3-540-45449-7_11}, volume = {2211}, year = {2001}, } @inproceedings{4632, abstract = {We present a compositional trace-based model for probabilistic systems. The behavior of a system with probabilistic choice is a stochastic process, namely, a probability distribution on traces, or “bundle.” Consequently, the semantics of a system with both nondeterministic and probabilistic choice is a set of bundles. The bundles of a composite system can be obtained by combining the bundles of the components in a simple mathematical way. Refinement between systems is bundle containment. We achieve assume-guarantee compositionality for bundle semantics by introducing two scoping mechanisms. The first mechanism, which is standard in compositional modeling, distinguishes inputs from outputs and hidden state. The second mechanism, which arises in probabilistic systems, partitions the state into probabilistically independent regions.}, author = {De Alfaro, Luca and Henzinger, Thomas A and Jhala, Ranjit}, booktitle = {Proceedings of the 12th International Conference on on Concurrency Theory}, isbn = {9783540424970}, location = {Aalborg, Denmark}, pages = {351 -- 365}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Compositional methods for probabilistic systems}}, doi = {10.1007/3-540-44685-0_24}, volume = {2154}, year = {2001}, } @inproceedings{4633, abstract = {A procedure for the analysis of state spaces is called symbolic if it manipulates not individual states, but sets of states that are represented by constraints. Such a procedure can be used for the analysis of infinite state spaces, provided termination is guaranteed. We present symbolic procedures, and corresponding termination criteria, for the solution of infinite-state games, which occur in the control and modular verification of infinite-state systems. To characterize the termination of symbolic procedures for solving infinite-state games, we classify these game structures into four increasingly restrictive categories: 1 Class 1 consists of infinite-state structures for which all safety and reachability games can be solved. 2 Class 2 consists of infinite-state structures for which all ω-regular games can be solved. 3 Class 3 consists of infinite-state structures for which all nested positive boolean combinations of ω-regular games can be solved. 4 Class 4 consists of infinite-state structures for which all nested boolean combinations of ω-regular games can be solved. We give a structural characterization for each class, using equivalence relations on the state spaces of games which range from game versions of trace equivalence to a game version of bisimilarity. We provide infinite-state examples for all four classes of games from control problems for hybrid systems. We conclude by presenting symbolic algorithms for the synthesis of winning strategies (“controller synthesis”) for infinitestate games with arbitrary ω-regular objectives, and prove termination over all class-2 structures. This settles, in particular, the symbolic controller synthesis problem for rectangular hybrid systems.}, author = {De Alfaro, Luca and Henzinger, Thomas A and Majumdar, Ritankar}, booktitle = {Proceedings of the 12th International Conference on on Concurrency Theory}, isbn = {9783540424970}, location = {Aalborg, Denmark}, pages = {536 -- 550}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Symbolic algorithms for infinite-state games}}, doi = {10.1007/3-540-44685-0_36}, volume = {2154}, year = {2001}, } @inproceedings{4634, abstract = {A controller is an environment for a system that achieves a particular control objective by providing inputs to the system without constraining the choices of the system. For synchronous systems, where system and controller make simultaneous and interdependent choices, the notion that a controller must not constrain the choices of the system can be formalized by type systems for composability. In a previous paper, we solved the control problem for static and dynamic types: a static type is a dependency relation between inputs and outputs, and composition is well-typed if it does not introduce cyclic dependencies; a dynamic type is a set of static types, one for each state. Static and dynamic types, however, cannot capture many important digital circuits, such as gated clocks, bidirectional buses, and random-access memory. We therefore introduce more general type systems, so-called dependent and bidirectional types, for modeling these situations, and we solve the corresponding control problems. In a system with a dependent type, the dependencies between inputs and outputs are determined gradually through a game of the system against the controller. In a system with a bidirectional type, also the distinction between inputs and outputs is resolved dynamically by such a game. The game proceeds in several rounds. In each round the system and the controller choose to update some variables dependent on variables that have already been updated. The solution of the control problem for dependent and bidirectional types is based on algorithms for solving these games.}, author = {De Alfaro, Luca and Henzinger, Thomas A and Mang, Freddy}, booktitle = {Proceedings of the 12th International Conference on on Concurrency Theory}, isbn = {9783540424970}, location = {Aalborg, Denmark}, pages = {566 -- 581}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{The control of synchronous systems, Part II}}, doi = {10.1007/3-540-44685-0_38}, volume = {2154}, year = {2001}, } @inproceedings{4635, abstract = {We show how model checking techniques can be applied to the analysis of connectivity and cost-of-traversal properties of Web sites.}, author = {De Alfaro, Luca and Henzinger, Thomas A and Mang, Freddy}, booktitle = {Proceedings of the 10th international conference on World Wide Web}, isbn = {9781581133486}, location = {Hong Kong, Hong Kong}, pages = {86 -- 87}, publisher = {ACM}, title = {{MCWEB: A model-checking tool for web-site debugging}}, year = {2001}, } @inproceedings{4636, abstract = {Abstract. Dynamic programs, or fixpoint iteration schemes, are useful for solving many problems on state spaces, including model checking on Kripke structures (“verification”), computing shortest paths on weighted graphs (“optimization”), computing the value of games played on game graphs (“control”). For Kripke structures, a rich fixpoint theory is available in the form of the µ-calculus. Yet few connections have been made between different interpretations of fixpoint algorithms. We study the question of when a particular fixpoint iteration scheme ϕ for verifying an ω-regular property Ψ on a Kripke structure can be used also for solving a two-player game on a game graph with winning objective Ψ. We provide a sufficient and necessary criterion for the answer to be affirmative in the form of an extremal-model theorem for games: under a game interpretation, the dynamic program ϕ solves the game with objective Ψ if and only if both (1) under an existential interpretation on Kripke structures, ϕ is equivalent to ∃Ψ, and (2) under a universal interpretation on Kripke structures, ϕ is equivalent to ∀Ψ. In other words, ϕ is correct on all two-player game graphs iff it is correct on all extremal game graphs, where one or the other player has no choice of moves. The theorem generalizes to quantitative interpretations, where it connects two-player games with costs to weighted graphs. While the standard translations from ω-regular properties to the µ-calculus violate (1) or (2), we give a translation that satisfies both conditions. Our construction, therefore, yields fixpoint iteration schemes that can be uniformly applied on Kripke structures, weighted graphs, game graphs, and game graphs with costs, in order to meet or optimize a given ω-regular objective.}, author = {De Alfaro, Luca and Henzinger, Thomas A and Majumdar, Ritankar}, booktitle = {Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science}, isbn = {076951281X}, location = {Boston, MA, USA}, pages = {279 -- 290}, publisher = {IEEE}, title = {{From verification to control: dynamic programs for omega-regular objectives}}, doi = {10.1109/LICS.2001.932504}, year = {2001}, }