Deciding the Precongruence for Deadlock Freedom Using Operating Guidelines

5th International Workshop on Logics, Agents, and Mobility (LAM'12), 1st International Workshop on Petri Net-based Security (WooPS'12), 2nd International Workshop on Petri Nets Compositions (CompoNet'12)

Richard Mu¨ller1 ; 2 ; Christian Stahl2 ; 2 Department of Mathematics ; Computer Science

Others  :  http://ceur-ws.org/Vol-853/componet3.pdf
PID  :  43067

来源: CEUR

【 摘 要 】

In the context of asynchronously communicating and deadlock free services, the refinement relation of services has been formalized by the accordance preorder. A service Impl accords with a service Spec if every controller of Spec—that is, every environment that can interact with service Spec without deadlocking—is a controller of Impl . The procedure to decide accordance of two services uses that the set of controllers of a finite-state service has a finite representation, called operating guideline. Recently, it has been shown that the accordance preorder is not a precongruence and thus the decision procedure based on operating guidelines cannot be used. In this paper, we adapt the results on operating guidelines to the precongruence setting : We define an operating guideline that represents all controllers of a service w.r.t. the accordance precongruence and show how this refinement relation of two services can be decided based on their operating guidelines.