Faster model checking for open systems

Madhavan Mukund; K. Narayan Kumar; Scott A. Smolka

doi:10.1007/3-540-46674-6_20

Faster model checking for open systems

Madhavan Mukund
, K. Narayan Kumar
, Scott A. Smolka

Computer Science

SPIC Science Foundation

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Advances in Computing Science - ASIAN 1999 - 5th Asian Computing Science Conference, Proceedings
Editors	Roland Yap, P.S. Thiagarajan
Publisher	Springer Verlag
Pages	227-238
Number of pages	12
ISBN (Print)	354066856X, 9783540668565
DOIs	https://doi.org/10.1007/3-540-46674-6_20
State	Published - 1999
Event	5th Asian Computing Science Conference on Advances in Computing Science, ASIAN 1999 - Phuket, Thailand Duration: Dec 10 1999 → Dec 12 1999

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1742
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	5th Asian Computing Science Conference on Advances in Computing Science, ASIAN 1999
Country/Territory	Thailand
City	Phuket
Period	12/10/99 → 12/12/99

Access to Document

10.1007/3-540-46674-6_20

Cite this

Mukund, M., Narayan Kumar, K., & Smolka, S. A. (1999). Faster model checking for open systems. In R. Yap, & P. S. Thiagarajan (Eds.), Advances in Computing Science - ASIAN 1999 - 5th Asian Computing Science Conference, Proceedings (pp. 227-238). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1742). Springer Verlag. https://doi.org/10.1007/3-540-46674-6_20

Mukund, Madhavan ; Narayan Kumar, K. ; Smolka, Scott A. / Faster model checking for open systems. Advances in Computing Science - ASIAN 1999 - 5th Asian Computing Science Conference, Proceedings. editor / Roland Yap ; P.S. Thiagarajan. Springer Verlag, 1999. pp. 227-238 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{873f8b79a1e547fbbf8da59ef106aaab,

title = "Faster model checking for open systems",

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.",

author = "Madhavan Mukund and \{Narayan Kumar\}, K. and Smolka, \{Scott A.\}",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1999.; 5th Asian Computing Science Conference on Advances in Computing Science, ASIAN 1999 ; Conference date: 10-12-1999 Through 12-12-1999",

year = "1999",

doi = "10.1007/3-540-46674-6\_20",

language = "English",

isbn = "354066856X",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "227--238",

editor = "Roland Yap and P.S. Thiagarajan",

booktitle = "Advances in Computing Science - ASIAN 1999 - 5th Asian Computing Science Conference, Proceedings",

}

Mukund, M, Narayan Kumar, K & Smolka, SA 1999, Faster model checking for open systems. in R Yap & PS Thiagarajan (eds), Advances in Computing Science - ASIAN 1999 - 5th Asian Computing Science Conference, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1742, Springer Verlag, pp. 227-238, 5th Asian Computing Science Conference on Advances in Computing Science, ASIAN 1999, Phuket, Thailand, 12/10/99. https://doi.org/10.1007/3-540-46674-6_20

Faster model checking for open systems. / Mukund, Madhavan; Narayan Kumar, K.; Smolka, Scott A.
Advances in Computing Science - ASIAN 1999 - 5th Asian Computing Science Conference, Proceedings. ed. / Roland Yap; P.S. Thiagarajan. Springer Verlag, 1999. p. 227-238 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1742).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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

AN - SCOPUS:84958811902

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 -

Mukund M, Narayan Kumar K, Smolka SA. Faster model checking for open systems. In Yap R, Thiagarajan PS, editors, Advances in Computing Science - ASIAN 1999 - 5th Asian Computing Science Conference, Proceedings. Springer Verlag. 1999. p. 227-238. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-46674-6_20

Faster model checking for open systems

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this