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

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

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)