Purpose. These notes are my own write-up of the lecture material from TU/e’s MSc course 2IMN25 — Quantitative Evaluation of Cyber-Physical Systems: Quantitative Formal Modeling and Worst-Case Performance Analysis and Quantitative Model Checking. I adapted the technical content into a blog-friendly format while preserving the formal detail, examples, and connections to my broader research work.
1. Introduction
Petri-nets, synchronous dataflow (SDF) models, and Markov chains are three important mathematical tools for reasoning about concurrent systems. Each provides a different viewpoint:
- Petri-nets emphasize structure: places (buffers), transitions (actors), and tokens (resources).
- SDFs emphasize scheduling and performance: periodicity, throughput, and latency in data-driven systems.
- Markov chains emphasize stochastic behaviour: random transitions and probabilistic timing.
This post integrates these perspectives. We begin with the formal construction of production/consumption systems as Petri-nets, then derive deterministic performance bounds using SDF theory, and finally extend the framework to stochastic execution traces via Markov chains.
2. Production and Consumption Systems (Petri-nets)
A Petri-net can be formalised as a production/consumption system (PCS). This is given by the tuple:
$ \langle A, B, P, C, \pi, \varsigma, \iota, \tau \rangle $
where:
- $A$: set of actors (transitions).
- $B$: set of buffers (places).
- $P$: set of production edges.
- $C$: set of consumption edges.
- $\pi: P \to (A \times B)$: production map, where $\pi(p)=(a,b)$ means actor $a$ produces into buffer $b$.
- $\varsigma: C \to (B \times A)$: consumption map, where $\varsigma(c)=(b,a)$ means actor $a$ consumes from buffer $b$.
- $\iota: B \to \mathbb{N}$: initial token assignment.
- $\tau: A \to \mathbb{R}$: execution time of each actor.
2.1 Executions as Partially Ordered Sets
An execution of a PCS is a partially ordered set (prefix order) $ \langle U, \le \rangle $, where $U$ is the set of execution events. The order satisfies:
- Reflexivity: $\forall u\in U: u \le u$.
- Transitivity: $\forall u,v,w: (u\le v \wedge v\le w) \Rightarrow u\le w$.
- Anti-symmetry: $\forall u,v: (u\le v \wedge v\le u) \Rightarrow u=v$.
- Downward totality: $\forall u,v,w: (u\le w \wedge v\le w) \Rightarrow (u\le v \vee v\le u)$.
2.2 State Interpretation
-
Tokens in buffer $b$ after execution $u$:
$\sigma_b(u) \in \mathbb{N}$. -
Aggregate state:
$\sigma: U \to (B \to \mathbb{N}), \quad \sigma(u)(b) = \sigma_b(u)$. -
Firing counts per edge $x \in P \cup C$:
$\sigma_x: U \to \mathbb{N}$.
Monotonicity holds: if $u \le v$, then $\sigma_x(u) \le \sigma_x(v)$.
2.3 Multisets and Ordering
A multiset is a function $f: A \to \mathbb{N}$. Two multisets are ordered pointwise:
$f \le g \iff \forall a \in A: f(a) \le g(a)$.
2.4 Petri-net Execution Rules
Petri-net interpretations must satisfy:
-
Consume on all inputs:
$\forall c,c’ \in C,\ \varsigma_A(c)=\varsigma_A(c’) \Rightarrow \sigma(c)=\sigma(c’)$. -
Produce on all outputs:
$\forall p,p’ \in P,\ \pi_A(p)=\pi_A(p’) \Rightarrow \sigma(p)=\sigma(p’)$. -
Conservation per actor:
$\forall p,c:\ \pi_A(p)=\varsigma_A(c) \Rightarrow \sigma(p) \le \sigma(c)$. -
No consumption from empty buffers:
$\forall b,u:\ \iota(b) + \sum_{b=\pi_B(p)} \sigma(p) - \sum_{b=\varsigma_B(c)} \sigma(c) \ge 0$.
3. Cycles and Token Invariance
Cycles in Petri-nets are closed paths where tokens circulate. For a cycle $X$:
-
Actor set:
$A_X = \bigcup_{p\in X \cap P} \pi_A(p) = \bigcup_{c \in X \cap C} \varsigma_A(c)$. -
Buffer set:
$B_X = \bigcup_{p\in X \cap P} \pi_B(p) = \bigcup_{c \in X \cap C} \varsigma_B(c)$.
Token count function:
$f(b,u) = \iota(b) + \sum_{b=\pi_B(p)} \sigma(p) - \sum_{b=\varsigma_B(c)} \sigma(c)$.
Invariant: The total number of tokens circulating in a cycle remains constant.
4. Time and Scheduling
4.1 Elapsed Time
Elapsed time function:
$\sigma_t: U \to \mathbb{R}, \quad u \le v \Rightarrow \sigma_t(u) \le \sigma_t(v)$.
4.2 WCET Constraint
If actor $a$ has WCET $\tau(a)$, then:
$\sigma_t(u’) - \sigma_t(u) \ge \tau(a) \ \Rightarrow\ \sigma_p(u’) \ge \sigma_p(u)$.
4.3 Scheduling Policies
- Eager scheduling: fire when enabled.
- Periodic scheduling: each actor $a$ has period $T_a$ and offset $t_a$:
$ \sigma_c(u) = \max{ \lfloor (\sigma_t(u) - t_a)/T_a \rfloor + 1,\ 0 }. $ —
5. Throughput and Maximum Cycle Mean
5.1 Throughput
Throughput of an output edge $p$:
$\lim_{u\to\infty} \frac{\sigma_p(u)}{\sigma_t(u)}$.
5.2 Maximum Cycle Mean (MCM)
$\mathrm{MCM} = \max_{\text{cycles } X} \frac{\sum_{a\in A_X} \tau(a)}{\sum_{b\in B_X} \iota(b)}$.
Thus,
$\text{Throughput} \ge \min{ T_{\text{input}},\ 1/\mathrm{MCM} }$.
5.3 Worked example: throughput from cycle means (SDF / eager schedule)
Problem.
Assume each actor’s label denotes its worst-case response time (WCRT). For this question only, assume the input source can always supply enough tokens to keep the graph saturated and that actors use eager scheduling. For the dataflow graph in Figure 5, what long-run throughput can you guarantee?

Solution.
-
Principle: Throughput $\ge$ min over all cycles (tokens / sum of times).
- Cycles:
- Cycle 1: token count $l$, time sum $C+E$, bound $l/(C+E)$.
- Cycle 2: token count $m+k$, time sum $C+B+D$, bound $(m+k)/(C+B+D)$.
- Cycle 3: token count $n$, time sum $B$, bound $n/B$.
- Minimum bound:
$\text{Throughput} \ge \min{ l/(C+E),\ (m+k)/(C+B+D),\ n/B }$.
5.4 Tightness of Throughput Bounds
So far, we have shown lower bounds on throughput using eager firing and the maximum cycle mean. The natural question is: are these bounds tight?
Two theorems answer this:
-
Lower bound with input constraint.
If the system uses eager scheduling, WCET timing, and the input source guarantees at least $T_{\text{input}}$, then
$\lim_{n \to \infty} \frac{n}{p_{\text{output}}(n)} \ge \min{ 1/\mathrm{MCM},\ T_{\text{input}} }$. -
Upper bound from BCRT.
For any scheduling policy and any graph structure,
$\lim_{n \to \infty} \frac{n}{p_{\text{output}}(n)} \le 1/\mathrm{MCM}$.
Together, these results show that the throughput bound is both achievable and fundamental: eager scheduling reaches the lower bound, and no policy can exceed the upper bound.
6. Response Times
6.1 Worst-case Response Time (WCRT)
$x(n) = \sup{\sigma_t(u) \mid \sigma_x(u) \le n}$.
$p(n) \le \max{ q(n-\iota(b)) } + \tau(a)$.
6.2 Best-case Response Time (BCRT)
$x(n) = \inf{\sigma_t(u) \mid \sigma_x(u) \le n}$.
6.3 Periodic Scheduling Construction
Periodic scheduling provides a constructive way to reach the throughput guaranteed by the maximum cycle mean.
Feasibility condition.
Suppose all actors share a global period $T$. If actor $a$ feeds actor $a’$ through buffer $b$ with $\iota(b)$ initial tokens, then:
$t_{a’} \ge t_a + \tau(a) - \iota(b)T$.
Construction algorithm.
- Compute $\mathrm{MCM}$ of the graph.
- Choose any $T \ge \mathrm{MCM}$.
- Propagate offsets forward:
$t_{a’} = \max{ 0,\ t_a + \tau(a) - \iota(b)T }$.
Optimised construction.
Offsets can also be computed backward:
$t_a \le t_{a’} - \tau(a) + \iota(b)T$.
Setting $t_{\text{out}}=0$ and shifting all offsets to be nonnegative yields a feasible schedule with smaller latency.
7. Latency Bounds
With periodic scheduling:
$\mathrm{Latency} \le t_{\text{out}} + (B-1)T$.
With boot-up improvements:
$\mathrm{Latency}^\ast \le t_{\text{out}} + (B-1)T - t_a$.
8. Buffering and Backpressure
Control buffer requirement:
$B \ge \lceil (t_{a’} - t_a)/T \rceil$.
9. Markov Chains and Stochastic Execution
9.1 Definition
State set $S={s_1,\dots,s_n}$.
Transition probability matrix $P$:
$P_{ij} = \Pr(X_{t+1}=s_j \mid X_t=s_i), \quad \sum_{j} P_{ij}=1$.
9.2 Connection to Petri-nets
- Marking = state.
- Actor firing = transition.
- Firing probability = matrix entry.
Example:
$P = \begin{bmatrix}
0.1 & 0.9 & 0.0
0.0 & 0.3 & 0.7
0.5 & 0.0 & 0.5
\end{bmatrix}$.
9.3 Stationary Distribution
$\pi P = \pi, \quad \sum_i \pi_i = 1$.
10. Hybrid Deterministic–Stochastic View
- Deterministic guarantees: throughput, latency bounds (SDF).
- Stochastic extensions: expectations and variance (Markov chains).
11. Conclusion
Petri-nets, SDFs, and Markov chains provide complementary tools:
- Petri-nets: structure and correctness.
- SDFs: scheduling, throughput, latency.
- Markov chains: stochastic behaviour.
Combined, they form a rigorous framework balancing worst-case safety with probabilistic efficiency.
References
- TU/e MSc Course 2IMN25 — Quantitative Evaluation of Cyber-Physical Systems: Quantitative Formal Modeling and Worst-Case Performance Analysis and Quantitative Model Checking.
- Course notes: QEES — Quantitative Evaluation of Embedded Systems (lecture notes, Eindhoven University of Technology).
- Murata, T. Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE, 77(4):541–580, 1989.
- Lee, E. A. and Messerschmitt, D. G. Static Scheduling of Synchronous Data Flow Programs for Digital Signal Processing. IEEE Transactions on Computers, C-36(1):24–35, 1987.
- Kemeny, J. G. and Snell, J. L. Finite Markov Chains. Springer, 1976.
-
Previous
Automated Reasoning — A Working Guide to SAT, SMT, BDDs, and Model Checking -
Next
Formal Verification of an ASML EUV Wafer Stepper