
Accession Number : ADA317576
Title : Model Checking Algorithms for the muCalculus,
Corporate Author : CARNEGIEMELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
Personal Author(s) : Berezin, Sergey ; Clarke, Edmund ; Jha, Somesh ; Marrero, Will
PDF Url : ADA317576
Report Date : 23 SEP 1996
Pagination or Media Count : 28
Abstract : The propositional mucalculus is a powerful language for expressing properties of transition systems by using least and greatest fixpoint operators. Recently, the mucalculus has generated much interest among researchers in computeraided verification. This interest stems from the fact that many temporal and program logics can be encoded into the mucalculus. In addition, important relations between transition systems, such as weak and strong bisimulation equivalence, also have fixpoint characterizations. Widespread 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.
Descriptors : *ALGORITHMS, *COMPUTER PROGRAM VERIFICATION, COMPUTER LOGIC, PROGRAMMING LANGUAGES, SEMANTICS, MATHEMATICAL PROGRAMMING, SYSTEMS ANALYSIS, CALCULUS, SYNTAX, CONTROL SEQUENCES, STRUCTURED PROGRAMMING.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE