Accession Number : ADA317576

Title :   Model Checking Algorithms for the mu-Calculus,

Corporate Author : CARNEGIE-MELLON 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 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.

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