A logic for distributed transition systems

Abstract

We present a logical characterization of a particular aspect of concurrency called the concurrent step notion. We do so by providing a sound and complete axiomatization of models called distributed transition systems. In a distributed transition system an old state is transformed into a new state through a set of actions occurring concurrently. Our logical language has the minimal features of linear time temporal logic and that of propositional dynamic logic. Our main result implies that satisfiability in our logical system is decidable.