@inproceedings{4482,
abstract = {We apply the theory of abstract interpretation to the verification of game properties for reactive systems. Unlike properties expressed in standard temporal logics, game properties can distinguish adversarial from collaborative relationships between the processes of a concurrent program, or the components of a parallel system. We consider two-player concurrent games –say, component vs. environment– and specify properties of such games –say, the component has a winning strategy to obtain a resource, no matter how the environment behaves– in the alternating-time μ-calculus (Aμ ). A sound abstraction of such a game must at the same time restrict the behaviors of the component and increase the behaviors of the environment: if a less powerful component can win against a more powerful environment, then surely the original component can win against the original environment.
We formalize the concrete semantics of a concurrent game in terms of controllable and uncontrollable predecessor predicates, which suffice for model checking all Aμ properties by applying boolean operations and iteration. We then define the abstract semantics of a concurrent game in terms of abstractions for the controllable and uncontrollable predecessor predicates. This allows us to give general characterizations for the soundness and completeness of abstract games with respect to Aμ properties. We also present a simple programming language for multi-process programs, and show how approximations of the maximal abstraction (w.r.t. Aμ properties) can be obtained from the program text. We apply the theory to two practical verification examples, a communication protocol developed at the Berkeley Wireless Research Center, and a protocol converter. In the wireless protocol, both the use of a game property for specification and the use of abstraction for automatic verification were instrumental to uncover a subtle bug.},
author = {Thomas Henzinger and Majumdar, Ritankar S and Mang, Freddy Y and Raskin, Jean-François},
pages = {220 -- 239},
publisher = {Springer},
title = {{Abstract interpretation of game properties}},
doi = {10.1007/978-3-540-45099-3_12},
volume = {1824},
year = {2000},
}
@inproceedings{4483,
abstract = {Model-checking algorithms can be used to verify, formally and automatically, if a low-level description of a design conforms with a high-level description. However, for designs with very large state spaces, prior to the application of an algorithm, the refinement-checking task needs to be decomposed into subtasks of manageable complexity. It is natural to decompose the task following the component structure of the design. However, an individual component often does not satisfy its requirements unless the component is put into the right context, which constrains the inputs to the component. Thus, in order to verify each component individually, we need to make assumptions about its inputs, which are provided by the other components of the design. This reasoning is circular: component A is verified under the assumption that context B behaves correctly, and symmetrically, B is verified assuming the correctness of A. The assume-guarantee paradigm provides a systematic theory and methodology for ensuring the soundness of the circular style of postulating and discharging assumptions in component-based reasoning.We give a tutorial introduction to the assume-guarantee paradigm for decomposing refinement-checking tasks. To illustrate the method, we step in detail through the formal verification of a processor pipeline against an instruction set architecture. In this example, the verification of a three-stage pipeline is broken up into three subtasks, one for each stage of the pipeline.},
author = {Thomas Henzinger and Qadeer,Shaz and Rajamani, Sriram K},
pages = {245 -- 252},
publisher = {IEEE},
title = {{Decomposing refinement proofs using assume-guarantee reasoning}},
doi = {10.1109/ICCAD.2000.896481},
year = {2000},
}
@inproceedings{4512,
abstract = {Masaccio is a formal model for hybrid dynamical systems which are built from atomic discrete components (difference equations) and atomic continuous components (differential equations) by parallel and serial composition, arbitrarily nested. Each system component consists of an interface, which determines the possible ways of using the component, and a set of executions, which define the possible behaviors of the component in real time.
Version 1.0 (May 2000).
},
author = {Thomas Henzinger},
pages = {549 -- 563},
publisher = {Springer},
title = {{Masaccio: A formal model for embedded components}},
doi = {10.1007/3-540-44929-9_38},
volume = {1872},
year = {2000},
}
@inbook{4513,
author = {Thomas Henzinger},
booktitle = {Verification of Digital and Hybrid Systems},
editor = {Inan, M. Kemal and Kurshan, Robert P.},
pages = {265 -- 292},
publisher = {Springer},
title = {{The theory of hybrid automata}},
volume = {170},
year = {2000},
}
@article{4598,
abstract = {A hybrid system is a dynamical system with both discrete and continuous state changes. For analysis purposes, it is often useful to abstract a system in a way that preserves the properties being analyzed while hiding the details that are of no interest. We show that interesting classes of hybrid systems can be abstracted to purely discrete systems while preserving all properties that are definable in temporal logic. The classes that permit discrete abstractions fall into two categories. Either the continuous dynamics must be restricted, as is the case for timed and rectangular hybrid systems, or the discrete dynamics must be restricted, as is the case for o-minimal hybrid systems. In this paper, we survey and unify results from both areas.},
author = {Alur, Rajeev and Thomas Henzinger and Lafferriere, Gerardo and Pappas, George J.},
journal = {Proceedings of the IEEE},
number = {7},
pages = {971 -- 984},
publisher = {IEEE},
title = {{Discrete abstractions of hybrid systems}},
doi = {10.1109/5.871304 },
volume = {88},
year = {2000},
}