|Year of Publication||2014|
|Authors||Allwein, G., and W. L. Harrison|
|Series Title||NRL Memorandum Report|
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 for each component and to relate one component's local worlds to another using either relations or special maps. To this end, we introduce distributed logics. Distributed 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 modal logic''. The connections between domains are realized as ``distributed modal connectives'' where these connectives take propositions in one logic to propositions in another. More generally, weak distributed systems require neighborhood semantics and hence the connection between domains becomes a neighborhood map linking each world in one domain to a collection of worlds in another domain. In sufficiently strong distributed systems, the maps may be Kripke relations linking worlds from two different domains. We illustrate distributed 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.
|NRL Publication Release Number|| |