Merging Process Algebra and Action-based Computation Tree Logic

TL;DR

This paper introduces a new process calculus combining process algebra and temporal logic, enabling unified specification and verification of reactive systems with compositional reasoning.

Contribution

It proposes a LLTS-oriented process calculus integrating algebraic and logical operators, and explores its connection with Action-based Computation Tree Logic (ACTL).

Findings

Supports mixing operational and logic operators

Preserves properties of logic connectives

Links calculus with ACTL through characteristic formulae

Abstract

Process algebra and temporal logic are two popular paradigms for the specification, verification and systematic development of reactive and concurrent systems. These two approaches take different standpoint for looking at specifications and verifications, and offer complementary advantages. In order to mix algebraic and logic styles of specification in a uniform framework, the notion of a logic labelled transition system (LLTS) has been presented and explored by Luttgen and Vogler. This paper intends to propose a LLTS-oriented process calculus which, in addition to usual process-algebraic operators, involves logic connectives (conjunction and disjunction) and standard temporal operators (always and unless). This calculus preserves usual properties of these logic operators, allows one to freely mix operational and logic operators, and supports compositional reasoning. Moreover, the links between this calculus and Action-based Computation Tree Logic (ACTL) including characteristic formulae of process terms, characteristic processes of ACTL formulae and Galois connection are explored.