Efficient on-the-fly model checking for CTL
Published 19 November 2002
Girish Bhat, Rance Cleaveland, Orna Grümberg
Citations117
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
An on-the-fly algorithm for determining whether a finite-state system satisfies a formula in the temporal logic CTL, and it performs as well as the best known global algorithms for the sublogics CTL and LTL.
Abstract
This paper gives an on-the-fly algorithm for determining whether a finite-state system satisfies a formula in the temporal logic CTL. The time complexity of our algorithm matches that of the best existing "global algorithm" for model checking in this logic, and it performs as well as the best known global algorithms for the sublogics CTL and LTL. In contrast with these approaches, however, our routine constructs the state space of the system under consideration in a need-driven fashion and will therefore perform better in practice.
Keywords
Computer Science
The Design and Analysis of Computer Algorithms
9,456 Citations1974Alfred V. Aho, John E. Hopcroft
This text introduces the basic data structures and programming techniques often used in efficient algorithms, and covers use of lists, push-down stacks, queues, trees, and graphs.
ACM Transactions on Programming Languages and SystemsAutomatic verification of finite-state concurrent systems using temporal logic specifications
3,555 Citations1986E. M. Clarke, E. Allen Emerson +1 more
It is argued that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems.
Information and ComputationSymbolic model checking: 1020 States and beyond
2,674 Citations1992Jerry R. Burch, E. M. Clarke +3 more
It is shown how the novel mu-calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment of finite omega -automata.
Lecture notes in computer scienceSpecification and verification of concurrent systems in CESAR
1,277 Citations1982J. P. Queille, Joseph Sifakis
By an example, the alternating bit protocol, the use of CESAR, an interactive system for aiding the design of distributed applications, is illustrated.
Open Repository and Bibliography (University of Liège)An Automata-Theoretic Approach to Automatic Program Verification
1,254 Citations1986Moshe Y. Vardi, Pierre Wolper
Journal of the ACM“Sometimes” and “not never” revisited
996 Citations1986E. Allen Emerson, Joseph Y. Halpern
A language, CTL*, in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined and the expressive power of a number of sublanguages is compared.
Munich Personal RePEc Archive (Ludwig Maximilian University of Munich)Symbolic model checking: an approach to the state explosion problem
980 Citations1992Kenneth L. McMillan
Checking that finite state concurrent programs satisfy their linear specification
618 Citations1985Orna Lichtenstein, Amir Pnueli
An algorithm for checking satisfiability of a linear time temporal logic formula over a finite state concurrent program and a formal proof in case the formula is valid over the program is presented.
Journal of the ACMAn automata-theoretic approach to branching-time model checking
616 Citations2000Orna Kupferman, Moshe Y. Vardi +1 more
It is shown that alternating tree automata are the key to a comprehensive automata-theoretic framework for branching temporal logics, and can be used to obtain optimal decision procedures and make it possible to derive optimal model-checking algorithms.
ACM Transactions on Programming Languages and SystemsThe concurrency workbench
555 Citations1993Rance Cleaveland, Joachim Parrow +1 more
The Concurrency Workbench is an automated tool for analyzing networks of finite-state processes expressed in Milner's Calculus of Communicating Systems and a large number of interesting verification methods can be formulated as combinations of a small number of primitive algorithms.
Formal Methods in System DesignMemory-efficient algorithms for the verification of temporal properties
498 Citations1992C. Courcoubetis, M. Vardi +2 more
Algorithms are presented that solve the emptiness problem without explicitly constructing the strongly connected components of the graph representing the product automaton by allowing the algorithms to err with some probability.
Science of Computer ProgrammingModalities for model checking: branching time logic strikes back
327 Citations1987E. Allen Emerson, Chin‐Laung Lei
This paper presents a unified approach for efficient model checking under a broad class of generalized fairness constraints in a branching time framework extending that of Clarke et al. (1983), and argues that branching time logic is always better than linear time logic for model checking.
Formal Methods in System DesignA linear-time model-checking algorithm for the alternation-free modal mu-calculus
223 Citations1993Rance Cleaveland, Bernhard Steffen
A model-checking algorithm for a logic that permits propositions to be defined using greatest and least fixed points of mutually recursive systems of equations is developed, which improves on the best known algorithm for similar fixed-point logics.
IEEE Transactions on ComputersAutomatic Verification of Sequential Circuits Using Temporal Logic
203 Citations1986Browne, Clarke +2 more
An automatic verification system for sequential circuits in which specifications are expressed in a propositional temporal logic, which does not require any user assistance and is quite fast—experimental results show that state machines with several hundred states can be checked for correctness in a matter of seconds.
Information and ControlDeciding full branching time logic
191 Citations1984E. Allen Emerson, A. Prasad Sistla
It is shown that the problem of determining if a CTL* formula is satisfiable in a structure generated by a binary relation is decidable in triple exponential time.
Formal Methods in System DesignAnother Look at LTL Model Checking
191 Citations1997Edmund M. Clarke, Orna Grümberg +1 more
The SMV model checking system developed by McMillan can be extended to permit LTL specifications and the results that are obtained are quite surprising.
Formal Methods in System DesignVerification of the Futurebus+ cache coherence protocol
169 Citations1995Edmund M. Clarke, Orna Grümberg +5 more
A hardware description language is used to construct a formal model of the cache coherence protocol described in the IEEE Futurebus+standard, and temporal logic model checking techniques are applied to find errors in the standard.
Theoretical Computer ScienceCTL∗ and ECTL∗ as fragments of the modal μ-calculus
160 Citations1994Mads Dam
Direct embeddings of the full branching-time CTL ∗ and its extension ECTL ∗ into the modal μ-calculus use tableaux as intermediate representations of formulas, and use extremal fixed points to characterise those paths through tableaux that satisfy an admissibility criterion, guaranteeing eventualities to be eventually satisfied.
Theoretical Computer ScienceModel checking and boolean graphs
134 Citations1994Henrik Reif Andersen
A global model checking algorithm for the modal μ-calculus of alternation depth one, which has time-complexity A¦¦T¦, where ¦A¦ is the size of the assertion and ¦T² is thesize of the model (a labelled transition system).
Lecture notes in computer scienceYet another process logic
83 Citations1984Moshe Y. Vardi, Pierre Wolper
A process logic that differs from the one introduced by Harel, Kozen and Parikh in several ways is presented, which uses the extended temporal logic of Wolper for statements about paths and allows a “repeat” operator in the programs.
Lecture notes in computer scienceA linear local model checking algorithm for CTL
45 Citations1993B. Vergauwen, Johan Lewi
Computation Tree Logic, a form of branching time temporal logic, is used as a specification tool and a local model checking algorithm ALMC is presented, which mechanically checks whether S0 satisfies formula S0.
Lecture notes in computer scienceModel checking and boolean graphs
44 Citations1992Henrik Reif Andersen
Lecture notes in computer scienceComputation tree logic and regular ω-languages
32 Citations1989Wolfgang Thomas
A characterization of CTL* by a "non-counting property" for sets of trees shows that it is decidable whether an ECTL*- formula can be written as a CTL-formula.