A Modal Logic for a Subclass of Event Structures
DOI:
https://doi.org/10.7146/dpb.v16i220.7571Abstract
This paper introduces a non-interleaved model for the behaviour of distributed computing systems, and an accompanying temporal logic with an explicit treatment of concurrency (based on a notion of local rather than global states).
A subclass of event structures (called n-agent event structures) is used as the underlying model -- intended to describe the computational behaviour of n communicating, sequential (and possibly non-deterministic) agents. The logic is centered around indexed modalities to describe the states of knowledge of the individual agents during such a computation.
An axiom system for the logic is presented, and a full proof of its soundness and completeness (Henkin style proof) is given.
Downloads
Published
How to Cite
Issue
Section
License
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.