اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدEpistemic Model Checking for Knowledge-Based Program Implementation: an Application to Anonymous Broadcast
137
0
0.0
(
0
)
تأليف
Omar I. Al-Bataineh
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Knowledge-based programs provide an abstract level of description of protocols in which agent actions are related to their states of knowledge. The paper describes how epistemic model checking technology may be applied to discover and verify concrete implementations based on this abstract level of description. The details of the implementations depend on the specific context of use of the protocol. The knowledge-based approach enables the implementations to be optimized relative to these conditions of use. The approach is illustrated using extensions of the Dining Cryptographers protocol, a security protocol for anonymous broadcast.
قيم البحث
اقرأ أيضاً
The paper describes an abstraction for protocols that are based on multiple rounds of Chaums Dining Cryptographers protocol. It is proved that the abstraction preserves a rich class of specifications in the logic of knowledge, including specification
s describing what an agent knows about other agents knowledge. This result can be used to optimize model checking of Dining Cryptographers-based protocols, and applied within a methodology for knowledge-based program implementation and verification. Some case studies of such an application are given, for a protocol that uses the Dining Cryptographers protocol as a primitive in an anonymous broadcast system. Performance results are given for model checking knowledge-based specifications in the concrete and abstract models of this protocol, and some new conclusions about the protocol are derived.
This paper shows that conditional independence reasoning can be applied to optimize epistemic model checking, in which one verifies that a model for a number of agents operating with imperfect information satisfies a formula expressed in a modal mult
i-agent logic of knowledge. The optimization has been implemented in the epistemic model checker MCK. The paper reports experimental results demonstrating that it can yield multiple orders of magnitude performance improvements.
Fidelity is one of the most widely used quantities in quantum information that measure the distance of quantum states through a noisy channel. In this paper, we introduce a quantum analogy of computation tree logic (CTL) called QCTL, which concerns f
idelity instead of probability in probabilistic CTL, over quantum Markov chains (QMCs). Noisy channels are modelled by super-operators, which are specified by QCTL formulas; the initial quantum states are modelled by density operators, which are left parametric in the given QMC. The problem is to compute the minimumfidelity over all initial states for conservation. We achieve it by a reduction to quantifier elimination in the existential theory of the reals. The method is absolutely exact, so that QCTL formulas are proven to be decidable in exponential time. Finally, we implement the proposed method and demonstrate its effectiveness via a quantum IPv4 protocol.
While model checking has often been considered as a practical alternative to building formal proofs, we argue here that the theory of sequent calculus proofs can be used to provide an appealing foundation for model checking. Since the emphasis of mod
el checking is on establishing the truth of a property in a model, we rely on the proof theoretic notion of additive inference rules, since such rules allow provability to directly describe truth conditions. Unfortunately, the additive treatment of quantifiers requires inference rules to have infinite sets of premises and the additive treatment of model descriptions provides no natural notion of state exploration. By employing a focused proof system, it is possible to construct large scale, synthetic rules that also qualify as additive but contain elements of multiplicative inference. These additive synthetic rules -- essentially rules built from the description of a model -- allow a direct treatment of state exploration. This proof theoretic framework provides a natural treatment of reachability and non-reachability problems, as well as tabled deduction, bisimulation, and winning strategies.
Coalition logic is one of the most popular logics for multi-agent systems. While epistemic extensions of coalition logic have received much attention, existence of their complete axiomatisations has so far been an open problem. In this paper we settl
e several of those problems. We prove completeness for epistemic coalition logic with common knowledge, with distributed knowledge, and with both common and distributed knowledge, respectively.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
