Rojo Randrianomentsoa ; Hans van Ditmarsch ; Roman Kuznets - Impure Simplicial Complexes: Complete Axiomatization

lmcs:10379 - Logical Methods in Computer Science, October 18, 2023, Volume 19, Issue 4 -
Impure Simplicial Complexes: Complete AxiomatizationArticle

Authors: Rojo Randrianomentsoa ORCID; Hans van Ditmarsch ORCID; Roman Kuznets ORCID

    Combinatorial topology is used in distributed computing to model concurrency and asynchrony. The basic structure in combinatorial topology is the simplicial complex, a collection of subsets called simplices of a set of vertices, closed under containment. Pure simplicial complexes describe message passing in asynchronous systems where all processes (agents) are alive, whereas impure simplicial complexes describe message passing in synchronous systems where processes may be dead (have crashed). Properties of impure simplicial complexes can be described in a three-valued multi-agent epistemic logic where the third value represents formulae that are undefined, e.g., the knowledge and local propositions of dead agents. In this work we present an axiomatization for the logic of the class of impure complexes and show soundness and completeness. The completeness proof involves the novel construction of the canonical simplicial model and requires a careful manipulation of undefined formulae.

    Volume: Volume 19, Issue 4
    Published on: October 18, 2023
    Accepted on: July 22, 2023
    Submitted on: November 28, 2022
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Distributed, Parallel, and Cluster Computing

    Consultation statistics

    This page has been seen 887 times.
    This article's PDF has been downloaded 297 times.