The increasing interconnectivity of embedded software systems has led to the rise of new types of Multi-Agent Systems, such as Distributed Cyber-Physical Systems, where agents synchronize by exchanging observations and local actions with remote agents. This inter-agent message passing involves (transmission, propagation, queuing, and processing) delays, which may compromise safety in safety-critical decision-making systems due to outdated information. Therefore, we proposed a methodology to derive explicit delay-robust models (resilient to δ -delays) preserving safety from safe abstract models that assume zero-delays. However, this procedure requires iterative model checking steps. In this paper, we motivate to eliminate the need for costly iterations by exploring behavioral equivalences between explicit and abstract models to define a consistency notion. This consistency facilitates the systematic transfer of verified guarantees to unverified models, efectively eliminating the need for additional model checking.
A graph G = (Gv, Ge, sG, tG) consists of a set Gv of nodes, a set Ge of edges, a source function sG: Ge →
GV, and a target function tG: Ge → Gv. Let G = (Gv, Ge, sG, tG) be a graph. Let Gs = (Gvs, Ges, sGs, tGs)
be a subgraph of G, if. Gvs ⊆ Gv and Ges ⊆ Ge. G|Gs denotes Gs is a subgraph of G. For a set X of clocks
Φ (X) denotes the set of all clocks contraints ϕ generated by ϕ ::= x1 ∼ c | xa - xj ∼ c | ϕ ∧ ϕ , where ∼ ∈
{<, >, ≤ , ≥ }, c ∈ N ∪ {∞} are constants, and xa, xj ∈ X are clocks. Let X be a set of clocks. V(X) denotes
the set of all functions v: X → R and is called Clock valuation. Let v: X → R and X’ ⊆ X. Then v[X’ :=
0] : X → R is a clock reset such that for any x ∈ X holds if x ∈ X’, then v[X’ := 0](x) = 0 else v[X’ :=
0](x) = v(x). Let v: X → R and δ ∈ R . Then v + δ : X → R is a clock increment such that for any x → X
holds (v + δ )(x) = v(x)+ δ . Let v: X → R and ϕ be some constraint over X. Then v |= ϕ denotes that
v satisfies the constraint ϕ . Let v0: X → R be the initial clock valuation if v0(x) = 0 for every x ∈ X.
V0(X) is the singleton set containing the unique initial clock valuation. Let H = (Hv, He, sH, tH) and
G be two graphs. An injective graph morphism (short: morphism) mg: G → H is a pair of mappings
mv: Gv → Hv and me: Ge → He, where mv ◦ sG = sH ◦ me and mv ◦ tG = tH ◦ me. Graph Conditions
(GCs) are used to state properties on graphs requiring the presence or absence of certain subgraphs in a
host graph using propositional connectives and (nested) existential quantification over graph patterns.
Let TG be a distinguished graph, called type graph. A type graph has attributes connected to local
variables and an attribute condition (AC) over many-sorted first-order attribute logic, which is used
to specify the values for those local variables. Tg = (G, mg’) is a typed graph, where G is a graph and
mg’ is a morphism: G → TG. Let Tg1 = (T1, t1) and Tg2 = (T2, t2) be two typed graphs. A typed graph
morphism tgm: Tg1 → Tg2 is a morphism mg”: T1 → T2, which is compatible with the typing functions,
i.e., t2 ◦ mg” = t1. Let ρ = (L, R, K, NAC, l: K → L, r: K → R, ω, prio) be a Graph Transformation Rule
(short: rule), if L (called left-hand side of rule), K (called interface graph of rule), R (called right-hand
side of rule) are (typed) graphs, l and r are two (typed) morphisms, NAC is a finite set of forbidden
(typed) graphs X containing L, prio: R → N assigns a priority to each rule, and ω is the Application
Condition (ApC) that is expressed as a graph condition. The transformation procedure defining a graph
transformation approach introduced by the Double Pushout Approach [
To bypass model checking of SA1 and ease the general proposed methodology, we aim to transfer verified safeness from S E1 to SA1 by design. The underlying idea to archieve this, is to explore the formal relationship between the two models (i.e., SE1 and SA1) to leverage model consistency, which enables transferring safety. Therefore, we define the following research questions.
• Are SE1 and SA1 formally in relation? • How can model-based guarantees be systematically transferred from SE1 to SA1 by design? To address this research gap, we aim to identify potential behavioral equivalences among SE1 and SA1. Establishing such a formal relation may facilitate the transfer of safety guarantees from SE1 to SA1 by design, thereby eliminating the need for model checking of the latter. However, this approach presents challenges in determining the appropriate level of abstraction required. Furthermore, SE1 may introduce potential states that violate safety, which were not reachable in SE0.
Since model-based consistency research is inherently tied to its domain, and approaches that formally
reason about consistency assume additional information about what is being analyzed with respect to
the consistency notion [
In this paper, we discussed the motivation for reducing the computational cost and the number of modelchecking iterations in our previously proposed approach by defining a consistency relation between SE1 and SA1. Such a formal relation could serve as the foundation for systematically transferring modelbased guarantees. In this context, we identified key research questions and the associated challenges related to achieving this objective.