## Alternating Refinement Relations

*Rajeev Alur, Thomas A. Henzinger, Orna Kupferman and
Moshe Vardi*
*Alternating transition systems* are a general model for composite
systems which allow 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 establish alternating trace containment to be 2EXPTIME-complete.
Finally, we present
a logical characterization of 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'98),
LNCS 1466, pp. 163--178,
Springer-Verlag, 1998.