Improved model checking of hierarchical systems

DOI10.1016/J.IC.2011.10.008MaRDI QIDQ418123zbMATH OpenOpenAlexFDO

Authors Benjamin Aminof, Orna Kupferman, Aniello Murano

Publication date 24 May 2012

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

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

zbMATH Keywords

model checkingtwo-player gamesparity gamesabstraction-refinementbranching-time temporal logicshierarchical systems

Mathematics Subject Classification ID

Applications of game theory (91A80) 2-person games (91A05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Improved model checking of hierarchical systems
• Program Complexity in Hierarchical Module Checking
• Mathematical Foundations of Computer Science 2004
• Model Checking Games for Branching Time Logics
• Fixpoint logics over hierarchical structures

Cites work

• scientific article; zbMATH DE number 1693039 (Why is no real title available?)
• scientific article; zbMATH DE number 3926220 (Why is no real title available?)
• scientific article; zbMATH DE number 2080197 (Why is no real title available?)
• scientific article; zbMATH DE number 1500644 (Why is no real title available?)
• scientific article; zbMATH DE number 1796135 (Why is no real title available?)
• scientific article; zbMATH DE number 1903350 (Why is no real title available?)
• A game-based framework for CTL counterexamples and 3-valued abstraction-refinement
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Alternating automata on infinite trees
• Alternating tree automata, parity games, and modal \(\mu\)-calculus
• An automata-theoretic approach to branching-time model checking
• Automata for the modal \(\mu \)-calculus and related results
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Complexity of equivalence problems for concurrent systems of finite agents
• Complexity results on branching-time pushdown model checking
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Languages of Nested Trees
• On the power of bounded concurrency I
• Program Complexity in Hierarchical Module Checking
• Pushdown processes: Games and model-checking
• Reachability analysis of pushdown automata: Application to model-checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification of scope-dependent hierarchical state machines
• When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus

Cited in

(20)

• Mathematical Foundations of Computer Science 2004
• LTL with arithmetic and its applications in reasoning about hierarchical systems
• CTL\(^\ast\) with graded path modalities
• Hierarchical cost-parity games
• Hierarchical cost-parity games
• Model-checking hierarchical structures
• Fixpoint logics over hierarchical structures
• Program Complexity in Hierarchical Module Checking
• Hierarchical network formation games
• Model checking properties on reduced trace systems
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Multi-valued verification of strategic ability
• Improving parity games in practice
• Solving parity games using an automata-based algorithm
• Improved model checking of hierarchical systems
• Verification of hierarchical state/Event systems using reusability and compositionality
• A Parametrized Analysis of Algorithms on Hierarchical Graphs
• scientific article; zbMATH DE number 1852148 (Why is no real title available?)
• An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information
• scientific article; zbMATH DE number 1852146 (Why is no real title available?)

This page was built for publication: Improved model checking of hierarchical systems

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