Abstract
In this paper we improve a model checking algorithm based on the tableau method of Stirling and Walker. The algorithm proves whether a property expressed in the modal mu-calculus holds for a state in a finite transition system. It makes subsequent use of subtableaux which were calculated earlier in the proof run. These subtableaux are reduced to expressions. Examples show that both size of tableaux and execution time of the algorithm are reduced.
supported by Siemens AG, Corporate Research and Development
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Julian Bradfield, Verifying Temporal Properties of Systems, Birkhäuser,1992.
J.R.Burch, E.M.Clarke, K.L.McMillan, D.L.Dili and L.J.Hwang, Symbolic model checking: 1020 states and beyond, in: Information and Computation, Vol 98, Num 2, June 1992, (141–170).
Julian Bradfield and Colin Stirling, Verifying Temporal Properties of Processes, CONCUR 1990, in: LNCS 458, Springer Verlag, Berlin, 1991, (115–125).
Ranee Cleaveland, Tableau Based Model Checking in the Propositional Mu-Calculus, in: Acta Informatica, 1990, (725–747).
Ranee Cleaveland and Bernhard Steffen, A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus, in: Proc. of the Third Workshop on Computer Aided Verification, LNCS 575, 1992, (48–58).
Ranee Cleaveland and Bernhard Steffen, Computing Behavourial Relations, Logically, in: Proc. 1CALP '91, 1991.
Reinhard Enders, Thomas Filkorn, Dirk Taubner, Generating BDDs for Symbolic Model Checking in CCS, in: Proc. of the Third Workshop on Computer Aided Verification, LNCS 575, 1992, (203–213).
E.Allen Emerson and Ching-Luang Lei, Efficient model checking in fragments of the propositional mu-calculus, in: Proc. of Symposium on Logic in Computer Science, IEEE, 1986, (267–278).
Colin Stirling, Modal and Temporal Logics, in: S.Abramsky, D.Gabbay, and T.Maibaum, editors, Handbook of Logic in Computer Science, Oxford University Press.
Colin Stirling and David Walker, Local model checking in the modal mu-calculus, in: Proc. International Conference on Theory and Practice of Software Development, LNCS 351, Springer Verlag, Berlin, 1989, (369–382).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mader, A. (1993). Tableau recycling. In: von Bochmann, G., Probst, D.K. (eds) Computer Aided Verification. CAV 1992. Lecture Notes in Computer Science, vol 663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56496-9_26
Download citation
DOI: https://doi.org/10.1007/3-540-56496-9_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56496-6
Online ISBN: 978-3-540-47572-9
eBook Packages: Springer Book Archive