Observational Preorders for Alternating Transition Systems.

We define two notions of observational preorders on Alternating transition systems. The first is based on the notion of being able to enforce a property. The second is based on the idea of viewing strategies as a generalised notion of context. We show that alternating simulation as defined by Alur et al. [ 3 ] is a sound proof technique for the enforcing preorder and a complete proof technique for the “contextual” preorder. We conclude by comparing alternating simulation with the classic notion of simulation on labelled transition systems.