Game-theoretic simulation checking tool

DOI10.1134/S0361768811040013MaRDI QIDQ764005zbMATH OpenFDO

Authors P. E. Bulychev

Publication date 12 March 2012

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

zbMATH Keywords

model checkingspecificationtemporal logicprogram correctnessKripke structurelabeled transition systemssimulation checking game-theoretic approach

Mathematics Subject Classification ID

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

Recommendations

• Model checking downward simulations
• Bisimulation, modal logic and model checking games
• scientific article; zbMATH DE number 2080188
• Software model checking based on game semantics and CSP
• scientific article; zbMATH DE number 910719

Cites work

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

Cited in

(2)

• Equivalence checking 40 years after: a review of bisimulation tools
• Model checking downward simulations

Describes a project that uses

Uses Software

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

This page was built for publication: Game-theoretic simulation checking tool

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