Modal logics typically have only one domain of discourse—i.e., the collection of worlds or states. For distributed computing systems, however, it makes sense to have several collections of worlds and to relate one domain’s local worlds to another’s using either relations or special maps. To this end, we introduce distributed modal logics. Distributed modal logics lift the distribution structure of a distributed system directly into the logic, thereby parameterizing the logic by the distribution structure itself. Each domain supports a “local logic” (which can itself be a modal logic). The connections between local logics are realized as “distributed modal connectives” where these connectives take propositions in one logic to propositions in another. Weak distributed logic systems require neighborhood semantics and, hence, the connection between domains becomes a neighborhood map linking each world in one domain to a collection of neighborhoods in another domain. In sufficiently strong distributed logic systems, the maps may be Kripke relations linking worlds from two different domains. We briefly illustrate distributed modal logics with the outline of a security verification for a hardware distributed system (i.e., a system-on-a-chip) with components that must be woven into proofs of security statements. Distributed modal logics also support probabilistic systems using stochastic relations.
Allwein, G., & Harrison, W. L. (2016). Distributed Modal Logic. In Outstanding Contributions to Logic (Vol. 8, pp. 331–362). Springer. https://doi.org/10.1007/978-3-319-29300-4_16