Local Logics for Traces

Igor Walukiewicz

January 2000


A mu-calculus over dependence graph representation of traces is considered. It is shown that the mu-calculus cannot express all monadic second order (MSO) properties of dependence graphs. Several extensions of the mu-calculus are presented and it is proved that these extensions are equivalent in expressive power to MSO logic. The satisfiability problem for these extensions is PSPACE complete

Available as PostScript, PDF.


Last modified: 2003-06-08 by webmaster.