FDR is an explicit-state refinement checker for the process algebra CSP and, as such, is vulnerable to the state-explosion problem. In this paper, we show how a form of partial-order reduction, an automatic state reduction mechanism, can be utilised to soundly reduce the number of states that must be visited. In particular, we develop a compositional method for partial-order reduction that takes advantage of FDR’s internal, compositional, process representation. Further, we develop novel methods of preserving the traces of a process which allow partial-order reduction to be applied to arbitrary FDR refinement checks. We also provide details on how to efficiently implement the algorithms required for partial-order reduction.
CITATION STYLE
Gibson-Robinson, T., Hansen, H., Roscoe, A. W., & Wang, X. (2015). Practical partial order reduction for CSP. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9058, pp. 188–203). Springer Verlag. https://doi.org/10.1007/978-3-319-17524-9_14
Mendeley helps you to discover research relevant for your work.