From ACTL to ?-calculus

When speaking about concurrent systems described by process algebras and modelled by finite Labelled Transition Systems, an action-based logic, such ACTL, provides a suitable language to express system properties. Relevant classes of system properties are safety, liveness and cyclic properties. Safety properties claim that something bad does not happen; liveness properties claim that something good eventually happens; cyclic properties claim that the periodic repetition of a sequence of actions occurs forever. A logic is also a way to characterize a concurrent system with respect some behavioural relations. This corresponds to defining a formula for each concurrent system, named characteristic formula. This describes the entire behaviour of a system in such a way that two systems have an equivalent formula if and only if they are in the same behavioural equivalence class. In this case the logic is said to be expressive with respect to the given equivalence.