On guarding nested fixpoints

DOI10.1007/3-540-48168-0_34MaRDI QIDQ4945246zbMATH OpenFDO

Authors Helmut Seidl, Andreas Neumann

Publication date 20 September 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48168-0_34

zbMATH Keywords

\(\mu\)-calculusdistributive latticeguardednesshierarchical system of equationsloop-connectednessregular tree pattern-matchingvariable dependence graph

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

For every hierarchical system of equations \(S\) over some complete and distributive lattice we construct an equivalent system with the same set of variables which additionally is guarded. The price to be paid is that the resulting right-hand sides may grow exponentially. We therefore present methods how the exponential blow-up can be avoided. Especially, the loop structure of the variable dependence graph is taken into account. Also we prove that size \({\mathcal O}(m\cdot|S|)\) suffices whenever \(S\) originates from a fixpoint expression where the nesting-depth of fixpoints is at most \(m\). Finally, we sketch an application to regular tree pattern-matching. For the entire collection see [Zbl 0929.00039].

Recommendations

• Fast and simple nested fixpoints
• An improved algorithm for the evaluation of fixpoint expressions
• Quasipolynomial computation of nested fixpoints
• Solving fixed-point equations by derivation tree analysis
• Equivalence and normal forms for the restricted and bounded fixpoint in the nested algebra

Cited in

(4)

• Crossing the syntactic barrier: hom-disequalities for \({\mathcal H}_1\)-clauses
• The mu-calculus and Model Checking
• Paths, tree homomorphisms and disequalities for H₁-clauses
• Size measures and alphabetic equivalence in the -calculus

This page was built for publication: On guarding nested fixpoints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4945246)