Communication Pattern Models: An Extension of Action Models for Dynamic-Network Distributed Systems

TL;DR

This paper introduces communication pattern models, extending action models to efficiently represent dynamic-network distributed systems, enabling more compact and scalable formal analysis of knowledge evolution in such environments.

Contribution

It proposes a new class of communication pattern models that extend action models, providing systematic construction methods for dynamic-network models, including oblivious systems.

Findings

Communication pattern models remain constant in oblivious systems.

The models enable compact representation of dynamic network behaviors.

Systematic construction methods improve analysis scalability.

Abstract

Halpern and Moses were the first to recognize, in 1984, the importance of a formal treatment of knowledge in distributed computing. Many works in distributed computing, however, still employ informal notions of knowledge. Hence, it is critical to further study such formalizations. Action models, a significant approach to modeling dynamic epistemic logic, have only recently been applied to distributed computing, for instance, by Goubault, Ledent, and Rajsbaum. Using action models for analyzing distributed-computing environments, as proposed by these authors, has drawbacks, however. In particular, a direct use of action models may cause such models to grow exponentially as the computation of the distributed system evolves. Hence, our motivation is finding compact action models for distributed systems. We introduce communication pattern models as an extension of both ordinary action models and their update operator. We give a systematic construction of communication pattern models for a large variety of distributed-computing models called dynamic-network models. For a proper subclass of dynamic-network models called oblivious, the communication pattern model remains the same throughout the computation.