On decidability of simulation in data-centeric business protocols

Abstract

We consider the problem of analyzing specifications of data-centric services. Specifications of such services incorporate data in business protocols. We focus our study on the decidability of the problem of checking the simulation preorder in the framework of the Colombo model. Colombo is a data-centric service that appears, at a first glance, to have a limited expressivity. Our first result, presented in this paper, shows that even in this restricted framework, both simulation and state reachability problems are already undecidable. Even worse, these problems remain undecidable in the case of non-communicating, read-only services. © 2013 Springer-Verlag Berlin Heidelberg.