NetworkCalculus.md

Discussion on Network Calculus

Following the NC as defined in "Formal Verification of Real-time Networks", Chapter 3 defines four main sections:

• Algebraic Structures
• Instances
• Properties
• Coq Development

We can take a look at the details of their construction, and make use of their algebraic framework.

Algebraic structures (Target Similar)

The paper defines a dioid, which we can take to just be an idempotent algebra, aka a min($\oplus$)-plus($\otimes$) semiring (this will be useful for identifying what Coq libraries we need). For example, "A Coq Formalization of Data Provenance" mechanizes these tropical semirings to get the provenance of combined data with respect to initial data. We can start to see how this strucure might be useful for temporal bounds.

Def. (Dioid): A set $D$ with two operators $\oplus$ and $\otimes$ that satisfies associativity, commutativity, distributivity, neutrality and absorption, idempotence.

Theorem 1: Any subset $D' \subseteq D$ that includes the neutral elements (0 and 1) and is stable under $\oplus$, $\otimes$, and infinite sums (Kleene Star) is also a complete dioid.

Def. (Kleene Star): Defines $a^*$ as the infinite sum of powers of $a$ under $\otimes$.

$$ a^* = \oplus_{i=0}^\infty a^i $$

Theorem 2: Establishes the Kleene star $a^* \otimes b$ as the least solution to $x = (a \otimes x) \oplus b$

The intuition behind this Theorem 2 is as follows:

1.1 We imagine starting with $b$. If you do nothing else, $x=b$. 1.2 If we apply $a$ once and then continue with $x$, we get $x = a \otimes x \oplus b$. This means we first apply $a$ then combine it with the result of $x$ and add $b$.

2.1 If we repeat this process, applying $a$ multiple times, we start building up terms like $b, a \otimes b, a \otimes (a \otimes b)$, and so on. 2.2 The terms can be represented as $b, a \otimes b, a^2 \otimes b,...$

3.1 Kleene star encapsulates the idea of applying $a$ any number of times. Therefore we are given the smallest possible solution.

Instances (Target Similar)

The following theorems are important for our NC because they extend the applicability of our previous dioid structures to more specific sets of functions used in NC (these theorems should be targeted for the specific property we seek to prove). In this case, $F^+$ and $F^\uparrow$ are complete dioids, and the NC ensures that these sets can be used to model and analyze non-negative and non-decreasing data flows and delays.

Theorem 3: The set of functions $F$ with $\oplus = \land$ (minimum) and $\otimes = *$ (convolution) forms a complete dioid.

This theorem shows the set of functions with minimum and convolution operations forms a complete dioid.

Def. (Minimum): Defined as the minimum operation $\land$. For two functions $f, g \in F$,

$$ (f \oplus g)(t) = \mathsf{min}(f(t), g(t)). $$

Def. (Convolution): For two functions $f$ and $G$ in the set $F$ of non-negative, non-decreasing functions:

$$ (f \otimes g)(t) = \mathsf{inf}_{0 \leq s \leq t} {f(s) + g(t-s)} $$

Intuitively, we can break down the definition as follows:

1.1 $f(t)$ represents the cumulative effect or workload up to a time $t$ for one process. 1.2 $g(t)$ represents the cumulative effect or workload up to a time $t$ for another process.

Our goal is to combine these effects to understand the total impact up to time $t$

2.1 The convolution $(f \otimes g)(t)$ looks at all possible ways to split the interval $[0, t]$ into two parts: $s$ and $t-s$. 2.2 For each split point $s$, it calculates the sum of the effects: $f(s)$ for the first part and $g(t-s)$ for the second part. 2.3 The result is the minimum sum obtained overa ll possible split points $s$.

The dioid has the follow our properties as defined in the previous section, thus we have:

• $\land$ and $*$ are associative.
• $\land$ is commutative, although $*$ is not necessarily commutative.
• $\land$'s neutral element is a function that returns $\infty$ for all inputs, representing the maximum element.
• $*$'s neutral element is the delta function $\delta$, which acts like an identity element in convolution:

$$ (f * \delta)(t) = f(t) $$

• $*$ distributes over $\land$.
• The minimum operator $\land$ is idempotent.

Theorem 4: The sets $F^+$ (non-negative functions) and $F^\uparrow$ (non-decreasing functions) are also complete dioids under the same operations.

This theorem extends the framework to specific subsets of functions, confirming their suitability for modeling realistic network behaviors in real-time systems.

We follow a similar reasoning as the previous theorem to achieve these results.

Model (Target Difference)

Here we are exposed to the actual model as the defined in the paper. For our cases, this model might be modified with different definitions depending on our target implementation.

Def. (Cumulative Function): A function $f: \mathbb{R}^+ \to \mathbb{R}^+$ that is non-decreasing, starts at 0, and is left-continuous.

This definition represents the total amount of some quantity accumulated over time. Left continuity means that at any point in time, the function value is the limit of the function values just before that time.

Def. (Server): A server $S \subseteq C \times C$ that ensures for every arrival function $A \in C$, there exists a departure function $D \in C$ such that $D \leq A$.

This definition represents a network component that processes incoming data and produces outgoing data. The arrival function $A$ is a cumulative function representing the total data that has arrived at the server up to a given time. The departure function $D$ is a cumulative function representing the total data that has been processed and departed from the server up to any given time. $D \leq A$ ensures that the amount of data that has departed by any time $t$ is at most the amount of data that has arrived by that time, capturing the idea that a server can only process that it has received.

Def. (Arrival Curve): A function $\alpha \in F^\uparrow$ is an arrival curve for $A$ if $A \leq A^*\alpha$.

This definition represented a bound on the arrival process, describing the maximum amount of data that can arrive over any interval of time. Our condition $A \leq A^* \alpha$ ensures that the actual arrival function $A$ is bounded by the arrival curve, meaning that for any interval of time, the total data that arrives does not exceed the amount specified by the arrival curve.

Def. (Minimal Service): A server $S$ offers a minimal service curve $\beta \in F^+$ if for every $(A,D) \in S, A^*\beta \leq D$.

Our service curve $\beta$ described the guaranteed processing capability of a server. The condition $A * B \leq D$ ensures that the processed (departed) data $D$ is at least the convolution of the arrival data $A$ and the service curve $\beta$. This means that the server guarantees to process at least as much data as specified by the service curve over any interval of time.

Properties (Target Difference) more in Static Priority

This section is the most distinct from our project, as the properties they target are specific. But we can still analyze them as follows.

• The delay experienced by the flow from arrival $A$ to departure $D$ is denoted $d(A, D)$.
• Different server policies such as FIFO and they provide a theorem bounding the delay for each packet in a FIFO server. We will not go into detail because it is out of scope.