Translating between models of concurrency (Q2182666)

The main idea of this study is to harness a model checker for coarser semantics to model check finer semantics, using an operator with respect to which the coarser semantics is not compositional. In the experiments in this study, the coarser semantics is trace semantics and the operator is priority. The finer semantics may be any known semantics between stable acceptances and traces, and it is conjectured that it may also be any ``reasonable'' unknown semantics in this range. The stable acceptance semantics records finite sequences consisting of alternating precise (as opposed to minimal) stable acceptance sets / non-observation markers and visible actions. The study covers the whole range from abstract theory to medium-scale concrete experiments. The writing is CSP-specific, but at least the general ideas are formalism-independent. The last third of the study extends the ideas to timed CSP, yielding the first practical automated compositional method that uses the FDR tool. Where points of comparison were available, the new approach proved somewhat but not horribly less efficient than the earlier ones. The authors speculate that with bigger alphabets, the results may become worse. However, the goal is not to beat custom implementations but to provide something useful in their absence.