Model checking and boolean graphs

DOI10.1016/0304-3975(94)90266-6zbMATH Open0798.03017OpenAlexW2756011084MaRDI QIDQ1325844FDOQ1325844

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

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

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)

Cites Work

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

Cited In (30)

• First-Order Model-Checking in Random Graphs and Complex Networks
• Partially dynamic maintenance of minimum weight hyperpaths
• Combining static analysis and case-based search space partitioning for reducing peak memory in model checking
• FO model checking on geometric graphs
• Equivalence checking 40 years after: a review of bisimulation tools
• Sequential and distributed on-the-fly computation of weak tau-confluence
• Operations on fixpoint equation systems
• A graphical \(\mu\)-calculus and local model checking.
• Fast and simple nested fixpoints
• Model checking the full modal mu-calculus for infinite sequential processes
• A compositional \(\mu\)-calculus proof system for statecharts processes
• Is your model checker on time? On the complexity of model checking for timed modal logics
• Symbolic bounded synthesis
• Polynomial approximations for model checking
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• 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 \(\mu \)-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
• Title not available (Why is that?)
• An improved algorithm for the evaluation of fixpoint expressions
• 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)