Refinement for Transition Systems with Responses

Marco Carbone
Thomas Hildebrandt
Gian Perrone
Andrzej Wąsowski

Motivated by the response pattern for property specifications and applications within flexible workflow management systems, we report upon an initial study of modal and mixed transition systems in which the must transitions are interpreted as must eventually, and in which implementations can contain may behaviors that are resolved at run-time. We propose Transition Systems with Responses (TSRs) as a suitable model for this study. We prove that TSRs correspond to a restricted class of mixed transition systems, which we refer to as the action-deterministic mixed transition systems. We show that TSRs allow for a natural definition of deadlocked and accepting states. We then transfer the standard definition of refinement for mixed transition systems to TSRs and prove that refinement does not preserve deadlock freedom. This leads to the proposal of safe refinements, which are those that preserve deadlock freedom. We exemplify the use of TSRs and (safe) refinements on a small medication workflow.

In Sebastian Bauer and Jean-Baptiste Raclet: Proceedings Fourth Workshop on Foundations of Interface Technologies (FIT 2012), Tallinn, Estonia, 25th March 2012, Electronic Proceedings in Theoretical Computer Science 87, pp. 48–55.
Published: 15th July 2012.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: