M Mukund, K Narayan Kumar and S A Smolka
Proc. ASIAN '99, Springer LNCS 1742 (1999) 227-238.
© Springer-Verlag Berlin Heidelberg
We investigate OReX, a temporal logic for specifying open systems. Path properties in OReX are expressed using omega-regular expressions, while similar logics for open systems, such as ATL* of Alur et al., use LTL for this purpose. Our results indicate that this distinction is an important one. In particular, we show that OReX has a more efficient model-checking procedure than ATL*, even though it is strictly more expressive. To this end, we present a single-exponential model-checking algorithm for OReX; the model-checking problem for ATL* in contrast is provably double-exponential.