Model Checking Algorithms for the mu-Calculus,
Abstract
The propositional mu-calculus is a powerful language for expressing properties of transition systems by using least and greatest fixpoint operators. Recently, the mu-calculus has generated much interest among researchers in computer-aided verification. This interest stems from the fact that many temporal and program logics can be encoded into the mu-calculus. In addition, important relations between transition systems, such as weak and strong bisimulation equivalence, also have fixpoint characterizations. Wide-spread use of binary decision diagrams has made fixpoint based algorithms even more important, since methods that require the manipulation of individual states do not take advantage of this representation.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 23, 1996
- Accession Number
- ADA317576
Entities
People
- Edmund M. Clarke
- Sergey Berezin
- Somesh Jha
- Will Marrero
Organizations
- Carnegie Mellon University