Tampere University of Technology

TUTCRIS Research Portal

Practical Partial Order Reduction for CSP

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review


Original languageEnglish
Title of host publicationNasa Formal Methods
Subtitle of host publication7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings
PublisherSpringer International Publishing
Number of pages16
ISBN (Electronic)978-3-319-17524-9
ISBN (Print)978-3-319-17523-2
Publication statusPublished - 2015
Publication typeA4 Article in a conference publication
EventNASA Formal Methods Symposium - , United States
Duration: 6 Apr 2009 → …

Publication series

NameLecture Notes in Computer Science


ConferenceNASA Formal Methods Symposium
CountryUnited States
Period6/04/09 → …


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.

Publication forum classification

Field of science, Statistics Finland