Adding Conflict and Confusion to CSP

Speaker: Christie Marr (nee Bolton)

23rd November 2005 , 2pm , Devonshire G21/G22 Conference Room

Abstract

In this talk we explore the truly concurrent notions of conflict,whereby transitions can occur individually but not together from a given state, and confusion, whereby the conflict set of a given transition is altered by the occurence of another transition with which it does not interfere. Having provided a translation from Petri nets, a truly concurrent formalism, to CSP, an interleaving formalism, we demonstate how the CSP model-checker FDR can be used to detect the presence of both conflict and confusion in Petri nets.