A linear algorithm to solve fixed-point equations on transition systems

DOI10.1016/0020-0190(88)90029-4MaRDI QIDQ1115196zbMATH OpenOpenAlexFDO

Authors André Arnold, Paul Crubille

Publication date 1988

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(88)90029-4

zbMATH Keywords

correctnessfixed point equationmodel-checkertemporal logicstime complexitytransition system

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Graph theory (including graph drawing) in computer science (68R10)

Review text

The authors give an algorithm to compute the least fixed point of a system of equations over a transition system. This algorithm has a time complexity linear in the size of the transition system. The proof of the correctness of the presented algorithm is given.

Recommendations

• An example of sequentialization of a parallel algorithm
• COMPUTING LEAST FIXED POINTS OF PROBABILISTIC SYSTEMS OF POLYNOMIALS
• Precise Fixpoint Computation Through Strategy Iteration
• scientific article; zbMATH DE number 4066981
• An improved algorithm for the evaluation of fixpoint expressions

Cites work

• A unified approach for studying the properties of transition systems
• An algebraic and algorithmic method for analysing transition systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Depth-First Search and Linear Graph Algorithms
• Formal verification of parallel programs
• Results on the propositional \(\mu\)-calculus

Cited in

(21)

• Characterizing finite Kripke structures in propositional temporal logic
• An example of sequentialization of a parallel algorithm
• Model checking and boolean graphs
• Fast and simple nested fixpoints
• An improved algorithm for the evaluation of fixpoint expressions
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Is your model checker on time? On the complexity of model checking for timed modal logics
• A planner agent that tries its best in presence of nondeterminism
• Consistent consequence for Boolean equation systems
• The mu-calculus and Model Checking
• Solving Linear Equations in *-continuous Action Lattices
• Inf-datalog, Modal Logic and Complexities
• Sequential and distributed on-the-fly computation of weak tau-confluence
• A selection property of the boolean \mu -calculus and some of its applications
• Efficient local correctness checking for single and alternating boolean equation systems
• Verification and comparison of transition systems
• Compositional checking of satisfaction
• A linear-time model-checking algorithm for the alternation-free modal mu-calculus
• Compositional checking of satisfaction
• The expressive power of implicit specifications
• A unified approach for showing language inclusion and equivalence between various types of -automata

This page was built for publication: A linear algorithm to solve fixed-point equations on transition systems

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