Sharing actions and attributes in modal action logic

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, …