Verification of reactive systems via instantiation of parameterised Boolean equation systems

DOI10.1016/j.ic.2010.11.025zbMath1215.68133MaRDI QIDQ716322

B. Ploeger, J. W. Wesselink, Tim A. C. Willemse

Publication date: 28 April 2011

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2010.11.025

zbMATH Keywords

verification; model checking; modal \(\mu \)-calculus; parameterised Boolean equation systems

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Related Items

Abstraction in Fixpoint Logic

Uses Software

• mCRL2
• CAESAR_SOLVE
• PGSolver

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Programming languages and their definition. Selected papers ed. by C. B. Jones
• Results on the propositional \(\mu\)-calculus
• A calculus of communicating systems
• Model-checking processes with data
• Parameterised Boolean equation systems
• A lattice-theoretical fixpoint theorem and its applications
• Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems
• An Optimal Strategy Improvement Algorithm for Solving Parity and Payoff Games
• Invariants for Parameterised Boolean Equation Systems
• Static Analysis Techniques for Parameterised Boolean Equation Systems
• Solving Parity Games in Practice
• Process Algebra
• Branching time and abstraction in bisimulation semantics
• A Multi-Core Solver for Parity Games
• Solving Parity Games in Big Steps
• Instantiation for Parameterised Boolean Equation Systems
• Symbolic transition graph with assignment