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: https://link.springer.com/chapter/10.1007%2F3-540-...
Related URL: http://dx.doi.org/10.1007/3-540-46674-6_20
Abstract
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
