Pattern Models: A Dynamic Epistemic Logic For Distributed Systems

We introduce pattern models, a dynamic epistemic logic for analyzing distributed systems. First, we present a version of pattern models where the full-information protocol, widely studied in distributed computability, is static in the product definition of pattern models. Next, we parametrize such a logic so as to add the capability to model dynamics of arbitrary deterministic protocols. We thus give a systematic construction of pattern models for a large variety of distributed-computing models called dynamic-network models. Using pattern models, the epistemic dynamics of a proper subclass of dynamic-network models called oblivious can be described using a static pattern model, hence using constant space. For this case, we present a sufficient unsolvability condition for the consensus task that can be easily verified analyzing the structure of the initial epistemic model and the pattern model for a given oblivious dynamic-network model.