Abstract reduction in directed model checking CCS processes (Q715051)

This paper proposes an interesting and effective approach to address state explosion issues that typically affect the verification of concurrent systems. In particular, the developed technique is applied to systems specified as sets of processes in the Calculus of Communicating Systems (CSS) and it is based on the combined use of semantic abstraction and heuristic search during state-space exploration. Semantic abstraction is achieved by considering, during the verification of a given property, only the subset of actions of the system behaviour that may impact on its satisfaction. Toward this, the authors introduce a suitable temporal logic for specifying system properties, called selective mu-calculus, which is derived from mu-calculus by modifying the modal operators so that only interesting actions can appear in the formulae. The selective mu-calculus has the same expressiveness of mu-calculus but enables to define a non-standard operational semantics which, in turn, allows the construction of an abstract transition system that has remarkably less states than the standard one. In particular, the operational semantics of the selective mu-calculus is based on a transition relation which abstracts from non-interesting actions but remembers the number of actual actions that must be performed in order to execute an interesting one. Such information is exploited by the heuristic employed during the state-space exploration. The use of heuristic search algorithms for driving the exploration of the state space are at the basis of direct model-checking techniques. The authors show how the non-standard semantics for the selective mu-calculus can be further exploited for defining an heuristic function which estimates the cost to reach a goal node from the current one. In particular, they prove that such function is admissible, viz. it never overestimates the actual cost, and then allows to exploit both greedy and optimal, e.g. A*, search strategies. The reported experimental results, which were conducted on a set of standard benchmark case studies, confirm that the approach performs better than traditional techniques mainly for that regards the state reduction. Only in some cases the employed time is a little bit worse. In conclusion, the manuscript, which is well written and almost self contained, shows how a clever combination of abstraction techniques and heuristic search, results in a good tool for harnessing the state explosion problem. Table 4 contains some typos in \textbf{Res}\(_2\) and \textbf{Res}\(_3\).