TTL: a formalism to describe local and global properties of distributed systems

The behaviour of distributed systems is described in terms of typed branching-time logics. Distributed systems are considered to be composed of a finite number of interacting parts, each of which stays in exactly one active phase at any time. There is no central control. Here, just as in Wedd's interacting systems, the evolution in time of each part is "mainly'' determined by a program internal to that part itself: interactions among the parts are represented as constraints on the phases that can be freely entered (mutual exclusion) or that can be freely exited (synchronization). This concept of a distributed system brings the authors to consider each part as having a local time. Consequently, they show that a suitable typization of formulas can enable temporal logics to describe distributed systems. The theories developed in the paper are based on a typization of the unified system of branching time (UB), the temporal logic introduced by Ben-Ari, Pnueli, and Manna. The authors introduce a set of types and define a formalism called typed temporal logic (TTL), in which types are related to the local times of the various parts of the distributed system. Moreover, they define an observation function that specifies, for each type, the set of well-formed formulas pertaining to that type or, in other words, the pieces of information that each part can access. Local properties are defined by means of typed formulas, and global properties of the system are obtained using inference rules which relate local and global formulas. The authors develop two TTL theories, one local and the other local and global. They show that theorem proving is reducible to model checking, and that the two theories are both decidable in P-time.