Abstract interpretation of trace semantics for concurrent calculi
In this paper we show how the Cousots' approach to abstract interpretation can be easily and profitably applied to the analysis of concurrent calculi. Actually, when dealing with concurrent processes, a number of interesting properties are independent from the computed values, while they strongly depend on the behavior of processes in terms of performed sequences of actions. In this paper abstract interpretation is applied to the analysis of such a behavior. For this reason, we refer to a quite basic concurrent language: Calculus of Communicating Systems (CCS) without values. The analysis we want to perform can be called interesting actions analysis: the behavior of a process P is observed in an "abstract" way, disregarding all the non-interesting actions. This abstraction can be used as a method for efficiently verifying properties of CCS processes. The abstract semantics we present for such language is able to build a reduced transition system which maintains, with respect to the set of interesting actions, the behavior of the original CCS process. We show how the use of our abstract semantics leads to a reduced transition system on which the properties can be equivalently checked. We consider., as the meaning of CCS processes, the well-known trace semantics, which describes the sequences of actions which can be performed by a process. The interesting actions analysis is seen as an abstraction of such a concrete semantics. (C) 1999 Elsevier Science B.V. All rights reserved.
abstract interpretation concurrency formal semantics