Model checking and boolean graphs

DOI10.1016/0304-3975(94)90266-6MaRDI QIDQ1325844zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• A graphical \(\mu\)-calculus and local model checking.
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Local model checking in the modal mu-calculus
• scientific article; zbMATH DE number 2080055
• On model checking for the \(\mu\)-calculus and its fragments

Cites work

• scientific article; zbMATH DE number 4131643 (Why is no real title available?)
• scientific article; zbMATH DE number 5542185 (Why is no real title available?)
• scientific article; zbMATH DE number 4056971 (Why is no real title available?)
• scientific article; zbMATH DE number 177838 (Why is no real title available?)
• A lattice-theoretical fixpoint theorem and its applications
• A linear algorithm to solve fixed-point equations on transition systems
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Compositional checking of satisfaction
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• On the computational power of pushdown automata
• Programming languages and their definition. Selected papers ed. by C. B. Jones
• Results on the propositional \(\mu\)-calculus
• Tableau-based model checking in the propositional mu-calculus

Cited in

(30)

• Equivalence checking 40 years after: a review of bisimulation tools
• An improved algorithm for the evaluation of fixpoint expressions
• Partially dynamic maintenance of minimum weight hyperpaths
• Model checking in the modal \(\mu \)-calculus and generic solutions
• Polynomial approximations for model checking
• Sequential and distributed on-the-fly computation of weak tau-confluence
• CADP 2010: a toolbox for the construction and analysis of distributed processes
• A graphical \(\mu\)-calculus and local model checking.
• Model checking for hybrid logic
• Game-theoretic simulation checking tool
• FO model checking on geometric graphs
• Fast mu-calculus model checking when tree-width is bounded.
• Step semantics of Boolean nets
• On Diagrams and General Model Checkers
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Temporal verification of programs via first-order fixpoint logic
• Fast and simple nested fixpoints
• scientific article; zbMATH DE number 1406235 (Why is no real title available?)
• The mu-calculus and Model Checking
• A selection property of the boolean $\mu $-calculus and some of its applications
• Operations on fixpoint equation systems
• Compositional verification of asynchronous concurrent systems using CADP
• Combining static analysis and case-based search space partitioning for reducing peak memory in model checking
• Is your model checker on time? On the complexity of model checking for timed modal logics
• Symbolic bounded synthesis
• First-Order Model-Checking in Random Graphs and Complex Networks
• Model checking the full modal mu-calculus for infinite sequential processes
• Computation Tree Regular Logic for Genetic Regulatory Networks
• Probabilistic temporal logics via the modal mu-calculus
• A compositional \(\mu\)-calculus proof system for statecharts processes

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

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