Trace- and failure-based semantics for responsiveness

W. Vogler, C. Stahl, R. Müller

Research output: Contribution to journalArticleAcademicpeer-review

2 Citations (Scopus)
81 Downloads (Pure)

Abstract

We study open systems modeled as Petri nets with an interface for asynchronous (i.e., buffered) communication with other open systems. As a minimal requirement for successful communication, we investigate responsiveness, which guarantees that an open system and its environment always have the possibility to communicate. We investigate responsiveness with and without final states and also their respective bounded variants, where the number of pending messages never exceeds a previously known bound. Responsiveness accordance describes when one open system can be safely replaced by another open system. We present a trace-based characterization for each accordance variant. As none of the relations turns out to be compositional (i.e., it is no precongruence), we characterize the coarsest compositional relation (i.e., the coarsest precongruence) that is contained in each relation, using a variation of should testing. For the two unbounded variants, the precongruences are not decidable, but for the two bounded variants we show decidability.
Original languageEnglish
Pages (from-to)499-552
Number of pages54
JournalActa Informatica
Volume51
Issue number8
DOIs
Publication statusPublished - 2014

Fingerprint Dive into the research topics of 'Trace- and failure-based semantics for responsiveness'. Together they form a unique fingerprint.

Cite this