Open AccessA Modal Logic for a Subclass of Event Structures
Author(s) -
Kamal Lodaya,
P. S. Thiagarajan
Publication year - 1987
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v16i220.7571
Subject(s) - soundness , concurrency , subclass , axiom , modal logic , fragment (logic) , computer science , completeness (order theory) , temporal logic , theoretical computer science , event (particle physics) , dynamic logic (digital electronics) , discrete mathematics , mathematics , algorithm , modal , programming language , medicine , mathematical analysis , chemistry , physics , geometry , quantum mechanics , transistor , voltage , polymer chemistry , antibody , immunology
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.