返回Google圖書搜尋

Demonstration Programs for CTL and [mu]-calculus Symbolic Model Checking

出版	University of Cambridge, Computer Laboratory, 1997
URL	http://books.google.com.hk/books?id=E04gAQAAIAAJ&hl=&source=gbs_api

註釋Abstract: "This paper presents very simple implementations of Symbolic Model Checkers for both Computational Tree Logic (CTL) and [mu]- 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 [mu]-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 is [sic] implemented in MCPL. A brief summary of MCPL is given at the end."