@device(postscript)
@libraryfile(Mathematics10)
@libraryfile(Accents)
@style(fontfamily=timesroman,fontscale=11)
@pagefooting(immediate, left "@c<Technical Report 1996>",
center "@c<Computer Science>",
right "@c<Carnegie Mellon>")
@heading(Model Checking Algorithms for the @g<m>-Calculus)
@heading(CMU-CS-96-180)
@center(@b(Sergey Berezin, Edmund Clarke, Somesh Jha, Will Marrero))
@center(September 1996)
@center(FTP: CMU-CS-96-180.ps)
@blankspace(1)
@begin(text)

The propositional @g(m)-calculus is a powerful language for expressing
properties of transition systems by using least and greatest fixpoint
operators.  Recently, the @g<m>-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 @g<m>-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.

@blankspace(2line)
@begin(transparent,size=10)
@b(Keywords:@ )@c<Automatic verification, temporal logic, model checking,
binary decision diagrams, bisimulation>
@end(transparent)
@blankspace(1line)
@end(text)
@flushright(@b[(28 pages)])