scholarly journals Decidability of Fair Termination of Gossip Protocols

10.29007/62s4 ◽  
2018 ◽  
Author(s):  
Krzysztof Apt ◽  
Dominik Wojtczak
Keyword(s):  
Private Information ◽  
Epistemic Logic ◽  
Distributed Programs ◽  
Partial Correctness ◽  
Gossip Protocols

Gossip protocols deal with a group of communicating agents, each holding some private information, and aim at arriving at a situation in which all the agents know each other secrets. Distributed epistemic gossip protocols are particularly simple distributed programs that use as guards formulas from an epistemic logic. We showed recently that the implementability of these distributed gossip protocols and the problems of their partial correctness and termination are decidable, but the problem of decidability of their fair termination was left open. We study here rule-fair and agent-fair termination of these protocols and show that both properties are decidable.

scholarly journals On the Computational Complexity of Gossip Protocols

2017 ◽  
Author(s):  
Krzysztof R. Apt ◽  
Eryk Kopczyński ◽  
Dominik Wojtczak
Keyword(s):  
Computational Complexity ◽  
Private Information ◽  
Epistemic Logic ◽  
Distributed Programs ◽  
Distributed Protocols ◽  
Partial Correctness ◽  
Complete Problem ◽  
Gossip Protocol ◽  
Np Complete ◽  
Gossip Protocols

Gossip protocols deal with a group of communicating agents, each holding a private information, and aim at arriving at a situation in which all the agents know each other secrets. Distributed epistemic gossip protocols are particularly simple distributed programs that use formulas from an epistemic logic. Recently, the implementability of these distributed protocols was established (which means that the evaluation of these formulas is decidable), and the problems of their partial correctness and termination were shown to be decidable, but their exact computational complexity was left open. We show that for any monotonic type of calls the implementability of a distributed epistemic gossip protocol is a P^{NP}_{||}-complete problem, while the problems of its partial correctness and termination are in coNP^{NP}.

scholarly journals Verification of Distributed Epistemic Gossip Protocols

2018 ◽  
Vol 62 ◽  
pp. 101-132 ◽  
Author(s):  
Krzysztof R. Apt ◽  
Dominik Wojtczak
Keyword(s):  
Epistemic Logic ◽  
Group Communications ◽  
Partial Correctness ◽  
Knowledge Based ◽  
Point To Point ◽  
Definition Of ◽  
Gossip Protocols

Gossip protocols aim at arriving, by means of point-to-point or group communications, at a situation in which all the agents know each other secrets. Distributed epistemic gossip protocols use as guards formulas from a simple epistemic logic and as statements calls between the agents. They are natural examples of knowledge based programs.We prove here that these protocols are implementable, that their partial correctness is decidable and that termination and two forms of fair termination of these protocols are decidable, as well. To establish these results we show that the definition of semantics and of truth of the underlying logic are decidable.

Sign in / Sign up

Export Citation Format

Share Document