{'fraction_non_alphanumeric': 0.06555361852398194, 'fraction_numerical': 0.015801707567833355, 'mean_word_length': 4.068879574034213, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 4, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 18, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Formal Analysis of the Sampling Behaviour of Stochastic Event-Triggered Control

Analyzing Event-Triggered Control's (ETC) sampling behaviour is of paramount importance, as it enables formal assessment of its sampling performance and prediction of its sampling patterns. In this work, we formally analyze the sampling behaviour of stochastic linear periodic ETC (PETC) systems by computing bounds on associated metrics. Specifically, we consider functions over sequences of state measurements and intersampling times that can be expressed as average, multiplicative or cumulative rewards, and introduce their expectations as metrics on PETC's sampling behaviour. We compute bounds on these expectations, by constructing appropriate Interval Markov Chains equipped with suitable reward structures, that abstract stochastic PETC's sampling behaviour. Our results are illustrated on a numerical example, for which we compute bounds on the expected average intersampling time and on the probability of triggering with the maximum possible intersampling time in a finite horizon.


Introduction
In the past two decades, Event-Triggered Control (ETC), followed by its sibling Self-Triggered Control, has constituted the primary research focus of the control systems community towards reducing resource consumption in Networked Control Systems [1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17]. ETC is a sampling paradigm, where communication between the sensors and the controller takes place only when a state-dependent triggering condition is satisfied. Even though ETC's event-based sampling typically reduces the amount of communications (compared to conventional periodic sampling), it also generates an erratic and generally a-priori unknown sampling behaviour. Understanding and predicting ETC's sampling behaviour is of paramount importance as it enables: a) forecasting an ETC design's sampling performance (e.g., how frequently or erratically an ETC system is expected to sample), and b) scheduling data traffic 1 in networks shared by multiple ETC loops, to avoid packet collisions.
Even though analyzing ETC's sampling behaviour is fundamental, research around it is scarce [10][11][12][13][14][15][16][17]. One branch of it composes of analytic approaches [10][11][12]. In particular, [10] studies deadbeat stochastic linear PETC (periodic ETC, e.g. [3]; a practical variant of ETC) systems. Owing to deadbeat control, studying the sampling behaviour of the system simplifies to analyzing a Markov chain, which can be used to compute quantitative metrics over the sampling performance. Nevertheless, assuming deadbeat control is admittedly restrictive. Furthermore, [11] and [12] investigate asymptotic properties of the intersampling times of 2-D linear ETC systems with quadratic triggering conditions. Despite the interesting insights, these works also suffer from certain limitations: a) they consider only planar systems, b) they are dependent on the type of triggering condition considered, and most importantly c) they do not provide quantitative information on all possible sampling patterns that may be exhibited by an ETC system; as such, they may not be employed for e.g. computing metrics on ETC's sampling performance or predicting its sampling patterns.
The other branch of research studying ETC's sampling behaviour is abstraction-based approaches [13][14][15][16][17], among which the present work is placed. These construct finite-state systems, abstracting a given ETC system's sampling: the set of their traces contains all possible sequences of intersampling times that may be exhibited by the ETC system. Contrary to the analytic approaches, they do not place restrictive assumptions on the type of controller, and they depend neither on the system dimensions (modulo computational complexity) nor on the triggering condition (except that minor steps in the abstraction's construction might vary). Meanwhile, in exchange for high computational complexity, they provide quantitative information on ETC's diverse sampling patterns, allowing for computing performance metrics and predicting sampling patterns. For example, [14][15][16][17] construct abstractions in the context of ETC traffic scheduling, while [13] utilizes them to compute the minimum average intersampling time.
Thus far, in [13][14][15][16][17] only non-stochastic systems have been considered. Specifically, [13][14][15] consider linear ETC and PETC systems, whereas [16] and [17] address nonlinear systems with bounded disturbances. In this work, we consider stochastic systems, for the first time. Among others, for verification purposes, the probabilistic framework of stochastic systems is naturally less strict than the deterministic one, as it takes into account the disturbances' probability distribution, instead of being bound by worst case scenarios.
In particular, we consider stochastic narrow-sense linear PETC systems. We define their sampling behaviour as the set Y of all possible sequences of state-measurements and intersampling times along with its associated probability measure. Studying ETC's sampling behaviour is formalized by computing expectations of functions defined over these sequences g : Y → R. Here, we focus on functions g described as cumulative, average or multiplicative rewards, i.e. g with ∈ {cum, avg, mul}. This class of functions is rather standard in the context of quantitative analysis of stochastic systems, and it extends to including specifications of PCTL (Probabilistic Computation Tree Logic, see [18]). Besides, it is able to describe various metrics on ETC's sampling performance, as demonstrated through examples. In fact, as shown in one example, including state-measurements in the sampling behaviour's definition allows for incorporating control-performance metrics as well. The problem statement of this work is to obtain bounds on expectations of functions g .
To address the problem, we construct IMCs (interval Markov chains; Markov chains with interval transition probabilities) that capture PETC's sampling behaviour. Then, we equip the IMCs with appropriate state-dependent rewards and prove that the {cum, avg, mul} reward over the paths of the IMC indeed bounds the expectation of g (Theorem 4.1). The IMC rewards can easily be computed via well-known value-iteration algorithms (see, e.g., [19]).
The main challenge in constructing the IMC is computing the IMC's probability intervals. For that, we study the joint probabilities of transitioning from one region of the state-space to another one with the intersampling time taking a specific value. Computation of these probabilities is more complicated than the traditional transition probabilities that appear in the literature of IMCabstractions (e.g., [20][21][22][23]), due to the presence of intersampling time as an event. To cope with that, we employ a series of convex relaxations and the fact that the system's state is a Gaussian process. That way, we reformulate computing these probabilities as optimization problems of log-concave objective functions and hyperrectangle constraint sets, which are easy to solve. Finally, our results are demonstrated through a numerical example, where we compute bounds on the expected average intersampling time and on the probability of triggering with the maximum possible intersampling time in a finite horizon.
In summary this work's main contributions are: • It is the first one to abstract the sampling behaviour of stochastic ETC.
• It computes bounds on performance metrics over stochastic PETC's sampling behaviour, allowing for its formal assessment and prediction of its patterns.
A preliminary version of the present work was presented in [24]. In [24], only cumulative rewards are addressed and the derived upper and lower bounds on transition probabilities are different (here, they are tighter). Furthermore, the proof of Lemma 5.2, which shows log-concavity of our optimization problems' objective functions, appears here for the first time. Finally, the proof of

Notation
R stands for the set of real numbers, N for the natural numbers including 0, and N + without 0. Given ]. I n is the n-dimensional identity matrix. Given a set S in some space X, we denote: its indicator function by 1 S (·), its Borel σ-algebra by B(S), its complement by S = X \ S, and the k-times Cartesian product S = S × . . . × S by S k . Given x ∈ R n , denote by {x} k : both the k-times Cartesian product {x} × . . . × {x} and the kn-dimensional vector x . . . x . Given sets Q 1 , Q 2 and Q = Q 1 × Q 2 , for any q = (q 1 , q 2 ) ∈ Q denote proj Q1 (q) = q 1 and proj Q2 (q) = q 2 . Given two sets Q 1 , Q 2 in some space, denote Given a random variable x and an associated probability measure P, we denote its expectation w.r.t. P by E P [x] (when P is clear from the context, it might be omitted). We use the term 'path' or 'sequence' interchangeably. Given a finite path ω = q 0 , q 1 . . . , q N , denote ω(i) = q i and ω(end) = ω(N ) = q N . Given a function g(ω) of paths ω, we denote E q0 [g(ω)] ≡ E[g(ω)|ω(0) = q 0 ]. Finally, N (µ, Σ) denotes the Gaussian distribution with mean µ and covariance matrix Σ.

Rewards over Paths
Consider a set Q and a set of paths Y of length N + 1, such that: ω(i) ∈ Q, for all ω ∈ Y and 0 ≤ i ≤ N . Assume a probability measure P over B(Y) (for how to define B(Y) in our context, see Section 3.2). Define a reward function R : Q → [0, R max ]. We define the following expectations: These expectations can describe a wide range of quantitative/qualitative properties of paths in Y, and they have been employed for verification in numerous settings, such as (interval) Markov chains (e.g. [20][21][22][23]), stochastic hybrid systems (e.g., [25]), etc. Later, we showcase their descriptive power within our framework (see Section 3.2).

Interval Markov Chains (IMCs)
Interval Markov Chains are Markov models with interval transition probabilities, and they are defined as: ). An IMC is a tuple S imc = {Q,P ,P }, where: Q is a finite set of states, andP ,P : Q × Q → [0, 1] are functions, withP (q, q ) andP (q, q ) representing lower and upper bounds on the probability of transitioning from state q to q , respectively.
For all q ∈ Q, we have thatP (q, q ) ≤P (q, q ) and IMC is a sequence of states ω = q 0 , q 1 , q 2 , . . . , with q i ∈ Q. Denote the set of the IMC's finite paths by P aths f in (S imc ). Given a state q ∈ Q, a transition probability distribution p q : Q → [0, 1] is called feasible ifP (q, q ) ≤ p q (q ) ≤P (q, q ) for all q ∈ Q. Given q ∈ Q, its set of feasible distributions is denoted by Γ q . We denote by Γ Q = {p q : p q ∈ Γ q , q ∈ Q} the set of all feasible distributions for all states.
Definition 2.2 (Adversary). Given an IMC S imc , an adversary is a function π : P aths f in (S imc ) → Γ Q , such that π(ω) ∈ Γ ω(end) , i.e. given a finite path it returns a feasible distribution w.r.t. the path's last element.
The set of all adversaries is denoted by Π. Given a π ∈ Π and ω(0) = q 0 , an IMC path evolves as follows: at any time-step i > 0 π chooses a distribution p ∈ Γ ω(i−1) from which ω(i) is sampled.
3 The Sampling Behaviour of Stochastic PETC: Framework and Problem Statement

Linear Stochastic PETC Systems
Consider a state-feedback stochastic linear control system: where: A, B, K, B w are matrices of appropriate dimensions, ζ(t) ∈ R n ζ is the state, and W (t) is an n w -dimensional Wiener process on a complete probability space (Ω, F, {F t } t≥0 , P). Ω denotes the sample space, F the σ-algebra generated by W , {F t } t≥0 the natural filtration and P the probability measure. We denote the solution of the above stochastic differential equation with initial condition ζ 0 by ζ(t; ζ 0 ). In PETC, the control input is held constant between consecutive sampling times (or event times) t i , t i+1 and is only updated on such times: Sampling times are determined by the triggering condition: where t 0 = 0, h > 0 is a checking period, k ∈ N + , φ is called triggering function and t i+1 − t i is called intersampling time. PETC works as follows during an intersampling interval [t i , t i+1 ): at time t i the triggering function φ(ζ(t i ), ζ(t i )) is negative; the sensors check periodically, with period h, if the triggering function is positive; if it is found positive, or if kh time has elapsed since t i , a new event t i+1 is triggered, the latest state-measurement is sent to the controller which updates the control action, and the whole process is repeated again. The forced upper-bound kh on intersampling times prevents the system from operating open-loop indefinitely. We call the combination (1)-(2) (stochastic) PETC system. Intersampling time is a random variable that depends on the previously measured state and we denote it as follows: τ (x) = min kh, min kh : k ∈ N, φ ζ(kh; x), x > 0 where x ∈ R n is the previously measured state. Note that, because the system is time-homogeneous, reasoning w.
Assumption 1. We assume the following: 2. The checking period h = 1.
Item 1 guarantees that ζ(t) is a non-degenerate Gaussian random variable (see [22]). Item 2 is for ease of presentation and without loss of generality. Regarding item 3, φ is the well-studied Lebesgue-sampling triggering function [1] with an ∞-norm instead of a 2-norm. We restrict to this case for clarity, but our results are extendable to more general functions.

Sampling Behaviour and Associated Metrics
A stochastic PETC system may exhibit different sequences of state-measurements and intersampling times (ζ 0 , t 0 ), (ζ(t 1 ), t 1 − t 0 ), (ζ(t 2 ), t 2 − t 1 ), . . . , where t i are sampling times. We call sampling behaviour, the set of all possible such sequences: Definition 3.1 (Sampling Behaviour). We call N -sampling behaviour of stochastic PETC system (1)-(2) the set: where N ∈ N. When N is clear from the context, it is omitted.
We denote Q := R n ζ ×N [0,k] . Given an initial condition y 0 = (x 0 , s 0 ) ∈ Q, the set Y N is associated to a probability measure P y0 Y N (conditioned on y 0 ) which is inductively defined over B(Y N ) as follows 2 : This measure is well-defined, even when the horizon N = +∞, according to the Ionescu-Tulcea theorem [27].
Remark 2. As noted in Section 3.1, typically it is assumed that the first sampling time t 0 = 0, which implies that the first intersampling time s 0 = t 0 − 0 = 0 and the initial condition is y 0 = (x 0 , 0).

Remark 3.
Under item 3 of Assumption 1, and in every Zeno-free ETC scheme, P(τ (x) = 0) = 0 for any x ∈ R n ζ , because the triggering function is strictly negative for k = 0. Thus, for any i ≥ 1 and ω ∈ Y N : Studying PETC's sampling behaviour may be formalized by defining functions g : Y N → R and computing their expectations Here, we focus on functions that can be described as cumulative g cum,N , average g avg,N or multiplicative g mul,N rewards (see Section 2.2). By appropriately choosing the reward R, these classes of functions can describe many interesting properties of PETC's sampling behaviour: is the expected average intersampling time: the larger it is, the less frequently the system is expected to sample, saving more bandwidth and energy.
• Example 2: Consider R(x, s) = min(α 1 |x|+ε + βs, R max ), with α, β, ε > 0, penalizing paths that overshoot far from the origin or exhibit a high sampling frequency. A bigger E P y 0 Y N [g cum,N (ω)] implies better performance in terms of stabilization speed and sampling frequency. Observe how incorporating state-measurements x in our definition of sampling behaviour, allows to include control-performance related metrics, apart from sampling-performance metrics.
• Example 3: Consider the reward: Then, we have that: is the probability that there is no intersampling time s = k in the next N events. The smaller it is, the more probable it is that the system samples, at least once in the first N triggers, with intersampling time s = k, implying that a bigger maximum intersampling time could be used, allowing the system to sample even less frequently and saving more bandwidth.
Observe that, if the initial condition (x 0 , s 0 ) is only known to obey some distribution p 0 : Q → [0, 1], the expected reward can be described as: Thus, reasoning about individual initial conditions y 0 is sufficient and immediately extends to the general case of random initial conditions. Overall, defining PETC's sampling behaviour Y N , associating it to its induced probability measure P y0 Y N given in (4)-(5), and studying expectations E P y 0 ] constitutes a formal framework for the study of PETC's sampling behaviour.

Problem Statement
Unfortunately, exact computation of E P y 0 Y N [g ,N (ω)] is generally infeasible. Among others, how to obtain the measure P y0 Y N over the uncountable set of paths Y N and then integrate over it? Hence, we aim at computing bounds over such expectations: Problem Statement. Consider the PETC system (1)-(2) and its sampling behaviour Y N , for some N ∈ N. Let Assumption 1 hold. Consider a reward function R : Q → [0, R max ]. For all initial conditions y 0 ∈ X × N [0,k] , where X ⊂ R n ζ is compact, compute (non-trivial) lower and upper bounds on In the rest of this article, we address the problem by constructing an IMC that abstracts the sampling behaviour Y N along with P y0 Y N , equipping it with suitable reward functions R, R, and computing (sup π∈Π and) inf π∈Π E q0 π [g ,N (ω)], with ∈ {cum, avg, mul}, to obtain the bounds we are looking for. Specifically, in the next section we show how to construct such an IMC, by partitioning the state space and providing conditions (eq. (7)- (8)) that have to be satisfied by the IMC's transition probability intervals. We prove in Theorem 4.1 that this IMC equipped with suitable rewards gives rise to bounds on E P y 0 Y N [g ,N (ω)]. Later, in Section 5, we show how to computeP andP such that they satisfy (7)-(8), by solving optimization problems with log-concave objective functions. Finally, the desired bounds (sup π∈Π and) inf π∈Π E q0 π [g ,N (ω)] are obtained via well-known value iteration algorithms, as demonstrated through a numerical example in Section 6. A flowchart of the steps followed to compute the desired bounds is shown in Figure 1.
Remark 4. By assuming that y 0 = (x 0 , s 0 ) ∈ X × N [0,k] , we essentially assume that the initial state of the system x 0 ∈ X. Compactness of X is vital, to partition it into a finite number of subsets R i and end up with a finite-state IMC. Nonetheless, this is not an unrealistic assumption, as in practice the initial conditions of the system are usually known to be bounded in some set. Furthermore, s 0 ∈ N [0,k] for generality, but, as mentioned in Remark 2, typically in ETC s 0 = 0.
Remark 5. We constrain ourselves to {cum, avg, mul} rewards for clarity, but our approach extends to a more general framework. As commented in Section 4.2, our IMCs can be employed for computing bounds on bounded-until probabilities: where S, G ⊆ Q. Bounded-until constitutes the backbone of PCTL [20], as all PCTL formulas can be written with bounded-until operations. In short, our approach directly extends to PCTL. Moreover, by extending our proofs according to [21] and [23], we could incorporate probabilistic ω−regular or LTL (Linear Temporal Logic) properties.

Constructing the IMC
Typically, to abstract a stochastic behaviour Y and its probability measure P Y through an IMC: i) the state space is partitioned into a finite number of regions, each of which corresponds to an IMC-state, ii) if the state space is unbounded, then one of these regions is unbounded, and its IMC-state is made absorbing 3 , and iii) the bounds on transition probabilitiesP (q, q ),P (q, q ) are derived such In this work, we adopt the above methodology. Observe that the state space from which the sampling behaviour emerges is the set According to the aforementioned methodology, the states of the IMC would be of the form (q, s) ∈ Q R ∪ {X} × N [0,k] . Nonetheless, for compactness of the IMC, we group all states (X, s) (for s ∈ N [0,k] ) that correspond to X into a single absorbing state q abs : From now on, we abusively use (R i , s) (resp. q abs ) to denote both the corresponding IMC-state and the set R i × {s} (resp. X × N [0,k] ). Finally, the set of the IMC-states is: Regarding the transition probability boundsP (q, q ) andP (q, q ), since we need to bound for all x ∈ q, by employing (5), we have that for all (R, k), (S, s) ∈ Q R ×N [0,k] : and for all q ∈ Q imc :P The computation ofP andP such that they satisfy (7)- (8) is addressed in Section 5 and it involves bounding the solutions to the optimization problems of (7). The summation in the last two inequalities of (7) results from the fact that q abs is a grouping of all states (X, s) with s ∈ N [0,k] , while (8) indicates that q abs is indeed absorbing. In view of Remark 3, since we know that P(τ (x) = 0) = 0, then for any q ∈ Q imc and S ∈ Q R , it suffices to writeP (q, (S, 0)) =P (q, (S, 0)) = 0; that is, states (S, 0) only have outgoing transitions and no incoming ones. Finally, we define the IMC that abstracts the sampling behaviour as follows: where Q imc is given by (6) andP ,P are given by (7)- (8).
To demonstrate how the constructed IMC abstracts the PETC system's sampling behaviour, let us relate paths ω ∈ Y N to pathsω ∈ P aths f in (S imc ). First, consider a path ω such that ω(i) ∈ q abs for all i ≤ N . Then, this path is related to a pathω ∈ P aths f in (S imc ) of the same length, for which ω(i) ∈ω(i) for all i ≤ N . Next, consider a path such that ω(i) ∈ q abs for some i ≤ N and ω(j) ∈ q abs for all j < i. Then, ω is related toω ∈ P aths f in (S imc ) of the same length, for which ω(j) ∈ω(j) for all j ≤ i andω(k) = q abs for all k ≥ i. This latter relation indicates that all paths in Y N that enter X (even those that eventually return to X) are mapped to IMC-paths that enter q abs at the same time and stay there.

Bounds on Sampling-Behaviour Rewards via IMCs
The IMC described above, if equipped with suitable rewards R, R, can be employed for the computation of lower and upper bounds on E P y 0 Y N [g ,N (ω)]: Theorem 4.1. Consider the IMC S imc given by (9). Define reward functions R, R : Q imc → [0, R max ] such that: [1,k] R(x, s), if q = q abs (10) and the associated rewards over pathsω ∈ P aths f in (S imc ) denoted by g ,N , g ,N , where ∈ {cum, avg, mul}. Then, for any initial condition y 0 = (x 0 , s 0 ) ∈ X × N [0,k] and N ∈ N: where q 0 is such that y 0 ∈ q 0 .
Proof Sketch. The above expectations are written as value functions defined via value iteration (see Lemma 9.1), and mathematical induction over the iteration is employed. For the full proof, see Appendix 9.1.
Hence, to compute bounds on expectations E P y 0 Y N [g ,N (ω)], we equip the IMC (9) with the reward functions R, R from (10) and compute the expectations inf π∈Π E q0 π [g ,N (ω)] and sup π∈Π E q0 π [g ,N (ω)]. As mentioned in Section 2.3, these expectations can be computed via value-iteration algorithms (e.g. see [19]), with polynomial complexity in the number of IMC-states. In fact, the value iteration used for {cum, mul} rewards is given here by equations (26) and (37) respectively in the Appendix (the avg reward is the same as cum with γ = 1, and in the last step we just divide by N + 1). Moreover, since bounded-until probabilities on IMCs, and thus PCTL properties, may be computed through a similar value iteration [20], our proofs can be adapted to show that we can bound bounded-until probabilities defined over Y N by using the constructed IMC.
Finally, Theorem 4.1 indicates that the same IMC can be used to derive bounds for any chosen {cum, avg, mul} reward, for any horizon N , and any initial condition y 0 ∈ X × N [0,k] . It is also worth noting that a proof like that of Theorem 4.1 was missing from the literature on IMCabstractions [20][21][22][23], where it was (correctly) taken for granted that the quantitative metric (e.g., a reward) evaluated over the IMC bounds the metric evaluated over the original stochastic behaviour, due to the way that the transition probabilities are constructed.
Remark 6. For any q ∈ Q imc , the rewards R and R serve as conservative estimates of the real reward obtained if the system operates in q. In fact, specifically for q abs , R and R are global lower and upper bounds, respectively, on the actual reward R(x, s) (except for the case s = 0, which happens with zero probability, except for initial conditions). Due to this, for states (R, s) ∈ Q imc with R being "near" X (i.e., near the boundary of X), which tend to obtain larger transition probabilities to q abs , the lower and upper bounds inf π∈Π E q0 π [g ,N (ω)] and sup π∈Π E q0 π [g ,N (ω)] are more conservative, compared to when R is further inside X. This is showcased by Figure 4. For that reason, in practice, to construct the IMC, it is better to partition a superset Y ⊇ X into regions R i , so that the regions that comprise X are further inside Y , and the corresponding bounds are not that conservative.

Remark 7.
Our results extend to infinite horizons (i.e. N = +∞), when the rewards are well-defined, as it has already been proven in [24, Theorem IV.1]; in fact, the proof for N = +∞ is simpler, as it suffices to consider time-invariant adversaries.
The only thing that remains is to describe how to compute the transition probability bounds given by (7). This is carried out in the coming section.

Computing the Transition Probability Bounds
Here, we compute lower bounds on the minima and upper bounds on the maxima in (7), thus completing the IMC's construction. Through a series of convex relaxations, and employing Proposition 5.1 and Lemma 5.2, the min/max expressions in (7) are formulated as optimization problems of log-concave functions (in fact, Gaussian integrals) over hyperrectangles, which are straightforward to solve. To facilitate this analysis, we introduce the following assumption: The set X and all sets R i ∈ Q R are hyperrectangles.
This assumption is without loss of generality, as in the case where X is not a hyperrectangle, our approach could be applied by under/overapproximating X by a hyperrectangle Y ⊇ X and partitioning Y into a finite set of hyperrectangles R i .
For the rest of the document, for any s ∈ N [1,N ] , we denote ζ s,x = ζ(s; x) andζ s,x = [ζ 1,x ζ 2,x . . . ζ s,x ] . The following statements are instrumental in our derivations: Thus, given some set S ⊆ R sn ζ , the following holds: Proof. Application of the expectation and covariance operators to the solution of linear SDE (1) (see [28, pp. 96]).
Lemma 5.2. Consider a function h : R n → [0, 1] with n ∈ N + defined by: where Σ is a covariance matrix, S(x) ⊆ R m with m ∈ N + is linear on x and convex for all x ∈ R n , and f : R n → R m is an affine function. The function h(x) is log-concave on x.
In what follows we transform the probabilities involved in (7) to set-membership ones P(ζ s,x ∈ S(x)), where S(x) is a polytope, but neither necessarily convex nor linear on x. Afterwards, we break them down to simpler ones and employ some convex relaxations, such that the set of integration of the resulting Gaussian integrals is convex and linear on x and Lemma 5.2 is enabled. Finally, we end up with optimization problems of log-concave functions over the hyperrectangle R, and solve them to obtain lower and upper bounds on the expressions in (7).

Transition Probabilities as Set-Membership Probabilities
For now, let us focus on transitions from any state (R, k) ∈ Q imc \q abs to any state (S, s) ∈ Q R ×N [1,k] : (max x∈R or) min x∈R P(ζ(s; x) ∈ S, τ (x) = s) Later, in Section 5.4, we show how transitions to q abs can be treated similarly to the case above. Moreover, remember that for s = 0 the above probability is trivially 0 (see Remark 3). Define the following hyperrectangle: Note that Φ(x) is convex and linear on x: Thus, the following equivalences hold: where, for brevity, in the case where s = 1 we have abusively denoted Φ 0 (x) × Φ(x) = Φ(x). In words, when s = k, the intersampling time is s if and only if the state belongs to Φ(x) at all checking times 1, 2, . . . , s − 1 and at time s it lies outside Φ(x). When s = k, it suffices that the state belongs to Φ(x) at all checking times 1, 2, . . . , k − 1. Thus, for s ∈ N [1,k−1] : and for s = k: In the following we combine (12)-(13) with some convex relaxations, to enable Lemma 5.2 and obtain bounds on (max x∈R and) min x∈R P(ζ(s; x) ∈ S, τ (x) = s) through solving optimization problems with log-concave functions. In particular, observe that µζ s,x is already an affine function of x (see Proposition 5.1), thus satisfying one of the two conditions of Lemma 5.2. Hence, our efforts focus on transforming the integration sets in (12)-(13) such that they become linear on x and convex.

Lower Bounds on Transition Probabilities
Let us start by determining lower bounds on: The special case when s = k, which is given by (13), is simple. Observe that the set Φ k−1 (x) × S is convex (since Φ(x) and S ∈ Q R are hyperrectangles) and linear on x, as it can be written as: The set R is the dashed square on the left, S is the one on the right, and Φ(x) is the one centered at x. For the given x on the figure, Φ(x)∩ S is non-convex. For different x ∈ R the set Φ(x) ∩ S has a different shape; thus, Φ(x) ∩ S is not linear on x.
(b) The set x∈R Φ(x), and consequently S \ x∈R Φ(x), does not depend on x. The set S\ x∈R Φ(x) can be partitioned into a finite number (minimum one, here) of hyperrectangles.
(c) The set S \ x∈R Φ(x) can be partitioned into a finite number (minimum two, here) of hyperrectangles. Thus, when s = k, the objective function P(ζ(s; x) ∈ S, τ (x) = s) of minimization problem (14) is log-concave (due to (13) and Lemma 5.2). The constraint set R is a hyperrectangle. Thus, the minimization problem attains its solution at one of the vertices of R [29, pp. 343, Theorem 32.2]; we simply have to evaluate the objective function for each of the vertices, to find the minimum.
When s = k, the set of integration in (12) is neither convex nor linear on x due to Φ(x) ∩ S (see Figure 2a); thus, we cannot invoke Lemma 5.2 and there is no indication that it is straightforward to compute (14). In this case, we resort to convex relaxations, each of which yield a lower bound on (14) that can be computed easily. These are the following: For examples of S \ x∈R Φ(x) see Figures 2b and 2c. Observe that, since x∈R Φ(x) does not depend on x, the set S \ x∈R Φ(x) does not depend on x; it is a fixed set, in contrast to Φ(x) ∩ S. Moreover, since both S and x∈R Φ(x) are hyperrectangles, then S \ x∈R Φ(x) can always be partitioned into a finite number of hyperrectangles S 1 , . . . , S r , where r ≤ n and r = 0 in the case where S \ x∈R Φ(x) is empty. Thus: The integration sets Φ s−1 (x) × S i are convex and linear on x. Thus, in the last expression of (15) we are dealing with log-concave objective functions, and the r minimization problems attain their minimum at vertices of R. Hence, we easily solve the r minimization problems to obtain a lower bound on (14).
Relaxation 2 Here, we employ the law of total probability to write: which gives the following relationship: The minimization problem in the right-hand side of (16) is similar to the ones discussed before (log-concave objective function and hyperrectangle constraint set), and the minimum can be computed easily. However, the set Φ(x) ∩ S not being linear on x makes the maximization problem hard to solve. By employing that Φ(x) ∩ S ⊆ S ∩ x∈R Φ(x), we relax it by writing: The set S ∩ x∈R Φ(x) is a (possibly empty) hyperrectangle and does not depend on x; thus, is convex and linear on x. Hence, the maximization problem in the righthand side of the above equation is a convex program (log-concave objective function over the convex constraint set R), and can be easily solved via regular convex optimization techniques. By computing the exact minimum in the right-hand side of (16) and an upper bound on the maximum-term as discussed here, we obtain a lower bound on (14). (16), we propose a different relaxation for the maximization problem in the right-hand side of (16). Specifically, by employing Bayes's rule:

Relaxation 3 Continuing from
The term max x∈R P(ζ s,x ∈ S) can be computed exactly easily, as P(ζ s,x ∈ S) is log-concave on x. For the term max x∈R P ζ s,x ∈ Φ s (x)|ζ s,x ∈ S , we make use of the following bound: Proposition 5.3. The following holds: Proof. The proof is the same as in [30,Lemma 2].
Proof. Straightforward application of the well-known formula for conditional normal distributions [31].
Thus, we have that: max Observe that µ ξ (x, v) is affine on the optimization variables (x, v), and Φ s (x) is obviously convex and linear on x. Thus, the objective function of the above maximization problem is log-concave. Finally, since the set of constraints R × S is convex, we deduce that computing the right-hand side of (18) is a convex program. Combining (18) with (17) and (16) yields an easily computable bound on (14).
Remark 8. Gaussian integrals over hyperrectangles are often encountered in fields such as statistics and learning, and many algorithms exist for their numerical computation (e.g., Genz's algorithm [32] or python's scipy.stats.multivariate normal [33]).

Upper Bounds on Transition Probabilities
We proceed to computing upper bounds on: Again, the case where s = k is easy: it corresponds to a convex program, and (19) is computed exactly. For the case where s = k, we employ a relaxation similar to Relaxation 3 described in the previous. In particular, as in (16), we write: The term max x∈R P ζ s,x ∈ Φ s−1 (x) × S is computed easily, through convex optimization. For the other term in the right-hand side of (20), we write as in (17): Given the discussion of the previous section, it is clear that: a) min x∈R P(ζ s,x ∈ S) is computed exactly (by traversing the vertices of R), and b) a lower bound on min x∈R P ζ s,x ∈ Φ s (x)|ζ s,x ∈ S is computed by employing Proposition 5.3 and Corollary 5.4, which yield log-concave minimization over the polytope R × S.

Transitions to q abs
According to the last two inequalities in (7), for transitions to q abs we are interested in: We focus on the maximization, as minimization follows identical steps. By the law of total probability, we have: max Note that, since X is a hyperrectangle, the term min x∈R P(ζ(s; x) ∈ X, τ (x) = s) can be treated exactly as discussed in the previous sections (where X takes the place of S). Regarding P(τ (x) = s), we have the following two cases: s = k In this case: Thus, max x∈R P(τ (x) = s) = max x∈R P(ζ s−1,x ∈ Φ s−1 (x)), which can be computed easily (logconcave objective function and hyperrectangular constraint set). s = k In this case, by the law of total probability: where when s = 1 we have abusively denotedζ 0,x = x and Φ 0 (x) = x. Thus, we have: and both terms in the right-hand side can be computed easily as discussed in the previous sections (log-concave objective functions and hyperrectangular constraint sets).

Numerical Examples
We, now, demonstrate our theoretical results with a numerical example. Consider a stochastic PETC system (1)-(2) with: and = 0.25, h = 0.006, k = 3. We are interested in assessing the sampling behaviour of the system for initial conditions in X = [−1.2, 1.2] 2 . Following Remark 6, we partition Y = [−2, 2] 2 into 2500 equal rectangles, and construct the IMC as described in the previous. First, consider the multiplicative reward from Example 3 in Section 3.2 and a horizon N = 5. Recall that, in this case, the expected reward expresses the probability that there is no intersampling time s = k in the first 5 triggers. As dictated by Theorem 4.1, we equip the IMC with rewards R, R, which are as follows for any q ∈ Q imc : For all q 0 ∈ Q imc \ q abs , we calculate inf π∈Π E q0 π [g mul,N (ω)] and sup π∈Π E q0 π [g mul,N (ω)], by employing the value iteration introduced in (37). The adversary that gives rise to each bound is the so-called o-maximizing MDP and can be found easily (see [19] and [20]).  Figure 3: The blue and red lines are the computed lower and upper bounds, respectively, on the expected multiplicative reward from Example 3 in Section 3.2 starting from any initial condition x 0 ∈ R i (initial intersampling time is assumed s 0 = 0), for all regions R i ⊂ [−1.2, 1.2] 2 in the partition. The yellow (middle) line is the statistical estimate of the expected reward for a random initial condition from each region.
The obtained bounds for all q 0 = (R, 0) ∈ Q R × {0}, with R ⊂ [−1.2, 1.2] 2 , are shown in Figure  3. We only consider the case where the initial intersampling time s 0 = 0, as commented in Remark 2 4 . From the obtained bounds, one can expect from the system a high probability of sampling with intersampling time k. Thus, based on that observation, an engineer who is to implement the PETC system, could decide to further increase the maximum allowed intersampling time, in order to allow the system to sample even less frequently.  Specifically, for all q 0 ∈ Q R × {0} with R ⊂ [−1.2, 1.2] 2 , we pick a random initial condition y 0 ∈ q 0 and simulate 1000 sample paths, with a horizon of 5 triggers (the simulation stops after the 5th trigger). Each sample path that does not generate any intersampling time s = k is counted, and the total count is divided by 1000 to obtain a statistical estimate of the true probability. Figure 3 shows that, as expected by Theorem 4.1, the statistical estimate is confined within the computed bounds. Finally, Figure 4 is a surface plot illustrating the obtained bounds and the statistical estimate for all regions R i ∈ [−2, 2] 2 , supporting what is discussed in Remark 6: regions closer to the boundary of the partition correspond to more conservative bounds.
Next, to demonstrate our results' extension to PCTL, we derive bounds on the following boundeduntil probability: 5] s.t. proj N (ω(i)) = k and ∀k ≤ i, ω(k) / ∈ q abs (23) This is the probability that the state stays in Y until there is a trigger s = k, in a horizon N = 5. Figure 5 shows the results. Finally, for completeness, we calculate bounds on the expected average intersampling time for N = 5, as introduced in Example 1, Section 3.2. Since we assume s 0 = 0, which implies that we are only interested in the average of the 5 subsequent triggers, we use N in the denominator, instead of N + 1. The results are illustrated in Figure 6. The obtained bounds could be used to compare the average sampling performance of this particular PETC design with some other implementation; e.g. it is evident that, on average, it samples considerably more efficiently than a periodic implementation with period h. Alternatively, they could be used to forecast the expected average occupation of the communication channel.

Conclusion
In this work, we have computed bounds on metrics associated to the sampling behaviour of linear stochastic PETC systems, by constructing IMCs abstracting the sampling behaviour and equipping them with suitable rewards. The metrics are expectations of functions of sequences of intersampling times and state measurements, that take the form of cumulative, average or multiplicative rewards. Numerical examples have been provided to demonstrate the effectiveness of the proposed framework in practice. Specifically, for a given system, we have computed the expected average intersampling time and the probability of triggering with the maximum allowed intersampling time, in a finite horizon Moreover, we have computed bounds on a bounded-until probability, demonstrating extensibility of our approach to PCTL properties. Overall, the framework presented here, enables the formal study of PETC's sampling behaviour and the assessment of its sampling (vs. control) performance.
Future work will focus on the following: a) extending the class of systems considered, b) investigating how the state-space partition proposed in [15] for deterministic linear systems can be employed here, for better and more scalable results, and c) endowing the IMCs with actions, which will allow for scheduling ETC data traffic in networks shared by multiple ETC loops, such that performance criteria are met and optimized (e.g. minimizing packet collisions).

Acknowledgements
The authors thank Daniel Jarne Ornia and Gabriel de Albuquerque Gleizer for helpful discussions on this work. In this subsection, we first provide some technical lemmas, and then prove Theorem 4.1. Let us introduce some notation and terminology. We constrain ourselves to Markovian adversaries. The value of such adversaries depends only on the time-step i and the given state q ∈ Q imc , i.e. π(i, q) = p i,q ∈ Γ q . From now on, we abusively write π(i, q, q ) = p i,q (q ), for any q ∈ Q imc , to denote the transition probability from q to q at time i, under adversary π. Moreover, for s i , s i+1 ∈ N [0,k] , x i ∈ R n ζ , X i+1 ⊆ R n ζ , denote: This notation is common in the literature of stochastic systems and T is often called transition kernel. Let us abuse notation and write Q T (dy |y), for some y ∈ Q, to denote s ∈N [0,k] R n T ((dx , s )|y). We proceed to stating the technical lemmas. The first one provides a relationship indicating that the expected cumulative reward can be written as a value function defined via value iteration, which is a trivial extension of the value iteration in [19] to finite horizons and time-varying adversaries. The second and third lemmas provide some useful bounds, which are employed in the proof of Theorem 4.1.
Lemma 9.1. Given IMC S imc from (9), equipped with a reward function R : Q imc → R max , any Markovian adversary π ∈ Π and any q 0 ∈ Q imc , we have that: where for all q ∈ Q imc and i ∈ N [0,N −1] : Similarly, for all y 0 ∈ Q: where for all y ∈ Q and i ∈ N [0,N −1] : Consequently, we have: Proof. We prove (25) by induction. The proof of (27) is identical, and then (29) follows immediately. It obviously holds that V π,N (q 0 ) = R(q 0 ) = E π [ N j=N γ j−N R(ω(j))|ω(N ) = q 0 ] for all q 0 ∈ Q imc . Now, assume that (25) holds for some i ∈ N [1,N ] . Then: where: • in the second equality we used the induction assumption that we made; • in the third equality we put γ inside the expectation, and we used the law of total expectation; • and in the fourth equality we put R(q 0 ) inside the expectation.
Thus (25) is proven by induction, and the proof is completed.
Lemma 9.2. Given any adversary π ∈ Π, for all y ∈ R n ζ × N [1,k] and for all i ∈ N [1,N ] : Proof. From Lemma 9.1, we know that: [1,k] R(x, s) where in the second equation, the second equality comes from the fact that q abs is absorbing for any π ∈ Π and the third equality comes from (10). From Remark 3, since y ∈ R n ζ × N [1,k] we can deduce that for all j ∈ N [i,N ] we have: Thus, we have: min (x,s)∈R n ζ ×N [1,k] R(x, s) ≤ R(ω(j)), for all j ∈ N [i,N ] a.s.
Only thing remaining is to explain how this proof generalizes to average and multiplicative rewards. The average reward is very simple, as it is just the time-average of a cumulative reward with γ = 1: E[g avg,N (ω)] = 1 N + 1 E[ N 0 R(ω(i))]. Finally, for multiplicative rewards, only thing that changes w.r.t. cumulative rewards is the value iteration, which becomes: V π,N (q) = R(q) V π,i (q) = R(q) · q ∈Qimc V π,i+1 (q )π(i, q, q ) (37)

Proofs of Statements from Section 5
Proof of Lemma 5.2. This proof draws inspiration from the proof of [34,Proposition 2]. Let us first prove log-concavity of the following simpler case: with S ⊆ R n not dependent on x. Observe that: where S − {x} is still a convex set as a mere translation of S. Then, g(x) can be written as: where P (·) is a probability measure over B(R n ) induced by the distribution N (0, Σ). Since N (z|0, Σ) is log-concave, from [35, Theorem 2] we know that P is a log-concave measure, meaning that for every pair of convex sets S 1 , S 2 ⊆ R n and any λ ∈ (0, 1): Moreover, for any x 1 , x 2 ∈ R n and any λ ∈ (0, 1) we have: where the last equality is because v = λy + (1 − λ)w is a convex combination of any two points y, w ∈ S and S is convex 6 . Finally, for any x 1 , x 2 ∈ R n and any λ ∈ (0, 1) we have: = (g(x 1 )) λ (g(x 2 )) 1−λ where in the second equality we used (39) and for the inequality we used (38). Thus, it follows that g(x) is log-concave.
For the general case, since S(x) ⊆ R m is linear on x and convex, then it can be written as S(x) = S + {Gx}, where S ⊆ R m is convex and G ∈ R m×n . Thus we have: where g(x) = S N (dz|x, Σ). The function h(x) = g(f (x) − Gx) is log-concave as the composition of the log-concave function g(x) with the affine function f (x) − Gx.