Sharing actions and attributes in modal action logic

Abstract

Distributed systems may be specified in Structured Modal Action Logic by decomposing them into agents which interact by sharing attributes (memory) as well as actions.

In the formalism we describe, specification texts denote theories, and theories denote the set of semantic structures which satisfy them. The semantic structures are Kripke models, as is usual for modal logic. The “possible worlds” in a Kripke model are the states of the agent, and there is a separate relation on the set of states for each action term.

Agents potentially share actions as well as attributes in a way controlled by locality annotations in the specification texts. These become locality axioms in the logical theories the texts denote. These locality axioms provide a refined way of circumscribing the effects of actions.

Safety and liveness conditions are expressed (implicitly) by deontic axioms, which impose obligations and deny permissions on actions. We show that “denotic defaults” exist so that the specifier need not explicitly grant permissions or avoid obligations in situations where normative behaviour is not an issue.