Fachbereich Informatik

Embedded Systems Group (ES)

Desynchronization Hierarchy

The following nodes show by examples that the following hierarchy of nodes is strict: Sequential ⊊ Endochrony ⊊ Weak Endochrony ⊊ Strong Confluence ⊊ Confluence = Weak Confluence ⊊ UniqueOutput. Note that by Newman's lemma confluence and weak confluence are the same for all noetherian relations, and since the operational semantics of DPN nodes with finite input streams are always noetherian, it proves already the equivalence of confluence and weak confluence for DPNs with finite inputs. Second, for infinite inputs, we always consume finite prefixes for an infinite input, and can therefore always close a divergent transition sequence for them. Thus, confluence and weak confluence are the same for DPNs. The other inclusions follow by proven theorems, and the examples below demonstrate the strictness of these inclusions.

Gustave : Sequential ⊊ Endochrony
This is a version of Berry's Gustave function. It is not a sequential function, but is endochronous, since even after desynchronization, there are no overlapping firing rules. It can therefore be safely desynchronized. It therefore proves that the inclusion of the sequential functions in the endochronous set of functions is a strict one.
cp2 : Endochrony ⊊ Stable
This is a simple node that copies values coming from two input streams to two corresponding output streams. The node is not endochronous, since there are overlapping firing rules after desynchronization (if we do not match ⊡ with variables, there are no overlapping rules in the synchronous version). The node is however weakly endochronous, and it is also a stable function, which means that f(inf{x1,x2}) = inf{f(x1),f(x2)}. Note that if there is an overlapping, we have a shared consumed input alpha, continued with further inputs beta1 and beta2, and then alpha = inf{alpha*beta1,alpha*beta2} and thus stability means that f(alpha) = inf{f(alpha*beta1),f(alpha*beta2)}. Hence, after a branching no further shared outputs are generated. It therefore proves that the inclusion of the endochronous functions in the stable functions is a strict one.
ParOR : Stable ⊊ Weak Endochrony
This is a parallel OR node that generates a true value on the single boolean output stream if one of the two input streams provides a value true. Only if both provide value false, it generates value false. The node is not endochronous, since after desynchronization, there are overlapping firing rules, and it is also not stable since ParOR(inf{([true],[true;true]),([true;true],[true])}) = ParOR([true],[true]) = [true;true], but inf{ParOR([true],[true;true]), ParOR([true;true],[true])} = inf{[true;true;true],[true;true;true]} = [true;true;true]. Hence, the node proves that the inclusion of the stable functions in the weakly endochronous set of functions is a strict one.
cp2LookAhead3 : Weak Endochrony ⊊ Strong Confluence
cp2LookAhead3 shows the difference between weak endochrony and strong confluence: The node is not weakly endochronous, since for the two overlapping rules, the difference action is not contained in the table. Obviously, the second rule can be however replaced by three rule applications of the first rule, so that the node is strongly confluent. It therefore proves that the inclusion of the weakly endochronous functions in the set of functions that are strongly confluent is a strict one.
cpSomeParallel : Strong Confluence ⊊ Confluence
This example is similar to the previous one in that some atomic rules can be composed to construct the remaining ones: The final five rules copy single inputs to the corresponding output channel, similar to single copy nodes. The first two rules, however, demand that the first three and the last three values are copied together. The node is not strongly confluent, since from state s0 = ([a],[b],[c],[d],[e] | [],[],[],[],[]) we can go to s1 = ([],[],[],[d],[e] | [a],[b],[c],[],[]) using rule r0 and also to state s2 = ([a],[b],[],[],[] | [],[],[c],[d],[e]) using rule r1. We can close this, using rules r5 and r6 from state s1, and using rules r2 and r3 from state s2 to a shared state ([],[],[],[],[] | [a],[b],[c],[d],[e]). However, closing the diamond requires more than one rule application on both sides, so that the node is not strongly confluent, but still confluent.
CopySome02 : Confluent ⊊ UniqueOutput
This is yet another version of a copy node: It copies values of input stream x0 to the output stream, but only if another value is found on one of the other input streams. The node is therefore not endochronous and also not weakly endochronous. It is even at the synchronous level nondeterminstic concerning the consumption of the input streams, but it generates a unique output stream. It therefore proves that the set of confluent nodes is strictly contained in the set of nodes that generate a unique output stream
NonDet
This is a difficult node: The output stream consists just of a sequence of ones. But how many will be generated? For an infinite input stream of 1s on x0 or on x2, there is an infinite output stream of ones which can be generated in different ways. If both x0 and x2 are however finite, we can used r2 and r3 to copy all pairs of 11 to the output, so that finally either nothing or a single 1 is left in buffers x0 and x2. Now, it depends on whether there is a 1 in x1. To which class does this node belong?