On-the-fly reachability and cycle detection for recursive state machines

Rajeev Alur; Swarat Chaudhuri; Kousha Etessami; P. Madhusudan

doi:10.1007/978-3-540-31980-1_5

On-the-fly reachability and cycle detection for recursive state machines

Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan

Research output: Contribution to journal › Conference article › peer-review

Abstract

Searching the state space of a system using enumerative and on-the-fly depth-first traversal is an established technique for model checking finite-state systems. In this paper, we propose algorithms for on-the-fly exploration of recursive state machines, or equivalently pushdown systems, which are suited for modeling the behavior of procedural programs. We present algorithms for reachability (is a bad state reachable?) as well as for fair cycle detection (is there a reachable cycle with progress?). We also report on an implementation of these algorithms to check safety and liveness properties of recursive boolean programs, and its performance on existing benchmarks.

Original language	English (US)
Pages (from-to)	61-76
Number of pages	16
Journal	Lecture Notes in Computer Science
Volume	3440
DOIs	https://doi.org/10.1007/978-3-540-31980-1_5
State	Published - 2005
Event	11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 - Edinburgh, United Kingdom Duration: Apr 4 2005 → Apr 8 2005

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Online availability

10.1007/978-3-540-31980-1_5

Library availability

Discover UIUC Full Text

Cite this

@article{526545cb9fb7475bb0a9756971fc883e,

title = "On-the-fly reachability and cycle detection for recursive state machines",

abstract = "Searching the state space of a system using enumerative and on-the-fly depth-first traversal is an established technique for model checking finite-state systems. In this paper, we propose algorithms for on-the-fly exploration of recursive state machines, or equivalently pushdown systems, which are suited for modeling the behavior of procedural programs. We present algorithms for reachability (is a bad state reachable?) as well as for fair cycle detection (is there a reachable cycle with progress?). We also report on an implementation of these algorithms to check safety and liveness properties of recursive boolean programs, and its performance on existing benchmarks.",

author = "Rajeev Alur and Swarat Chaudhuri and Kousha Etessami and P. Madhusudan",

year = "2005",

doi = "10.1007/978-3-540-31980-1_5",

language = "English (US)",

volume = "3440",

pages = "61--76",

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

issn = "0302-9743",

publisher = "Springer",

note = "11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 ; Conference date: 04-04-2005 Through 08-04-2005",

}

TY - JOUR

T1 - On-the-fly reachability and cycle detection for recursive state machines

AU - Alur, Rajeev

AU - Chaudhuri, Swarat

AU - Etessami, Kousha

AU - Madhusudan, P.

PY - 2005

Y1 - 2005

N2 - Searching the state space of a system using enumerative and on-the-fly depth-first traversal is an established technique for model checking finite-state systems. In this paper, we propose algorithms for on-the-fly exploration of recursive state machines, or equivalently pushdown systems, which are suited for modeling the behavior of procedural programs. We present algorithms for reachability (is a bad state reachable?) as well as for fair cycle detection (is there a reachable cycle with progress?). We also report on an implementation of these algorithms to check safety and liveness properties of recursive boolean programs, and its performance on existing benchmarks.

AB - Searching the state space of a system using enumerative and on-the-fly depth-first traversal is an established technique for model checking finite-state systems. In this paper, we propose algorithms for on-the-fly exploration of recursive state machines, or equivalently pushdown systems, which are suited for modeling the behavior of procedural programs. We present algorithms for reachability (is a bad state reachable?) as well as for fair cycle detection (is there a reachable cycle with progress?). We also report on an implementation of these algorithms to check safety and liveness properties of recursive boolean programs, and its performance on existing benchmarks.

UR - http://www.scopus.com/inward/record.url?scp=24644501837&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=24644501837&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-31980-1_5

DO - 10.1007/978-3-540-31980-1_5

M3 - Conference article

AN - SCOPUS:24644501837

SN - 0302-9743

VL - 3440

SP - 61

EP - 76

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

T2 - 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005

Y2 - 4 April 2005 through 8 April 2005

ER -

On-the-fly reachability and cycle detection for recursive state machines

Abstract

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this