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 de pend on the behavior of processes in terms of performed sequences of action s. 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 w ant to perform can be called interesting actions analysis: the behavior of a process P is observed in an "abstract" way, disregarding all the non-inte resting actions. This abstraction can be used as a method for efficiently v erifying 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 origi nal CCS process. We show how the use of our abstract semantics leads to a r educed transition system on which the properties can be equivalently checke d. We consider., as the meaning of CCS processes, the well-known trace sema ntics, which describes the sequences of actions which can be performed by a process. The interesting actions analysis is seen as an abstraction of suc h a concrete semantics. (C) 1999 Elsevier Science B.V. All rights reserved.