A logic for a coordination model with multiple spaces

This paper introduces and studies PoliS, a coordination model to specify the software architecture of distributed applications. PoliS is based on multiple dataspaces containing both data and programs. We define PoliS syntax and semantics, and show how it can be used as a formal notation for specifying open systems. We adopt TLA logic to reason on PoliS specifications. Finally, we discuss an application field for PoliS, namely we use it to specify and reason on software architectures of some simple distributed systems.