The Algebraic Mu-Calculus and MTBDDs
Christel Baier, Edmund Melson Clarke · 1998
The paper presents a new calculus (called algebraic mu-calculus) which generalizes Park's relational mu-calculus by representing arithmetric expressions and real-valued functions rather than formulas and relations. Moreover, we give an algorithm for computing the MTBDD-representation of the semantics for the expressions and terms and show how several problems (such as graph theoretic problems or verification problems) can be embedded into the algebraic mu-calculus (and hence, can be solved using our MTBDD-based method). 1 Introduction In several disciplines of mathematics and theoretical computer science, fixed point problems play a crucial role. For example, reachability problems in graph theory, solving linear or non-linear equation systems for real or complex numbers, the computation of eigenvalues of matrices, the definition of denotational semantics for recursive programs or various verification problems for parallel or randomized systems can be reduced to certain fixed poin...