Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic

DOI10.1007/978-3-642-20674-0_7MaRDI QIDQ3003427zbMATH OpenOpenAlexFDO

Authors Xiaowei Huang, Cheng Luo, Ron van der Meyden

Publication date 27 May 2011

Published in Model Checking and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-20674-0_7

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
• Bounded model checking for temporal epistemic logic in synchronous multi-agent systems
• A New Approach to Bounded Model Checking for Branching Time Logics
• scientific article; zbMATH DE number 7280017
• The complexity of epistemic model checking: clock semantics and branching time
• A SAT-based approach to unbounded model checking for alternating-time temporal epistemic logic
• Parallel model checking for temporal epistemic logic
• Symbolic model checking for temporal-epistemic logic
• Model checking temporal-epistemic logic using alternating tree automata

Cites work

• Complete axiomatizations for reasoning about knowledge and branching time
• Computer Aided Verification
• scientific article; zbMATH DE number 1799521 (Why is no real title available?)
• scientific article; zbMATH DE number 2064229 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• scientific article; zbMATH DE number 1390338 (Why is no real title available?)
• scientific article; zbMATH DE number 5051652 (Why is no real title available?)
• Improving the translation from ECTL to SAT
• Logic and time
• Model checking Russian cards
• The Byzantine Generals Problem
• The dining cryptographers problem: Unconditional sender and recipient untraceability

Cited in

(8)

• Completeness of bounded model checking temporal logic of knowledge
• Optimizing epistemic model checking using conditional independence (extended abstract)
• Achieving completeness in the verification of action theories by bounded model checking in ASP
• A New Approach to Bounded Model Checking for Branching Time Logics
• Implementing a fair monodic temporal logic prover
• scientific article; zbMATH DE number 2182497 (Why is no real title available?)
• scientific article; zbMATH DE number 7280017 (Why is no real title available?)
• QBF-Based Symbolic Model Checking for Knowledge and Time

Describes a project that uses

Uses Software

• MCMAS
• VerICS
• CUDD
• MCK

This page was built for publication: Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic

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