An improved algorithm for the evaluation of fixpoint expressions

DOI10.1016/S0304-3975(96)00228-9zbMath0901.68118OpenAlexW1974672595MaRDI QIDQ1391536

D. Massart

Publication date: 22 July 1998

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(96)00228-9

zbMATH Keywords

verification procedures

Mathematics Subject Classification ID

Parallel algorithms in computer science (68W10) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (25)

Verifying persistent security properties ⋮ Symmetric Strategy Improvement ⋮ The mu-calculus and Model Checking ⋮ Fast and simple nested fixpoints ⋮ From Parity and Payoff Games to Linear Programming ⋮ Solving parity games in big steps ⋮ Deciding Parity Games in Quasi-polynomial Time ⋮ Towards the hierarchical verification of reactive systems ⋮ Unnamed Item ⋮ Parameterized Algorithms for Parity Games ⋮ Improved complexity analysis of quasi-polynomial algorithms solving parity games ⋮ Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games ⋮ Model checking the full modal mu-calculus for infinite sequential processes ⋮ Inf-datalog, Modal Logic and Complexities ⋮ GR(1)*: GR(1) specifications extended with existential guarantees ⋮ Assume-admissible synthesis ⋮ Unnamed Item ⋮ Three notes on the complexity of model checking fixpoint logic with chop ⋮ The alternation hierarchy in fixpoint logic with chop is strict too ⋮ Solving Parity Games in Big Steps ⋮ Quasipolynomial computation of nested fixpoints ⋮ Performance heuristics for GR(1) synthesis and related algorithms ⋮ Parity Games: Zielonka's Algorithm in Quasi-Polynomial Time ⋮ The modal mu-calculus alternation hierarchy is strict ⋮ Probabilistic temporal logics via the modal mu-calculus

Cites Work

• Unnamed Item
• A unified approach for showing language inclusion and equivalence between various types of \(\omega\)-automata
• A linear algorithm to solve fixed-point equations on transition systems
• Symbolic model checking: \(10^{20}\) states and beyond
• Model checking and boolean graphs
• Graph-Based Algorithms for Boolean Function Manipulation

This page was built for publication: An improved algorithm for the evaluation of fixpoint expressions