Sharing attributes and actions in modal action logic

Mark Ryan, Jose Fiadeiro, Tom Maibaum

Research output: Chapter in Book/Report/Conference proceedingConference contribution

31 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationInternational Symposium on Theoretical Aspects of Computer Software
Subtitle of host publicationTACS 1991
Number of pages25
ISBN (Electronic)9783540476177
ISBN (Print)9783540544159
Publication statusPublished - 1991

Publication series

NameLecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)
PublisherSpringer Verlag
ISSN (Print)0302-9743


Dive into the research topics of 'Sharing attributes and actions in modal action logic'. Together they form a unique fingerprint.

Cite this