Interval Specification for Actually Concurrent Logic

Abstract

We extend the -calculus to allow the expression of attributes that hold true throughout the execution of an action,
therefore obtaining a framework for the definition of genuine concurrency in reactive systems. Transition systems
are used to represent the ST-semantics, which provide the basis for the interpretation of this logic. We demonstrate
the unparalleled expressive capability of this logic and step equivalence. We further demonstrate that the logic
describes the ST-bisimulation equivalence for synchronization-free finite process algebra expressions.