## Alternating Refinement Relations

*Rajeev Alur,
Thomas A. Henzinger,
Orna Kupferman, and Moshe Y. Vardi*

*Alternating transition systems* are a general model for composite
systems which allows the study of collaborative as well as adversarial
relationships between individual system components. Unlike in labeled
transition systems, where each transition corresponds to a possible step of
the system (which may involve some or all components), in alternating
transition systems, each transition corresponds to a possible move in a game
between the components. In this paper, we study refinement relations between
alternating transition systems, such as "Does the implementation refine the
set *A* of specification components without constraining the components
not in *A*?" In particular, we generalize the definitions of the
simulation and trace containment preorders from labeled transition systems to
alternating transition systems. The generalizations are called
*alternating simulation* and *alternating trace containment*.
Unlike existing refinement relations, they allow the refinement of individual
components within the context of a composite system description. We show
that, like ordinary simulation, alternating simulation can be checked in
polynomial time using a fixpoint computation algorithm. While ordinary trace
containment is PSPACE-complete, we prove alternating trace containment to be
EXPTIME-complete. Finally, we present logical characterizations for the two
preorders in terms of ATL, a temporal logic capable of referring to games
between system components.

*Proceedings of the
Ninth International Conference on Concurrency Theory*
(CONCUR),
Lecture Notes in Computer Science 1466,
Springer, 1998, pp. 163-178.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1998 Springer.