An improved algorithm for the evaluation of fixpoint expressions

DOI10.1016/S0304-3975(96)00228-9MaRDI QIDQ1391536zbMATH OpenOpenAlexFDO

Authors D. Massart, Anca Browne, Edmund Clarke, Somesh Jha, David E. Long, Will Marrero

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

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

Recommendations

• IMPROVING THE COMPUTATIONAL EFFICIENCY OF FIXED POINT ALGORITHMS
• An improvement to the fixed point iterative method
• A Step Up in Expressiveness of Decidable Fixpoint Logics
• scientific article; zbMATH DE number 1231479
• A Faster Algorithm for Finding Tarski Fixed Points
• Improvement of fixed point algorithms from a triangulation
• An improved exact algorithm for the exact satisfiability problem
• Programmological aspects of the fixed point method
• scientific article; zbMATH DE number 123812
• scientific article; zbMATH DE number 4024646

Cites work

• A linear algorithm to solve fixed-point equations on transition systems
• A unified approach for showing language inclusion and equivalence between various types of -automata
• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• Model checking and boolean graphs
• Symbolic model checking: \(10^{20}\) states and beyond

Cited in

(38)

• A linear algorithm to solve fixed-point equations on transition systems
• An example of sequentialization of a parallel algorithm
• The modal mu-calculus alternation hierarchy is strict
• Fast and simple nested fixpoints
• Verifying persistent security properties
• Model checking the full modal mu-calculus for infinite sequential processes
• GR(1)*: GR(1) specifications extended with existential guarantees
• Quasipolynomial computation of nested fixpoints
• Performance heuristics for GR(1) synthesis and related algorithms
• The alternation hierarchy in fixpoint logic with chop is strict too
• Probabilistic temporal logics via the modal mu-calculus
• Parameterized Algorithms for Parity Games
• Synthesising strategy improvement and recursive algorithms for solving 2.5 player parity games
• The mu-calculus and Model Checking
• From Parity and Payoff Games to Linear Programming
• Solving parity games in big steps
• Symmetric strategy improvement
• Inf-datalog, Modal Logic and Complexities
• Fixpoints and search in PVS
• scientific article; zbMATH DE number 1536554 (Why is no real title available?)
• A distributed fixed-point algorithm for extended dependency graphs
• On guarding nested fixpoints
• Deciding Parity Games in Quasi-polynomial Time
• scientific article; zbMATH DE number 7533361 (Why is no real title available?)
• Parity Games: Zielonka's Algorithm in Quasi-Polynomial Time
• Assume-admissible synthesis
• Parity games with weights
• Three notes on the complexity of model checking fixpoint logic with chop
• Solving Parity Games in Big Steps
• Towards the hierarchical verification of reactive systems
• Improved complexity analysis of quasi-polynomial algorithms solving parity games
• Efficient Algorithms for Omega-Regular Energy Games
• A direct symbolic algorithm for solving stochastic Rabin games
• GR(1)*: GR(1) specifications extended with existential guarantees
• Priority promotion with Parysian flair
• A quasi-polynomial black-box algorithm for fixed point evaluation
• An objective improvement approach to solving discounted payoff games
• An objective improvement approach to solving discounted payoff games

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

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