Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOptimizing Epistemic Model Checking Using Conditional Independence (Extended Abstract)
76
0
0.0
(
0
)
Added by
EPTCS
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Authors
Ron van der Meyden
Ask ChatGPT about the research
No Arabic abstract
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 multi-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.
rate research
Read More
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 model 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.
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 specifications 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.
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.
While there have been many attempts, going back to BAN logic, to base reasoning about security protocols on epistemic notions, they have not been all that successful. Arguably, this has been due to the particular logics chosen. We present a simple logic based on the well-understood modal operators of knowledge, time, and probability, and show that it is able to handle issues that have often been swept under the rug by other approaches, while being flexible enough to capture all the higher- level security notions that appear in BAN logic. Moreover, while still assuming that the knowledge operator allows for unbounded computation, it can handle the fact that a computationally bounded agent cannot decrypt messages in a natural way, by distinguishing strings and message terms. We demonstrate that our logic can capture BAN logic notions by providing a translation of the BAN operators into our logic, capturing belief by a form of probabilistic knowledge.
Process behaviour is often defined either in terms of the tests they satisfy, or in terms of the logical properties they enjoy. Here we compare these two approaches, using extensional testing in the style of DeNicola, Hennessy, and a recursive version of the property logic HML. We first characterise subsets of this property logic which can be captured by tests. Then we show that those subsets of the property logic capture precisely the power of tests.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
