Dieses Kapitel vertieft die Feinheiten der Modellierung und Analyse großflächiger verteilter eingebetteter Echtzeitsysteme und konzentriert sich auf die Herausforderungen, die komplexes Koordinationsverhalten und stochastisches Versagen mit sich bringen. Er beginnt mit der Diskussion der Beschränkungen bestehender modellgetriebener Ansätze, insbesondere probabilistischer Zeitdiagrammtransformationssysteme (PTGTS), denen es an Unterstützung für stochastisches Verhalten mangelt. Die wichtigste Innovation ist die Einführung von Stochastic Timed Graph Transformation Systems (STGTS), einer Erweiterung von PTGTS, die stochastisches Verhalten durch den Einsatz von kumulativen Verteilungsfunktionen (CDFs) berücksichtigt. Diese Erweiterung ermöglicht die Modellierung von Systemen mit probabilistischen und stochastischen Ausfällen, wie sie in Automobil- und Eisenbahnverkehrssystemen zu finden sind. Das Kapitel bietet eine detaillierte Syntax und Semantik von STGTS, die ihre Fähigkeiten anhand eines laufenden Beispiels eines Shuttle-Systems veranschaulicht, das eine Gleistopologie mit stochastischen Ampelausfällen steuert. Darüber hinaus wird ein Ansatz zur Modellüberprüfung für STGTS skizziert, der bestehende Techniken anpasst, um die neuen stochastischen Variablen und ihre Abtastung zu handhaben. Das Kapitel schließt mit einer Diskussion zukünftiger Arbeiten, einschließlich der Formalisierung und Implementierung des Algorithmus zur Modellprüfung und der Erweiterung eines bestehenden Simulators zur Unterstützung von STGTS. Diese umfassende Erforschung von STGTS stellt einen bedeutenden Fortschritt im Bereich der modellgestützten Analyse dar und bietet ein präziseres und robusteres Rahmenwerk für das Verständnis und die Verbesserung des Verhaltens komplexer verteilter eingebetteter Echtzeitsysteme.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
The correct operation of safety-critical distributed embedded systems is crucial. Following a model-driven approach, the relevant system aspects must be captured and rigorous ideally fully-automatic analysis of (probabilistic) timed safety properties must be supported. Probabilistic Timed Graph Transformation Systems (PTGTSs) support the modeling of such systems and analysis of such properties via model checking or simulation. However, they only support the modeling of probabilistic choice with a fixed numbers of outcomes and non-deterministic timing delays via timing constraints limiting applicability (descriptive expressiveness) and usefulness (precision of analysis results).
To remedy this drawback of PTGTSs, we (a) extend PTGTSs to Stochastic Timed Graph Transformation Systems (STGTSs) integrating discrete/continuous random variables to capture stochastic behavior and (b) outline an adaptation of PTGTS model checking for STGTSs to enable analysis w.r.t. probabilistic timed safety properties. Relying on a running example in which shuttles navigating on a track topology must avoid derailing, we exemplify STGTS support for modeling and analysis.
1 Introduction
Large-scale distributed embedded real-time systems often encompass complex coordinating behavior or spatial movement of numerous interacting agents. Such agents behave according to timing constraints and may exhibit probabilistic behavior and stochastic failures. The analysis of whether such systems and their agents adhere to given specifications describing admissible or desired system behavior is crucial in safety-critical environments. An abundance of model-driven approaches has been applied in the past for designing, understanding, and improving the behavior of such systems in domains such as automotive or railway transportation. These approaches rely on adequate modeling formalisms that define system states and steps by capturing the relevant system aspects at a desired level of abstraction (omitting certain details) benefiting from a suitable descriptive expressiveness (to achieve acceptable applicability) while enabling at the same time an ideally fully-automatic analysis of desired behavioral properties (to enable the derivation of useful insights on the system behavior).
For example, in the embedded real-time RailCab [52, 54, 66] system, shuttles navigate on a large-scale track segment topology where driving behavior is restricted by installed traffic lights ordering shuttle deceleration and local maneuver coordination using shuttle-to-shuttle communication. The resolution of non-determinism determines which shuttle performs the next step, where that shuttle navigates to for alternative successor track segments, and when that shuttle navigates to the next track segment. Timing constraints model the shuttles’ speeds based on their driving modes. Probabilistic choice models whether inter-shuttle communication attempts and traffic light observation on pass-by fail. To concisely exemplify the novel modeling capabilities of STGTS, we consider a simple variant of this system (detailed in Section 4) with reduced probabilistic and structural behavior in which one shuttle approaches a construction site preceded by two traffic lights. As a stochastic behavior not be previously modeled, we consider stochastic failures of traffic lights exhibiting sudden complete failures.
Anzeige
In the past, attributed graphs as a universal visual comprehensive modeling language have been used to model system states allowing to capture global system information, local actor states, and the communication architecture between actors and physical components with great flexibility, while not imposing domain-specific language-based restrictions. Therefore, attributed graphs are employed in many contexts such as UML-based system design [61] and graph databases [2, 58, 69]. The Turing complete formalism of Graph Transformation Systems (GTSs) [21] then relies on rules to describe viable steps among graph-based states in terms of local graph structure modifications and attribute reassignments. GTSs have been extended to Probabilistic Timed Graph Transformation Systems (PTGTSs) [52] integrating clock-based timing constraints as in Timed Automata (TA) [1] using lower and upper time bounds as well as discrete probabilistic choice as in Probabilistic Automata (PA) [72] among a fixed set of outcomes. Non-determinism in PTGTSs originates (in line with the running example) from which rule is applied, where it is applied in the graph, and when it is applied. Quantitative analysis of PTGTSs w.r.t. probabilistic timed reachability/safety properties delivers a worst-case to best-case probability interval of probabilities for different resolutions of non-determinism. For our running example, we note that the stochastic failures cannot be modeled adequately using PTGTSs because the only way to model such failures using PTGTSs is to permanently permit the non-deterministic occurrence of such failures, which precludes the derivation of meaningful quantitative results using analysis.
A deficiency of PTGTSs as a modeling formalism is its lacking support for stochastic behavior. Regarding time, the PTGTS support for clock-based timing constraints has proven useful in many domains (including their use in TA and Probabilistic Timed Automata (PTA) [48]). However, continuous distributions would be needed to model probabilistically distributed delays governing, e.g., arrival times or stochastic failures (e.g., malfunctioning hardware affecting system operation). Regarding choice, PTGTS supports probabilistic choice among a fixed number of outcomes enabling the modeling of, e.g., probabilistic failures on demand. However, discrete distributions governing probabilistic choice among a statically unknown, large, or largely varying number of outcomes would be needed to model, e.g., some probabilistic distributed consensus algorithms where pseudo-random number generators are used to generate uniformly distributed integers from 1 to the number n of processes.
In this paper, to resolve this modeling deficiency of PTGTSs w.r.t. stochastic behavior, we introduce Stochastic Timed Graph Transformation Systems (STGTSs) (as an extension of PTGTSs) by providing its formal syntax and concrete semantics. STGTSs support the modeling of not only structure dynamics, timed behavior, and probabilistic behavior but also of stochastic behavior because, in STGTSs, rules are additionally equipped with information on how stochastic discrete/continuous variables are to be probabilistically sampled using Cumulative Distribution Functions (CDFs), following loosely the extension of PTA into Stochastic Timed Automata (STA) [14]. To derive model checking for STGTSs w.r.t. best-case/worst-case probabilistic timed reachability/safety properties, we adapt the existing PTGTS model checking approach to the STGTS extension incorporating stochastic discrete/continuous variables, their sampling, and usage in timing constraints. We exemplify the novel STGTSs modeling capabilities and the model checking approach using our running example.
This paper is structured as follows. In Section 2, we discuss related work regarding model-driven analysis of (embedded) systems. In Section 3, we present preliminaries and notation. In Section 4, we introduce STGTSs and present the STGTS model for our running example. In Section 5, we discuss a model checking approach for STGTSs based on our running example STGTS. Finally, in Section 6, we conclude the paper and provide an outlook on future work.
Anzeige
2 Related Work
In the past, GTSs [21] have been extended with concepts of time, probabilism, and stochastics along the lines of different automata formalisms into which these graph-based formalisms can be translated to enable their analysis using automata-based techniques: (a) Timed Graph Transformation Systems (TGTSs) [12, 59] extend GTSs by including timing constraints based on clocks, guards, invariants, and clock resets along the lines of TA [1], (b) Probabilistic Graph Transformation Systems (PGTSs) [44, 46] extend GTSs by allowing steps to have different effects each associated with a probability value along the lines of PA or Markov Decision Processes (MDPs) [65, 72], (c) PTGTSs [50‐52] combine TGTSs and PGTSs along the lines of PTA [47, 48], (d) Interval Probabilistic Timed Graph Transformation Systems (IPTGTSs) [55, 56] extend PTGTSs by supporting a non-deterministic specification of probabilities for cases where probabilities can only be estimated along the lines of Interval Probabilistic Timed Automata (IPTA) [43, 77], (e) Stochastic Graph Transformation Systems (SGTSs) [34, 35, 49] extend GTSs by supporting exponentially distributed delay modeling along the lines of Continuous Time Markov Chains (CTMCs) [5‐7, 22, 41, 60], and (f) Hybrid Graph Transformation Systems (HGTSs) [9‐11, 25] extend GTSs by supporting differential equations for delay modeling along the lines of Hybrid Automata (HA) [37]. Note that SGTSs and CTMCs are deterministic (all steps compete based on their exponential distributions) while TGTSs, PTGTSs, and IPTGTSs are non-deterministic (adversaries are used to resolve the non-determinism between timed and discrete steps). Other variants of GTS with time where each step consumes a specified amount of time (instead of using TA-like clock handling) have been considered in [27, 28, 71].
Analysis for these graph-based formalisms is often obtained by translating them into their automata counterparts and applying model checking tools such as Prism [16, 43, 46‐48, 64], Uppaal [74], Kronos [15, 17, 45], and the Modest toolset [14, 30, 57] on the resulting automata.
We focus on probabilistic timed reachability properties to express quantitative safety properties because further formulas, e.g., of Probabilistic Timed Computation Tree Logic (PTCTL) [47, 48] are not supported by model checkers due to the computational complexity of the required model checking algorithms.
Note that an abundance of graph-based analysis approaches for varying properties have been developed in, e.g., [20, 21, 53, 54, 63, 70, 71] and are supported by graph-based tools such as Groove [24, 26, 39], Augur2 [4, 42], Henshin [3, 36, 52], AutoGraph, and the PTGTS-simulator [78, 79].
STA [14] and Stochastic Hybrid Automata (SHA) [30] support the modeling of delay distributions using CDFs and differential equations via the compositional programming languages Modest and HModest [14, 30, 33, 57]. However, they lack domain specific support for high-level operations such as GT (attributed graphs can capture many relevant kinds of system states and their domain specific adaptations more naturally (simpler, more concise, and with fewer model steps) compared to the C programming language like data structures of, e.g., Modest). Similarly, e.g., UML Statecharts providing hierarchical modeling have been extended with probabilistic and stochastic capabilities in [38, 40] also supporting a translation into Modest. Analysis support for STA and SHA is very limited as of now and the authors instead state the goal of integrating sensible modeling capabilities first (obtaining Modest and HModest) to then develop/integrate analysis tools on that common ground. Besides simulation and the simple subclass case of PTA [31, 32] relying on standard PTA model checking using Prism, analysis of STA has only been derived by approximating STA using PTA [23, 29], which also means that full model-checking support is not yet available for STA. In fact, we note that STGTSs model checking as discussed later on is not supported by existing STA analysis approaches.
Fig. 1.
An example of a GT step as an application of a GT rule
3 Preliminaries
For a partial function
, \(\textsf{support}(f) =\{a\in A\mid \exists b.\;f(a)=b\}\) and \(\textsf{range}(f) =\{b\in B\mid \exists a.\;f(a)=b\}\). For injective functions
and
,
.
Graphs: We consider typed attributed graphs (such as the graph \(G_1\) in Figure 1c(left)), which are typed over a type graph (such as the one in Figure 1a) relying on a variation of symbolic graphs [62] from [71]. To capture the graph attribution, Attribute Conditions (ACs) over a many sorted first-order attribute logic are used for which we denote the set of all ACs with (free) variables from X of sort s as \(\textsf{AC}(s,X) \). In a graph G, each attribute is connected to a unique variable from \(\textsf{vars}(G) \) and their values are captured using an AC \(\textsf{ac}(G) \) from \(\textsf{AC}(\textsf{bool},\textsf{vars}(G)) \) such as \(\textsf{ac}(G_1) =(v_1=1\wedge v_2=6)\) in Figure 1c. In a graph G to be transformed, each attribute/variable is restricted by \(\textsf{ac}(G)\) to at most one value (for GTS to exactly one value but in Section 4 certain kinds of variables are not restricted) resulting in a (partial) valuation
where D is the union of data sets across all sorts. An injective graph morphism
matches an occurrence of a graph H in a graph G and must satisfy that \(\textsf{ac}(G) \) implies \(m(\textsf{ac}(H))\). For example, if \(\textsf{ac}(H) =(x\ge 2)\), \(\textsf{ac}(G) =(y=4)\), and m matches the variable x to variable y, then \(y=4\) must imply \(m(x\ge 2)=(y\ge 2)\), which is the case. Type graphs such as \(\textsf{TG}_{\textsf{ex}}\) in Figure 1a have the AC \(\bot \) (false) thereby not restricting attribute values in typed graphs.
Graph Transformation (GT): A GT step from a graph \(G_1\) to a graph \(G_2\) (see Figure 1c for an example) is obtained by applying a GT rule
for a match
(see [21, 71] for technical details), written \((G_1,(\rho ,m),G_2)\in \textsf{GTsteps} \). Intuitively, the rule morphisms \(\ell \) and r model that the elements in K are preserved, the elements in \(L-\ell (K)\) are deleted, and the elements in \(R-r(K)\) are created (see Figure 1b for an example GT rule in which we use an integrated notation where \(\ominus \) and \(\oplus \) indicate the elements to be deleted and created). The graphs L, K, and R have the AC \(\top \) (true) thereby not imposing restrictions on matches: instead, the AC \(\gamma \) specifies how values of variables are related between \(G_1\) and \(G_2\) using the variables from L and R in unprimed and primed form (in Figure 1b, we split the AC \(i_1<3\wedge i_2'=i_1+i_2\) into an attribute guard and an attribute effect for readability). While the AC of a graph essentially represents a valuation for all attributes (a partial valuation later on), the use of ACs is required to express attribute modifications in rules as well as to state properties on graphs as exemplified later on. Technically, the structural changes of a GT step are constructed using a Double Pushout (DPO) diagram (see Figure 1d) and we therefore also write \((G_1,(\rho ,m,k,\bar{m},\ell ',r'),G_2)\in \textsf{GTsteps} \) when further morphisms from this diagram are to be referred to. To ease presentation, we consider graphs up to isomorphism: for GT steps, this means that we assume that \((G_1,\kappa ,G_2),(G_3,\kappa ',G_4)\in \textsf{GTsteps} \) implies that \(G_i\) and \(G_j\) are equal when they are isomorphic (\(i,j\in \{1,2,3,4\}\)); during state space generation, derived steps can easily be manipulated to satisfy this requirement when an isomorphism between inequal graphs would be observed.
Clock-based Timing Constraints: PTA [47] and PTGTSs [50‐52] employ clocks and Clock Constraints (CCs) thereon, as introduced for TA [1], to model possible timed steps (i.e., delays) between discrete steps. For a set of clock variables X, CCs \(\psi \in \textsf{CC}(X) \subseteq \textsf{AC}(\textsf{bool},X) \) are finite conjunctions of clock comparisons of the form \(c_1\sim r\) and \(c_1-c_2\sim r\) where \(c_1,c_2\in X\), \({\sim }\in \{<,>,\le ,\ge \}\), and
.1 Moreover, Extended Clock Constraints (ECCs) \(\psi \in \textsf{ECC}(X,Y) \subseteq \textsf{AC}(\textsf{bool},X\cup Y) \) are ACs that can be simplified to CCs from \(\textsf{CC}(X) \) after substituting all non-clock variables in \(Y-X\). Clock valuations
satisfy CCs \(\psi \), written \( vc \models \psi \), as expected. For a clock valuation \( vc \) and a set of clocks \(X'\), \( vc [X':=0] \) is the clock valuation mapping the clocks from \(X'\) to 0 and all other clocks according to \( vc \). For a clock valuation \( vc \) and a duration
, \( vc +\delta \) is the clock valuation mapping each clock x to \( vc (x)+\delta \).
Probability Foundations: We recall standard notions and notations (see, e.g., [19, 73]). If \(\varOmega \) is a set, \(\mathcal {F}\subseteq \textrm{2}^{\varOmega } \), \(\varOmega \in \mathcal {F}\), and \(\mathcal {F}\) is closed under countable union and complement w.r.t. \(\varOmega \), then \(\mathcal {F}\) is a \(\sigma \)-algebra on \(\varOmega \) and \((\varOmega ,\mathcal {F})\) is a measurable space with measurable sets \(\mathcal {F}\). If \((\varOmega ,\mathcal {O})\) is a topological space (such as the euclidean topology \((\textbf{R} ^n,\mathcal {O})\) using open sets/balls or the discrete topology \((\varOmega ,\textrm{2}^{\varOmega })\)), then \(\mathcal {B}(\varOmega ) =\sigma (\mathcal {O})\) denotes the smallest \(\sigma \)-algebra on \(\varOmega \) containing \(\mathcal {O}\) and is called Borel \(\sigma \)-algebra. The extended reals \(\overline{\textbf{R}} \) are given by \(\textbf{R} \cup \{\infty ,-\infty \}\). If \((\varOmega ,\mathcal {F})\) is a measurable space,
, \(\mu (x)\ge 0\), \(\mu (\emptyset )=0\), and \(\mu (\bigcup x_i)=\sum \mu (x_i)\) for all countably many disjoint sets \(x_i\), then \(\mu \) is a measure on \((\varOmega ,\mathcal {F})\) and \((\varOmega ,\mathcal {F},\mu )\) is a measure space. If \((\varOmega ,\mathcal {F},P)\) is a measure space and \(P(\varOmega )=1\), then P is a probability measure and \((\varOmega ,\mathcal {F},P)\) is a probability space. If \((\varOmega _1,\mathcal {F}_1)\) and \((\varOmega _2,\mathcal {F}_2)\) are measurable spaces,
, \(f^{-1}(X)\in \mathcal {F}_1\) for each \(X\in \mathcal {F}_2\), then f is a measurable function
. If \((\varOmega _1,\mathcal {F}_1,\mu )\) is a measure space,
is a measurable function,
, and \(X_*(\mu )=\mu \circ X^{-1}\), then \(X_*(\mu )\) is the pushforward measure of \(\mu \). If \((\varOmega _1,\mathcal {F}_1,P)\) is a probability space,
is a measurable function, then X is an \((\varOmega _2,\mathcal {F}_2)\)-valued random variable and \(X_*(P)\) is a probability measure and the distribution of X; \(X_*(P)(S)\) and \(X_*(P)(\{s\})\) are written \(P(X\in S)\) and \(P(X=s)\); discrete random variables have countable image \(X(\varOmega _1)\) and random variables use \((\varOmega _2,\mathcal {F}_2)=(\textbf{R},\mathcal {B}(\textbf{R}))\). If
is a discrete random variable,
, and \(p_X(x)=P(X=x)\), then \(p_X\) is the Probability Mass Function (PMF) of X (\(p_X\) distributes the joint probability of 1 across the countable outcomes of X). If
is a random variable,
, and \(F_X(x)=P(X\in (-\infty ,x])\) (also written \(P(X\le x)\)), then \(F_X\) is the CDF of X (\(F_X(x)\) is the probability of a value of at most x); if \(F_X\) is absolutely continuous then there is a unique f satisfying \(f(x)=\textrm{d}F(x)/\textrm{d}x\) called the Probability Density Function (PDF) of X.
The Sierpiński-Dynkin’s \(\pi \)-\(\lambda \) theorem [19, Theorem A.1.5] implies the unique existence of a probability measure P(F) for a CDF F; this allows us to switch from CDFs to probability measures as needed. The Hahn-Kolmogorov (or Carathéodory’s extension) theorem [19, Theorem A.1.1] for \(\sigma \)-finite probability spaces (which is the case here since we assume probability measures based on real-valued random variables), implies the unique existence of a product (probability) measure \(\prod \textbf{P}\) of n (probability) measures \(\textbf{P}_i\) (where the Borel operator \(\mathcal {B}\) distributes over countable products: \(\prod _I\mathcal {B}(\textbf{R}) =\mathcal {B}(\prod _I\textbf{R}) \)); this allows to measure multiple random variables at once (when multiple CDFs are sampled in a single STGTS step later on). We use \(\textsf{Prob}(\varSigma ) \) to denote the set of all probability measures on \((\varSigma ,\mathcal {B}(\varSigma ))\); later, \(\varSigma \) is the set of all system states.
Discrete/Continuous Probabilistic Choice: To model discrete probabilistic behavior including (pseudo)random number generation, we employ PMFs for choosing probabilistically from a finite set of outcomes. In general, discrete distributions and PMFs also support the case of non-finite countably many outcomes with non-zero probabilities but this would yield non-finite branching in the symbolic semantics in Section 5, preventing model checking, and has no practical relevance for the modeling of finite-state finite-software embedded systems.
To model continuous probabilistic behavior, we employ parameterized CDFs to capture the likelihood for possible delay intervals.
Timed Probabilistic Transition Systems (TPTSs): We capture the semantics of STGTSs in terms of their induced TPTSs later on in Section 4 (cf. [30, 76]). A TPTS \(T \) consists of a set of states \(\textsf{states}(T) \), a unique start state \(\textsf{start}(T) \in \textsf{states}(T) \), a set of events (step labels) \(\textsf{events}(T) \) containing
, a probabilistic step relation \(\textsf{steps}(T) \subseteq \textsf{states}(T) \times \textsf{events}(T) \times \textsf{Prob}(\textsf{states}(T)) \), a set of state Atomic Propositions (APs) \(\textsf{aps}(T) \), and a state labeling function
.
Timed Probabilistic Reachability Properties: TPTSs induced by STGTSs are to be analyzed w.r.t. timed probabilistic reachability/safety properties. Different resolutions of non-determinism result in minimal/maximal probabilities for timed reachability capturing best and worst cases.
Evaluate \(\mathcal {P}_{ op =?}(\textsf{F}_{\sim c}\; ap )\) for a TPTS \(T \) with \( op \in \{\textsf{min},\textsf{max} \}\), \({\sim }\in \{\le ,<\}\), \(c\in \textbf{N} \cup \{\infty \}\), and \( ap \in \textsf{aps}(T) \) to obtain the infimal/supremal probability (depending on \( op \)) over all adversaries to reach some \( ap \)-labeled state at time \(t\sim c\).
This problem is solved for a PTGTS (i.e., STGTSs without stochastic variables) by translating it into a PTA and then applying the Prism model checker [52]. In Section 5, we adapt this model checking procedure for general STGTSs.
4 Stochastic Timed Graph Transformation Systems
Fig. 2.
Type graph, STGTS AP/invariant, and start graph for running example
We introduce the syntax of STGTSs in terms of their components in Subsection 4.1 and define the concrete STGTSs semantics in terms of the induced TPTSs in Subsection 4.2.
4.1 Syntax of Stochastic Timed Graph Transformation Systems
Each STGTS employs a type graph and contains a single start graph (for our running example, see again Figure 2). In our running example, the shuttle \(S_1\) initially drives fast on the track topology and will reach the construction site at track \(T_7\) with that speed unless the shuttle navigator observes one of the two traffic lights \(Y_1\) or \(Y_2\) decreasing the shuttle speed. However, both traffic lights may exhibit technical failure before the shuttle reaches them making their observation impossible. Also, the shuttle navigator may still fail to observe a functional traffic light based on his alertness and the traffic lights visibility.
For STGTSs, we assign to each variable of the type graph one variable group from \(\{\textsf{A},\textsf{C},\textsf{SC},\textsf{SD}\}\). For the running example, this assignment is given behind the sort in Figure 2a for each variable. Group \(\textsf{A}\) contains the attribute variables for storing regular attribute values of arbitrary sort, group \(\textsf{C}\) contains the clock variables for measuring durations of sort \(\textsf{real}\), group \(\textsf{SC}\) contains the stochastic continuous variables for storing sampled continuous values of sort \(\textsf{real}\) such as time points, and group \(\textsf{SD}\) contains the stochastic discrete variables for storing sampled discrete values of sort \(\textsf{real}\) such as numbers of a pseudo-random number generator, which may be simply integer values when using, e.g., the discrete uniform distribution. The variables \(\textsf{vars}(G) \) of a typed graph G are split into \(\textsf{varsA}(G) \), \(\textsf{varsC}(G) \), \(\textsf{varsSC}(G) \), and \(\textsf{varsSD}(G) \) accordingly. Also, we use \(\textsf{varsS}(G) \) for all stochastic variables \(\textsf{varsSC}(G) \cup \textsf{varsSD}(G) \) together.
STGTS states contain a graph and valuations for its clock variables, stochastic continuous variables, and stochastic discrete variables.
Definition 2 (STGTS State)
An STGTS state\(s \) has 4 components.
\(\textsf{graph}(s) =G\) is a finite graph.
maps the clock variables to non-negative reals.
maps the stochastic continuous variables to reals.
maps the stochastic discrete variables to reals.
Moreover, we define the following three abbreviations.
\(\textsf{valA}(s) \) is the restriction of the valuation \(\textsf{val}(G) \) (see Section 3) to \(\textsf{varsA}(G) \),
\(\textsf{val}(s) \) is the joint valuation \(\textsf{valC}(s) \cup \textsf{valSC}(s) \cup \textsf{valSD}(s) \cup \textsf{valA}(s) \), and
\(s +\delta \) is the time advanced STGTS state obtained from \(s \) by changing \(\textsf{valC}(s) \) to \(\textsf{valC}(s) +\delta \) and keeping the other components unchanged.
In STGTS states, the three valuations are captured outside the graph (as opposed to the valuation for the attribute variables, which is recorded as an AC in the graph)to simplify the definition of concrete/symbolic semantics; in particular, our integration of structural GT-behavior with timed and stochastic behavior ensures that (especially discrete) STGTS steps can only read/write the clock and stochastic variables in the desired restricted way. The start state of an STGTS consists of the start graph and the three valuations mapping all (real-valued) variables to 0.
STGTS invariants state clock constraints based on graph patterns; the states of an STGTS \(S \) are those STGTS states satisfying all STGTS invariants of \(S \). Most commonly, STGTS invariants provide upper bounds such as \(c\le r\) to prevent the progress of time when the clock c reaches r to enforce the occurrence of a discrete step at that time (if the progress of time is prevented while no discrete step is enabled, the state is in a time lock and an STGTS with such a state being reachable is invalid). Technically, STGTS invariants are pairs of a graph I and an ECC \(\psi \in \textsf{ECC}(\textsf{varsC}(I),\textsf{vars}(I)) \) (ranging over all variables) and are satisfied by an STGTS state \(s \) when for every match
, \(\psi \) is satisfied in the sense that \(\textsf{val}(s) (m(\psi ))\) is equivalent to \(\top \). In principle, STGTS invariants can also be used to rule out discrete steps based on structurally forbidden patterns using \(\psi =\top \) but, in our experience, this results in a more complex STGTS with degraded separation of concerns with the threat of unexpectedly prevented steps. For our running example, all STGTS invariants are of the form \((I,\psi )\) where I is the left hand side graphs of some STGTS rule; we therefore provide the ECCs \(\psi \) alongside the corresponding STGTS rules later on. For now, we refer to Figure 2c to provide the STGTS invariant \({\textsf{inv}}_{\textsf{drive}}\) expressing that shuttles must advance to the next track within \( is +2\) time units for which the duration that a shuttle is on its current track is measured using the clock \( driveClock =c\). This STGTS invariant is satisfied by the start state \(s \) (see again Figure 2d for the start graph) because the shuttle is 0 time units on its current track (due to \(\textsf{valC}(s) ( cs _1)=0\)) while it may be up to 4 time units on that track (due to the STGTS invariant requiring \( cs _1\le 2+2\) using the \( invSpeed \) attribute of the shuttle). Technically, for \({\textsf{inv}}_{\textsf{drive}} =(I,\psi )\) and the only existing match
, we obtain the ECC \(m(\psi )=( cs _1\le is _1+2)\) (assuming that \( is _1\) is the variable attached to the \( invSpeed \) attribute of the shuttle \(S_1\) with value 2) and then \(\textsf{val}(s) (m(\psi ))=(0\le 2+2)\equiv \top \).
STGTS APs are given by graphs; in the concrete semantics, each state \(s\) is labeled with the STGTS APs A for which a match
exists. In contrast to STGTS invariants, STGTS APs may not depend on clock/stochastic variables as a consequence of how the model checking algorithm from Section 5 operates on the symbolic semantics. Also note that if \(\textsf{ac}(A)\) refers to such a clock/stochastic variable, m cannot be a match as its implication check cannot be satisfied because G does not record a value for such variables. In our running example, we employ the STGTS AP \({\textsf{ap}}_{\textsf{unsafe}}\) from Figure 2b capturing states where a fast shuttle (advancing every 2 to 4 time units to the next track) is at a construction site.
To clarify our assumptions on and handling of distributions in STGTSs, we rely on a Distribution Structure (DS) capturing the required information for each supported distribution (such as whether it is a discrete/continuous distribution, its parameters, and requirements on these parameters). For each distribution, we hereby only assume oracles allowing to apply the distributions PMF/CDF and to generate random variates (i.e., sample random variables) and thereby abstract from whether the CDF must be approximated for CDFs without closed form (such as for the normal distribution) or which sampling technique is employed.
Definition 3 (Distribution Structure (DS))
A DS\(\varGamma \) has 7 components.
\(\textsf{dist}(\varGamma ) =D\) is a set of (symbols for) distributions.
\(\textsf{kind}(\varGamma ) (d)\in \{\textsf{d},\textsf{c} \}\) defines for each \(d\in D\) its discrete/continuous kind.
\(\textsf{varsP}(\varGamma ) =P\) is a set of parameter variables.
\(\textsf{param}(\varGamma ) (d)\in \textrm{2}^{P} \times \textsf{AC}(\textsf{bool},P) \) defines for each \(d\in D\) its set p of parameter variables and an AC \(\gamma \) restricting instantiations of p. For \(\textsf{param}(\varGamma ) (d)=(p,\gamma )\) and
, we write \(v\in \langle \textsf{param}(\varGamma ) (d)\rangle \) when v satisfies \(\gamma \).
\(\textsf{pmf}(\varGamma ,d,v) \) for \(d\in D\) with \(\textsf{kind}(\varGamma ) (d)=\textsf{d} \) and \(v\in \langle \textsf{param}(\varGamma ) (d)\rangle \) is the PMF \(p_X\) of a d(v)-distributed random variable X returning for some value \(x\in \textbf{R} \) the probability \(p\in [0,1]\) that X takes the value x.
\(\textsf{cdf}(\varGamma ,d,v) \) for \(d\in D\) with \(\textsf{kind}(\varGamma ) (d)=\textsf{c} \) and \(v\in \langle \textsf{param}(\varGamma ) (d)\rangle \) is the CDF \(F_X\) of a d(v)-distributed random variable X returning for some value \(x\in \textbf{R} \) the probability \(p\in [0,1]\) that X takes a value in \((-\infty ,x]\).
\(\textsf{sample}{(\varGamma ,d,v)} \) for \(d\in D\) and \(v\in \langle \textsf{param}(\varGamma ) (d)\rangle \) returns a random variate for a d(v)-distributed random variable X whenever it is used.
Subsequently, we assume a fixed DS \(\varGamma \) containing, e.g., the distributions \(\textsf{dist}(\varGamma ) =\{\textsf{exp},\textsf{normal},\textsf{uniformC},\textsf{weibull},\textsf{uniformD},\textsf{bernoulli},\textsf{binomial} \}\) for the exponential, normal, (continuous) uniform, Weibull, (discrete) uniform, bernoulli, and binomial distribution. For example, for the exponential distribution, we include \(\lambda \in \textsf{varsP}(\varGamma ) \) and \(\textsf{param}(\varGamma ) (\textsf{exp})=(\{\lambda \},\lambda >0)\). Clearly, distribution convolutions such as \(X\sim Y+2\times Z\) where \(Y\sim \textsf{exp} (2)\) and \(Z\sim \textsf{exp} (4)\) are exponentially distributed (for this particular case, see [75]) or bathtub distributions combining multiple Weibull distributions [68, p. 614] (allowing to express decreasing, constant, and increasing failure rates across a components life span) from reliability/deterioration engineering [8, 67] may be (a) included explicitly in \(\varGamma \) (when oracles for their CDF/PMF and sampling can be provided) or (b) obtained by combining sampled values for the underlying distributions at use time. To simplify analysis, option (a) appears advantageous for non-trivial convolutions.
STGTS rules describe how discrete steps between STGTS states are to be derived. Each STGTS rule contains a set of underlying GT rules leading to (usually) different STGTS states; they have a common left hand side graph L implying that these GT rules are all applicable based on just one match m from L into the graph of the current STGTS state. Each of these GT rules is equipped with a weight expression based on the attribute and stochastic discrete variables, which express relative probabilities among each other.2 The STGTS rules also contain a clock guard given by an ECC that must be satisfied for the STGTS rule to be applicable (the guard is simplified to a CC by substituting all variables by values except for the clock variables and applying trivial simplification).3 The STGTS rules also capture for each underlying GT rule \(\rho \) the clocks (from the right hand side of \(\rho \)) that must be reset to 0 when applying \(\rho \). To capture the novel sampling of stochastic continuous/discrete variables, the STGTS rule also provides for such variables (from the right hand side of \(\rho \)), based on the assumed DS, the distributions and their parameters (given by ACs over the attribute variables of L) to be used using a map \(\textsf{stoch}(\sigma ) \).4 Note that not all stochastic continuous/discrete variables must be (re)sampled in each step meaning that \(\textsf{stoch}(\sigma ) (\rho )\) is a partial map and that precisely the parameters of the chosen distribution must be instantiated (leading to the partial map of type
). Lastly, each STGTS rule is equipped with a priority from \(\textbf{N} \) meaning that it is only applicable when no other STGTS rule is applicable with a higher priority.
Definition 4 (STGTS Rule)
An STGTS rule\(\sigma \) has 7 components.
\(\textsf{lhs}(\sigma ) =L\) is a graph (a common left-hand side to be matched).
\(\textsf{rules}(\sigma ) \) is a finite non-empty set of GT rules \(\rho \) with \(\textsf{lhs}(\rho )=L\) where \(\textsf{lhs}(\rho )\) is the left-hand side graph of \(\rho \).
\(\textsf{weight}(\sigma ) (\rho )\in \textsf{AC}(\textsf{real},\textsf{varsA}(L) \cup \textsf{varsSD}(L)) \) assigns a probability weight expression to each underlying GT rule \(\rho \in \textsf{rules}(\sigma ) \) using only attributes variables and stochastic discrete variables of L.
\(\textsf{guard}(\sigma ) \in \textsf{ECC}(\textsf{varsC}(L),\textsf{vars}(L)) \) is a guard defined as an ECC over the variables from the left-hand side graph L.
\(\textsf{reset}(\sigma ) (\rho )\subseteq \textsf{varsC}(\textsf{rhs}(\rho )) \) identifies the clocks to be reset for each underlying GT rule \(\rho \in \textsf{rules}(\sigma ) \) where \(\textsf{rhs}(\rho ) \) is the right-hand side graph of \(\rho \).
assigns to each underlying GT rule \(\rho \in \textsf{rules}(\sigma ) \) and to some stochastic variables \(x\in \textsf{rhs}(\rho ) \) available after application of \(\rho \) a stochastic assignment (d, i) containing the distribution \(d\in \textsf{dist}(\varGamma ) \) to be used and an instantiation map i mapping arguments of d to an AC over attribute variables of L where \(\textsf{kind}(\varGamma ) (d)=\textsf{c} \) iff \(x\in \textsf{varsSC}(\textsf{rhs}(\rho )) \) (ensures that only continuous/discrete distributions are used for stochastic continuous/discrete variables) and \(\textsf{param}(\varGamma ) (d)=(p,\gamma )\) implies \(\textsf{support}(i) =p\) (ensures that the arguments of d are instantiated).
\(\textsf{prio}(\sigma ) \in \textbf{N} \) is the priority assigned to \(\sigma \).
For our running example, see Figure 3 for the STGTS rules and their described behavior where trivial components are omitted. For simplicity, we employ exponential distributions to model the failures of traffic lights while, e.g., Weibull or bathtub distributions could be more adequate if domain knowledge on the used hardware components would be available.
Fig. 3.
The STGTS rules for our running example.
An STGTS then collects the components presented so far. For our running example, see Figure 2 and Figure 3 for these components.
Definition 5 (STGTS)
An STGTS\(S \) has 4 components.
\(\textsf{start}(S ) \) is a finite start graph.
\(\textsf{rules}(S ) \) is a finite set of STGTS rules.
\(\textsf{invs}(S ) \) is a finite set of STGTS invariants.
\(\textsf{aps}(S ) \) is a finite set of STGTS APs.
Moreover, \(\textsf{states}(S ) \) contains the \(\textsf{invs}(S ) \)-satisfying STGTS states of \(S \) (i.e., \(s \in \textsf{states}(S ) \) iff for all \((I,\psi )\in \textsf{invs}(S ) \) and
, \(\textsf{val}(s) \circ m\models \psi \)).
4.2 Semantics of Stochastic Timed Graph Transformation Systems
We now introduce the STGTS (single) step relation based on which we then define the TPTS induced by an STGTS subsequently. As for all modeling formalisms based on clocks as used in TA, STGTSs define (a) timed steps where only time elapses adding the same delay to all clock variables and (b) discrete steps where clocks may be reset but where, with more technical effort, the other components of the STGTS states may be adapted. We note that the step relation operates only on the states of the given STGTS, requiring that all STGTS invariants are satisfied, which also holds for the states implicitly traversed during a timed step. For the discrete steps, we consider six construction steps in the following definition. Step (1): this step entails a standard GT step applying one GT rule of the STGTS rule; but the valuation of the stochastic discrete variables has to be temporarily added to the graph to enable their usage. Step (2): as for PTGTSs, the clock guard is checked and the resulting clock valuation is obtained by preserving clock values (along the morphisms of the GT step) and setting all created clocks and clocks to be reset to 0. Step (3): the resulting valuation of stochastic discrete variables is obtained by adapting it, similarly to clock variables, along the morphisms of the GT step, setting created stochastic discrete variables to 0, and sampling the specified stochastic discrete variables using the DS according to the given distribution and its evaluated arguments (also checking the admissibility of those parameters using the constraints in the DS). Also, the CDF (belonging to the PMF) as well as the sampling reassignments are recorded in the step label (F and \( sr \)) for the subsequent definition of the induced TPTS. Step (4): this step is analogous to the previous but for the stochastic continuous variables. Step (5): we check that all GT rules of the STGT rule are applicable for the given match (thereby checking also the STGTS invariants) with a weight from
and that the sum of all weights is in
to be able to obtain a PMF from these weights. Step (6): as for PTGTSs, we rule out the applicability of an STGTS rule with higher priority.
Definition 6 (STGTS Step)
An STGTS \(S \) defines timed and discrete steps.
Timed Step:\((s,\delta ,s +\delta )\in \textsf{steps}(S ) \) where \(s \in \textsf{states}(S ) \) and
, if
\(\circ \)
Clock Invariants:\((s +\delta ')\in \textsf{states}(S ) \) for each delay \(\delta '\in [0,\delta ]\).
Discrete Step:\((s_{1},(\sigma ,m,\rho , pw , F , sr ),s_{2})\in \textsf{steps}(S ) \) where \(s_{1},s_{2}\in \textsf{states}(S ) \) are STGTS states, \(\sigma \in \textsf{rules}(S ) \) is an STGTS rule,
is a match, and \(\rho \in \textsf{rules}(\sigma ) \) is a GT rule of \(\sigma \), if all following items are satisfied.
\((G_1,(\rho ,m,k,\bar{m},\ell ',r'),G_2)\in \textsf{GTsteps} \) where \(G_1\) is obtained from \(\textsf{graph}(s_{1})\) by adding \(\textsf{valSD}(s_{1})\) to \(\textsf{ac}(\textsf{graph}(s_{1})) \) and \(\textsf{graph}(s_{2})\) is obtained from \(G_2\) by restricting \(\textsf{ac}(G_2) \) to \(\textsf{varsA}(G_2) \).5
(2)
Clock Guards, Resets, and Invariants:
\(\circ \)
\(\textsf{val}(s_{1})\models \textsf{guard}(\sigma ) \) (i.e., the clock guard of the STGTS rule \(\sigma \) is satisfied),
\(\circ \)
for \(c\in \textsf{varsC}({s_{2}}) \), if \(c\in \bar{m}(\textsf{reset}(\sigma ) (\rho ))\) (i.e., c is reset), then \(\textsf{valC}(s_{2})(c)=0\), elseif \(c\in \textsf{varsC}(s_{2})-\textsf{range}(r') \) (i.e., c is created), then \(\textsf{valC}(s_{2})(c)=0\), else (i.e., c is preserved) \(\textsf{valC}(s_{2})(c)=\textsf{valC}(s_{1})(\varDelta (r',\ell ')(c))\).
(3)
Sampling of Stochastic Discrete Variables:
\(\circ \)
for \(x\in \textsf{varsSD}({s_{2}}) \), if \(x\in \bar{m}(\textsf{support}(\textsf{stoch}(\sigma ) (\rho )))\) (i.e., x is sampled), then \(\textsf{valSD}(s_{2})(x)=\theta \) (see next item for \(\theta \)), elseif \(x\in \textsf{varsSD}(s_{2})-\textsf{range}(r') \) (i.e., x is created), then \(\textsf{valSD}(s_{2})(x)=0\), else (i.e., x is preserved) \(\textsf{valSD}(s_{2})(x)=\textsf{valSD}(s_{1})(\varDelta (r',\ell ')(x))\).
\(\circ \)
(Sampling of \(\theta \)) If \(x\in \bar{m}(\textsf{support}(\textsf{stoch}(\sigma ) (\rho )))\), there are y, d, and \(v'\) satisfying \(x=\bar{m}(y)\) and \(\textsf{stoch}(\sigma ) (\rho )(y)=(d,v')\); we abbreviate \(v''=\textsf{valA}(s_{1})\circ m\circ v'\) as the valuated parameters of d; if \(v''\in \langle \textsf{param}(\varGamma ) (d)\rangle \), we sample \(\theta =\textsf{sample}{(\varGamma ,d,v'')} \) and derive no step otherwise. Also, the partial maps \( F \) and \( sr \) with domain \(\textsf{varsS}({s_{2}}) \) map x to (the CDF belonging to) \(\textsf{pmf}(\varGamma ,d,v'') \) and \(\theta \) as sampling record.
(4)
Sampling of Stochastic Continuous Variables:
\(\circ \)
(analogously to stochastic discrete variable sampling)
(5)
Derivability of all Probabilistic Outcomes:
\(\circ \)
\( pw =\textsf{val}(s_{1})(m(\textsf{weight}(\sigma ) (\rho )))\ge 0\) is the valuated probability weight.
\(\circ \)
For all \(\rho '\in \textsf{rules}(\sigma ) \) there is \((s_{1},(\sigma ,m,\rho ',\_,\_,\_),\_)\in \textsf{steps}(S ) \).
\(\circ \)
For some \(\rho '\) there is \((s_{1},(\sigma ,m,\rho ', pw ',\_,\_),\_)\in \textsf{steps}(S ) \) with \( pw '>0\).
(6)
Restriction to Highest Priority Steps:
\(\circ \)
If there is some \(\sigma '\in \textsf{rules}(S ) \) with \((s_{1},(\sigma ',\_,\_,\_,\_,\_),\_)\in \textsf{steps}(S ) \), then \(\textsf{prio}(\sigma ') \le \textsf{prio}(\sigma ) \).
We now define the semantics of STGTSs in terms of their induced TPTSs. Besides formally capturing the start state discussed above, this definition entails the aggregation of steps from \(\textsf{steps}(S ) \) that belong to the same probabilistic decision (defined by source state \(s_{1}\), STGTS rule \(\sigma \), and match m) into steps of the resulting TPTS. Firstly, considering the case without sampling of stochastic variables, the probability to reach a certain state is defined using the probability weights of the GT rules of \(\sigma \) when being evaluated using m: to obtain a PMF from these weights, we construct a probability weight map
that assigns a weight \(w(y)>0\) to some \(y\in Y\); this map induces the unique PMF
with \(p(y)=w(y)/\sum _{y\in Y}w(y)\). Based on this PMF p, for a possible outcome \(o\in \textsf{states}(S ) \), we add up the probabilities \(p(\rho )\) assigned to GT rules \(\rho \) of \(\sigma \) that lead to the outcome o (for cases where the same outcome o is obtained for multiple GT rules). Secondly, when extending this consideration to the sampling of stochastic variables, we note that the probability of a single outcome is 0, which is why CDFs capture the probabilities of sets of outcomes \(O\subseteq \textsf{states}(S ) \). Focusing on a single GT rule \(\rho \), we consider all steps for \(s_{1}\), \(\sigma \), m, and \(\rho \) differing in how stochastic variables are sampled and obtain the \(n(\rho )\) many variables \(\pmb x(\rho )\) sampled for \(\rho \) and the CDFs \(\pmb F(\rho )\) used for that sampling, which correspond to probability measures \(\pmb P(\rho )\). Filtering the given set O to those states that can be reached using these steps, we obtain a set of assignments for the sampled variables. We note that the resulting probability measure from \(\textsf{Prob}(\textsf{states}(T)) \) (to obtain a TPTS) is obtained as the convex combination using p from above of the product measures obtained from each \(\pmb P(\rho )\).6
Definition 7 (TPTS Induced by STGTS)
Each STGTS \(S \) induces a unique TPTS\(T \) as follows.
\(\textsf{states}(T) \) is the smallest subset of \(\textsf{states}(S ) \) such that \(\textsf{steps}(T) \) and \(\textsf{start}(T) \) below are well-defined.
\(\textsf{start}(T) =(\textsf{start}(S ),\textbf{0},\textbf{0},\textbf{0})\) where \(\textbf{0}\) maps each argument to 0.
\(\textsf{events}(T) \) is the smallest set containing
and tuples \((\sigma ,m)\) where \(\sigma \in \textsf{rules}(S ) \) and m is a match such that \(\textsf{steps}(T) \) below is well-defined.
\((s_{1},a,\mathcal {P})\in \textsf{steps}(T) \), if one of the two following cases applies.
\(\circ \)
Timed Step: if all following items are satisfied.
\(\triangleright \)
\((s_{1},a,s_{2})\in \textsf{steps}(S ) \) is a timed step of \(S \).
\(\triangleright \)
\(\mathcal {P}(\{s_{2}\})=1\).
\(\circ \)
Discrete Step: if all following items are satisfied.
\(\triangleright \)
\(a=(\sigma ,m)\in \textsf{events}(T) \) is a partial step label.
\(\triangleright \)
\(\mathcal {P}(O)=\sum _{\rho \in \textsf{rules}(\sigma )}p(\rho )\times X(\rho )_*(P(\rho ))(O)\) for which we define p, X, and P.
\(\triangleright \)
\( steps (\rho )\) contains all \((s_{1},(\sigma ,m,\rho , pw , F , sr _j),s_{2,j})\in \textsf{steps}(S ) \). These steps agree in \( pw \), F, and \(\textsf{graph}(s_{2,j})\). Requiring that \( steps (\rho )\) is not empty implies that all GT rules \(\rho \) of \(\sigma \) have been applied successfully (which may fail due to dangling edges, STGTS invariant violation, or unsatisfiable attribute change requirements), we denote \( pw \) and F for a fixed \(\rho \) by \(\textsf{pw}(\rho )\) and \(\textsf{F}(\rho )\).
\(\triangleright \)
p is the unique PMF induced by the probability weight map \(\textsf{pw}(\rho )\).
\(\triangleright \)
\(\pmb x(\rho )=(x_1,\dots ,x_{n(\rho )})\) is an ordering of the \(n(\rho )\in \textbf{N} \) sampled stochastic continuous/discrete variables \(x_i\in \textsf{support}(\textsf{F}(\rho )) \) contained in \(\textsf{graph}(s_{2,j})\).
\(\triangleright \)
\(\pmb F(\rho )=(F_1,\dots ,F_{n(\rho )})\) is the corresponding list of CDFs used to sample the variables \(\pmb x(\rho )\) defined by \(F_i=\textsf{F}(\rho )(x_i)\).
\(\triangleright \)
\(\pmb P(\rho )=(P_1,\dots ,P_{n(\rho )})\) is the corresponding list of probability measures obtained from the CDFs \(\pmb F(\rho )\) defined by \(P_i=P(F_i)\).
\(\triangleright \)
\(P(\rho )=\prod \pmb P(\rho )\) is the product measure of the \(n(\rho )\) probability measures \(\pmb P(\rho )\) (see Section 3).
\(\triangleright \)
maps \(\pmb r=(r_1,\dots ,r_{n(\rho )})\) to the \(s_{2,j}\) where \(\forall 1\le i\le n(\rho ).\; sr _j(x_i)=r_i\).7
\(\textsf{aps}(T) =\textsf{aps}(S ) \).
.
5 Model Checking Approach
PTGTS model checking support w.r.t. probabilistic timed reachability/safety properties has been obtained by constructing a symbolic PTGTS state space on which standard PTA model checking algorithms can be applied. We now outline an extension of this approach for the setting of STGTSs omitting a formal definition due to space restrictions. While STGTSs and STA have different semantics due to the STGTS use of priorities and invariants and the STA use of urgent steps to enable compositional modeling, we conjecture that our STGTS model checking approach can also be adapted to STA for which only sampling based analysis exists (essentially flattening the stochastic distributions to probabilistic PTA steps exists).
Model checking requires the construction of a state space with finitely many states and steps. However, STGTS employ (a) real valued clocks that are changed using timed steps of varying length8 and (b) real-valued stochastic continuous variables changed using sampling steps. Both, (a) and (b), result in infinitely many states and steps where even single states are exited by infinitely many steps (infinite branching). Consequently, we require the construction of a symbolic state space (based on symbolic states and symbolic steps between them) in which these two notions are captured symbolically aggregating enough possibilities together such that a finite symbolic state space is obtained for which model checking can be applied equivalently w.r.t. the original properties to be analyzed.
First, for real-valued clocks, this problem has been solved in TA, PTA, as well as PTGTS model checking based on the zone-abstraction (see [47, 48, 52]). In particular, symbolic states \((G,\psi )\) contain a CC \(\psi \in \textsf{CC}(X) \) called zone and represent all concrete states \((G, vc )\) with clock valuations
for which \( vc \) satisfies \(\psi \). Zones can easily be compared because they can be uniquely represented using finite Difference Bound Matrices (DBMs) [13, 18]. Discrete and (symbolic) timed steps are then always applied in tandem when constructing symbolic state spaces using this zone-abstraction and the effects of clock guards, resets, and invariants are applied based on standard DBM operations. The syntax of CCs and their usage in guards and invariants (as introduced for TA) ensures that concrete states represented by symbolic states have the same subsequent behavior. Lastly, this zone-abstraction results in a finite equivalent symbolic state space for TA, PTA, and PTGTS (when the set of reachable graphs is finite).
For probabilistic formalisms (such as PTA, PTGTSs, and now STGTSs) using the zone-abstraction for constructing a finite symbolic state space, we note that model checking must be performed backwards from the target states specified in the property to be analyzed. Thereby, symbolic states are constructed backwards from the target applying discrete and timed steps in tandem deriving weakest preconditions.9 In particular, backward analysis is required to check which successor states \((G_i,\psi _{i})\) each symbolically representing the paths starting in them do not contradict each other: for example, for a clock x, a continuation from one successor may require \(x\le 1\) while the continuation from another successor requires \(2\le x\) making them incompatible. During backward analysis, all such subsequent constraints are propagated backwards enabling the analysis of compatibility when needed.
Second, as our core extension of PTGTS model checking to STGTS model checking, we need to capture real-valued stochastic continuous variables symbolically, which are sampled in discrete steps and are used in the evaluation of clock guards of later discrete steps. We note that stochastic continuous variables would not be a challenge when their sampling and the usage of that sampling would always occur in single discrete STGTS steps (thereby the stochastic sampling would have only a local effect on step derivation). Instead, the STGTS semantics allows to execute sampling in one step also when the sampled values are not used immediately for clock guard evaluation, which we call eager sampling. For our running example, this is of course required to sample a \( failTime \) for the traffic lights, which will fail based on that \( failTime \) later on. During symbolic backward state space generation and model checking, when constructing a step backwards from a state s, we replace each stochastic continuous variable t that occurs in a clock guard \(\psi \) by a clock counterpart \(t_c\) and employ the TA-based zone-abstraction to then propagate the adapted clock guard \(\psi '=\psi \{t_c/t\}\) obtained by replacing t by \(t_c\) backwards. During this backward propagation, we infer lower and upper bounds \(a\le t_c\le b\) for \(t_c\) along the way based on the STGTS invariants applicable on intermediate states and guards of applied steps. Such restrictions of the clock \(t_c\) indirectly restrict the possible samplings of t that could lead to the state s from which we started the backward propagation of restrictions. Also, if a sampled continuous stochastic variable is used in multiple continuation paths of a (probabilistic) step, the mechanism discussed above for CCs readily evaluates their compatibility. Finally, when the sampling step for the continuous stochastic variable t is reached, unrestricted sampling of t (in the defined forward semantics) can be replaced by applying the CDF on the restriction given by an interval \(a\le t_c\le b\) specified for \(t_c\) in the CC of the reached symbolic state.
The following exemplary application of our model checking approach demonstrates that sampling can be replaced by CDF applications during model checking once the relevant arguments for the CDFs have been derived via backward propagation.
See Figure 3 where the rule \({\sigma }_{\textsf{init}}\) samples a duration for a stochastic continuous variable also resetting a clock to measure that duration and where \({\sigma }_{\textsf{fail}}\) checks in its guard and invariant whether that duration has elapsed already (i.e., \( failClock \) is the proposed clock to be associated with the stochastic continuous variable \( failTime \)). STGTS symbolic state space generation reveals that, due to its speed of 2 to 4 time units per track, the shuttle is at the traffic lights at times \(X\in [4,8]\) and \(Y\in [8,16]\) depending on how non-determinism is resolved and the traffic lights have failed until time t with probabilities \(P(X\le t)=1-\textrm{e}^{-0.001\times t}\) and \(P(Y\le t)=1-\textrm{e}^{-0.002\times t}\). To obtain best-case/worst-case probabilities, non-determinism would let the shuttle reach these traffic lights at the lower/upper borders of these intervals. For the best-case, we obtain the minimal probability for derailing at track \(T_7\) reaching the construction site there with \( invSpeed \) of 2 of \((P(X\le 4)+P(X>4)\times (1-0.95\times 0.99))\times (P(Y\le 8)+P(Y>8)\times (1-0.95\times 0.9))\approx {1.6 \times 10^{-4}}\) given by the product of not slowing down twice where (for \(r\in \{4,8\}\)) \(P(X\le r)\) checks for the probability of reaching the traffic light after it has failed and \(P(X>r)\times (1-0.95\times p)\) (for \(p\in \{0.99,0.9\}\)) is the probability of reaching the traffic light before it has failed but the navigator not observing it based on alertness and limited visibility. Lastly, we report the worst-case probability \(4.2 \times 10^{-4}\).
This exemplary analysis for our running example already indicates that backward model checking indeed needs to accumulate constraints on stochastic variables (by determining duration intervals for the additional clocks \(t_c\) for the stochastic variables t from the CC of the current state). For the example, the two clocks measuring the time since sampling are constrained to the intervals \([4,8]\) and \([8,16]\) as required. These constraints are then probabilistically evaluated by applying the CDFs when reaching the sampling steps for the stochastic continuous variables t to minimize/maximize the resulting probability.
6 Conclusion and Future Work
We extended the formalism of PTGTSs to STGTSs to obtain a high-level description language for the modeling and analysis of complex distributed embedded probabilistic real-time systems with stochastic behavior where CDFs are sampled to capture in particular pseudo-random number generators and stochastic delays. This extension thereby improves the modeling capabilities as exemplified in our running example featuring stochastic failures. Moreover, we outlined a model checking approach for STGTSs w.r.t. worst-case/best-case probabilistic timed reachability properties based on prior work on PTGTSs.
As future work, we plan to formalize, implement, and evaluate the outlined model checking algorithm for an extension of our running example featuring shuttle convoy establishment from [52] with more complex structural behavior thereby also enabling analysis for those STA that can be encoded into STGTSs. Moreover, we plan to employ standard CDF sampling techniques to extend an already existing PTGTS simulator for large-scale systems to STGTSs.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
\(\textsf{varsC}(L) \) and \(\textsf{varsS}(L) \) are excluded to make the probabilistic aspect independent from the clock-based and stochastic timing aspect.
The guard is not just a CC over the clock variables of L to allow that attributes store, e.g., the speed of a shuttle while also stating CCs based on that shuttle speed. Also, the stochastic continuous variables must be allowed in clock guards to model urgent rules in which components fail. Also, only for the symbolic semantics, we need to ensure that the guard can be simplified to a CC; for the concrete semantics, we just need to evaluate it to a Boolean after substituting all its variables.
\(\textsf{varsC}(L) \) and \(\textsf{varsS}(L) \) are excluded as concrete parameter variables to make the probabilistic aspect independent from the clock-based timing and to prevent sampling based on sampled values, which should rather be implemented using further convoluted distributions in the DS.
That is, \(\textsf{val}(G_1) (x)\) is \(\textsf{val}(\textsf{graph}(s_{1})) (x)\) for \(x\in \textsf{varsA}(G_1) \), \(\textsf{valSD}(s_{1})(x)\) for \(x\in \textsf{varsSD}(G_1) \), and undefined otherwise. Also, \(\textsf{val}(\textsf{graph}(s_{2})) (x)\) is \(\textsf{val}(G_2) (x)\) for \(x\in \textsf{varsA}(G_2) \) and undefined otherwise.
If
is a PMF, \((\textbf{R} ^{n(y)},\mathcal {B}(\textbf{R} ^{n(y)}),P(y))\) are probability spaces (for \(y\in Y\)), and
are random variables (for \(y\in Y\)), then \((\varOmega ,\mathcal {F},\mathcal {P})\) is a probability space with \(\mathcal {P}(O)=\sum _{y\in Y}p(y)\times X(y)_*(P(y))(O)\) where \(X(y)_*(P(y))\) is the pushforward measure of P(y) (see Section 3).
Note that \( sr _j\) and \(s_{2,j}\) are bound together by being in a single step in \(\textsf{steps}(\rho )\) defined above and that \(s_{2,j}\) is unique because the different \(s_{2,j}\) only vary in how the stochastic variables are sampled.
For PTGTSs and now STGTSs, we first identify all reachable graphs and the steps between them by constructing a (symbolic) forward state space and then restrict the symbolic backward state space to use only discrete steps from this (symbolic) forward state space. Hereby, we also apply sampling of the discrete stochastic variables (assuming a small number of results) while we may consider approaches to also handle their sampling symbolically in the future. This construction of the (symbolic) forward state space is not necessary for TA and PTA because locations and steps are provided explicitly upfront for them.
, \(\textsf{support}(f) =\{a\in A\mid \exists b.\;f(a)=b\}\) and \(\textsf{range}(f) =\{b\in B\mid \exists a.\;f(a)=b\}\). For injective functions
and
,
.
where D is the union of data sets across all sorts. An injective graph morphism
matches an occurrence of a graph H in a graph G and must satisfy that \(\textsf{ac}(G) \) implies \(m(\textsf{ac}(H))\). For example, if \(\textsf{ac}(H) =(x\ge 2)\), \(\textsf{ac}(G) =(y=4)\), and m matches the variable x to variable y, then \(y=4\) must imply \(m(x\ge 2)=(y\ge 2)\), which is the case. Type graphs such as \(\textsf{TG}_{\textsf{ex}}\) in Figure 1a have the AC \(\bot \) (false) thereby not restricting attribute values in typed graphs.
for a match
(see [21, 71] for technical details), written \((G_1,(\rho ,m),G_2)\in \textsf{GTsteps} \). Intuitively, the rule morphisms \(\ell \) and r model that the elements in K are preserved, the elements in \(L-\ell (K)\) are deleted, and the elements in \(R-r(K)\) are created (see Figure 1b for an example GT rule in which we use an integrated notation where \(\ominus \) and \(\oplus \) indicate the elements to be deleted and created). The graphs L, K, and R have the AC \(\top \) (true) thereby not imposing restrictions on matches: instead, the AC \(\gamma \) specifies how values of variables are related between \(G_1\) and \(G_2\) using the variables from L and R in unprimed and primed form (in Figure 1b, we split the AC \(i_1<3\wedge i_2'=i_1+i_2\) into an attribute guard and an attribute effect for readability). While the AC of a graph essentially represents a valuation for all attributes (a partial valuation later on), the use of ACs is required to express attribute modifications in rules as well as to state properties on graphs as exemplified later on. Technically, the structural changes of a GT step are constructed using a Double Pushout (DPO) diagram (see Figure 1d) and we therefore also write \((G_1,(\rho ,m,k,\bar{m},\ell ',r'),G_2)\in \textsf{GTsteps} \) when further morphisms from this diagram are to be referred to. To ease presentation, we consider graphs up to isomorphism: for GT steps, this means that we assume that \((G_1,\kappa ,G_2),(G_3,\kappa ',G_4)\in \textsf{GTsteps} \) implies that \(G_i\) and \(G_j\) are equal when they are isomorphic (\(i,j\in \{1,2,3,4\}\)); during state space generation, derived steps can easily be manipulated to satisfy this requirement when an isomorphism between inequal graphs would be observed.
.1 Moreover, Extended Clock Constraints (ECCs) \(\psi \in \textsf{ECC}(X,Y) \subseteq \textsf{AC}(\textsf{bool},X\cup Y) \) are ACs that can be simplified to CCs from \(\textsf{CC}(X) \) after substituting all non-clock variables in \(Y-X\). Clock valuations
satisfy CCs \(\psi \), written \( vc \models \psi \), as expected. For a clock valuation \( vc \) and a set of clocks \(X'\), \( vc [X':=0] \) is the clock valuation mapping the clocks from \(X'\) to 0 and all other clocks according to \( vc \). For a clock valuation \( vc \) and a duration
, \( vc +\delta \) is the clock valuation mapping each clock x to \( vc (x)+\delta \).
, \(\mu (x)\ge 0\), \(\mu (\emptyset )=0\), and \(\mu (\bigcup x_i)=\sum \mu (x_i)\) for all countably many disjoint sets \(x_i\), then \(\mu \) is a measure on \((\varOmega ,\mathcal {F})\) and \((\varOmega ,\mathcal {F},\mu )\) is a measure space. If \((\varOmega ,\mathcal {F},P)\) is a measure space and \(P(\varOmega )=1\), then P is a probability measure and \((\varOmega ,\mathcal {F},P)\) is a probability space. If \((\varOmega _1,\mathcal {F}_1)\) and \((\varOmega _2,\mathcal {F}_2)\) are measurable spaces,
, \(f^{-1}(X)\in \mathcal {F}_1\) for each \(X\in \mathcal {F}_2\), then f is a measurable function
. If \((\varOmega _1,\mathcal {F}_1,\mu )\) is a measure space,
is a measurable function,
, and \(X_*(\mu )=\mu \circ X^{-1}\), then \(X_*(\mu )\) is the pushforward measure of \(\mu \). If \((\varOmega _1,\mathcal {F}_1,P)\) is a probability space,
is a measurable function, then X is an \((\varOmega _2,\mathcal {F}_2)\)-valued random variable and \(X_*(P)\) is a probability measure and the distribution of X; \(X_*(P)(S)\) and \(X_*(P)(\{s\})\) are written \(P(X\in S)\) and \(P(X=s)\); discrete random variables have countable image \(X(\varOmega _1)\) and random variables use \((\varOmega _2,\mathcal {F}_2)=(\textbf{R},\mathcal {B}(\textbf{R}))\). If
is a discrete random variable,
, and \(p_X(x)=P(X=x)\), then \(p_X\) is the Probability Mass Function (PMF) of X (\(p_X\) distributes the joint probability of 1 across the countable outcomes of X). If
is a random variable,
, and \(F_X(x)=P(X\in (-\infty ,x])\) (also written \(P(X\le x)\)), then \(F_X\) is the CDF of X (\(F_X(x)\) is the probability of a value of at most x); if \(F_X\) is absolutely continuous then there is a unique f satisfying \(f(x)=\textrm{d}F(x)/\textrm{d}x\) called the Probability Density Function (PDF) of X.
, a probabilistic step relation \(\textsf{steps}(T) \subseteq \textsf{states}(T) \times \textsf{events}(T) \times \textsf{Prob}(\textsf{states}(T)) \), a set of state Atomic Propositions (APs) \(\textsf{aps}(T) \), and a state labeling function
.
maps the clock variables to non-negative reals.
maps the stochastic continuous variables to reals.
maps the stochastic discrete variables to reals.
, \(\psi \) is satisfied in the sense that \(\textsf{val}(s) (m(\psi ))\) is equivalent to \(\top \). In principle, STGTS invariants can also be used to rule out discrete steps based on structurally forbidden patterns using \(\psi =\top \) but, in our experience, this results in a more complex STGTS with degraded separation of concerns with the threat of unexpectedly prevented steps. For our running example, all STGTS invariants are of the form \((I,\psi )\) where I is the left hand side graphs of some STGTS rule; we therefore provide the ECCs \(\psi \) alongside the corresponding STGTS rules later on. For now, we refer to Figure 2c to provide the STGTS invariant \({\textsf{inv}}_{\textsf{drive}}\) expressing that shuttles must advance to the next track within \( is +2\) time units for which the duration that a shuttle is on its current track is measured using the clock \( driveClock =c\). This STGTS invariant is satisfied by the start state \(s \) (see again Figure 2d for the start graph) because the shuttle is 0 time units on its current track (due to \(\textsf{valC}(s) ( cs _1)=0\)) while it may be up to 4 time units on that track (due to the STGTS invariant requiring \( cs _1\le 2+2\) using the \( invSpeed \) attribute of the shuttle). Technically, for \({\textsf{inv}}_{\textsf{drive}} =(I,\psi )\) and the only existing match
, we obtain the ECC \(m(\psi )=( cs _1\le is _1+2)\) (assuming that \( is _1\) is the variable attached to the \( invSpeed \) attribute of the shuttle \(S_1\) with value 2) and then \(\textsf{val}(s) (m(\psi ))=(0\le 2+2)\equiv \top \).
exists. In contrast to STGTS invariants, STGTS APs may not depend on clock/stochastic variables as a consequence of how the model checking algorithm from Section 5 operates on the symbolic semantics. Also note that if \(\textsf{ac}(A)\) refers to such a clock/stochastic variable, m cannot be a match as its implication check cannot be satisfied because G does not record a value for such variables. In our running example, we employ the STGTS AP \({\textsf{ap}}_{\textsf{unsafe}}\) from Figure 2b capturing states where a fast shuttle (advancing every 2 to 4 time units to the next track) is at a construction site.
, we write \(v\in \langle \textsf{param}(\varGamma ) (d)\rangle \) when v satisfies \(\gamma \).
). Lastly, each STGTS rule is equipped with a priority from \(\textbf{N} \) meaning that it is only applicable when no other STGTS rule is applicable with a higher priority.
assigns to each underlying GT rule \(\rho \in \textsf{rules}(\sigma ) \) and to some stochastic variables \(x\in \textsf{rhs}(\rho ) \) available after application of \(\rho \) a stochastic assignment (d, i) containing the distribution \(d\in \textsf{dist}(\varGamma ) \) to be used and an instantiation map i mapping arguments of d to an AC over attribute variables of L where \(\textsf{kind}(\varGamma ) (d)=\textsf{c} \) iff \(x\in \textsf{varsSC}(\textsf{rhs}(\rho )) \) (ensures that only continuous/discrete distributions are used for stochastic continuous/discrete variables) and \(\textsf{param}(\varGamma ) (d)=(p,\gamma )\) implies \(\textsf{support}(i) =p\) (ensures that the arguments of d are instantiated).
, \(\textsf{val}(s) \circ m\models \psi \)).
and that the sum of all weights is in
to be able to obtain a PMF from these weights. Step (6): as for PTGTSs, we rule out the applicability of an STGTS rule with higher priority.
, if
is a match, and \(\rho \in \textsf{rules}(\sigma ) \) is a GT rule of \(\sigma \), if all following items are satisfied.
that assigns a weight \(w(y)>0\) to some \(y\in Y\); this map induces the unique PMF
with \(p(y)=w(y)/\sum _{y\in Y}w(y)\). Based on this PMF p, for a possible outcome \(o\in \textsf{states}(S ) \), we add up the probabilities \(p(\rho )\) assigned to GT rules \(\rho \) of \(\sigma \) that lead to the outcome o (for cases where the same outcome o is obtained for multiple GT rules). Secondly, when extending this consideration to the sampling of stochastic variables, we note that the probability of a single outcome is 0, which is why CDFs capture the probabilities of sets of outcomes \(O\subseteq \textsf{states}(S ) \). Focusing on a single GT rule \(\rho \), we consider all steps for \(s_{1}\), \(\sigma \), m, and \(\rho \) differing in how stochastic variables are sampled and obtain the \(n(\rho )\) many variables \(\pmb x(\rho )\) sampled for \(\rho \) and the CDFs \(\pmb F(\rho )\) used for that sampling, which correspond to probability measures \(\pmb P(\rho )\). Filtering the given set O to those states that can be reached using these steps, we obtain a set of assignments for the sampled variables. We note that the resulting probability measure from \(\textsf{Prob}(\textsf{states}(T)) \) (to obtain a TPTS) is obtained as the convex combination using p from above of the product measures obtained from each \(\pmb P(\rho )\).6
and tuples \((\sigma ,m)\) where \(\sigma \in \textsf{rules}(S ) \) and m is a match such that \(\textsf{steps}(T) \) below is well-defined.
maps \(\pmb r=(r_1,\dots ,r_{n(\rho )})\) to the \(s_{2,j}\) where \(\forall 1\le i\le n(\rho ).\; sr _j(x_i)=r_i\).7
.
for which \( vc \) satisfies \(\psi \). Zones can easily be compared because they can be uniquely represented using finite Difference Bound Matrices (DBMs) [13, 18]. Discrete and (symbolic) timed steps are then always applied in tandem when constructing symbolic state spaces using this zone-abstraction and the effects of clock guards, resets, and invariants are applied based on standard DBM operations. The syntax of CCs and their usage in guards and invariants (as introduced for TA) ensures that concrete states represented by symbolic states have the same subsequent behavior. Lastly, this zone-abstraction results in a finite equivalent symbolic state space for TA, PTA, and PTGTS (when the set of reachable graphs is finite).
in CCs is required because we compare clocks to real-valued stochastic continuous variables later leading to such CCs in the symbolic semantics.
is a PMF, 
are random variables (for 
