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

time complexityfixed point equationtemporal logicscorrectnesstransition systemmodel-checker

Mathematics Subject Classification ID

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

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)

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

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)