Local Logics for Traces

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.