Model checking and boolean graphs

DOI10.1016/0304-3975(94)90266-6zbMath0798.03017OpenAlexW2756011084MaRDI QIDQ1325844

Henrik Reif Andersen

Publication date: 3 November 1994

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

Full work available at URL: https://doi.org/10.1016/0304-3975(94)90266-6

zbMATH Keywords

modal \(\mu\)-calculusmodel checking algorithmmarking of a Boolean graphsatisfaction problem

Mathematics Subject Classification ID

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

Related Items (18)

Combining static analysis and case-based search space partitioning for reducing peak memory in model checking ⋮ The mu-calculus and Model Checking ⋮ Fast and simple nested fixpoints ⋮ An improved algorithm for the evaluation of fixpoint expressions ⋮ Equivalence checking 40 years after: a review of bisimulation tools ⋮ Sequential and distributed on-the-fly computation of weak tau-confluence ⋮ Symbolic bounded synthesis ⋮ Computation Tree Regular Logic for Genetic Regulatory Networks ⋮ A graphical \(\mu\)-calculus and local model checking. ⋮ CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes ⋮ A selection property of the boolean $\mu $-calculus and some of its applications ⋮ Partially dynamic maintenance of minimum weight hyperpaths ⋮ Game-theoretic simulation checking tool ⋮ A compositional \(\mu\)-calculus proof system for statecharts processes ⋮ Probabilistic temporal logics via the modal mu-calculus ⋮ Model checking for hybrid logic ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics ⋮ Compositional verification of asynchronous concurrent systems using CADP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Compositional checking of satisfaction
• Programming languages and their definition. Selected papers ed. by C. B. Jones
• Results on the propositional \(\mu\)-calculus
• A linear algorithm to solve fixed-point equations on transition systems
• Tableau-based model checking in the propositional mu-calculus
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• On the computational power of pushdown automata
• A lattice-theoretical fixpoint theorem and its applications
• Linear-time algorithms for testing the satisfiability of propositional horn formulae

This page was built for publication: Model checking and boolean graphs