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

DOI10.1016/0020-0190(88)90029-4zbMath0663.68075OpenAlexW2002570665MaRDI QIDQ1115196

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 equationtime complexitytransition systemtemporal logicsmodel-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)

Related Items

Model checking and boolean graphs, Consistent Consequence for Boolean Equation Systems, Verification and comparison of transition systems, The mu-calculus and Model Checking, Fast and simple nested fixpoints, Characterizing finite Kripke structures in propositional temporal logic, An improved algorithm for the evaluation of fixpoint expressions, A planner agent that tries its best in presence of nondeterminism, Sequential and distributed on-the-fly computation of weak tau-confluence, Efficient local correctness checking for single and alternating boolean equation systems, Inf-datalog, Modal Logic and Complexities, A selection property of the boolean $\mu $-calculus and some of its applications, Compositional checking of satisfaction, The expressive power of implicit specifications, A unified approach for showing language inclusion and equivalence between various types of \(\omega\)-automata, 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

Cites Work

• Results on the propositional \(\mu\)-calculus
• 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
• Formal verification of parallel programs
• Depth-First Search and Linear Graph Algorithms