Abstract
Transition systems play a central role as formal models for reactive and concurrent systems. A promising technique for automatically verifying transition systems is model checking. In the model-theoretic approach one mechanically determines whether a given transition system S 0 meets a specification f by checking whether S 0 is a model for f. In this paper Computation Tree Logic, a form of branching time temporal logic, is used as a specification tool. The paper presents a local model checking algorithm ALMC for CTL. Given a system state S 0 (typically the initial system state) and a CTL formula S 0, algorithm ALMC mechanically checks whether S 0 satisfies formula S 0. ALMC has time complexity linear in both the size of the system and the size of the formula to be checked. Furthermore ALMC is goal-oriented, i.e., in order to decide whether a formula S 0 is true in a state S 0, only a necessary part of the system-formula space is investigated. This is to be contrasted with the well-known global labeling algorithm of [4,5], where a priori all subformulae of S 0 are checked for all states.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Andersen, H. R.: Model Checking and Boolean Graphs, ESOP'92, LNCS 582, 1992
Arnold, A., Crubille, P.: A linear algorithm to solve fixed-points equations on transition systems, Information Processing Letters, vol. 29, 57–66, 1988
Brown, M.C., Clarke, E.M., Dill, D.L., Mishra, B.: Automatic verification of sequential circuits using temporal logic, IEEE Transactions on Computers, C-35, No. 12, pp. 1035–1044, 1986
Clarke, E.M., Browne, M.C., Emerson, E.A., Sistla, A.P.: Using Temporal Logic for Automatic Verification of Finite State Systems, in NATO ASI Series, Vol. F13, Logics and Models of Concurrent Systems, ed. K.R.Apt, Springer-Verlag Berlin Heidelberg, 1985
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finitestate concurrent systems using temporal logic specifications, ACM Transactions on Progr. Languages and Systems, Vol. 8, No. 2, pp. 244–263, April 1986
Cleaveland, R.: Tableau-Based Model hecking in the Propositional Mu-Calculus, Acta Informatica, 1990
Cleaveland, R., Steffen, B.: Computing Behavioural Relations, Logically, ICALP 91, pp. 127–138, LNCS 510
Cleaveland, R., Lein, M., Steffen, B.: Faster Model Checking for the Modal Mu-Calculus, CAV'92, Forthcoming
Dicky, A.: An algebraic and algorithmic method of analysing transition systems, TCS, 46, 285–303, 1986
Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional μ-calculus, LICS, 267–278, 1986
Kozen, D.: Results on the propositional mu-calculus, TCS 17, 1983
Larsen, K.G.: Proof systems for Hennessy-Milner logic with recursion, CAAP, 1988
Larsen, K.G.: Efficient local correctness checking, CAV'92, Forthcoming
Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification, (Proc.) 12th ACM annual Symposium on Principles of Programming Languages, pp. 97–107, 1985
Stirling, C., Walker, D.: Local model checking in the modal mu-calculus, TCS, October 1991, see also LNCS 351, 369–383, CAAP 1989
Vergauwen, B., Lewi, J.: A linear algorithm for solving fixed points equations on transition systems, CAAP'92, LNCS 581, 322–341
Winskel, G.: A note on model checking the modal ν-calculus, ICALP, LNCS 372, 1989, see also TCS 83, 1991
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vergauwen, B., Lewi, J. (1993). A linear local model checking algorithm for CTL. In: Best, E. (eds) CONCUR'93. CONCUR 1993. Lecture Notes in Computer Science, vol 715. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57208-2_31
Download citation
DOI: https://doi.org/10.1007/3-540-57208-2_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57208-4
Online ISBN: 978-3-540-47968-0
eBook Packages: Springer Book Archive