@device(postscript)
@libraryfile(Mathematics10)
@libraryfile(Accents)
@style(fontfamily=timesroman,fontscale=11)
@pagefooting(immediate, left "@c",
center "@c",
right "@c")
@heading(Model Checking Algorithms for the @g-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-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-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
@end(transparent)
@blankspace(1line)
@end(text)
@flushright(@b[(28 pages)])