|
Local Logics for Traces
Igor Walukiewicz January 2000 |
Abstract:
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. |