Hierarchical compression for model-checking CSP or How to check dining philosophers for deadlock

Andrew W. Roscoe
Poul H.B. Gardiner
Michael H. Goldsmith
Jason R. Hulance
David M. Jackson
J. Bryan Scattergood

In TACAS, pages 187--200

Abstract:

We discuss the integration of hierarchical, semantic-based compression techniques for state machines into FDR, the CSP-based refinement checker. These include normalisation, bisimulation, factorisation by semantic equivalence and a new technique we term diamond elimination. The resulting system, FDR 2, is thus able to check and debug systems which, dependent on the characteristics of the example under consideration, may be exponentially larger than those within the scope of the original tool.

Comments
Oxfor University and Formal Systems Europe, Oxford, England.

Available as PostScript, DVI.

BRICS WWW home page