7.7AIAug 8, 2022
Truth Set Algebra: A New Way to Prove UndefinabilitySophia Knight, Pavel Naumov, Qi Shi et al.
The article proposes a new technique for proving the undefinability of logical connectives through each other and illustrates the technique with several examples. Some of the obtained results are new proofs of the existing theorems, others are original to this work.
3.3DCJun 16
An Epistemic Analysis of Random Coordinated AttackSophia Knight, David Lehnherr, Sergio Rajsbaum
The coordinated attack problem models the challenge of coordinating a joint action within a bounded time by communicating over unreliable links. It was the first distributed computing problem proven unsolvable. Its analysis also revealed the importance of common knowledge, a central concept in epistemic logic. However, the randomized version of coordinated attack, which is solvable, has not, to the best of our knowledge, been studied through the lens of probabilistic epistemic logic, where processes generate randomness by flipping coins. We present an epistemic logic framework for studying randomized algorithms that execute for a bounded number of rounds. The framework applies to coordinated attack, approximate agreement, and consensus, and supports dynamic graph models: synchronous systems in which reliable processes execute a bounded number of rounds while an adversary determines which messages are lost. Our approach combines techniques from the logical characterization of dynamic networks and task solvability with ideas from probabilistic dynamic epistemic logic. It is inspired by the operational model of Varghese and Lynch for randomized coordinated attack. More broadly, the resulting notion of probabilistic epistemic task solvability provides a foundation for the epistemic study of randomized distributed computation. Using this framework, we analyze the Varghese-Lynch algorithm from a knowledge-theoretic perspective, providing a formal treatment of the algorithm and its lower bound. As a byproduct, we strengthen the lower bound and show it is tight. The proof relies on indistinguishability arguments, demonstrating that reasoning about knowledge remains essential in the probabilistic setting. We also formalize the notion of information level introduced by Varghese and Lynch, showing that it corresponds to a specific epistemic formula.
1.2PLAug 19, 2015
Proceedings 8th Interaction and Concurrency ExperienceSophia Knight, Ivan Lanese, Alberto Lluch Lafuente et al.
This volume contains the proceedings of ICE 2015, the 8th Interaction and Concurrency Experience, which was held in Grenoble, France on the 4th and 5th of June 2015 as a satellite event of DisCoTec 2015. The ICE procedure for paper selection allows PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a discussion forum with access restricted to the authors and to all the PC members not declaring a conflict of interest. The PC members post comments and questions to which the authors reply. Each paper was reviewed by three PC members, and altogether 9 papers, including 1 short paper, were accepted for publication (the workshop also featured 4 brief announcements which are not part of this volume). We were proud to host three invited talks, by Leslie Lamport (shared with the FRIDA workshop), Joseph Sifakis and Steve Ross-Talbot. The abstracts of the last two talks are included in this volume together with the regular papers.