Symbolic model checking for temporal-epistemic logic

DOI10.1007/978-3-642-29414-3_10MaRDI QIDQ2900477zbMATH OpenOpenAlexFDO

Authors Alessio Lomuscio, Wojciech Penczek

Publication date 23 July 2012

Published in Logic Programs, Norms and Action (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-29414-3_10

Mathematics Subject Classification ID

Logics of knowledge and belief (including belief change) (03B42) Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2182497
• A SAT-based approach to unbounded model checking for alternating-time temporal epistemic logic
• Bounded model checking for temporal epistemic logic in synchronous multi-agent systems
• Parallel model checking for temporal epistemic logic
• Symbolic Model Checking of Logics with Actions

Cited in

(20)

• A SAT-based approach to unbounded model checking for alternating-time temporal epistemic logic
• A three-value abstraction technique for the verification of epistemic properties in multi-agent systems
• Parallel model checking for temporal epistemic logic
• The complexity of epistemic model checking: clock semantics and branching time
• Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic
• Formal semantics of meta-level architectures: Temporal epistemic reflection
• Symbolic Model Checking for Dynamic Epistemic Logic
• Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic
• A data symmetry reduction technique for temporal-epistemic logic
• Symbolic model checking for Dynamic Epistemic Logic — S5 and beyond*
• Linear temporal logic symbolic model checking
• scientific article; zbMATH DE number 2182497 (Why is no real title available?)
• scientific article; zbMATH DE number 2087624 (Why is no real title available?)
• Symbolic Model Checking of Logics with Actions
• QBF-Based Symbolic Model Checking for Knowledge and Time
• Decidability of model checking with the temporal logic EF
• Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic
• To know or not to know: Epistemic approaches to security protocol verification
• Interpreting knowledge-based programs
• Complexity of multi-agent conformant planning with group knowledge

Describes a project that uses

Uses Software

• CUDD
• Verics
• MCK
• SPIN
• NuSMV
• MCMAS

This page was built for publication: Symbolic model checking for temporal-epistemic logic

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