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