A trace-based service semantics guaranteeing deadlock freedom

C. Stahl, W. Vogler

Research output: Contribution to journalArticleAcademicpeer-review

9 Citations (Scopus)

Abstract

We revise the accordance preorder in the context of deadlock freedom for asynchronously communicating services. Accordance considers all controllers of a service—that is, all environments that can interact with the service without deadlocking. A service Impl accords with a service Spec if every controller of Spec is also a controller of Impl. We model finite-state and infinite-state services as Petri nets and formalize the semantics of such models with a traditional concurrency semantics, a trace-based semantics. As benefits, we get an easier characterization of the accordance preorder, prove that it is a fully abstract precongruence, and present an algorithm to decide refinement of two finite-state services. Previously, operating guidelines have been introduced to study the behavior of finite-state services; they characterize all controllers of a given service and can be used to decide accordance. An operating guideline is a finite automaton annotated with Boolean formulae that describes the semantics of a service from the perspective of its controllers rather than from the perspective of the service. We show that our trace-based semantics can be translated back and forth into operating guidelines, thereby providing a more conceptual understanding of operating guidelines. An extended abstract appeared under the title "A Trace-Based View on Operating Guidelines" in M. Hofmann, ed., FoSSaCS 2011, vol. 6604 of Lecture Notes in Computer Science, pp. 411–425, Germany, 2011. Springer.
Original languageEnglish
Pages (from-to)69-103
JournalActa Informatica
Volume49
Issue number2
DOIs
Publication statusPublished - 2012

Fingerprint

Dive into the research topics of 'A trace-based service semantics guaranteeing deadlock freedom'. Together they form a unique fingerprint.

Cite this