Game-theoretic simulation checking tool

DOI10.1134/S0361768811040013zbMath1242.68154MaRDI QIDQ764005

P. E. Bulychev

Publication date: 12 March 2012

Published in: Programming and Computer Software (Search for Journal in Brave)

zbMATH Keywords

model checkingtemporal logicspecificationprogram correctnessKripke structurelabeled transition systemssimulation checking game-theoretic approach

Mathematics Subject Classification ID

Applications of game theory (91A80) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Equivalence checking 40 years after: a review of bisimulation tools

Uses Software

• SIGREF
• SPIN
• NuSMV
• CUDD
• Concurrency Workbench
• PyCUDD

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• An invariant-based approach to the verification of asynchronous parameterized networks
• An implementation of an efficient algorithm for bisimulation equivalence
• Characterizing finite Kripke structures in propositional temporal logic
• The temporal semantics of concurrent programs
• Model checking and boolean graphs
• Fair simulation
• NuSMV: A new symbolic model checker
• A lattice-theoretical fixpoint theorem and its applications
• Computing Stuttering Simulations
• Counterexample-guided abstraction refinement for symbolic model checking
• Sigref – A Symbolic Bisimulation Tool Box
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• Three logics for branching bisimulation
• Branching time and abstraction in bisimulation semantics
• Simulation-based minimization
• Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata
• Perspectives of System Informatics