Faster model checking for open systems

Mukund, Madhavan ; Narayan Kumar, K. ; Smolka, Scott A. (1999) Faster model checking for open systems In: 5th Asian Computing Science Conference, 10-12 Dec 1999, Phuket, Thailand.

Full text not available from this repository.

Official URL:

Related URL:


We investigate OREX, a temporal logic for specifying open systems. Path properties in OREX are expressed using ε-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.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Springer-Verlag.
Keywords:Model Check; Temporal Logic; Regular Expression; Winning Strategy; Label Transition System
ID Code:114221
Deposited On:25 May 2018 04:53
Last Modified:25 May 2018 04:53

Repository Staff Only: item control page