TY - GEN
T1 - Faster model checking for open systems
AU - Mukund, Madhavan
AU - Narayan Kumar, K.
AU - Smolka, Scott A.
N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1999.
PY - 1999
Y1 - 1999
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84958811902
U2 - 10.1007/3-540-46674-6_20
DO - 10.1007/3-540-46674-6_20
M3 - Conference contribution
SN - 354066856X
SN - 9783540668565
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 227
EP - 238
BT - Advances in Computing Science - ASIAN 1999 - 5th Asian Computing Science Conference, Proceedings
A2 - Yap, Roland
A2 - Thiagarajan, P.S.
PB - Springer Verlag
T2 - 5th Asian Computing Science Conference on Advances in Computing Science, ASIAN 1999
Y2 - 10 December 1999 through 12 December 1999
ER -