Module checking

DOI10.1006/inco.2000.2893zbMath1003.68071OpenAlexW2913210435MaRDI QIDQ1854407

Pierre Wolper, Moshe Y. Vardi, Orna Kupferman

Publication date: 14 January 2003

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

Full work available at URL: https://doi.org/10.1006/inco.2000.2893

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)

Related Items

Modular strategies for recursive game graphs, Graded modalities in strategy logic, Querying Regular Graph Patterns, Schedulability of asynchronous real-time concurrent objects, Automata-theoretic decision of timed games, Reasoning About Strategies, Connectivity games over dynamic networks, Enriched μ–Calculus Pushdown Module Checking, Reasoning About Substructures and Games, Reasoning about graded strategy quantifiers, Unnamed Item, Hierarchical cost-parity games, Practical Efficient Modular Linear-Time Model-Checking, Exploring the boundary of half-positionality, Refinement modal logic, Model checking properties on reduced trace systems, Compositional schedulability analysis of real-time actor-based systems, Pushdown module checking, Strategy logic, Cycle detection in computation tree logic, ATL with Strategy Contexts and Bounded Memory, Improving parity games in practice, Solving Parity Games Using an Automata-Based Algorithm, Quantitatively fair scheduling, Uniform strategies, rational relations and jumping automata

Uses Software

• CESAR

Cites Work

• Results on the propositional \(\mu\)-calculus
• Automata-theoretic techniques for modal logics of programs
• Characterizing finite Kripke structures in propositional temporal logic
• A near-optimal method for reasoning about action
• Automatic verification methods for finite state systems. International workshop, Grenoble, France, June 12-14, 1989. Proceedings
• Propositional dynamic logic of regular programs
• Reasoning about infinite computations
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Deciding full branching time logic
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• Buy one, get one free!!!
• An automata-theoretic approach to branching-time model checking
• Interpolants and Symbolic Model Checking
• An axiomatic basis for computer programming
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item