TY - GEN
T1 - Sharing attributes and actions in modal action logic
AU - Ryan, Mark
AU - Fiadeiro, Jose
AU - Maibaum, Tom
PY - 1991
Y1 - 1991
N2 - 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 "deontic defaults" exist so that the specifier need not explicitly grant permissions or avoid obligations in situations where normative behaviour is not an issue.
AB - 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 "deontic defaults" exist so that the specifier need not explicitly grant permissions or avoid obligations in situations where normative behaviour is not an issue.
U2 - 10.1007/3-540-54415-1_65
DO - 10.1007/3-540-54415-1_65
M3 - Conference contribution
SN - 9783540544159
VL - 526
T3 - Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)
SP - 569
EP - 593
BT - International Symposium on Theoretical Aspects of Computer Software
PB - Springer
ER -