Technical reports
Demonstration programs for CTL and μ-calculus symbolic model checking
August 1997, 41 pages
DOI: 10.48456/tr-434
Abstract
This paper presents very simple implementations of Symbolic Model Checkers for both Computational Tree Logic (CTL) and μ-calculus. They are intended to be educational rather than practical. The first program discovers, for a given non-deterministic finite state machine (NFSM), the states for which a given CTL formula holds. The second program does the same job for μ-calculus formulae.
For simplicity the number of states in the NFSM has been limited to 32 and a bit pattern representation is used to represent the boolean functions involved. It would be easy to extend both programs to use ordered binary decision diagrams more normally used in symbolic model checking.
The programs include lexical and syntax analysers for the formulae, the model checking algorithms and drivers to exercise them with respect to various simple machines. The programs are implemented in MCPL. A brief summary of MCPL is given at the end.
Full text
PDF (1.8 MB)
BibTeX record
@TechReport{UCAM-CL-TR-434, author = {Richards, Martin}, title = {{Demonstration programs for CTL and $\mu$-calculus symbolic model checking}}, year = 1997, month = aug, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-434.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-434}, number = {UCAM-CL-TR-434} }