Model checking of non-finite state processes by finite approximations

In this paper we present a verification methodology, using an action-based logic, able to check logical properties for full CCS terms, thus allowing complete generality of the class of reactive systems that can be specified. Obviously, for some properties we are only able to give a semidecision procedure. The idea is to use (a sequence of) finite state transition systems which approximate the, possibly infinite state, transition system corresponding to a term. To this end we define a particular notion of approximation, which is stronger than simulation and is very expressive with respect to liveness and safety properties. We show some examples of chains based on this notion and built using different operational semantics. In particular, we define an approximation chain which is very expressive with respect to liveness and safety properties. In order to reason on the properties that we are able to prove with approximation chains, we also give a syntactic characterization of different kinds of properties, which allows us to to prove a set of interesting results. Moreover, we define a criterion, based on the set of checkable properties, to compare the suitability of approximation chains to prove properties. We show how the approach has been implemented in the JACK environment, thus extending its model checking functionalities to the verification of ACTL formulae on non-finite state LTS's.