Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Trace- and failure-based semantics for responsiveness

  • Original Article
  • Published:
Acta Informatica Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13

Similar content being viewed by others

Notes

  1. To simplify the notation, we do not add the alphabets of \(w_1\) and \(w_2\) to operators \(\Vert \) and \(\Uparrow \); the alphabets will be always clear from the context.

References

  1. Acciai, L., Boreale, M.: Responsiveness in process calculi. Theor. Comp. Sci. 409(1), 59–93 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  2. Akyildiz, I., Su, W., Sankarasubramaniam, Y., Cayirci, E.: Wireless sensor networks: a survey. Comput. Netw. 38(4), 393–422 (2002)

    Article  Google Scholar 

  3. Basu, S., Bultan, T., Ouederni, M.: Synchronizability for verification of asynchronously communicating systems. In: VMCAI 2012, LNCS, vol. 7148. Springer, Berlin, pp. 56–71 (2012)

  4. Boreale, M., De Nicola, R., Pugliese, R.: Basic observables for processes. Inf. Comput. 149(1), 77–98 (1999)

    Article  MATH  Google Scholar 

  5. Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bravetti, M., Zavattaro, G.: A foundational theory of contracts for multi-party service composition. Fundam. Inform. 89(4), 451–478 (2008)

    MathSciNet  MATH  Google Scholar 

  7. Brinksma, E., Rensink, A., Vogler, W.: Fair testing. In: CONCUR 1995, LNCS, vol. 962. Springer, Berlin, pp. 313–327 (1995)

  8. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  9. Chen, T., Chilton, C., Jonsson, B., Kwiatkowska, M.Z.: A compositional specification theory for component behaviours. In: ESOP, LNCS, vol. 7211. Springer, Berlin, pp. 148–168 (2012)

  10. Chilton, C., Jonsson, B., Kwiatkowska, M.: An Algebraic Theory of Interface Automata. Tech. Rep. RR-13-02, DCS (2013)

  11. de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC/SIGSOFT FSE 2001, pp. 109–120 (2001)

  12. Desai, A., Gupta, V., Jackson, E., Qadeer, S., Rajamani, S.K., Zufferey, D.: P: safe asynchronous event-driven programming. In: PLDI 2013. ACM, pp. 321–332 (2013)

  13. Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press, New York (1989)

  14. Gamboni, M., Ravara, A.: Responsive choice in mobile processes. In: TGC, LNCS, vol. 6084. Springer, Berlin, pp. 135–152 (2010)

  15. Haddad, S., Hennicker, R., Møller, M.H.: Channel properties of asynchronously composed petri nets. In: Petri Nets, LNCS, vol. 7927. Springer, Berlin, pp. 369–388 (2013)

  16. Kobayashi, N.: A type system for lock-free processes. Inf. Comput. 177(2), 122–159 (2002)

    Article  MATH  Google Scholar 

  17. Larsen, K.G.: Modal specifications. In: AVMFSS 1989, LNCS, vol. 407. Springer, Berlin, pp. 232–246 (1990)

  18. Lohmann, N., Massuthe, P., Wolf, K.: Operating guidelines for finite-state services. In: ICATPN 2007, LNCS, vol. 4546. Springer, Berlin, pp. 321–341 (2007)

  19. Lohmann, N., Verbeek, E., Dijkman, R.M.: Petri net transformations for business processes—a survey. In: ToPNoC II, LNCS 5460. Springer, Berlin, pp. 46–63 (2009)

  20. Lohmann, N., Wolf, K.: Compact representations and efficient algorithms for operating guidelines. Fundam. Inform. 107, 1–19 (2011)

    MathSciNet  Google Scholar 

  21. Malik, R., Streader, D., Reeves, S.: Conflicts and fair testing. Int. J. Found. Comput. Sci. 17(4), 797–813 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  22. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  23. Mooij, A.J., Stahl, C., Voorhoeve, M.: Relating fair testing and accordance for service replaceability. J. Log. Algebr. Program. 79(3–5), 233–244 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  24. Müller, R.: On the notion of deadlocks in open nets. In: M. Schwarick, M. Heiner (eds.) AWPN 2010, CEUR Workshop Proceedings, vol. 643, pp. 130–135. CEUR-WS.org (2010)

  25. Müller, R., Stahl, C., Vogler, W.: Undecidability of accordance for open systems with unbounded message queues. Inform. Process. Lett. 114, 663–669 (2014)

  26. Müller, R., Stahl, C., Vogler, W.: Deciding Conformance for Bounded Responsiveness (2014). Submitted paper

  27. Natarajan, V., Cleaveland, R.: Divergence and fair testing. In: ICALP 1995, LNCS, vol. 944. Springer, Berlin, pp. 648–659 (1995)

  28. Padovani, L.: From lock freedom to progress using session types. To appear for PLACES 2013

  29. Papazoglou, M.P.: Web Services: Principles and Technology. Pearson, Upper Saddle River (2007)

    Google Scholar 

  30. Reed, J.N., Roscoe, A.W., Sinclair, J.E.: Responsiveness and stable revivals. Formal Asp. Comput. 19(3), 303–319 (2007)

    Article  MATH  Google Scholar 

  31. Rensink, A., Vogler, W.: Fair testing. Inf. Comput. 205(2), 125–198 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  32. Stahl, C., Massuthe, P., Bretschneider, J.: Deciding substitutability of services with operating guidelines. In: ToPNoC II, LNCS 5460. Springer, Berlin, pp. 172–191 (2009)

  33. Stahl, C., Vogler, W.: A trace-based service semantics guaranteeing deadlock freedom. Acta Inf. 49(2), 69–103 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  34. van Glabbeek, R.J.: The coarsest precongruences respecting safety and liveness properties. In: TCS 2010, IFIP, vol. 323. Springer, Berlin, pp. 32–52 (2010)

  35. Vogler, W.: Modular Construction and Partial Order Semantics of Petri Nets, LNCS, vol. 625. Springer, Berlin (1992)

  36. Vogler, W., Stahl, C., Müller, R.: A trace-based semantics for responsiveness. In: ACSD 2012. IEEE, pp. 42–51 (2012)

  37. Vogler, W., Stahl, C., Müller, R.: Trace- and failure-based semantics for bounded responsiveness. In: Advances in Service-Oriented and Cloud Computing, CCIS, vol. 393. Springer, Berlin, pp. 129–143 (2013)

  38. Vogler, W., Stahl, C., Müller, R.: Trace- and failure-based semantics for responsiveness. BPM Center Report BPM-13-14, BPMcenter.org (2013). http://bpmcenter.org/wp-content/uploads/reports/2013/BPM-13-14.pdf

  39. Voorhoeve, M., Mauw, S.: Impossible futures and determinism. Inf. Process. Lett. 80(1), 51–58 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  40. Wolf, K.: Does my service have partners? In: ToPNoC II, LNCS, vol. 5460. Springer, Berlin, pp. 152–171 (2009)

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Augsburg, Augsburg, Germany

    Walter Vogler

  2. Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, Eindhoven, The Netherlands

    Christian Stahl & Richard Müller

Authors
  1. Walter Vogler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christian Stahl
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Richard Müller
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Walter Vogler.

Additional information

This paper is a full and revised version, based on the extended abstracts [36, 37].

Appendix (Proofs)

Appendix (Proofs)

In the following, we provide the proofs that have been left out in the previous sections.

1.1 Proof of Lemma 46

With Lemma 46 in Sect. 3.2, we show that \(\fancyscript{F}^+_{fin}\)-refinement is a precongruence for labeled nets and operator \(\Vert \).

Proof

Let \(Impl\) and \(Spec\) be two interface-equivalent labeled nets, and let the labeled net \(C\) be composable with \(Spec\). Let further \(Impl\sqsubseteq _{\fancyscript{F}^+_{fin}} Spec\). We show that \(Impl\Vert C \sqsubseteq _{\fancyscript{F}^+_{fin}} Spec\Vert C\), following to a large extent the proof of [31, Lemma 46]. To improve the readability of the proof, we first develop the particular case \(\varSigma _Spec= \varSigma _C\). Here, the projection functions in the construction of the synchronized fintree failures become the identity over the complete alphabet and, hence, disappear.

Consider a fintree failure \((w, X_{Impl} \cup X_C, Y_{Impl} \cup Y_C) \in \fancyscript{F}^+_{fin}(Impl\Vert C)\) such that \((w, X_{Impl}, Y_{Impl}) \in \fancyscript{F}^+_{fin}(Impl)\) and \((w, X_C, Y_C) \in \fancyscript{F}^+_{fin}(C)\). By Definition 37, we have to show that there exists \(x \in \{\varepsilon \} \cup {\downarrow {(X_{Impl} \cup X_C)}} \cup {\downarrow {(Y_{Impl} \cup Y_C)}}\) such that \((wx, x^{-1}(X_{Impl} \cup X_C),\) \( x^{-1}(Y_{Impl} \cup Y_C)) \in \fancyscript{F}^+_{fin}(Spec\Vert C)\). We define the set

$$\begin{aligned} V = \{v \mid (wv, v^{-1}X_C, v^{-1}Y_C) \not \in \fancyscript{F}^+_{fin}(C)\} \end{aligned}$$

which contains those traces that can be added to \(X_C\) and \(Y_C\) according to CON2. We shift the traces in \(V\) from the refusal set of \(Impl\) to the refusal set of \(C\). To this end, we define four sets

$$\begin{aligned} \begin{array}{rcl} X'_{Impl} &{}=&{} X_{Impl} \setminus {\uparrow {V}}, \\ Y'_{Impl} &{}=&{} Y_{Impl} \setminus {\uparrow {V}},\\ X'_C &{}=&{} X_C \cup {\uparrow {V}}, \\ Y'_C &{}=&{} Y_C \cup {\uparrow {V}} \,. \end{array} \end{aligned}$$

We immediately see: \(X_{Impl} \cup X_C \subseteq X'_{Impl} \cup X'_C\) as well as \(Y_{Impl} \cup Y_C \subseteq Y'_{Impl} \cup Y'_C\) and \(X'_{Impl} \cup Y'_{Impl} \subseteq X_{Impl} \cup Y_{Impl} \cup X_C \cup Y_C\). By CON1, we have \((w, X'_{Impl}, Y'_{Impl}) \in \fancyscript{F}^+_{fin}(Impl)\).

Due to \(Impl\sqsubseteq _{\fancyscript{F}^+_{fin}} Spec\), there exists \(x \in \{\varepsilon \} \cup {\downarrow {X'_{Impl}}}\cup {\downarrow {Y'_{Impl}}}\) such that

$$\begin{aligned} (wx, x^{-1}X'_{Impl}, x^{-1}Y'_{Impl}) \in \fancyscript{F}^+_{fin}(Spec) \quad \quad \quad (1). \end{aligned}$$

We have \(x \notin {\uparrow {V}}\). Assume the contrary: \(x=\varepsilon \) implies \(\varepsilon \in V\) which is a contradiction to the construction of \(V\). \(x \in {\downarrow {X'_{Impl}}}\) implies \(\exists x' \in X'_{Impl}: x \sqsubseteq x' \wedge \exists v \in V: v \sqsubseteq x \sqsubseteq x'\) which is a contradiction to the definition of \(X'_{Impl}\). The same argument also applies to \(x \in Y'_{Impl}\).

From \(x \notin V\), it follows that \((wx, x^{-1}X_C, x^{-1}Y_C) \in \fancyscript{F}^+_{fin}(C)\). Further, for all \(u \in x^{-1}V\) (i.e., \(xu \in V\)), \((wxu, u^{-1}x^{-1}X_C, u^{-1}x^{-1}Y_C) \notin \fancyscript{F}^+_{fin}(C)\). By CON2, this implies \((wx, x^{-1}(X_C \cup V), x^{-1}(Y_C \cup V)) \in \fancyscript{F}^+_{fin}(C)\).

Consider the second ingredient of \((wx, x^{-1}(X_C \cup V), x^{-1}(Y_C \cup V)) \in \fancyscript{F}^+_{fin}(C)\). By CON3, this implies \((wx, {\uparrow {x^{-1}(X_C \cup V)}}, x^{-1}(Y_C \cup V)) \in \fancyscript{F}^+_{fin}(C)\). We have \({\uparrow {x^{-1}(X_C \cup V)}} \supseteq x^{-1}(X_C \cup {\uparrow {V}}) = x^{-1}X'_C\) by Lemma 16(3). Therefore, \((wx, x^{-1}X'_C, x^{-1}\) \((Y_C \cup V)) \in \fancyscript{F}^+_{fin}(C)\) by CON1.

Consider the third ingredient of \((wx, x^{-1}X'_C, x^{-1}(Y_C \cup V)) \in \fancyscript{F}^+_{fin}(C)\). By CON4, we extend \(x^{-1}(Y_C \cup V)\) to \(x^{-1}(Y_C \cup V) \cup x^{-1}X'_C \supseteq x^{-1}{\uparrow {V}} \cup x^{-1}Y_C = x^{-1}({\uparrow {V}} \cup Y_C) = x^{-1}Y'_C\). Thus, \((wx, x^{-1}X'_C, x^{-1}Y'_C) \in \fancyscript{F}^+_{fin}(C)\) by CON1.

By Lemma 42 and (1), we obtain \((wx, x^{-1}(X'_{Impl} \cup X'_C), x^{-1}(Y'_{Impl} \cup Y'_C)) \in \fancyscript{F}^+_{fin}(Spec\Vert C)\) . By CON1, we have \((wx, x^{-1}(X_{Impl} \cup X_C), x^{-1}(Y_{Impl} \cup Y_C)) \in \fancyscript{F}^+_{fin}(Spec\Vert C)\) where \(x \in (\{\varepsilon \} \cup {\downarrow {X'_{Impl}}} \cup {\downarrow {Y'_{Impl}}}) \subseteq (\{\varepsilon \} \cup {\downarrow {(X_{Impl} \cup X_C)}} \cup {\downarrow {(Y_{Impl} \cup Y_C)}})\).

Now consider the general case. Let \(\pi \) and \(\pi _C\) denote projections, projecting words from an arbitrary alphabet onto the alphabets \(\varSigma _Spec= \varSigma _{Impl}\) and \(\varSigma _C\), respectively. We have

  1. 1.

    \(\pi (V \cup W) = \pi (V) \cup \pi (W)\)

  2. 2.

    \(\pi ({\uparrow {V}}) \subseteq {\uparrow {\pi (V)}}\)

  3. 3.

    \(\pi (w^{-1}V) \subseteq \pi (w)^{-1}\pi (V)\)

Consider a fintree failure \((w, X_{Impl} \cup X_C, Y_{Impl} \cup Y_C) \in \fancyscript{F}^+_{fin}(Impl\Vert C)\) such that \((\pi (w), \pi (X_{Impl}), \pi (Y_{Impl})) \in \fancyscript{F}^+_{fin}(Impl)\) and \((\pi _C(w), \pi _C(X_C), \pi _C(Y_C)) \in \fancyscript{F}^+_{fin}(C)\). Define the set

$$\begin{aligned} V = \{v \mid (\pi _C(wv), \pi _C(v^{-1}X_C), \pi _C(v^{-1}Y_C)) \not \in \fancyscript{F}^+_{fin}(C)\} \,. \end{aligned}$$

We shift the traces in \(V\) from the refusal set of \(Impl\) to the refusal set of \(C\). To this end, we define four sets

$$\begin{aligned} \begin{array}{rcl} X'_{Impl} &{}=&{} X_{Impl} \setminus {\uparrow {V}}, \\ Y'_{Impl} &{}=&{} Y_{Impl} \setminus {\uparrow {V}},\\ X'_C &{}=&{} X_C \cup {\uparrow {V}}, \\ Y'_C &{}=&{} Y_C \cup {\uparrow {V}} \,. \end{array} \end{aligned}$$

We immediately see: \(X_{Impl} \cup X_C \subseteq X'_{Impl} \cup X'_C\) as well as \(Y_{Impl} \cup Y_C \subseteq Y'_{Impl} \cup Y'_C\) and \(X'_{Impl} \cup Y'_{Impl} \subseteq X_{Impl} \cup Y_{Impl} \cup X_C \cup Y_C\). By CON1, we have \((\pi (w), \pi (X'_{Impl}), \pi (Y'_{Impl})) \in \fancyscript{F}^+_{fin}(Impl)\).

Because of \(Impl\sqsubseteq _{\fancyscript{F}^+} Spec\), there exists \(x \in \{\varepsilon \} \cup {\downarrow {X'_{Impl}}} \cup {\downarrow {Y'_{Impl}}}\) such that \((\pi (wx), \pi (x)^{-1}\pi (X'_{Impl}), \pi (x)^{-1}\pi (Y'_{Impl})) \in \fancyscript{F}^+_{fin}(Spec)\). Hence, we have

$$\begin{aligned} (\pi (wx), \pi (x^{-1}X'_{Impl}), \pi (x^{-1}Y'_{Impl})) \in \fancyscript{F}^+_{fin}(Spec) \quad \quad \quad \quad (2) \end{aligned}$$

due to Item 3 and CON1.

Again, trace \(x \notin {\uparrow {V}}\) (by the same argumentation as in the proof of the case \(\varSigma _Spec= \varSigma _C\)), and we conclude that \((\pi _C(wx), \pi _C(x^{-1}X_C), \pi _C(x^{-1}Y_C)) \in \fancyscript{F}^+_{fin}(C)\). Further, for all \(u \in x^{-1}V\) (i.e., \(xu \in V\)), \((\pi _C(wxu), \pi _C(u^{-1}x^{-1}X_C), \pi _C(u^{-1}x^{-1}Y_C)) \notin \fancyscript{F}^+_{fin}(C)\), due to the definition of \(V\). Now, \((\pi _C(wxu), \pi _C(u)^{-1}\pi _C(x^{-1}X_C), \pi _C(u)^{-1}\pi _C(x^{-1}Y_C)) \notin \fancyscript{F}^+_{fin}(C)\) with Item 3 and CON1, and we obtain, by Item 1 and CON2,

$$\begin{aligned} (\pi _C(wx), \pi _C(x^{-1}(X_C \cup V)), \pi _C(x^{-1}(Y_C \cup V))) \in \fancyscript{F}^+_{fin}(C) \,. \end{aligned}$$

Consider the second ingredient, \(\pi _C(x^{-1}(X_C \cup V))\), of this fintree failure. Applying CON3, we obtain \((\pi _C(wx), {\uparrow {\pi _C(x^{-1}(X_C \cup V))}}, \pi _C(x^{-1}(Y_C \cup V))) \in \fancyscript{F}^+_{fin}(C)\), and with CON1 and Item 2, \((\pi _C(wx), \pi _C({\uparrow {x^{-1}(X_C \cup V)}}), \pi _C(x^{-1}(Y_C \cup V))) \in \fancyscript{F}^+_{fin}(C)\). Because \(x \notin {\uparrow {V}}\), we can apply Lemma 16(3) and CON1, and we arrive at \(\pi _C(x^{-1}(X_C \cup {\uparrow {V}})) = \pi _C(x^{-1}X'_C)\) and \((\pi _C(wx), \pi _C(x^{-1}X'_C), \pi _C(x^{-1}(Y_C \cup V))) \in \fancyscript{F}^+_{fin}(C)\).

For the third ingredient \(\pi _C(x^{-1}(Y_C \cup V))\) of this fintree failure, we obtain by CON4 \((\pi _C(wx), \pi _C(x^{-1}X'_C), \pi _C(x^{-1}(Y_C \cup V)) \cup \pi _C(x^{-1}X'_C) ) \in \fancyscript{F}^+_{fin}(C)\). By Item 1, we can transform this into \((\pi _C(wx), \pi _C(x^{-1}X'_C), \pi _C(x^{-1}(Y_C \cup V \cup X'_C)) ) \in \fancyscript{F}^+_{fin}(C)\) and by CON1 into \((\pi _C(wx), \pi _C(x^{-1}X'_C), \pi _C(x^{-1}(Y_C \cup {\uparrow {V}})) ) \in \fancyscript{F}^+_{fin}(C)\), thus \((\pi _C(wx), \pi _C(x^{-1}X'_C), \pi _C(x^{-1}Y_C')) \in \fancyscript{F}^+_{fin}(C)\).

By Lemma 42(2) and (2), we have \((wx, x^{-1}(X'_{Impl} \cup X'_C), x^{-1}(Y'_{Impl} \cup Y'_C)) \in \fancyscript{F}^+_{fin}(Spec\Vert C)\). Applying CON1 yields \((wx, x^{-1}(X_{Impl} \cup X_C), x^{-1}(Y_{Impl} \cup Y_C) \in \fancyscript{F}^+_{fin}(Spec\Vert C)\) where \(x \in (\{\varepsilon \} \cup {\downarrow {X'_{Impl}}} \cup {\downarrow {Y'_{Impl}}}) \subseteq (\{\varepsilon \} \cup {\downarrow {(X_{Impl} \cup X_C)}} \cup {\downarrow {(Y_{Impl} \cup Y_C)}})\). \(\square \)

1.2 Proof of Lemma 73

With Lemma 73 in Sect. 5.2, we show the following three statements: First, for every trace \(w\), which is neither a trace nor a \(bfr\)-uncoverable trace of \(N\), there exists a \(bfr\)-controller of \(N\) with \({bound_b}\)-violator \(w\). Second, for every trace \(w\), which is neither a \(stop\)-trace of \(N\) nor \(bfr\)-uncoverable, there exists a \(bfr\)-controller of \(N\) with \(dead\)-trace \(w\). Third, for every trace \(w\), which is neither a \(dead\)-trace of \(N\) nor \(bfr\)-uncoverable, there exists a \(bfr\)-controller of \(N\) with \(stop\)-trace \(w\).

Proof

(1) Let \(w \not \in {uL_{bfr}}(N)\) with \(w = w_1 \ldots w_k\) for \(j = 1, \dots , k\), \(w_j \in I_N \uplus O_N\). As \(w \not \in {uncov_{bfr}}(N)\), there exists a \(bfr\)-controller \(C\) of \(N\) with \(w \in L_{b}(C)\) by Definition 69. If \(w \notin {bound_b}(C)\), we construct from \(w\) and \(C\) a \(bfr\)-controller \(N_w^{bound} \oplus C'\) of \(N\) with \({bound_b}\)-violator \(w\) as follows: In a first step, we construct an open net \(N_w\) (cf. Fig. 14) that basically shifts all tokens from \(N\) to (a copy of) \(C\), and vice versa. Moreover, \(N_w\) tracks whether a firing sequence in \(C\) is (a “permutation” of) a prefix of \(w\) by moving a token from an initially marked place \(p_0\) to a place \(p_j\). Intuitively, a token on \(p_j\) means we already encountered (a “permutation” of) the trace \(w_1 \ldots w_j\); in other words, a token on the place \(p_k\) means that we encountered (a “permutation” of) the trace \(w_1 \ldots w_k = w\). For shifting, we introduce several transitions in \(N_w\) for each interface place in \(N\); these are the transitions \(t^x_i\), written \(txi\) in Fig. 14. In a second step, we will extend \(N_w\): If and only if the place \(p_k\) is marked, a “disaster” transition \(t_{ disaster }\) is enabled. Then, transition \(t_{ disaster }\) may put an arbitrary number of tokens onto an inner place \(p_{ disaster }\). This construction yields the open net \(N_w^{ bound }\), and guarantees that \(w\) is a \({bound_b}\)-violator of \(N_w^{ bound } \oplus C'\).

Let \(I' = \{i' \mid i \in I_C\}\) and \(O' = \{o' \mid o \in O_C\}\) be “fresh” copies of \(I_C\) and \(O_C\). We derive the open net \(C' = (P_C, T_C, F'_C, m_C, I', O', \varOmega _C)\) from \(C\) by renaming the interface of \(C\) and adjusting the flow relation accordingly. We define the open net \(N_w = (P', T', F', m_{N_w}, O_N \uplus O_{C'}, I_N \uplus I_{C'}, \varOmega _{N_w})\) with

  • \(P' = \begin{array}{ll} &{} \{p_i \mid 0 \le i \le k\} \\ \uplus &{} \{p_{err}\}, \\ \end{array}\)

  • \(T' = \begin{array}{ll} &{} \{t_i^x \mid 1 \le i \le k \wedge x \in O_N \uplus I_N \} \\ \uplus &{} \{t_{err}^x \mid x \in O_N \uplus I_N \} \\ \uplus &{} \{t_{err}\}, \\ \end{array}\)

  • \(F' = \begin{array}{ll} &{} \{(x,t_i^x),(t_i^x,x'),(p_{i-1},t_i^x) \mid 1 \le i \le k \wedge x \in O_N \} \\ \uplus &{} \{(x',t_i^x),(t_i^x,x),(p_{i-1},t_i^x) \mid 1 \le i \le k \wedge x \in I_N \} \\ \uplus &{} \{(t_i^x,p_i) \mid 1 \le i \le k \wedge x \in O_N \uplus I_N \wedge x = w_i \} \\ \uplus &{} \{(t_i^x,p_{err}) \mid 1 \le i \le k \wedge x \in O_N \uplus I_N \wedge x \ne w_i \} \\ \uplus &{} \{(x,t_{err}^x),(t_{err}^x,x'),(p_{err},t_{err}^x),(t_{err}^x,p_{err}) \mid x \in O_N \} \\ \uplus &{} \{(x',t_{err}^x),(t_{err}^x,x),(p_{err},t_{err}^x),(t_{err}^x,p_{err}) \mid x \in I_N \} \\ \uplus &{} \{(p_k,t_{err}), (t_{err},p_{err}) \}, \\ \end{array}\)

  • \(m_{N_w} = [p_0]\), and

  • \(\varOmega _{N_w} = \{[p] \mid p \in P' \}\).

Fig. 14
figure 14

Illustration of the construction of the open net \(N_w\) for \(N\) with \(I_N = \{a\},\, O_N = \{b\}\), and \(w = ab \not \in {uL_{bfr}}(N)\)

Full size image

Figure 14 illustrates the construction of \(N_w\). We have \(L(C) = L(N_w \oplus C'),\, {bound_b}(C) = {bound_b}(N_w \oplus C'),\, stop(C) = stop(N_w \oplus C')\), and \(dead(C) = dead(N_w \oplus C')\). Therefore, the open net \(N_w \oplus C'\) is, as \(C\), a \(bfr\)-controller of \(N\) by Proposition 65(1).

By construction of \(N_w\), there exists an invariant implying that the total number of tokens on the places \(p_0, \ldots , p_k, p_{err}\) is always \(1\). Let \(m\) be an arbitrary marking of \(env(N_w \oplus C')\) where \(p_k\) is marked and all interface places of \(N_w \oplus C'\) are empty. The key observation about \(N_w\) is that if a trace \(v\) of \(env(N_w \oplus C')\) leads to \(m\), then \(v \not \in L_{b}(N)\): By the choice of \(m\) and the construction of \(N_w\), the Parikh vectors of \(v\) and \(w\) agree and we can transform \(w\) into \(v\) by moving \(w_j \in O_{N_w \oplus C'} = I_N\) right and \(w_j \in I_{N_w \oplus C'} = O_N\) left, like in the proof of Theorem 31(1). Because \(w \not \in L_{b}(N)\) by assumption, moving \(w_j \in I_N\) right always results in a trace \(v \not \in L_{b}(N)\): If \(env(N)\) cannot fire a run underlying \(w\), then \(env(N)\) cannot fire a run with an even later provision of a token on the input place \(w_j^i\). Similarly, moving \(w_j \in O_N\) left always results in a trace \(v \not \in L_{b}(N)\): If \(env(N)\) cannot fire a run underlying \(w\), then \(env(N)\) cannot fire a run where a token on the output place \(w_j^o\) is needed earlier. We now show that

performing an induction on the number of tokens that \(m\) puts on the interface places of \(N_w \oplus C'\). The previous observation is the base case. If a place \(x^i\) is marked at \(m\) with \(x\) being an input place of \(N_w \oplus C'\), then a token on \(x^i\) was not needed to perform \(v\); thus, we can move the last \(x\) in \(v\) to the end, obtaining another trace \(v'\) of \(env(N_w \oplus C')\). Now \(v'=v''x\) has the prefix \(v'' \not \in L_{b}(N)\) by induction. Thus, \(v' \not \in L_{b}(N)\) and moving \(x\in O_N\) left results in \(v \not \in L_{b}(N)\) as argued previously. If an output place \(x^o\) is marked at \(m\) with \(x\) being an output place of \(N_w \oplus C'\), then also \(vx\) is a trace of \(env(N_w \oplus C')\) and \(vx \notin L_{b}(N)\) by induction, thus, \(v \notin L_{b}(N)\) because \(x\in I_N\) can always fire in \(env(N)\).

Next, we extend \(N_w = (P', T', F', m_{N_w}, O_N \uplus O_{C'}, I_N \uplus I_{C'}, \varOmega _{N_w})\) to an open net \(N_w^{ bound }\) by adding a disaster transition \(t_{ disaster }\). Formally, we define the open net \(N_w^{ bound } = (P'', T'', F'',\) \( m_{N_w}, O_N \uplus O_{C'}, I_N \uplus I_{C'}, \varOmega _{N_w})\) with

  • \(P'' = P' \uplus \{p_{ disaster }\}\),

  • \(T'' = T' \uplus \{t_{ disaster }\}\), and

  • \(F'' = F' \uplus \{(p_k,t_{ disaster }),\, (t_{ disaster }, p_k), (t_{ disaster }, p_{ disaster })\}\).

By construction of \(N^{bound}_w \oplus C'\), a run underlying a newly introduced strict \({bound_b}\)-violator \(v\) of \(N^{bound}_w \oplus C'\) (i.e., \(v \in {bound_b}(N^{bound}_w \oplus C') \setminus {bound_b}(N_w \oplus C')\)) marks place \(p_k\). By (1), we have \(v \not \in L_{b}(N) \supseteq stop_{b}(N) \supseteq dead_{b}(N) \supseteq {bound_b}(N)\). Clearly, \(N^{bound}_w \oplus C'\) is still a \(bfr\)-controller of \(N\) because of Proposition 65(1).

(2) Let \(w \in L(N) \setminus {ustop_{bfr}}(N)\) with \(w = w_1 \ldots w_k\) for \(j = 1, \dots , k\), \(w_j \in I_N \uplus O_N\). As \(w \not \in {uncov_{bfr}}(N)\), there exists a \(bfr\)-controller \(C\) of \(N\) with \(w \in L_{b}(C)\) by Definition 69. Then \(w \in L(C) \setminus {bound_b}(C)\); otherwise, \(C\) is not a \(bfr\)-controller of \(N\) by Proposition 65(1). As \(w\) is no \(stop\)-trace of \(N\), there is always some output \(o \in O_N\) that \(m_{env(N)}\) can perform after \(w\). For each such output, we conclude that \(wo \in L(N)\) and \(wo \in L(C)\), thus, \(wo\) is not a (strict) \({bound_b}\)-violator of \(N\) by Proposition 65(1).

Like in the proof of (1), we construct a \(bfr\)-controller \(N_w \oplus C'\) of \(N\) with \(dead\)-trace \(w\): We track whether a firing sequence in \(C\) is (a “permutation” of) a prefix of \(w\) by composing \(C\) with another open net \(N_w\). Open net \(N_w\) subsequently moves a token from the initially marked place \(p_0\) to the place \(p_k\); the place \(p_k\) is marked if and only if we encountered (a “permutation” of) the trace \(w_1 \ldots w_k = w\). If \(p_k\) is marked, we make \(N_w\) “intransparent” by preventing any output from \(N_w\), but allow input to \(N_w\). In addition, we put \(\varOmega _{N_w} = \{[p] \mid p \in P'\setminus \{p_k\} \}\). As \([p_{k}]\) is not a final marking of \(N_w\), \(w\) will be a \(dead\)-trace. Once \(N_w\) receives one input—some \(o \in O_N\) as discussed above—we make \(N_w\) transparent again.

Let \(I' = \{i' \mid i \in I_C\}\) and \(O' = \{o' \mid o \in O_C\}\) be “fresh” copies of \(I_C\) and \(O_C\). We derive the open net \(C' = (P_C, T_C, F'_C, m_C, I', O', \varOmega _C)\) from \(C\) by renaming the interface of \(C\) and adjusting the flow relation accordingly. We define the open net \(N_w = (P', T', F', m_{N_w}, O_N \uplus O_{C'}, I_N \uplus I_{C'}, \varOmega _{N_w})\) with

  • \(P' = \begin{array}{@{}c@{\ }l@{\ }} &{} \{p_i \mid 0 \le i \le k\} \\ \uplus &{} \{p_{err}\}, \\ \end{array}\)

  • \(T' = \begin{array}{@{}c@{\ }l@{\ }} &{} \{t_i^x \mid 1 \le i \le k+1 \wedge x \in O_N \} \\ \uplus &{} \{t_i^x \mid 1 \le i \le k \wedge x \in I_N \} \\ \uplus &{} \{t_{err}^x \mid x \in O_N \uplus I_N \}, \\ \end{array}\)

  • \(F' = \begin{array}{ll} &{} \{(x,t_i^x),(t_i^x,x'),(p_{i-1},t_i^x) \mid 1 \le i \le k+1 \wedge x \in O_N \} \\ \uplus &{} \{(x',t_i^x),(t_i^x,x),(p_{i-1},t_i^x) \mid 1 \le i \le k \wedge x \in I_N \} \\ \uplus &{} \{(t_i^x,p_i) \mid 1 \le i \le k \wedge x \in O_N \uplus I_N \wedge x = w_i \} \\ \uplus &{} \{(t_i^x,p_{err}) \mid 1 \le i \le k \wedge x \in O_N \uplus I_N \wedge x \ne w_i \} \\ \uplus &{} \{(t_{k+1}^x,p_{err}) \mid x \in O_N \} \\ \uplus &{} \{(x,t_{err}^x),(t_{err}^x,x'),(p_{err},t_{err}^x),(t_{err}^x,p_{err}) \mid x \in O_N \} \\ \uplus &{} \{(x',t_{err}^x),(t_{err}^x,x),(p_{err},t_{err}^x),(t_{err}^x,p_{err}) \mid x \in I_N \}, \\ \end{array}\)

  • \(m_{N_w} = [p_0]\), and

  • \(\varOmega _{N_w} = \{[p] \mid p \in P'\setminus \{p_k\} \}\).

Figure 15 illustrates the construction of \(N_w\). The same invariant as above implies that the total number of tokens on the places \(p_0, \ldots , p_k, p_{err}\) is always \(1\). Let \(m\) be an arbitrary marking of \(env(N_w \oplus C')\) where \(p_k\) is marked and all interface places of \(N_w \oplus C'\) are empty. The key observation is that if a trace \(v\) of \(env(N_w \oplus C')\) leads to \(m\), then \(v \not \in stop_{b}(N)\): By the choice of \(m\) and the construction of \(N_w\), the Parikh vectors of \(v\) and \(w\) agree and we can transform \(w\) into \(v\) by moving \(w_j \in O_{N_w \oplus C'} = I_N\) right and \(w_j \in I_{N_w \oplus C'} = O_N\) left, like in the proof of (1). Thus, a marking reached by \(v\) in \(env(N)\) can also be reached by \(w\), and we conclude that \(v \not \in stop_{b}(N)\).

Fig. 15
figure 15

Illustration of the construction of the open net \(N_w\) for \(N\) with \(I_N = \{a\},\, O_N = \{b\}\), and \(w = ab \in L(N) \setminus {ustop_{bfr}}(N)\)

Full size image

By the construction of \(N_w \oplus C'\), a run underlying a newly introduced \(dead\)- or \(stop\)-trace \(v\) of \(N_w \oplus C'\) (i.e., \(v \in dead_{b}(N_w \oplus C') \setminus dead_{b}(C)\) or \(v \in stop_{b}(N_w \oplus C') \setminus stop_{b}(C)\)) marks place \(p_k\) and leaves no token on an interface place of \(N_w \oplus C'\). Thus, by the observation above, we have \(v \not \in stop_{b}(N)\) and, hence, \(v \not \in dead_{b}(N)\). In addition, we have \(L(N_w \oplus C') \subseteq L(C)\) and \({bound_b}(N_w \oplus C') \subseteq {bound_b}(C)\) by the construction of \(N_w \oplus C'\). Therefore, the open net \(N_w \oplus C'\) is, as \(C\), a \(bfr\)-controller of \(N\) by Proposition 65(1).

(3) This is analogous to the proof of (2), except that we have to add several places and transitions to \(N_w\), yielding the open net \(N_w'\): The introduced \(dead\)-trace \(w\) of \(N_w \oplus C'\) may be a \(stop\)-trace of \(N\), i.e., \(w \in stop(N) \setminus dead(N)\). Thus, after \(N'_w\) recognizes (a “permutation” of) \(w\), we buffer all messages from \(C'\) to \(N'_w\) inside \(N'_w\): For each input place \(x \in O_{C'}\) of \(N_w\), we add a place \(\overline{x}\) and a transition \(t_{\overline{x}}\) such that \(\hbox {}^{\bullet }t_{\overline{x}} = \{x\}\), \(t_{\overline{x}}^{\bullet } = \{\overline{x}\}\), \(x^{\bullet } = \{t_{\overline{x}}\}\), and the postset of \(\overline{x}\) in \(N_w'\) is the postset of \(x\) in \(N_w\). In addition, we define all markings of \(N'_w\) as final markings. That way, we have \(w \in stop_{b}(N'_w \oplus C')\) while guaranteeing \(dead_{b}(N'_w \oplus C') \subseteq dead_{b}(C)\).\(\square \)

1.3 Proof of Lemma 87

With Lemma 87 in Sect. 5.3, we show that \(\fancyscript{F}^+_{b,fin}\)-refinement is a precongruence for labeled nets and operator \(\Vert \). For this proof, we will use the same four saturation conditions as for the \(\fancyscript{F}^+_{fin}\)-semantics (see the proof of Lemma 46 in Sect. 8.1), which also hold for the \(b\)-bounded \(\fancyscript{F}^+_{fin}\)-semantics:

$$\begin{aligned} \begin{array}{rl} \text {{CON}1: } &{} (w, X, Y) \in \fancyscript{F}^+_{b,fin}(N), X' \subseteq X, Y' \subseteq Y \text { implies } (w, X', Y') \in \fancyscript{F}^+_{b,fin}(N) \\ \text {{CON}2: } &{} (w, X, Y) \in \fancyscript{F}^+_{b,fin}(N) \wedge \forall z \in Z: (wz, z^{-1}X, z^{-1}Y) \not \in \fancyscript{F}^+_{b,fin}(N) \text { implies } \\ &{} (w, X \cup Z, Y \cup Z) \in \fancyscript{F}^+_{b,fin}(N) \\ \text {{CON}3: } &{} (w, X, Y) \in \fancyscript{F}^+_{b,fin}(N) \text { implies } (w, {\uparrow {X}}, {Y}) \in \fancyscript{F}^+_{b,fin}(N) \\ \text {{CON}4: } &{} (w, X, Y) \in \fancyscript{F}^+_{b,fin}(N) \text { implies } (w, X, X \cup Y) \in \fancyscript{F}^+_{b,fin}(N) \end{array} \end{aligned}$$

To see these conditions, consider first some \((w, X, Y)\in \fancyscript{F}^+_{fin}(N) \subseteq \fancyscript{F}^+_{b,fin}(N)\). Then, CON1–CON4 follow directly from Lemma 46. Now, consider a \(b\)-bounded fintree failure \((w, X, Y)\) with \(w \in {bound_b}(N)\); here, all four conditions are immediate because \((w, X', Y') \in \fancyscript{F}^+_{b,fin}(N)\) for any \(X' \in \fancyscript{P}((I \uplus O)^+)\) and \(Y' \in \fancyscript{P}((I \uplus O)^*)\).

In the following proof, we will denote the first set on the right-hand side in Lemma 84 by \(\fancyscript{F}1^+_{b,fin}(N_1,N_2)\). The precongruence result for \(\fancyscript{F}^+_{fin}\)-refinement in Lemma 46 holds for general sets of fintree failures (see Remark 47). We make use of this, although the equation in Lemma 42(2) does not match Lemma 84, but just gives \(\fancyscript{F}1^+_{b,fin}(N_1,N_2)\).

Proof

Let \(Impl\sqsubseteq _{\fancyscript{F}^+_{b,fin}} Spec\) and \(C\) be a composable labeled net for \(Impl\) and \(Spec\). We have to check the two items of Definition 78 in order to prove that \(Impl\Vert C \sqsubseteq _{\fancyscript{F}^+_{b,fin}} Spec\Vert C\). The first item follows from Proposition 55(1) because our assumption implies \({bound_b}(Impl)\subseteq {bound_b}(Spec)\) as well as—due to Lemma 81(1)—\(L_b(Impl)\subseteq L_b(Spec)\).

For the second item, we first consider some \((w,X,Y)\in \fancyscript{F}1^+_{b,fin}(Impl,C)\). We observe that, due to Definition 78(2), \(\fancyscript{F}^+_{b,fin}(Impl)\) is related to \(\fancyscript{F}^+_{b,fin}(Spec)\) in the sense of \(\fancyscript{F}^+_{fin}\)-refinement. So by Lemma 46, \(\exists x \in \{\varepsilon \} \cup {\downarrow {X}} \cup {\downarrow {Y}}: \, (wx, x^{-1}X, x^{-1}Y) \in \fancyscript{F}1^+_{b,fin}(Spec,C) \subseteq \fancyscript{F}^+_{b,fin}(Spec\Vert C)\). Second, we consider some \((w,X,Y) \in {finbound_b}\) \((Impl\Vert C)\). This time, due to \({bound_b}(Impl\Vert C) \subseteq {bound_b}(Spec\Vert C)\), we even have \((w, X, Y)\in {finbound_b}(Spec\Vert C) \subseteq \fancyscript{F}^+_{b,fin}(Spec\Vert C)\); that is, Definition 78(2) is satisfied taking \(x=\varepsilon \).\(\square \)

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Vogler, W., Stahl, C. & Müller, R. Trace- and failure-based semantics for responsiveness. Acta Informatica 51, 499–552 (2014). https://doi.org/10.1007/s00236-014-0205-y

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00236-014-0205-y

Search

Navigation