Date and Time: Thursday, 2 February 2012, 15:45 - 16:45

Location: HG 6.96

Speaker: Harsh Beohar (Formal System Analysis, Eindhoven University of Technology)

Title: Desynchronisation of synchronous systems with half-duplex communication mechanism

Abstract:

Desynchronisation is a technique to construct a correct asynchronous system from a given synchronous system. The idea is to first fabricate a synchronous system that satisfies a given set of requirements (via for example, model checking or synthesis); then, build an asynchronous system from this synchronous system by introducing two queues with a certain abstraction scheme. From our previous work, we know that if the synchronous system is well-posed, deterministic, and satisfies the diamond property, then the synchronous and asynchronous system are equivalent. However, we argue that the diamond property - one of the common conditions present in the literature - is very restrictive and difficult to establish in practice. To circumvent this we incorporate the semantics of asynchronous systems with a communication mechanism, called half-duplex, to ensure that the diamond property is not a prerequisite for desynchronisability. In hindsight, we relax the conditions on the structure of local processes by adapting the buffers to achieve desynchronisability of both deterministic and nondeterministic synchronous systems. Furthermore, our work indicates that contra-simulation is more appealing for desynchronisability of nondeterministic systems than branching bisimulation due to the delaying of non-deterministic choices that are present in a synchronous system.