Towards a temporal logic for causality and choice in distributed systems

Abstract

Which kind of properties of nonsequential systems should be considered essential for specification and abstraction purposes, is still an open problem. In this paper we discuss some particular properties such as absence of delay and various notions of concurrency. They turn out to be adequately representable in partial order semantics. The most fundamental version of Petri Nets appears to be convenient for such investigations. A (generalized) temporal logic is introduced, covering the intricate relationship among causality (sequentiality), choice and concurrency appearing in distributed systems.