# On the limits of refinement-testing for model-checking CSP

## Authors

NICTA

UNSW

University of Oxford

## Abstract

Refinement-checking, as embodied in tools like FDR, PAT and ProB, is a popular approach for model-checking refinement-closed predicates of CSP processes. We consider the limits of this approach to model-checking these kinds of predicates.

By adopting Clarkson and Schneider's hyperproperties framework, we show that every refinement-closed denotational predicate of finitely-nondeterministic, divergence-free CSP processes can be written as the conjunction of a safety predicate and the refinement-closure of a liveness predicate. We prove that every safety predicate is refinement-closed and that the safety predicates correspond precisely to the CSP refinement checks in finite linear observations models whose left-hand sides (i.e. specification processes) are independent of the systems to which they are applied.

We then show that there exist important liveness predicates whose refinement-closures cannot be expressed as refinement checks in any finite linear observations model, divergence-strict model, or non-divergence-strict divergence-recording model, i.e. in any standard CSP model suitable for reasoning about the kinds of processes that FDR can handle, namely finitely-branching ones. These liveness predicates include liveness properties under intuitive fairness assumptions, branching-time liveness predicates and non-causation predicates for reasoning about authority. We conclude that alternative verification approaches, besides refinement-checking, currently under development for CSP should be further pursued.

## BibTeX Entry

@article{Murray_13, author = {Murray, Toby}, doi = {10.1007/s00165-011-0183-6}, journal = {Formal Aspects of Computing}, keywords = {refinement-testing, expressiveness, csp, model-checking, hyperproperties.}, month = feb, number = {2}, pages = {219--256}, paperurl = {https://trustworthy.systems/publications/nicta_full_text/4907.pdf}, title = {On the Limits of Refinement-Testing for Model-Checking {CSP}}, volume = {25}, year = {2013} }