Model Checking ACTL Constrained Processes

Abstract

Logical constrained processes are loose specifications for partially defined systems: they are a combination of open terms in process algebras and a constraint constructed on temporal logics. Using open terms for loose specifications provides a way to bring advantages from process algebras, yet we are not restricted to a single equivalence class due to the appearances of free variables. Furthermore, these variables are constrained by logical formulae expressing the properties they should give respect to in further refinements. In this paper, we discuss the specifications and verifications of logical constrained processes using (i) regular process (sequential and non-deterministic process) as open terms and (ii) ACTL, an action-based version of CTL, as the underlying logic for constraints. The problem of verifying a (global) property in such logical constrained process is shown to be reducible into the classical validity /satisfiability verification of ACTL formulae. The transformation follows the style of the algorithm for CTL model checking.