Epistemic Model Checking for Knowledge-Based Program Implementation: an\n Application to Anonymous Broadcast

2010/04/25 by Omar I. Al-Bataineh, Al-Bataineh, Omar I., Ron van der Meyden +1 · 1 citation
Computer Science · #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Security and Verification in Computing

paper · pdf · doi:10.48550/arxiv.1004.5130

Abstract

Knowledge-based programs provide an abstract level of description of\nprotocols in which agent actions are related to their states of knowledge. The\npaper describes how epistemic model checking technology may be applied to\ndiscover and verify concrete implementations based on this abstract level of\ndescription. The details of the implementations depend on the specific context\nof use of the protocol. The knowledge-based approach enables the\nimplementations to be optimized relative to these conditions of use. The\napproach is illustrated using extensions of the Dining Cryptographers protocol,\na security protocol for anonymous broadcast.\n

Cited by

• Model Checking and Synthesis for Optimal Use of Knowledge in Consensus Protocols

Related

• Abstraction for Epistemic Model Checking of Dining Cryptographers-based Protocols
• Epistemic Model Checking of Atomic Commitment Protocols with Byzantine Failures
• Program Semantics and a Verification Technique for Knowledge-Based Multi-Agent Systems
• Interpreting Knowledge-based Programs (Extended Version with Proofs)
• Knowledge and Security