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) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

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

(19)

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

Describes a project that uses

Uses Software

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

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)