Dense-Time Petri Nets (TPNs) are now a well-established model to describe and study real time (quantitative) and functional (qualitative) properties of safety-critical, computer-controlled systems. Testing equivalences, used to compare systems' behaviors (processes) and reduce the structure of systems, are defined in terms of tests that processes may or must pass. The intention of the paper is to establish the interrelations between various semantics for must-testing equivalences with extended tests, in the framework of TPNs. This allows for studying in detail the timing behavior in addition to the degree of relative concurrency of processes generated when systems are functioning.
Dense-Time Petri Nets (TPNs) are suitable for qualitative and quantitative modelling and verifying of safety-critical, computer-controlled, real-time systems. Several semantics (behaviors) are explored in the literature for TPNs, that can be classified according to interleaving – partial order dichotomy. The classical interleaving behavior of the TPN is described by runs — sequences of changes in states by time elapsings and/or transition firings. The semantics allows for analyzing some safety and liveness properties of systems, however concurrency between net transitions is reduced to non-deterministic choice between sequences of transitions firings in any possible order. Step semantics of TPNs generalizes the interleaving approach by allowing several concurrent transitions (forming a step) to fire simultaneously. Partial order semantics of TPNs is most often represented by means of the so-called causal net processes which include events and conditions related by causal dependence (the absence of causality means concurrency) and equipped with timing information. Causal tree semantics summarizes the interleaving and partial order approaches by representing the behavior of the TPN in the form of a tree with nodes corresponding to runs, and edges labeled by actions with their times and causal predecessors.
Testing equivalences [
As safety-critical applications often require verification of real time characteristics, testing
equivalences are expanded in concurrent models with time. In the papers [
In this section, some terminology concerning the model of Petri nets with timing constraints (time intervals on the firings of transitions) and its concurrent semantics in terms of interleaving/step firing sequences, causal net processes and causal trees are defined.
We start with recalling the definitions of the structure and interleaving/step behavior of time Petri nets [15, 16]. We use as an alphabet of actions and N as a set of multisets over . Let the domain T of time values be the set of rational numbers. We denote by [ 1, 2] the closed interval between two time values 1, 2 ∈ T. Infinity is allowed at the upper bounds of intervals. Let be the set of all such intervals.
Definition 1. • A (labeled over ) time Petri net is a pair = ( , ), where = ( , , , 0, ) is a (labeled over ) underlying Petri net (with a finite set of places, a 1Testing equivalence with extended tests checks, after the executions of the experiments, the tests that are continuations of the experiments with steps/posets of actions, not with single actions.
: (∙ ∪ ∙ ) ∩ (∙ ′ ∪ ′∙ ) = ∅). define ∙ = ⋃︀ ∈ ∙ and ∙ = ⋃︀
∈ ∙ . ifnite set of transitions such that ∩ = ∅ and ∪ ̸= ∅, a flow relation ( × ) ∪ ( × ), an initial marking ∅ ≠ 0 ⊆ , a labeling function : → ) and : → is a static timing function associating with each transition a time interval. ⊆ For a transition ∈ , the boundaries of the interval () ∈ are called the earliest ifring time and latest firing time of . For ∈ ∪ , let ∙ = { | (, ) ∈ } and ∙ = { | (, ) ∈ } be the preset and postset of , respectively. For ⊆ ∪ , if ∙ ⊆ • A marking of is any subset of . A transition ∈ is enabled at a marking . Let ( ) be the set of transitions enabled at . A non-empty subset ∅ ̸= ⊆ is a step enabled at a marking , if (∀ ∈ ◇ ∈ ( )) and (∀ ̸= ′ ∈ marking and 0() = 0, for all ∈ (0).
A state of is a pair (, ), where is a marking and : ( ) →− timing function. The initial state of is a pair 0 = (0, 0), where 0 is the initial T is a dynamic A step enabled at a marking can fire from a state = (, ) after a delay time ∈ T if ( () ≤ () + ), for all ∈ , and ( (′) + ≤ (′)), for all ′ ∈ ( ). The firing of a step that can fire from a state = (, ) after a delay time leads to the new state ′ = ( ′, ′) (denoted →−
′) given by: (, ) () →−
′, () ∀′ ∈ ◇ ′(′) = ⎨ ⎧ (′) + ,
0, ⎩ undefined , otherwise.
if ′ ∈ ( ∖ ∙ ), if ′ ∈ ( ′) ∖ ( ∖ ∙ ), time Petri nets.
(, ) Then, we write →−
′, if = ( ) = Σ∈ () ∈ N, i.e. is a multiset over the set { ∈ | = () and ∈ }. We use the notation →− = (1, 1) . . . (, ) and = 0 (1, 1) 1 . . . − 1 (, ) = ′ ( ≥ →− →−
′ if
0). In this
0, and ( ) be the set of all reachable states of from 0. For
case, is a step firing sequence of from (to ′), and ′ is a reachable state of
from . Whenever | |= 1 for all 1 ≤ ≤ , we call an interleaving firing sequence
of . Let ℱ ()( ) be the set of all step (interleaving) firing sequences of from
= (1, 1) . . .
(, ) ∈ ℱ ()( ), ( ) = (1, 1) . . . (, ) if = () for all 1 ≤ ≤ .
We call -restricted if ∙ ̸= ∅ ≠ ∙ , for all transitions ∈ ; contact-free if whenever
a step can fire from the state = (, ) after some delay time , then ( ∖∙ )∩ ∙ = ∅,
for all ∈ ( ). In what follows, we shall consider only -restricted and contact-free
Example 1. A (labeled over = {, , }) time Petri net ̃︂ is shown in Figure 1. Here,
the places are represented by circles, and transitions — by bars; the names are depicted near the
net elements, the flow relation is drawn by the arcs, the initial marking is represented as the set
of the places with tokens (bold points), and the values of the labeling and timing functions are
, 3[
= ({1, 4}, 0.5) (3, 1) (2, 2) (5, 2) is a step firing sequence of ̃︂ from 0. Also, we have ( ) = (2′, 0.5) (, 1) (, 2) (, 2). Furthermore, it is easy to see that ̃︂ is really -restricted and contact-free.
In this subsection, the concept of causality-based net processes is presented in the context of TPNs.
We start with the definition of time causal nets, whose events and conditions are related by causal dependence and concurrency (absence of causality), and whose timing function associates with the events their occurrence times.
Definition 2.
A (labeled over ) time causal net is a finite, acyclic net = (, , , , ) with a set of conditions; a set of events; a flow relation ⊆ ( × ) ∪ ( × ) such that timing function : → T such that + ′ ⇒ () ≤ (′). | ∙ |≤ 1 ≥|
∙ |, for all ∈ , and ∙ = = ∙ ; a labeling function : → , and a For a time causal net = (, , , , ) and , ′ ∈ , define: • ∙ = { ∈ | ∙ = ∅}; • ≺ = +, ⪯ = * (causality);
∙ (); • () = {′ ∈ | ′ ≺
} (causal predecessors of ), () = {′ ∈ | (′) < ()} (time predecessors of ), and () = (()∙ ∪ ∙ ) ∖ timely sound subset of if ′ ⊂ and (′) ⊆ ′, for all ′ ∈ ′; • ′ is a downward-closed subset of if ′ ⊂ and (′) ⊆ ′, for all ′ ∈ ′; a • ⌣ ′ ⇐⇒
¬(( ≺ ′) ∨ (′ ≺ )) (concurrency); ∅ ̸= ⊆ is a step if ⌣ ′ and () = (′) for all ̸= ′ ∈ . Let ( ) = () for some ∈ (time of ); 1 ≤ ≤ , is an -linearization; • ( ) = ( , ⪯ ∩( × • a sequence = 1 . . . ( ≥
0) of steps of is an s-linearization of if ⋃︀ and ⋂︀ set of ⋃︀ ¬((′ ≺ and for all 1 ≤ < ≤ it holds: ⋃︀
1≤ ≤ is a downward-closed and timely sound sub1≤ ≤ >1 = ∅ (i.e. every event of appears in the sequence exactly once), 1≤ ≤ (i.e. both causal and time order are preserved: for all 1 ≤ < ≤ , ) ∨ ( (′) < ())), for all ∈ , ′ ∈ ). Whenever | | = 1 for all 1≤ ≤ = ), , ) is a time poset2. For time posets closed and timely sound subset of , ⪯ ′=⪯ ∩
′ × ′, ′ = |′ , and ′ = |′ .
= (, ⪯ , , ) and ′ = (′, ⪯ ′, ′, ′), is a pos-extension of ′ if ′ is a downwardWe are now ready to define the concept of causal net based processes of TPNs, proposed in [15].
Definition 3. = (, , , , ), hold:
Given a time Petri net = (( , , , 0, ), ) and a time causal net • a mapping : ∪ → ∪ is a homomorphism from to if the following – () ⊆ , () ⊆ ; – the restriction of to ∙ is a bijection between ∙ and ∙ (), and the restriction of to ∙ is a bijection between ∙ and ()∙ , for all ∈ ; – the restriction of to ∙ is a bijection between ∙ and 0; – () = ( ()), for all ∈ .
and is a homomorphism from to ; • a pair = ( , ) is a time process of a time Petri net if is a time causal net • a time process = ( , ) of is correct if for all ∈ it holds: (a) () ≥
TOE (∙ , ()) + ( ()), (b) ∀ ∈ ( (())) ◇ () ≤
TOE ((), ) + ().
Here, for a subset ′ ⊆
and a transition ∈ ( (′)), the time of enabling (TOE) of , i.e. the latest global time moment when tokens appear in all input places of , is defined as follows:
TOE (′, ) = max [′] = { ∈ ′ | () ∈ ∙ }.
Let ( ) denote the set of correct time processes of .
︁( { (∙ ) | ∈ [′] ∖ ∙ } ∪ {0} , where ︁)
We now present for the time Petri net the relationships between its correct time processes and its interleaving/step firing sequences from the initial state.
Proposition 1. [15, 16] Let be a time Petri net. Then, function : → T such that ⪯ ′ ⇒ () ≤ (′).
2A (labeled over ) time poset (partially ordered set) is a tuple = (, ⪯ , , ) consisting of a finite set of elements; a reflexive, antisymmetric and transitive relation ⪯ ; a labeling function : → ; and a timing (i) for any = ( , ) ∈ ( ) with an ()-linearization = 1 . . . of , there is a unique step (interleaving) firing sequence ( ) = ( (1), (1) − 0) . . . ( (), () − (− 1)) ∈ ℱ ()( ); (ii) for any step (interleaving) firing sequence ∈ ℱ ()( ), there is a unique (up to an isomorphism3) correct time process = ( , ) ∈ ( ) with a unique ()linearization of such that ( ) = .
For correct time processes = ( , ), ′ = ( ′, ′) ∈ ( ), we say that is a -extension of ′ in if ( ) is -extension of ( ′), ′ ⊂ , ′ = ∩ (′ × ′ ∪ ′ × ′), and ′ = |′∪′ .
We expand the above results to -extensions of correct time processes of TPNs. Lemma 1. Given a time Petri net , ∈ ℱ ()( ), and ∈ ( ) such that = ( ), where is an ()-linearization of , (i) if ̃︀ is a -extension of in , then there is ′ ∈ ℱ ()( ) such that ′ = ( ′), where ′ is an ()-linearization of ;
̃︀ ̃︀ (ii) if ′ ∈ ℱ ()( ), there is ̃︀ ∈ ( ) such that ̃︀ is a -extension of in and ′ = ( ′), where ′ is an ()-linearization of .
̃︀ ̃︀
Causal trees [17] are synchronisation trees which carry in their labels additional information about causes of actions thus providing us with an interleaving description of concurrent processes, which faithfully expresses causality. Time causal trees are generalizations of causal trees by adding timing. In the time causal tree of the TPN, the nodes are the interleaving firing sequences of the TPN, and an edge exists between two nodes if the second one is a direct extension of the first one. The causes in the edge labels are calculated based on the causality relations in the correct time processes of the TPN corresponding to the nodes (the interleaving ifring sequences).
Definition 4. The time causal tree of the TPN , ( ), is a tree (ℱ ( ), , ), where ℱ ( ) is the set of nodes with the root ; = {(, (, )) | , (, ) ∈ ℱ ( )} is the set of edges; is the labeling function such that ( ) = and (, (, )) = ( (), , ), with = ( = 1 . . . ), (, ) = (, ) ( (, ) = 1 . . . ), = { − + 1 | ≺ (, ) }. Let ℎ( ) be the path starting from the root and finishing in the node of ( )4.
3Time processes = ( , ) and ′ = ( ′, ′) ∈ ( ) are isomorphic (denoted ≃ ′) if there exists a bijective mapping : ∪ → ′ ∪ ′ such that (i) () = ′ and () = ′; (ii) ⇐⇒ () ′ (), for all , ∈ ∪ ; (iii) () = ′( ()), for all ∈ ; (iv) () = ′( ()), for all ∈ ; (v) () = ′( ()), for all ∈ ∪ .
4We assume ℎ( ) = . Notice that in ( ), for any node ∈ ℱ( ), there is a path starting from the root and finishing in . (, 0.5, ∅) (, 0.5, ∅) (, 1, {2}) (, 2, {1}) (, 2, {1, 3}). Example 2. Consider the time Petri net ̃︂ (see Figure 1) and its interleaving firing sequence = (1, 0.5) (4, 0) (3, 1) (2, 2) (5, 2) ∈ ℱ (̃︂ ). It is easy to get that (ℎ( )) = We finally establish some relationships between correct time processes and labeled paths in the time causal trees of two time Petri nets.
Proposition 2. Let , ′ be time Petri nets. Then,
(ℎ( ( ))) = ′(ℎ( ′ ( ( )))), for any -linearization of ; (i) for any ∈ ( ) and ′ ∈ ( ′) with an isomorphism : ( ) → ( ′ ), is an isomorphism : ( ) → ( ′ ) such that ( ) = ′ .
(ii) for any ∈ ℱ ( ) and ′ ∈ ℱ ( ′) such that (ℎ( )) = ′(ℎ( ′)), there
Interleaving testing equivalence deals with the experiments on the TPN — sequences of actions with their times — and the behaviors which are tested for after the experiments — sets of actions with their times. So, it checks whether actions with times, given as a test, can be executed after a sequence of actions with times, specified as an experiment. Here, both the experiments and tests represent interleaving semantics.
Definition 5.
Given time Petri nets and ′, • for a sequence ∈ ( × T)* and a set ⊆ ( × T), after MUST if for all firing sequences
∈ ℱ ( ) such that ( ) = , there exists an element (, ) ∈ and a firing sequence (, ) ∈ ℱ ( ) such that ( (, )) = (, ); sequences ∈ ( × T)* and for all sets ⊆ ( ×
• and ′ are interleaving testing equivalent (denoted ∼ ′) if for all after MUST
⇐⇒ ′ after MUST .
In step testing, the experiments on the TPN are sequences of multisets over sets of actions with their times and the tests checked after the experiments are sets of multisets over sets of actions with their times. So, it checks whether multisets over sets of actions with times, given as a test, can be executed after a sequence of multisets over sets of actions with times, specified as an experiment. Thereby, both the experiments and tests respect step semantics. Definition 6.
Given time Petri nets and ′, • for a sequence ∈ (N × T)* and a set ⊆ (N × T), after MUST if for all firing sequences
∈ ℱ ( ) such that ( ) = , there exists an element (, ) ∈ and a firing sequence (, ) ∈ ℱ ( ) such that ( (, )) = (, ); 1 : after MUST
⇐⇒ ′ after MUST .
The idea of partial order testing is that the experiments on the TPN are time posets and the tests, that are examined after the experiments, are sets of -extensions of the experiments. This contrasts with partial order based testing investigated in the paper in [14], where the tests contain sets of time posets extending the experiments by single actions with their times. From now on, we denote -extensions of a time poset by TP .
Definition 7.
Given time Petri nets and ′, • for a time poset and a set TP ⊆ TP , after MUST TP if for all time processes = ( , ) ∈ ( ) and for all isomorphisms : ( ) →− ,
there exists a time poset ′ ∈ TP, a time process ′ = ( ′, ′) ∈ ( ), and an isomorphism ′ : ( ′) →− ′, such that ′ is a -extension of and ⊂ ′; • and ′ are poset testing equivalent (denoted ∼ ′) if for all time posets and for all sets TP ⊆ TP , it holds: after MUSTTP
⇐⇒ ′ after MUSTTP.
Theorem 1. Given time Petri nets and ′, ∼ ′ =⇒ ∼ =⇒ ∼ ′.
The implications in the theorem above do not hold in the opposite directions, as demonstrated in the example below.
Example 3. The time Petri nets 1 and 2, shown in Figure 2, are ∼ –equivalent but they are neither ∼ – nor ∼ –equivalent. First, check that 1 and 2 are not ∼ – equivalent. It is easy to see that 1 after = (1′ + 1′, 1) MUST = ∅, because in ℱ ( 1) there is no firing sequence such that ( ) = . However, this is not the case in 2, since in ℱ ( 2) there exists a firing sequence such that ( ) = and it is impossible to find any element (, ) of so as to locate in ℱ ( 2) a firing sequence (, ) such that ( (, )) = (, ). Hence, it hods that ¬( 2 after = (1′ + 1′, 1) MUST = ∅). Second, verify that 1 and 2 are not ∼ –equivalent. Define a poset = ({1, 2}, ⪯ , , ) (with ⪯ = {(1, 1), (2, 2)}, (1) = , (2) = , (1) = (2) = 1). For any time process 1 = ( 1, 1) ∈ ( 1), there is no isomorphism 1 : ( 1) →− . So, it is true that 1 after MUST TP = ∅. However, this is not the case in 2 because there is a time process 2 = ( 2, 2) ∈ ( 2), with 2 containing two concurrent events labeled by and , both with time value 1, and an isomorphism 2 : ( 2) →− , and we cannot find any -extension of in TP. Hence, it hods that ¬( 2 after MUST TP = ∅).
The time Petri nets 3 and 4, shown in Figure 3, are ∼ –equivalent but not ∼ – equivalent. Let’s make sure of the latter. Define posets = ({1}, ⪯ , , ) (with ⪯ = {(1, 1)}, (1) = , (1) = 0) and ′ = ({1, 2, 3, 4}, ⪯ ′, ′, ′) (with ⪯ ′= {(, ) | 1 ≤ ≤ 4} ∪ {(2, 3)}, ′(1) = ′(2) = , ′(3) = ′(4) = , ′(1) = ′(2) = 0, and ′(3) = ′(4) = 2.9. It is easy to see that ′ is a -extension of . For any time process 1 = ( 1, 1) ∈ ( 3), with 1 consisting of an event with label and time value 0, and any isomorphism 1 : ( 1) →− , we can find a -extension 1′ = ( 1′ , ′1) ∈ ( 1), with 1′ consisting of two concurrent events, both with label and time value 0, and two concurrent events, both with label and time value 2.9, and, moreover, one of the two events labeled by is causally preceded by the added event labeled by , and an isomorphism 1′ : ( 1′ ) →− ′ such that 1 ⊂ 1′ . But this is not the case in 4.
The time Petri nets 5 and 6, depicted in Figure 4, are ∼ ⋆⋆–equivalent, for ⋆ ∈ {, , }. □
At last, the definition of testing equivalence based on the causal trees of TPNs is developed. In doing so the experiments are considered as sequences over the alphabet ( × T × 2N) (corresponding to labeled paths from the roots in the causal trees) and the tests are specified as sets of non-empty sequences over the same alphabet (corresponding to sets of extensions of the labeled paths in the causal trees). In the paper [14], the tests directly extend the experiments by single elements, not by sequences of elements, from the set ( × T × 2N). Definition 8. Given time Petri nets and ′ with their time causal trees ( ) and ( ′), respectively, • for a sequence ∈ ( × T × 2N)* and a set W ⊆ ( × T × 2N)+, we say ( ) after MUST W if for all paths in ( ) from its root to a node such that () = , there exists ′ ∈ W and a path ′ starting from the node , such that (′) = ′; • and ′ are causal tree testing equivalent ( ∼ ′) if for all sequences ∈ ( × T × 2N)* and sets W ⊆ ( × T × 2N)+, it holds: ( ) after MUSTW
⇐⇒ ( ′) after MUSTW.
We finally expand the main result of [ 14] by establishing the coincidence of poset and causal tree testing equivalences with extended tests, in the setting of TPNs.
Theorem 2. Given time Petri nets and ′,
∼ ′ ⇐⇒ ∼ ′.
We have specified and studied several testing equivalences based on concurrent semantics, in the setting of contact-free time Petri nets. In doing so, we dealt with various conceptions of the behavior of the time Petri net: interleaving/step firing sequences, time processes, from causal nets of which partial orders are derived, and time causal tree, constructed from interleaving ifring sequences and partial orders. We have demonstrated that interleaving testing equivalence (with the experiments as labeled interleaving firing sequences and with the tests as experiments extensions by single actions with their times) is coarser than step testing (with the experiments as labeled step firing sequences and the tests as sequences extensions by steps of concurrent actions with their times), which, in turn, is coarser than poset testing (with time posets as experiments and their -extensions as tests). As the main result, the latter equivalence has been established to coincide with causal tree testing (based on labeled paths and their extensions in time causal trees of TPNs).
As for future work, we plan to investigate the equivalences and semantics under consideration in the framework of Petri nets with weak timing policy [18]. Also, it would be interesting to see whether open intervals in the specification of TPNs influence the results obtained here. Netherlands, July 15-18, 1991, IEEE Computer Society, 1991, pp. 110–119. URL: https: //doi.org/10.1109/LICS.1991.151635. doi:10.1109/LICS.1991.151635. [9] M. Hennessy, T. Regan, A process algebra for timed systems, Inf. Comput. 117 (1995) 221–239. URL: https://doi.org/10.1006/inco.1995.1041. doi:10.1006/inco.1995.1041. [10] F. Corradini, W. Vogler, L. Jenner, Comparing the worst-case eficiency of asynchronous systems with PAFAS, Acta Informatica 38 (2002) 735–792. URL: https://doi.org/10.1007/ s00236-002-0094-3. doi:10.1007/s00236-002-0094-3. [11] L. F. L. Díaz, D. de Frutos-Escrig, Denotational semantics for timed testing, in: M. Bertran, T. Rus (Eds.), Transformation-Based Reactive Systems Development, 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS’97, Palma, Mallorca, Spain, May 21-23, 1997, Proceedings, volume 1231 of Lecture Notes in Computer Science, Springer, 1997, pp. 368–382. URL: https://doi.org/10.1007/ 3-540-63010-4_25. doi:10.1007/3-540-63010-4\_25. [12] E. Bihler, W. Vogler, Timed Petri nets: Eficiency of asynchronous systems, in: M. Bernardo, F. Corradini (Eds.), Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004, Revised Lectures, volume 3185 of Lecture Notes in Computer Science, Springer, 2004, pp. 25–58. URL: https://doi.org/ 10.1007/978-3-540-30080-9_2. doi:10.1007/978-3-540-30080-9\_2. [13] M. V. Andreeva, I. B. Virbitskaite, Observational equivalences for timed stable event structures, Fundam. Informaticae 72 (2006) 1–19. URL: http://content.iospress.com/articles/ fundamenta-informaticae/fi72-1-3-02. [14] E. N. Bozhenkova, I. B. Virbitskaite, Testing equivalences of time Petri nets, Program.
Comput. Softw. 46 (2020) 251–260. URL: https://doi.org/10.1134/S0361768820040040. doi:10. 1134/S0361768820040040. [15] T. Aura, J. Lilius, A causal semantics for time Petri nets, Theor. Comput. Sci. 243 (2000) 409– 447. URL: https://doi.org/10.1016/S0304-3975(99)00114-0. doi:10.1016/S0304-3975(99) 00114-0. [16] I. B. Virbitskaite, D. Bushin, E. Best, True concurrent equivalences in time Petri nets, Fundam. Informaticae 149 (2016) 401–418. URL: https://doi.org/10.3233/FI-2016-1454. doi:10.3233/FI-2016-1454. [17] P. Darondeau, P. Degano, Refinement of actions in event structures and causal trees, Theor. Comput. Sci. 118 (1993) 21–48. URL: https://doi.org/10.1016/0304-3975(93)90361-V. doi:10.1016/0304-3975(93)90361-V. [18] P. Reynier, A. Sangnier, Weak time Petri nets strike back!, in: M. Bravetti, G. Zavattaro (Eds.), CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, volume 5710 of Lecture Notes in Computer Science, Springer, 2009, pp. 557–571. URL: https://doi.org/10.1007/978-3-642-04081-8_37. doi:10.1007/978-3-642-04081-8\_37.