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.