Technical reports

Demonstration programs for CTL and μ-calculus symbolic model checking

Martin Richards

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}
}