# Refinements for Open Automata (Extended Version)

Ludovic Henrio, Eric Madelaine, Rabéa Ameur-Boulifa, Quentin Corradi

## ► To cite this version:

Ludovic Henrio, Eric Madelaine, Rabéa Ameur-Boulifa, Quentin Corradi. Refinements for Open Automata (Extended Version). RR-9517, Inria - Research Centre Grenoble - Rhône-Alpes. 2023. hal-04193421

HAL Id: hal-04193421

https://inria.hal.science/hal-04193421v1

Submitted on 6 Sep 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
<figure><img src="image_2.png" /></figure>

Refinements for Open
Automata
(Extended Version)

Rabéa Ameur-Boulifa, Quentin Corradi, Ludovic Henrio, Eric
Madelaine

RESEARCH
REPORT

Nº 9517

August 2023

Project-Teams CASH and
KAIROS

ISSN 0249-6399

ISRN INRIA/RR-9517-FR+ENG
<figure><img src="image_3.png" /></figure>
<figure><img src="image_4.png" /></figure>

Refinements for Open Automata
(Extended Version)

Rabéa Ameur-Boulifa *, Quentin Corradi †, Ludovic Henrio †,
Eric Madelaine ‡

Project-Teams CASH and KAIROS

Research Report n° 9517 — August 2023 — 32 pages

**Abstract:** Establishing equivalence and refinement relations between programs is an important mean for verifying their correctness. By establishing that the behaviours of a modified program simulate those of the source one, simulation relations formalise the desired relationship between a specification and an implementation, two equivalent implementations, or a program and its optimised implementation. This article discusses a notion of simulation between *open automata*, which are symbolic behavioural models for communicating systems. Open automata may have *holes* modelling elements of their context, and can be composed by instantiation of the holes. This allows for a compositional approach for verification of their behaviour. We define a simulation between open automata that may or may not have the same holes, and show under which conditions these refinements are preserved by composition of open automata.

**Key-words:** Labelled transition systems, Simulation, Refinement, Composition

RESEARCH CENTRE
GRENOBLE - RHÔNE-ALPES

Inovallée

655 avenue de l'Europe Montbonnot

38334 Saint Ismier Cedex

<footnote>* LTCI, Télécom Paris, Institut Polytechnique de Paris</footnote>

<footnote>† Université Lyon, EnsL, UCBL, CNRS, Inria, LIP</footnote>

<footnote>‡ INRIA Sophia Antipolis Méditérannée, UCA</footnote>
# Raffinements des Automates Ouverts

**Résumé** : Vérifier la correction d'un programme est une tâche complexe souvent réalisée de manière progressive en établissant une relation entre les comportements de deux programmes. La relation de simulation, qui met en corrépondance une spécification et une implémentation, ou un programme et sa version raffinée, permet d'assurer la correction. Cet article introduit et discute d'une relation entre des programmes représentés sous la forme d'automates ouverts, un modèle comportemental symbolique pour les systèmes de communication. Établir des relations d'équivalence et de raffinement sur les automates ouverts permet une approche compositionnelle pour vérifier leur comportement. L'aspect compositionnel des automates ouverts provient des trous, qui représentent des éléments du contexte. La composition de deux automates consiste à instancier un trou d'un automate avec l'autre automate. Dans cet article, nous définissons une relation de raffinement entre les automates ouverts qui peuvent avoir ou non les mêmes trous, sur le modèle des simulations. Nous montrons ensuite dans quelles conditions la composition d'automates ouverts préserve cette relation.

**Mots-clés** : Systèmes de transitions étiquetées, Simulation, Raffinement, Composition
# 1 Introduction

Compositional design is a highly convenient approach for specifying and verifying large systems. Automata are often used as the basic formalism for this approach, but most automata definitions allow only the specifications of finite closed systems. These systems can be verified efficiently, but programming often consists in writing systems that should be interfaced with others, and with potentially unbound behaviours. We investigate in our works the reasoning on open symbolic systems, with a strong focus on compositionality of properties. More precisely, we say that a system is open if it contains a “hole” to be filled by another system. Open systems are typically composition operators [15] or componentised systems where some of the components are yet to be provided [6]. This form of composition is more complex to handle than top-level interaction usually found in process algebra, as the behaviour of each entity in the system is parameterised both by classical symbolic variables and by process variables.

The refinement concept plays an important role in software engineering. In addition to helping to cope with the complexity of requirements and design, refinement provides a foundation for ensuring system correctness. The correctness of a system can be established by proving, that a system refines its specification with the idea that some properties of the specification are preserved in the refined system. Refinement entails that one system can be considered as a more precise version of another one that is considered to be the specification. The refined model features all the specified behaviours with more concrete details. From a formal point of view, refinement is a mathematical relations between a specification and its implementation, with trace inclusion or simulation being frequently used relations [20, 18].

In this article, we design a simulation theory for open symbolic systems. We build a very generic theory that should allow us to reason on simulation-based verification for most concurrent systems, as our base theory merely relies on automata parameterised by both variables and processes. As we shall see, our composition of automata is also very generic to account for any interaction mechanism found in concurrent systems. While our contribution is theoretical, it establishes the foundations for to the verification of any compositionally designed system, like component systems, algorithmic skeletons.

Open automata (that we abbreviate OA) were defined as a way to provide a semantics for open parameterised hierarchical labelled transition systems (abbreviated LTS). They were proposed as a theoretical foundation for parametrised automata used in verification tools and called *pNets*. An OA [15] is similar to a classical automaton but with variables and holes. Variables make automata symbolic and allow them to encode infinite state systems. Holes enable the composition of automata: an automaton with a hole is an operator that takes another automaton as parameter and reacts to the actions it emits; the composed automaton is an automaton where the behaviour of one “process parameter” of the main automaton has been provided. Due to their the generic nature, the notion of OA model is quite abstract but we already illustrated previously how to derive OAs for process algebra operators [15] or for component systems [6, 5].

In previous works [6, 22] a bisimulation relation was defined for OA and open parameterised hierarchical LTSs. It exhibited good properties concerning bisimulation, but refinement relations were not studied. In this article we go further to define a theory of simulation for OA. The simulation relation we introduce in the paper is based on the notion of simulation, in a similar way to that defined in classical automata theory [19, 8]. It possesses the common behaviour-preserving property: all the behaviour of the abstract specification must be followed by its (complex) implementation but additional behaviours may exist. However we also ensure that a whole scenario, made of several steps, of the specification can also be simulated by the refined system, which is slightly richer than the traditional simulation relation and allows us to obtain a compositionality result.
Our contribution in this paper is the definition of a simulation relation for OA that has the following characteristics:

* Classical simulation characterisation but also an additional criteria ensuring that simulation does not introduce deadlocks when following a trace from the simulated automaton.

* Good properties relatively to composition: we prove that composition preserves the simulation relation.

* Ability to take into account both composition and transitivity: this is a challenge because composition changes the set of holes of the OA and simulation takes into account the actions of the holes.

The simulation relation is introduced in two steps. First we define a simulation that relates two automata with the same holes, which allows us to focus on the automaton aspect. Second we introduce a relation that relates two automata with different sets of holes, which allows us to take into account the open nature of OA, and to deal with composition. Properties of the simulation are stated and proven on the second, more general version of the relation, thus also being valid for the first simpler simulation relation.

This paper is organized as follows. Section 2 recalls the definition of OA and defines their composition. We then define a simulation relation for OA, first only considering two automata with the same set of holes in Section 3 and generalize it to automata with a different set of holes in Section 4. Section 5 is dedicated to formalize and prove basic properties of the simulation defined, including the proof that simulation is a preorder and has nice composability properties. In Section 6 we review related works, and Section 7 concludes the paper.

# 2 Open Automata and their Composition

This section presents our notations and the principles of automata. Except for minor changes in the notations, compared to previous works [6] the only new contribution is the definition of a composition operator for OA.

## 2.1 Preliminaries and notations

Families of values (equivalent to maps) will be noted $x_i^{i \in I}$, $\{i \to x_i | i \in I\}$, or $\{i \leftarrow x_i | i \in I\}$, depending on what is more convenient (e.g. $i \leftarrow x_i$ is used for maps that are used as substitution). Statements like $\exists c_j^{i \in J}$ defines both $J$ and the mapping $j \to c_j$. The disjoint union on sets is noted $\oplus$. Disjoint union is also used on maps. There are several ways of ensuring a union is disjoint, we will indifferently either suppose sets are disjoint or rename conflicting objects (useful for variables). In a formula, a quantifier followed by a finite set will be used as a shorthand for the quantification on every variable in the set: $\forall \{a_1, \dots, a_n\}, \exists \{b_1, \dots, b_m\}, P$ means $\forall a_1, \dots, \forall a_n, \exists b_1, \dots, \exists b_m, P$.

Our expression algebra $E$ is the disjoint union of terms, actions, and formulas $E = \mathcal{T} \oplus \mathcal{A} \oplus \mathcal{F}$. $\mathcal{T}$ and $\mathcal{A}$ are term algebras. The set of formulas $\mathcal{F}$ contain at least first order formulas and equality<fnref n="1" /> over $\mathcal{T}$ and $\mathcal{A}$. For $e \in E$, $vars(e)$ is the set of variables in $e$ that are not bound by a binder. An expression is closed if $vars(e) = \emptyset$. The set $\mathcal{P}$ denotes values which is a subset of closed terms. $\mathcal{F}_V$ is the set of formulas $f$ that only uses variables in $V$, i.e., the formulas such that $vars(f) \subseteq V$. The parallel substitution of variables in $e$ by a map $\psi: V \to \mathcal{T}$ is denoted $e[\psi]$. We suppose given a decidable satisfiability relation on closed formulas, denoted $\vdash_f$. We will use two variants of the satisfiability relation:

<footnote n="1">¹Equality does not need to be only syntactic.</footnote>
* The satisfiability of a formula $f \in \mathcal{F}$ under some valuation $\sigma: V \to \mathcal{P}$ is defined as follows: $\sigma \vdash f \iff \exists \text{vars}(f\{\sigma\})$, $f\{\sigma\}$

* The satisfiability of a formula $f \in \mathcal{F}$ with some variable set $V$ as context is defined as follows: $V \vdash f \iff \forall V, \exists (\text{vars}(f) \setminus V), f$

## 2.2 Open Automata (OA)

OA are labelled transition systems with variables that can be used to compose other automata: they are made of transitions that are dependent on the actions of “holes”, a composition operation consists in filling a hole with another automaton to obtain a more complex automaton. The variables make the OA symbolic, and the holes allow for a partial definition of the behaviour.

**Definition 1 (Open transition, Open automaton).** An open automaton is a tuple $(S, s_0, V, \sigma_0, J, T)$ with $S$ a set of states, $s_0 \in S$ the initial state, $V$ the finite set of variable names, $\sigma_0: V \to \mathcal{P}$ the initial valuation of variables, $J$ the set of hole names and $T$ the set of open transitions.

An open transition is a tuple $\frac{\beta_j^{j \in J'}, g, \psi}{s \underset{s'}{\stackrel{\alpha}{\to}}}$ with $s, s' \in S$ the source and target states, $\alpha \in \mathcal{A}$ the produced action, $J' \subseteq J$ the holes involved in the transition, $\beta_j \in \mathcal{A}$ the actions of the holes, $g \in \mathcal{F}$ the guard and $\psi: V \to \mathcal{T}$ the variable assignments. To be well-formed, an open transition should use only variables of the automaton and variables appearing in the involved actions, formally:

$$ \text{vars}(g) \subseteq \text{vars}(\alpha) \cup \bigcup_{j \in J'} \text{vars}(\beta_j) \cup V $$

$$ \forall v \in V. \text{vars}(\psi(v)) \subseteq \text{vars}(\alpha) \cup \bigcup_{j \in J'} \text{vars}(\beta_j) \cup V $$

A pair consisting of a state and a valuation is called a configuration (of the automaton). We use two operators to access pieces of information of the OA.

**Definition 2 (Out-transition, Transition variables).** Let $V$ be the variable names of a considered automaton, $T$ its transitions and $r$ one of its states. $\text{OT}_T(r) \subset T$ are called the out-transitions of the state $r$. When the set $T$ is clear from the context, it will be omitted. The local variables of a transition $\text{vars}(t)$ are all variables appearing in transition $t$ except the variables of the automaton.

$$ \text{OT}_T(r) = \left\{ \frac{\beta_j^{j \in J'}, g, \psi}{s \underset{s'}{\stackrel{\alpha}{\to}}} \in T \mid s = r \right\} \quad \text{vars}\left(\frac{\beta_j^{j \in J'}, g, \psi}{s \underset{s'}{\stackrel{\alpha}{\to}}}\right) = \left( \text{vars}(\alpha) \cup \bigcup_{j \in J'} \text{vars}(\beta_j) \right) \setminus V $$

**Example 1 (prod-cons).** As a running example, we consider a classical producer-consumer pair interacting through FIFO buffer, named prod-cons. Fig. 1 reflects the overall structure of the system involving a producer process, a consumer process and an orchestrator that coordinates their activities.

The OA modelling the behaviour of such a system using an unbounded circular/ring buffer is depicted in Fig. 2. The automaton has a single state with two holes: $P$ and $Q$ that are the two interacting processes. $l$ (as last) indicates the next available position for enqueuing an element and $f$ (as first) is the position that contains the next element to be queued. The buffer reacts to a push from $P$ and enqueues it. Similarly, whenever $Q$ pops an element, it dequeues it. Additionally, whenever $Q$ produces an item, it is exposed as an external observable **print** action. When any process do its internal computation, it is exposed externally as unobservable action $\tau$.

The example uses several kinds of data. Variable $m$ holds a message (we can leave the message type abstract here). We additionally use arrays of messages with a syntax of the form $M[l]$ for
<figure><img src="image_5.png" /><figcaption>Figure 1: Structure of the example. Each box corresponds to a process whose ports are the actions it can perform. The actions observable by the environment are **push**, which indicates the enqueuing of an element, **pop** which indicates the dequeueing, and **print** which indicates the production of results.</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Figure 2: OA for the prod-cons system using FIFO circular buffer.</figcaption></figure>

array accesses; *M* is an array of *N* elements, from 0 to *N*−1. Finally, we use addition and modulo operation (%) on integers. □

**Open automata composition.** OA are partially specified automata, the partiality arises from the holes. A hole can be seen as a port in which we can plug an OA. The plugging operation is called composition. The composition of OA was already implicitly defined by the means of composition on pNets in previous work [15]. We provide here a (new) direct definition of composition for OA.

**Definition 3 (Composition of OA).** Let $A_c = \langle S_c, s_{0c}, V_c, \sigma_{0c}, J_c, T_c \rangle$ be an OA and $k$ one of its holes, $k \in J_c$. Let $A_p = \langle S_p, s_{0p}, V_p, \sigma_{0p}, J_p, T_p \rangle$ be another OA, the composition $A_c[A_p/k]$ that fills the hole $k$ of the context OA $A_c$ with the parameter OA $A_p$ is defined as follows:

$$A_c[A_p/k] ::= \langle S_c \times S_p, (s_{0c}, s_{0p}), V_c \uplus V_p, \sigma_{0c} \uplus \sigma_{0p}, J_p \uplus J_c \setminus \{k\}, T \rangle$$

with

$$T = \left\{ \begin{array}{l} \frac{\beta_j^{j \in J'_p \omega J'_c}, g_c \wedge g_p \wedge \alpha_p = \beta_k, \psi_c \uplus \psi_p}{(s_c, s_p) \xrightarrow{\alpha_c} (s'_c, s'_p)} \quad \left| \begin{array}{l} \beta_j^{j \in J'_c \omega \{k\}}, g_c, \psi_c \in T_c, \beta_j^{j \in J'_p}, g_p, \psi_p \in T_p \end{array} \right. \\ \cup \left\{ \frac{\beta_j^{j \in J'_c}, g_c, \psi_c}{(s_c, s_p) \xrightarrow{\alpha_c} (s'_c, s'_p)} \quad \left| \begin{array}{l} \beta_j^{j \in J'_c}, g_c, \psi_c \in T_c, k \notin J'_c, s_p \in S_p \end{array} \right. \right\} \end{array} \right.$$
<figure><img src="image_7.png" /><figcaption>Figure 3: (Left) A **producer**. It produces one item at a time and pushes it. (Right) A **consumer**. It pops an item, does some work and pushes the result.</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>Figure 4: OA for prod-cons|P/producer|.</figcaption></figure>

The first OA decides when the second can evolve by involving its hole in a transition: the action emitted when $A_p$ makes a transition is synchronised with the action of the hole $k$ in transitions of $A_c$.

**Example 2.** Fig. 3 shows a producer automaton and a consumer automaton that can be used to fill the holes P and Q of prod-cons defined in Example 1.

The OA on Fig. 4 is the composition of the system in Fig. 2 and the producer in Fig. 3 (left). The composition consists of two states (the product of the states of both automata). The transitions from one state to another come from the synchronisation of the transitions of the encompassing automaton with those of the producer filling the hole P. Transitions involving Q remain unchanged. $\square$

## 2.3 Relations between Open Automata

Establishing semantic equivalences and simulation relations between different OA requires to compare their states. For this purpose, we suppose that the variables of the two OA are disjoint (a renaming of variables may have to be applied before comparing OA states).

**Definition 4** (Relation on open automata configurations). Suppose $V_1$ and $V_2$ are disjoint. A relation on configurations of two OA $\langle S_1, s_{01}, V_1, \sigma_{01}, J_1, T_1 \rangle$ and $\langle S_2, s_{02}, V_2, \sigma_{02}, J_2, T_2 \rangle$ is a function $\mathcal{R} : S_1 \times S_2 \to \mathcal{R}_{V_1 \uplus V_2}$.

The idea is that two states are related depending on the satisfiability of the expression relying their variables, i.e., if the variables of the OA verify a certain formula. In other words, to each pair of states is attached a boolean formula that may refer to the variables of each of the two OA, stating whether the two states are related or not. Additionally, we say that the relation $\mathcal{R}$ relates the initial states of the automata if: $\sigma_{01} \uplus \sigma_{02} \vdash \mathcal{R}(s_{01}, s_{02})$.
## 2.4 A Bisimulation for Open Automata

Bisimulation between OA was defined in [6]. We show below the principles of this bisimulation. We first recall the usual definition of bisimulation. Bisimulation can be defined as follows for standard transition systems:

**Definition 5 (Classical Bisimulation).** A bisimulation is a relation $\mathcal{R}$ such that if $s \mathcal{R} t$ then:

$$ \forall l \ s', \ s \xrightarrow{l} s' \implies \exists t'. \ s' \ \mathcal{R} \ t' \wedge t \xrightarrow{l} t' $$

and conversely

$$ \forall l \ t', \ t \xrightarrow{l} t' \implies \exists s'. \ s' \ \mathcal{R} \ t' \wedge s \xrightarrow{l} s' $$

$$ \begin{array}{ccc} & s & \mathcal{R} \ t \\ l & \searrow & \searrow l \\ s' & \mathcal{R} & t' \end{array} \qquad \text{i.e.} $$

$s$ and $t$ are bisimilar, written $s \sim t$ iff there is a bisimulation relation $\mathcal{R}$ such that $s \mathcal{R} t$

A bisimulation relation relates pair of states and ensures that any behaviour of one automaton can be performed by the other one while staying in relation. We informally explain here the symbolic nature of the bisimulation for OA and the related complexity of its definition. The presence of holes in fact raises no strong difficulty but the variables must be handled carefully. Consider the two following simple OA:

<figure><img src="image_9.png" /></figure>

We should be able to consider these two OA as bisimilar. Both can input any $\beta(x)$ input on their hole and stores the value of $x$, emitting $\alpha(x)$ along the transition. The difference is the way $x$ is stored. We can then define a configuration relation $\mathcal{R}$ such that $\mathcal{R}(s, s_2)$ is true and $\mathcal{R}(t, t_2)$ holds when $z \ge 0$ and $y = z$, while $\mathcal{R}(t', t_2)$ holds when $z < 0$ and $y = -z$. This illustrates relation on configurations, but also shows that bisimulation on OA is more complex than in the classical case. Indeed, we need two transitions on the left OA to simulate a single one on the right OA. We should check that these two transitions cover all the cases accepted by the right hand side OA, and of course that destination states are in relation. Formally, FH-bisimulation is defined as follows [6]:

**Definition 6 (Strong FH-bisimulation).**

Suppose $\langle S_1, s_{01}, V_1, \sigma_{01}, J_1, T_1 \rangle$ and $\langle S_2, s_{02}, V_2, \sigma_{02}, J_2, T_2 \rangle$ are OA with identical holes of the same sort, with disjoint sets of variables ($V_1 \cap V_2 = \emptyset$).

Then $\mathcal{R}$, a relation on configurations of OA, is an FH-bisimulation if and only if for any states $s \in S_1$ and $t \in S_2$, we have the following:

* For any open transition OT in $T_1$: $\frac{\beta_j^{j \in J'} \cdot g_{OT}, \psi_{OT}}{s \xrightarrow{\alpha} s'}$ there exists an indexed set of open transitions $OT_x^{x \in X} \subseteq T_2$: $\frac{\beta_{j_x}^{j \in J_x} \cdot g_{OT_x}, \psi_{OT_x}}{t \xrightarrow{\alpha_x} t_x}$ such that $\forall x. J' = J_x$ and there exists $Pred_{s',t_x}$ such that $(s', t_x | Pred_{s',t_x}) \in \mathcal{R}$ and

$$ \mathcal{R}(s,t) \wedge g_{OT} \implies \bigvee_{x \in X} (\forall j. \beta_j = \beta_{jx} \wedge g_{OT_x} \wedge \alpha = \alpha_x \wedge \mathcal{R}(s', t_x \psi_{OT} \oplus \psi_{OT_x})) $$
* and symmetrically any open transition from *t* in *T*₂ can be covered by a set of transitions from *s* in *T*₁.

Two automata are bisimilar if there exists a strong FH-bisimulation $\mathcal{R}$ that relates their initial states.

Note that this definition matches an open transition $t_1$ to a family of covering open transitions $t_{2x}^{x \in X}$. Intuitively, this means that for every pair of related states $(s_1, s_2)$ of the two automata, and for every transition of the first automaton from $s_1$, there is a set of matching transitions of the second automaton from $s_2$ such that the produced action match, the actions of the same holes and the successors are related after variable update. Technically, the following sections do not rely on the definition of strong bisimulation on OA, but they follow the same principles and in particular the same way to faithfully simulate an open transition by a set of other open transitions.

## 2.5 Reachability

We finally define a new predicate abstracting state reachability for OA, it allows us to reason on reachable states in an automaton. It can be seen as an abstraction of the reachable states under the form of a predicate that must stay verified along the execution of the OA.

**Definition 7 (Reachability).** For any OA $A = \langle S, s_0, V, \sigma_0, J, T \rangle$, a reachability predicate $\check{\forall}_A : S \to \mathcal{F}_V$ is any predicate on states that is valid on initial state, and preserved across transitions:

$$ \sigma_0 \vdash \check{\forall}_A(s_0) \quad \wedge \quad \forall t = \frac{\beta_j^{j \in J'}, g, \psi}{s \underset{\alpha}{\to} s'} \in T, \text{vars}(t) \vdash (\check{\forall}_A(s) \wedge g \implies \check{\forall}_A(s') \{\psi\}) $$

Reachability takes into account all paths, and can over-approximate the reachable configurations. From an automation point of view, finding the most precise reachability predicate for a given automaton is not decidable because of the symbolic nature of OA, but only an over-approximation is necessary.

## 3 Simulation for Automata with the Same Holes

Similarly to FH-bisimulation [6] we are interested in finding simulation relations between configurations of two OA that contain variables and holes. When dealing with open systems it is common to define simulation in terms of a simulation relation. We rely on a classical notion of simulation inspired from [6]. The idea is to consider two configurations related by a relation; if one state can do a transition, then the other can also make this transition. Like for bisimulation, a simulation relation characterises when two states are related, and this characterisation is expressed as a predicate on the variables of the two automata. Simulation defines conditions on a relation $\mathcal{R}$ such that $\mathcal{R}(s_1, s_2)$ is a predicate (possibly involving variables of the automata) that is true when the state $s_1$ of $A_1$ simulates the state $s_2$ of $A_2$.

However here we want to build a simulation relation that also guarantees that no deadlock is introduced when refining the automaton. This property is quite frequent in simulation relation, and referred to as lack of new deadlocks [18] or complete simulation [21]. The notion of deadlock should however be specialised to our OA. Indeed, the possible transitions are better characterised by the guards of the outgoing transitions from a given state, rather than the simple existence of a transition. We thus define a deadlock reduction criterion based on how the outgoing transitions are guarded. As such, a simulation does not introduce deadlocks if in the conditions where no
transition is possible in the refined automaton, no transition were already possible in the more general one. More formally, for any pair of states $s_1$ and $s_2$ we introduce a criterion of the form:

$$ \forall(s_1, s_2) \in S_1 \times S_2, V_1 \uplus V_2 \vdash \mathcal{R}(s_1, s_2) \wedge \neg(\bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1)) \implies \neg(\bigvee_{t_2 \in \text{OT}(s_2)} \text{guard}(t_2)) $$

Which can be rewritten as:

$$ \forall(s_1, s_2) \in S_1 \times S_2, V_1 \uplus V_2 \vdash \mathcal{R}(s_1, s_2) \implies (\bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1)) \vee (\bigvee_{t_2 \in \text{OT}(s_2)} \text{guard}(t_2)) $$

Both statements being equivalent, as each of them may reveal more intuitive than the other in different situations, we use them interchangeably. We can now state the definition of simulation between OA that have the same set of holes.

**Definition 8 (Hole-equal simulation).** Consider two OA with identical set of holes: $A_1 = \langle S_1, s_{01}, V_1, \sigma_{01}, J_1, T_1 \rangle$ and $A_2 = \langle S_2, s_{02}, V_2, \sigma_{02}, J_2, T_2 \rangle$ where $J_1 = J_2$, the relation on configurations $\mathcal{R}: S_1 \times S_2 \to \mathcal{F}_{V_1 \uplus V_2}$ is a hole-equal simulation from $A_1$ to $A_2$ if the following conditions hold:

$$ (1) \quad \sigma_{01} \uplus \sigma_{02} \vdash \mathcal{R}(s_{01}, s_{02}) $$

$$ (2) \quad \forall (s_1, s_2) \in S_1 \times S_2, $$

$$ \begin{gathered} \forall t_1 = \frac{\beta_{1j}^{j \in J}, g_1, \psi_1}{s_1 \xrightarrow{\alpha_1} s'_1} \in \text{OT}(s_1). \quad \exists \left( t_{2x} = \frac{\beta_{2xj}^{j \in J}, g_{2x}, \psi_{2x}}{s_2 \xrightarrow{\alpha_{2x}} s'_{2x}} \right)_{x \in X} \in \text{OT}(s_2). \\ V_1 \uplus V_2 \uplus \text{vars}(t_1) \uplus \bigcup_x \text{vars}(t_{2x}) \vdash \end{gathered} $$

$$ \mathcal{R}(s_1, s_2) \wedge g_1 \implies \bigvee_{x \in X} \left( \begin{array}{l} \alpha_{2x} = \alpha_1 \wedge \bigwedge_{j \in J} \beta_{2xj} = \beta_{1j} \wedge \\ g_{2x} \wedge \mathcal{R}(s'_1, s'_{2x}) \{\psi_{2x} \uplus \psi_1\} \end{array} \right) $$

(3) Deadlock reduction:

$$ \forall(s_1, s_2) \in S_1 \times S_2, V_1 \uplus V_2 \vdash \mathcal{R}(s_1, s_2) \implies (\bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1)) \vee (\bigvee_{t_2 \in \text{OT}(s_2)} \text{guard}(t_2)) $$

If there is a hole-equal simulation from $A_1$ to $A_2$, then we say that $A_2$ simulates $A_1$; we denote it $A_2 \le A_1$.

The first and second conditions coincide with the natural way to prove inductively that an automaton simulates another by starting with the initial state. The third condition ensures that simulation prevents the introduction of deadlocks. Our definition captures a simple simulation for OA with the same holes that is more expressive than a strict simulation since it matches a transition with a family of transitions. For example, with such a relation we are able to check the simulation between two OA that differ by duplicated states, removed duplicated transitions, reinforced guards, different variables, etc. We will show in Section 5 that this simulation relation has good properties in terms of transitivity, compositionality, and reflexivity.

**Example 3.** To illustrate the simulation of OA, we consider a variation on the prod-cons example. Namely, we suppose that the two processes P and Q communicate through a one-place buffer. Fig. 5 shows the OA modelling this simpler version of the system, that we refer to as simprod-cons. We can easily check that this automaton simulates the one of Fig. 2. Indeed, one can see that $\mathcal{R} = \{(r_0, s_0) \to l = f, (r_0, s_1) \to f = l + 1\%N\}$ is a simulation relation. It follows that $\text{prod-cons} \le \text{simprod-cons}$. $\square$
The simulation relation defined above is insufficient in the setting of composition which is the main advantage of the OA-based approach. Indeed, it should be possible to refine an automaton by filling its hole, providing a concrete view of a part of the application that was not specified originally. More generally, it should be possible to relate automata that do not have the same holes because composition is a crucial part of system specification. However, filling holes can result in a system with more or less holes than the original system because the plugged subsystem can contain itself many holes. Next section defines a more powerful simulation relation able to reason on automata with different sets of holes.

# 4 A Simulation Relation that Takes Holes into Account

This section extends the preceding relation to automata where the set of holes is not the same. This is particularly useful to state whether the automaton after composition is a simulation of the original automaton or not. Indeed, when composing the set of holes changes. Being able to compare automata with only some of their holes in common seems useful in general.

One major challenge in the extension of simulation to different sets of holes is to maintain a form of transitivity while being able to take into account the actions of some of the holes. A naive definition of simulation would ensure that only the holes that are identical in the two OA are taken into account in the simulation. Unfortunately, considering all the common holes does not ensure transitivity of the simulation for the following reason. If $A_1$ simulates $A_2$ and $A_2$ simulates $A_3$, and one hole $j$ appears in $A_3$ and in $A_1$ but not in $A_2$ then we have no guarantee on the way $A_1$ and $A_3$ take the actions of this hole into account, thus a simulation between and $A_1$ and $A_3$ would require conditions involving actions of the hole $j$ which cannot be ensured. The way we solve this issue is to remember in the simulation relation which holes have been compared. This makes the relation parameterised by a subset of the set of holes that belong to the two automata that we want to take into account. This way, in the example above, we would have no guarantee on actions the hole $j$ by transitivity but can state a simulation relation with guarantees on the actions of the other holes.

In the following definition we add a parameter $H$ which is the set of holes tracked by the simulation relation and adapt the definition by ignoring actions of the holes that are not in $H$.

**Definition 9 (Hole-tracking simulation).** For two OA

$A_1 := \langle S_1, s_{01}, J_1, V_1, \sigma_{01}, T_1 \rangle$ and $A_2 := \langle S_2, s_{02}, J_2, V_2, \sigma_{02}, T_2 \rangle$, $A_1$ is a simulation of $A_2$ track-
ing holes $H$, noted $A_1 \leq_H A_2$, with $H \subseteq J_1 \cap J_2$, if there is a relation on configurations
$\mathcal{R} : (S_1 \times S_2) \to \mathcal{J}_{V_1 \prec V_2}$ such that:

$$
(1) \quad \sigma_{01} \prec \sigma_{02} \vdash \mathcal{R}(s_{01}, s_{02})
$$

<figure><img src="image_10.png" /><figcaption>Figure 5: The simprod-cons OA: the system using one-place buffer.</figcaption></figure>
$$ (2) \quad \forall (s_1, s_2) \in S_1 \times S_2, $$

$$ \forall \substack{\beta_{1j}^{j \in J_1'}, g_1, \psi_1 \\ s_1 \xrightarrow{\alpha_1} s_1} \in \text{OT}(s_1), \exists \left( \substack{\beta_{2xj}^{j \in J_2'x}, g_{2x}, \psi_{2x} \\ s_2 \xrightarrow{\alpha_{2x}} s_2'} \in \text{OT}(s_2) \right)^{x \in X}, $$

$$ (\forall x \in X, J_{2x}' \cap H = J_1' \cap H) \wedge $$

$$ V_1 \uplus V_2 \uplus \text{vars}(t_1) \vdash $$

$$ \left( \mathcal{R}(s_1, s_2) \wedge g_1 \implies \bigvee_{x \in X} \left( \substack{ \alpha_1 = \alpha_{2x} \wedge \bigwedge_{j \in J_{2x}'} \beta_{1j} = \beta_{2xj} \wedge \\ g_{2x} \wedge \mathcal{R}(s_1', s_2') \{\psi_1 \uplus \psi_{2x}\} } \right) \right) $$

(3) Deadlock reduction:

$$ \forall (s_1, s_2) \in S_1 \times S_2, V_1 \uplus V_2 \vdash \mathcal{R}(s_1, s_2) \implies (\bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1)) \vee (\neg (\bigvee_{t_2 \in \text{OT}(s_2)} \text{guard}(t_2))) $$

Note that every action of the holes outside $H$ is unconstrained according to the simulation relation.

**Property 1 (Relating simulations).** Hole-equal simulation is a particular case of hole-tracking simulation when $J_1 = J_2 = H$.

**Example 4.** Consider the automata of Examples 1 and 3. As we saw above, prod-cons $\leq$ simprod-cons, therefore prod-cons $\leq_{\{p,q\}}$ simprod-cons.

**Property 2 (Tracked holes).** By construction, if an automaton is the simulation of another one, it is also a simulation by tracking less holes.

$$ A_1 \leq_H A_2 \wedge H' \subseteq H \implies A_1 \leq_{H'} A_2 $$

Now that we have a simulation relation that takes both variable parameters and process parameters into account, we would like to ensure that it has properties one would expect for a simulation relation.

# 5 Properties of our Simulation Relations

Before reasoning on the properties of simulation, we need to introduce one additional notion that characterises when the composition of two automata does not introduce new blocked transitions.

## 5.1 Non-blocking Composition

Unfortunately, the deadlock reduction property in the definition of simulation is not compositional: the composition operator can itself introduce a deadlock. In other words, when filling the hole of two related automata with a third one, even if there is a deadlock reduction between the two original automata, there might not be a deadlock reduction in the composed ones. The same problem may arise when two related automata are composed in the same hole of a third one.

This creates a conflict between deadlock reduction and the properties involving composition. We call non-blocking composition a composition that can safely be used to compose OA that are involved in a deadlock reducing relation.
**Definition 10 (Non-blocking composition).** Consider two OA:

$A_1 := \langle S_1, s_{01}, V_1, \sigma_{01}, J_1, T_1 \rangle$ and $A_2 := \langle S_2, s_{02}, V_2, \sigma_{02}, J_2, T_2 \rangle$. Let A be the OA resulting from the composition $A = A_1[A_2/k] = \langle S, s_0, V, \sigma_0, J, T \rangle$. The composition $A_1[A_2/k]$ is non-blocking if A has a reachability predicate such that, for each reachable configuration, if there is a possible transition in $A_1$ then there is a possible transition in A:

$$ \forall s = (s_1, s_2) \in S, V \uplus \bigcup_{t \in \text{OT}(s_1)} vars(t) \vdash \left( \check{A}(s) \wedge \bigvee_{t \in \text{OT}(s_1)} guard(t) \implies \bigvee_{t \in \text{OT}(s)} guard(t) \right) $$

Like in the definition of simulation (Definition 8) we use guards to ensure that the transition can occur. In general, one would not want to only consider non-blocking composition as it may reveal a bit restrictive, but it is the best necessary condition that can be identified for compositionality of simulation. It will be used to prove composition theorems given below. In absence of non-blocking composition, simulation may also be checked specifically for a given composed automaton.

## 5.2 Properties

We now state the properties of our simulation, their proofs can be found in the appendices. We express these properties in terms of hole-tracking simulation because, thanks to Property 1 all the properties of hole-tracking simulation are also valid for hole-equal simulation. The first crucial theorem of simulation is that it is a preorder on the set of OA. This latter enables stepwise refinement.

**Theorem 1 (Simulation is a preorder).** Hole-tracking simulation is reflexive and transitive: it is a preorder on the set of OA.

*Proof sketch.* The relation $\leq_H$ is reflexive, $A \leq_H A$. This is shown by considering the relation $\mathcal{R}$ such that $\mathcal{R}(s_1, s_2) \triangleq s_1 = s_2 \wedge \bigwedge_{v \in vars(s_1)} v = v$ we can prove the conditions for Definition 9.

Appendix A presents the proof of transitivity. It is done classically by identifying the relation between $A_1$ and $A_3$ that is a simulation. What is less classical is the definition of this relation because it is a boolean formula. For each couple of states $s_1$ and $s_3$ of $A_1$ and $A_3$ we build a formula that defines the simulation. To do this, we take the disjunction of formulas relating $s_1$ and $s_3$, and passing by all states $s_2$ of $A_2$. More precisely, we define a relation of the following form:

$$ \mathcal{R}_{13}(s_1, s_3) = \bigvee_{s_2 \in S_2} (\mathcal{R}_{12}(s_1, s_2) \wedge \mathcal{R}_{23}(s_2, s_3)) $$

We then prove that this relation is a simulation, according to Definition 9. $\square$

<figure><img src="image_11.png" /></figure>

The next theorem states that if two automata are in simulation relation and the same automaton is placed in the same hole of the two automata, then the simulation is preserved. This is the first step toward proving that simulation is compositional in the sense that it is sufficient to prove simulation for the composed automata separately to obtain a simulation relation.

**Theorem 2 (Context refinement).** Let $A_1, A_2$ and $A_3$ be three OA with $A_1 \leq_H A_2$. Let $J_3$ be the set of holes of $A_3$ and suppose that $k \in H$. Suppose additionally that $A_1[A_3/k]$ is non-blocking. We have:

$$ A_1[A_3/k] \leq_{J_3 \uplus H \setminus \{k\}} A_2[A_3/k] $$
**Proof sketch.** The proof relies on a simulation relation that we consider is the one that makes $A_1$ and $A_2$ similar, complemented with identity of configurations for $A_3$. Then, by construction, all transitions of the composed automaton $A_1[A_3/k]$ are specified by open transitions of $A_1$. For the transitions that do not involve hole $k$, the transition of $A_1[A_3/k]$ is the same and simulation between $A_1$ and $A_2$ allows us to conclude directly. If the hole $k$ is involved the considered relation implies that valuations in $A_3$ are equal (i.e., the value for each variable are the same in both valuations), after a transition we should obtain “equal” valuations because post-conditions are deterministic. □

**Example 5.** Consider again the prod-cons and simprod-cons automata given in the examples above. Since prod-cons $\leq_{\{P,q\}}$ simprod-cons, then according to Theorem 2, we have prod-cons[producer/P] $\leq_{\{q\}}$ simprod-cons[producer/P].

The automaton of prod-cons[producer/P] is shown in Fig. 4. The automaton resulting from the composition of simprod-cons and producer is bigger and not shown here.

**Theorem 3 (Congruence).** Let $A_1, A_2$ and $A_3$ be three OA with $A_2 \leq_H A_3$. Let $J_1$ be the set of holes of $A_1$ and suppose that $k \in J_1$. Suppose additionally that the composition $A_1[A_2/k]$ is non-blocking. We have:

$$A_1[A_2/k] \leq_{J_1 \oplus H \setminus \{k\}} A_1[A_3/k]$$

Consequently, as the simulation is transitive we can compose the previous theorems and state the following:

**Theorem 4 (Composability).** Let $A_1, A_2, A_3$ and $A_4$ be four OA with $A_1 \leq_H A_2$ and $A_3 \leq_{H'} A_4$. Suppose that $k \in H$. We have:

$$A_1[A_3/k] \leq_{H \oplus H' \setminus \{k\}} A_2[A_4/k]$$

**Example 6.** As an example of the use of this theorem, if we design a refined version of the producer process of Example 2 called Refproducer. According to Theorem 4, we have prod-cons[producer/P] $\leq_{\{q\}}$ simprod-cons[Refproducer/P].

Note that the substitution operation can be extended to a multiple substitution that fills several holes at the same time, and the theorems can be adapted accordingly.

# 6 Related Work

The origins of refinement are in the approach of programming that aims to provide solid foundations for building correct programs [12]. Many work contributed to the development of elaborated notions of refinement in various area (e.g. [7, 10, 8]). In the context of process algebra, refinement between processes can be defined in terms of simulations relation (e.g. ([17, 20]). However, the concept of simulations presented so far has focused on the refinement of systems that are inherently closed, i.e., systems which are bounded and without environment,

The simulation ensures the preservation of safety properties as deadlock-freeness and, more generally, all linear temporal logic properties [1, 18]. The difference between the existing refinement principles have been studied in [13], for example the authors explain in what sense failure semantics is different from (bi)simulation in the compared systems and properties ensured. In this paper we particularly focus on the compositionality of simulation-based refinement.

There are not a lot of works that study refinement for open systems. Defining refinement of open systems as trace inclusion is addressed as a notion of subtyping in type theory (e.g.
[14, 9]). The definition of refinement is based on a connection between session types and communicating automata theories – a notion of session automata based on Communicating Finite-State Machines, that are used for modelling processes communicating through FIFO channels. The refinement of open systems is also defined in terms of alternating simulation [4, 3]. Alternating simulation is originating from the game theory [2], it allows the study of relation between individual components by viewing them as alternating transition systems. In particular, a refinement of game-based automata expresses that the refined component can offer more services (input actions) and fewer service demands (output actions). However, the composition of such automata may lead to illegal states, where one automaton issues an output that is not acceptable as input in the other one. The theory of alternating simulation provides an optimistic approach to compute compatibility between automata based on the fact that each automaton expects the other to provide legal inputs, i.e., two components can be composed if there is an environment where they can work together. Our approach has some commonalities with the above mentioned simulation [3]: both are process-oriented approaches even if they are not based on the same notion of simulation, and both include in the model how to compose and interact with processes that are accepted as parameters. Nevertheless, they differ in that our approach focuses on the compositional properties of the simulation, and not on the fact that entities can be composed.

Previous works on OA focused on equivalence relations compatible with composition. In [16], a computable bisimulation is introduced, while in [6] a weak version of the bisimulation is introduced. In this paper we tackle the refinement relation in the form of simulation, as is the case for the corresponding relations on labelled transition systems [8]. Unlike the standard simulation we deal with symbolic and open models. In [23], the authors exploit transition systems to reason about the systems that are partially specified by using variables, making the state space potentially infinite.

Some work target component-based refinement with the concern of preserving deadlock freedom (e.g. [11, 18]). These works are not concerned with the theory of open symbolic systems, and therefore do not focus on the same modularity as we do, in particular we provide preservation of refinement by composition.

# 7 Conclusion

In this article we investigated the notion of refinement for a symbolic and open model: open automata. OA are convenient for compositional software verification. Indeed, OA model parallel systems that are parameterised both by the use of variables and by the possibility to compose automata. The formalism supports compositional specification through the simulation paradigm. In this paper, we introduce a refinement relation between open automata. It relies on a simulation relation between the two automata; it specifies that the refined process must follow the behaviour of the simulated one. We finally showed that simulation is a preorder that is preserved by composition, both when filling a hole and when placing automata in comparable contexts.

# References

[1] Abrial, J.R.: The B-book - Assigning programs to meanings. Cambridge University Press (1996)

[2] de Alfaro, L.: Game models for open systems. In: Dershowitz, N. (ed.) Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th
Birthday. Lecture Notes in Computer Science, vol. 2772, pp. 269-289. Springer (2003).
https://doi.org/10.1007/978-3-540-39910-0_12

[3] de Alfaro, L., Henzinger, T.A.: Interface automata. In: Tjoa, A.M., Gruhn, V. (eds.) Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2001, Vienna, Austria, September 10-14, 2001. pp. 109-120. ACM (2001).
https://doi.org/10.1145/503209.503226

[4] Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR'98 Concurrency Theory. pp. 163-178. Springer Berlin Heidelberg, Berlin, Heidelberg (1998)

[5] Ameur-Boulifa, R., Henrio, L., Kulankhina, O., Madelaine, E., Savu, A.: Behavioural semantics for asynchronous components. Journal of Logical and Algebraic Methods in Programming **89**, 1-40 (2017). https://doi.org/10.1016/j.jlamp.2017.02.003, https://www.sciencedirect.com/science/article/pii/S2352220817300287

[6] Ameur-Boulifa, R., Henrio, L., Madelaine, E.: Compositional equivalences based on open pNets. Journal of Logical and Algebraic Methods in Programming **131**, 100842 (2023). https://doi.org/10.1016/j.jlamp.2022.100842, https://www.sciencedirect.com/science/article/pii/S2352220822000955

[7] Back, R., Sere, K.: Stepwise refinement of parallel algorithms. Science of Computer Programming **13**(2), 133-180 (1990). https://doi.org/10.1016/0167-6423(90)90069-P, https://www.sciencedirect.com/science/article/pii/S016764239090069P

[8] Bellegarde, F., Julliand, J., Kouchnarenko, O.: Ready-simulation is not ready to express a modular refinement relation. In: Maibaum, T. (ed.) Fundamental Approaches to Software Engineering. pp. 266-283. Springer Berlin Heidelberg, Berlin, Heidelberg (2000)

[9] Bravetti, M., Zavattaro, G.: Asynchronous session subtyping as communicating automata refinement. Softw. Syst. Model. **20**(2), 311-333 (2021). https://doi.org/10.1007/s10270-020-00838-x

[10] Butler, M.J., Grundy, J., Långbacka, T., Ruksenas, R., von Wright, J.: The refinement calculator: Proof support for program refinement. In: Groves, L., Reeves, S. (eds.) Proc. Conf. Formal Methods Pacific'97, Springer Series in Discrete Mathematics and Theoretical Computer Science (01/01/97). pp. 40-61 (1997), https://eprints.soton.ac.uk/250550/

[11] Dihego, J., Sampaio, A., Oliveira, M.: A refinement checking based strategy for component-based systems evolution. Journal of Systems and Software **167**, 110598 (2020).
https://doi.org/10.1016/j.jss.2020.110598

[12] Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)

[13] Eshuis, R., Fokkinga, M.M.: Comparing refinements for failure and bisimulation semantics. Fundam. Inf. **52**(4), 297-321 (Apr 2002)

[14] Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica **42**(2-3), 191-225 (2005). https://doi.org/10.1007/s00236-005-0177-z
[15] Henrio, L., Madelaine, E., Zhang, M.: A theory for the composition of concurrent processes. In: Albert, E., Lanese, I. (eds.) Formal Techniques for Distributed Objects, Components, and Systems. pp. 175–194. Springer International Publishing, Cham (2016)

[16] Hou, Z., Madelaine, E.: Symbolic bisimulation for open and parameterized systems. In: Proceedings of the 2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. pp. 14–26. PEPM 2020, Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3372884.3373161

[17] Jifeng, H.: Process simulation and refinement. Form. Asp. Comput. 1(1), 229–241 (mar 1989). https://doi.org/10.1007/BF01887207, https://doi.org/10.1007/BF01887207

[18] Kouchnarenko, O., Lanoix, A.: How to verify and exploit a refinement of component-based systems. In: Virbitskaite, I., Voronkov, A. (eds.) Perspectives of Systems Informatics. pp. 297–309. Springer Berlin Heidelberg, Berlin, Heidelberg (2007)

[19] Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., USA (1989)

[20] Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol. 92. Springer (1980). https://doi.org/10.1007/3-540-10235-3

[21] Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2012), https://hal.inria.fr/hal-00907026

[22] Wang, B., Madelaine, E., Zhang, M.: Symbolic Weak Equivalences: Extension, Algorithms, and Minimization - Extended version. Research Report RR-9389, Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France ; East China Normal University (Shanghai) (Jan 2021), https://hal.inria.fr/hal-03126313

[23] Zhang, L., Meng, Q., Lo, K.: Compositional abstraction refinement for component-based systems. Journal of Applied Mathematics **2014**, 1–12 (2014). https://doi.org/10.1155/2014/703098
A Proof of Transitivity for Refinement (Theorem 1)

If $A_1 \leq_H A_2$ and $A_2 \leq_{H'} A_3$, then $A_1 \leq_{H \cap H'} A_3$.

*Proof.* If $A_1 \leq_H A_2$ then there is $\mathcal{R}_{12}$ a relation between states of $A_1$ and of $A_2$; If $A_2 \leq_{H'} A_3$ then there is $\mathcal{R}_{23}$ a relation between states of $A_2$ and of $A_3$. We build a relation between states of $A_1$ and of $A_3$ as follows: for each pair of states $s_1, s_3$, for each state $s_2$ such that $\mathcal{R}_{12}$ relates $s_1$ and $s_2$, and $\mathcal{R}_{23}$ relates $s_2$ and $s_3$. Let $\mathcal{R}_{13}$ be the relation:

$$ \mathcal{R}_{13}(s_1, s_3) = \bigvee_{s_2 \in S_2} (\mathcal{R}_{12}(s_1, s_2) \wedge \mathcal{R}_{23}(s_2, s_3)) $$

We will show that $A_1 \leq_{H \cap H'} A_3$ by exhibiting $\mathcal{R}_{13}$ as a hole-tracking simulation of $A_1$ by $A_3$.

We have to prove that the relation $\mathcal{R}_{13}$ satisfies the three conditions of the definition of a refinement of OA.

1. Firstly, we have to $\mathcal{R}_{13}$ satisfies initial configurations:

$$ \sigma_{01} \oplus \sigma_{03} \vdash \mathcal{R}_{13}(s_{01}, s_{03}) $$

By knowing that substitutions only have an effect on the variables of the OA they belong to, they also produce terms containing only variables of the OA they belong to. We have:

$$ \begin{align*} (\sigma_{01} \oplus \sigma_{02} \vdash \mathcal{R}_{12}(s_{01}, s_{02})) \wedge (\sigma_{02} \oplus \sigma_{03} \vdash \mathcal{R}_{23}(s_{02}, s_{03})) &\implies \\ \mathcal{R}_{12}(s_{01}, s_{02}) \{\sigma_{01} \oplus \sigma_{02}\} \wedge \mathcal{R}_{23}(s_{02}, s_{03}) \{\sigma_{02} \oplus \sigma_{03}\} &\implies \\ \mathcal{R}_{12}(s_{01}, s_{02}) \wedge \mathcal{R}_{23}(s_{02}, s_{03}) \{\sigma_{01} \oplus \sigma_{02} \oplus \sigma_{03}\} &\implies \\ \underbrace{\mathcal{R}_{12}(s_{01}, s_{02}) \wedge \mathcal{R}_{23}(s_{02}, s_{03})}_{\implies \mathcal{R}_{13}(s_{01}, s_{03})} \{\sigma_{01} \oplus \sigma_{02} \oplus \sigma_{03}\} &\implies \end{align*} $$

Since $\sigma_{02}$ has no effect on variables of $s_{01}$ and $s_{03}$ thus we get the expected result.

2. Secondly, we need to prove that for any open transition $t_1$ in $T_1$ originating from $s_1$:

$$ \frac{\beta_{1j}^{j \in J'_1}, g_1, \psi_1}{s_1 \xrightarrow{\alpha_1} s'_1} \in \text{OT}(s_1) $$

there exists an indexed family of OTs originating from $s_3$:

$$ V_1 \oplus V_3 \oplus vars(t_1) \vdash $$

$$ \left( R_{13}(s_1, s_3) \wedge g_1 \implies \bigvee_{z \in Z} \left( \begin{array}{l} \alpha_1 = \alpha_{3z} \wedge \bigwedge_{j \in J'_{3z} \wedge (H \cap H')} \beta_{1j} = \beta_{3jz} \wedge \\ g_{3z} \wedge R_{12}(s'_1, s'_{3z}) \{\psi_1 \oplus \psi_{3z}\} \end{array} \right) \right) $$

The proof of this simulation step follows the same principles as the one given in [6] for the proof of transitivity of bisimulation<fnref n="2" />. It relies on the fact that one open transition of $A_1$ is simulated by a family of open transitions of $A_2$, and one open transition of $A_2$ is simulated by a family of open transitions of $A_3$. Transitivity leads to a doubly indexed family of simulating open transition.

<footnote n="2">²In particular, the bisimulation relation exhibited for proving transitivity is the same.</footnote>
3. Lastly, we have to prove the satisfaction of the deadlock reduction condition. To build $\mathcal{R}_{13}$ we need to rely on the disjunction of all possible paths to relate $s_1$ and $s_3$, which leads to

$$ \mathcal{R}_{13}(s_1, s_3) = \bigvee_{p \in P} (\mathcal{R}_{12}(s_1, s_{2p}) \wedge \mathcal{R}_{23}(s_{2p}, s_3)) $$

Consider any $(s_1, s_3) \in \mathcal{R}_{13}$ there is a set of states $(s_{2p})^{p \in P}$ of $A_2$ relating $s_1$ and $s_3$.

First, according to the relation between $A_1$ and $A_2$ OA, for all $(s_1, s_{2p}) \in S_1 \times S_2$ we have:

$$ V_1 \oplus V_2 \vdash \mathcal{R}_{12}(s_1, s_{2p}) \implies \bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1) \vee \neg(\bigvee_{t_{2p} \in \text{OT}(s_{2p})} \text{guard}(t_{2p})) $$

Second, according to the relation between $A_2$ and $A_3$ OA, for all $(s_{2p}, s_3) \in S_2 \times S_3$ we have:

$$ V_2 \oplus V_3 \vdash \mathcal{R}_{23}(s_{2p}, s_3) \implies \bigvee_{t_1 \in \text{OT}(s_{2p})} \text{guard}(t_{2p}) \vee \neg(\bigvee_{t_3 \in \text{OT}(s_3)} \text{guard}(t_3)) $$

With the conjunction of both, we get:

$$ V_1 \oplus V_2 \oplus V_3 \vdash \mathcal{R}_{12}(s_1, s_{2p}) \wedge \mathcal{R}_{23}(s_{2p}, s_3) \implies \bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1) \vee \neg(\bigvee_{t_3 \in \text{OT}(s_3)} \text{guard}(t_3)) $$

This is valid for all $s_{2p} \in (s_{2p})^{p \in P}$, then we have:

$$ V_1 \oplus V_2 \oplus V_3 \vdash \underbrace{\bigvee_{p \in P} (R_{12}(s_1, s_{2p}) \wedge R_{23}(s_{2p}, s_3))}_{R_{13}(s_1, s_3)} \implies (\bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1)) \vee \neg(\bigvee_{t_3 \in \text{OT}(s_3)} \text{guard}(t_3)) $$

By removing the $A_2$ variables that have not effect on $A_2$ et $A_3$, we get the desired result:

$$ V_1 \oplus V_3 \vdash \mathcal{R}_{13}(s_1, s_3) \implies (\bigvee_{t_1 \in \text{OT}(s_1)} \text{guard}(t_1)) \vee \neg(\bigvee_{t_3 \in \text{OT}(s_3)} \text{guard}(t_3)) $$

□

## B Proof of Context Refinement (Theorem 2)

Suppose that $A_1 \leq_H A_2$, $k \in H$ and that $A_1[A_3/k]$ is non-blocking. We have:

$$ A_1[A_3/k] \leq_{J_3 \oplus H \setminus \{k\}} A_2[A_3/k] $$

Pictorially, the theorem states the following result:
<figure><img src="image_12.png" /></figure>

*Proof.* Let us denote by $A_{13}$ (resp. $A_{23}$) the OA resulting from $A_1[A_3/k]$ (resp. $A_2[A_3/k]$), to prove the theorem it is sufficient to prove that there exists a relation between states of the two OA that satisfies the conditions of Definition 9.

We denote $A_1 = \langle S_1, s_{01}, J_1, V_1, \sigma_{01}, T_1 \rangle$ and $A_2 := \langle S_2, s_{02}, J_2, V_2, \sigma_{02}, T_2 \rangle$ and $A_3 = \langle S_3, s_{03}, J_3, V_3, \sigma_{03}, T_3 \rangle$. The proof requires to rename the variables of one instance of the two $A_3$ automata to avoid clashes in variable names (this is required by the definition of refinement). In practice we will use superscripts 1 and 2 to distinguish elements of the two instances of $A_3$.

Let $\mathcal{R}$ be the refinement relation relating states of $A_1$ and $A_2$. Let us denote with $t^1$ and $t^2$ the elements of $A_1$ and $A_2$ respectively. Consider any two states $s_{13} = (s_1, s_3^1)$ and $s_{23} = (s_2, s_3^2)$ ($s_3^1$ and $s_3^2$ are the same with renaming). We define a relation $\mathcal{R}'$ relating states of $s_{13}$ and $s_{23}$ as follows:

$$ \mathcal{R}'(s_{13}, s_{23}) = \mathcal{R}(s_1, s_2) \wedge \mathcal{R}_{A_{13}}(s_{13}) \wedge \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 $$

We want to prove that $(\mathcal{R}', H \uplus J_3 \setminus \{k\})$ is a hole-tracking simulation of $A_{13}$ and $A_{23}$. In the following we denote $H' = H \cup J_3 \setminus \{k\}$.

1. First, we have to prove the relation for initial states:

$$ \sigma_{013} \uplus \sigma_{023} \vdash \mathcal{R}'(s_{013}, s_{023}) $$

with $\sigma_{013} = \sigma_{01} \uplus \sigma_{03}^1$, $\sigma_{023} = \sigma_{02} \uplus \sigma_{03}^2$, $s_{013} = (s_{01}, s_{03}^1)$, and $s_{023} = (s_{02}, s_{03}^2)$.

By using the fact that $\mathcal{R}$ relates initial configurations of $A_1$ and $A_2$, we have: $(\sigma_{01} \uplus \sigma_{02} \vdash \mathcal{R}(s_{01}, s_{02}))$.

Considering that initial valuations $\sigma_{03}^1$ and $\sigma_{03}^2$ associate the same values to the “same” variables modulo renaming, so the following holds:

$$ \left( \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \right) \{\{\sigma_{03}^1 \uplus \sigma_{03}^2\}\} $$

Additionally, because the domains of the substitution function are disjoint, the substitution function has an effect only on the related elements, we get:

$$ \begin{align*} & (\sigma_{01} \uplus \sigma_{02} \vdash \mathcal{R}(s_{01}, s_{02})) \\ & \implies \mathcal{R}(s_{01}, s_{02}) \{\{\sigma_{01} \uplus \sigma_{02}\}\} \wedge \left( \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \right) \{\{\sigma_{03}^1 \uplus \sigma_{03}^2\}\} \\ & \implies \left( \mathcal{R}(s_{01}, s_{02}) \wedge \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \right) \{\{\sigma_{01} \uplus \sigma_{02} \uplus \sigma_{03}^1 \uplus \sigma_{03}^2 \uplus \sigma_{013}\}\} \\ & \implies \sigma_{013} \uplus \sigma_{023} \vdash \mathcal{R}'(s_{013}, s_{023}) \end{align*} $$

The last step comes from the additional fact that $\mathcal{R}_{A_{13}}(s_{013})$.

2. Second, we need to prove for any open transition $t_{13}$ in $T_{13}$ originating from $s_{13}$:

$$ \frac{\beta_{13j}^{j \in J'_{13}}, g_{13}, \psi_{13}}{s_{13} \xrightarrow{\alpha_{13}} s'_{13}} \in \text{OT}(s_{13}) $$
there exists an indexed family $t_{23x}$ of OTs originating from $s_{23}$ that simulate it:

$$ \left( \frac{\beta_{23xj}^{j \in J'_{23x}}, g_{23x}, \psi_{23x}}{s_{23} \xrightarrow{\alpha_{23x}} s'_{23x}} \in \text{OT}(s_{23}) \right)^{x \in X} $$

such that $(\forall x \in X, J'_{23x} \cap H' = J'_{13} \cap H')$ and

$$ V_{13} \uplus V_{23} \uplus \text{vars}(t_{13}) \vdash $$

$$ \mathcal{R}'(s_{13}, s_{23}) \wedge g_{13} \implies \bigvee_{x \in X} \left( \begin{array}{l} \alpha_{13} = \alpha_{23x} \wedge \bigwedge_{j \in J'_{23x} \cap H'} \beta_{13j} = \beta_{23xj} \wedge \\ g_{23x} \wedge \mathcal{R}'(s'_{13}, s'_{23x}) \{\{\psi_{13} \uplus \psi_{23x}\}\} \end{array} \right) $$

Recall that by definition of composition and OA refinement we have:

$$ V_{13} = V_1 \uplus V_3^1 \text{ and } V_{23} = V_2 \uplus V_3^2 $$

$$ H' \subseteq J_3 \uplus (J_1 \cap J_2) \setminus \{k\} = (J_3 \uplus J_1 \setminus \{k\}) \cap (J_3 \uplus J_2 \setminus \{k\}) $$

First of all, we have by hypothesis $A_1 \leqslant_H A_2$, then for any open transition $t_1$ in $T_1$ originating from $s_1$:

$$ \frac{\beta_{1j}^{j \in J'_1}, g_1, \psi_1}{s_1 \xrightarrow{\alpha_1} s'_1} \in \text{OT}(s_1) $$

there exists an indexed family of OTs originating from $s_2$:

$$ \left( \frac{\beta_{2xj}^{j \in J'_{2x}}, g_{2x}, \psi_{2x}}{s_2 \xrightarrow{\alpha_{2x}} s'_{2x}} \in \text{OT}(s_2) \right)^{x \in X} $$

such that $\forall x \in X, J'_{2x} \cap H = J'_1 \cap H$ and

$$ V_1 \uplus V_2 \uplus \text{vars}(t_1) \vdash $$

$$ \mathcal{R}(s_1, s_2) \wedge g_1 \implies \bigvee_{x \in X} \left( \begin{array}{l} \alpha_1 = \alpha_{2x} \wedge \bigwedge_{j \in J'_{2x} \cap H} \beta_{1j} = \beta_{2xj} \wedge \\ g_{2x} \wedge \mathcal{R}(s'_1, s'_2) \{\{\psi_1 \uplus \psi_{2x}\}\} \end{array} \right) (*) $$

Consider any transition $t_{13}$ in $A_{13}$. Based on the definition of composition $t_{13}$ can be obtained from two different cases, we will consider the two cases separately.

**First case: Both automata perform a transition.** The transition $t_{13}$ is obtained by

the composition of transitions $t_1 = \frac{\beta_{1j}^{j \in J'_1}, g_1, \psi_1}{s_1 \xrightarrow{\alpha_1} s'_1} \in \text{OT}(s_1)$ and

$$ t_3^1 = \frac{(\beta_{3j}^1)^{j \in J'_3}, g_3^1, \psi_3^1}{s_3^1 \xrightarrow{\alpha_1} s_3^{1'}} \in \text{OT}(s_3^1) \quad \text{when } k \in J'_1 $$
The result is:

$$t_{13} = \frac{\beta_{1j}^{j \in J'_1 \setminus \{k\}} \uplus (\beta_{3j}^1)^{j \in J'_3}, g_1 \wedge g_3^1 \wedge \alpha_3^1 = \beta_{1k}, \psi_1 \uplus \psi_3^1}{(s_1, s_3^1) \xrightarrow{\alpha_1} (s'_1, s'_3^1)} \quad \text{where } k \in J'_1$$

We then obtain a family of OTs by the simulation of $A_1$ by $A_2$ (as stated above). By hypothesis we have $k \in H$, so in the case where $k \in J'_1$, we deduce that $k \in J'_{2x}$ we can then build a family of OTs $t_{23x}^{x \in X}$ with the same transitions of $A_3$ (up to renaming) as those used to build $t_{13}$.

$$t_{23x} = \left( \frac{\beta_{2xj}^{j \in J'_{2x} \setminus \{k\}} \uplus (\beta_{3j}^2)^{j \in J'_{2j}}, g_{2x} \wedge g_3^2 \wedge \alpha_3^2 = \beta_{2xk}, \psi_{2x} \uplus \psi_3^2}{(s_2, s_3^2) \xrightarrow{\alpha_{2x}} (s'_{2x}, s'_{3^2})} \right)^{x \in X}$$

Recall that in this case $k \in J'_1$, so $\forall x \in X$ we have

$$
\begin{align*}
J'_{23x} \cap H' &= ((J'_{2x} \setminus \{k\}) \uplus J_3^{2'}) \cap (H \uplus J_3 \setminus \{k\}) \\
&= ((J'_{2x} \cap (H \uplus J_3)) \uplus (J_3^{2'} \cap (H \uplus J_3))) \setminus \{k\} \\
&= ((J'_{2x} \cap H) \uplus (J_3^{2'} \cap J_3)) \setminus \{k\} \\
&\qquad \text{since } J_3 \cap J'_{2x} = \emptyset \text{ and } H \cap J_3^{2'} = \emptyset \\
&= ((J'_{2x} \cap H) \uplus J_3^{2'}) \setminus \{k\} \text{ since } J_3^{2'} \subseteq J_3 \\
&= ((J'_1 \cap H) \uplus J_3^{1'}) \setminus \{k\} \text{ since } J_3^{1'} = J_3^{2'} \text{ and } J'_1 \cap H = J'_{2x} \cap H \\
&= ((J'_1 \cap H) \uplus (J_3^{1'} \cap J_3)) \setminus \{k\} \text{ since } J_3^{1'} \subseteq J_3 \\
&= (J'_1 \cap (J_3 \uplus H)) \uplus ((J_3^{1'} \cap (J_3 \uplus H)) \setminus \{k\}) \\
&\qquad \text{since } J_3 \cap J'_1 = \emptyset \text{ and } H \cap J_3^{1'} = \emptyset \\
&= ((J'_1 \uplus J_3^{1'}) \setminus \{k\}) \cap ((J_3 \uplus H) \setminus \{k\}) \\
&= J'_{13} \cap H'
\end{align*}
$$

In this case the composition gives:

$$g_{13} \Leftrightarrow g_1 \wedge g_3^1 \wedge \alpha_3^1 = \beta_{1k} \text{ and } g_{23x} \Leftrightarrow g_{2x} \wedge g_3^2 \wedge \alpha_3^2 = \beta_{2xk}$$

As $k \in H$ we have $\beta_{1k} = \beta_{2xk}$ then we deduce:

$$g_3^1 \wedge \alpha_3^1 = \beta_{1k} \Leftrightarrow g_3^2 \wedge \alpha_3^2 = \beta_{2xk}$$

The proof of the rest is based on the following facts:

(a) By construction of $t_{13}$ and $t_{23x}$ we have $\alpha_{13} = \alpha_1$ and $\alpha_{23x} = \alpha_{2x}$. So we deduce: $\alpha_1 = \alpha_{2x} \Rightarrow \alpha_{13} = \alpha_{23x}$.

(b) By composition we have also:

$$\beta_{13j}^{j \in J'_{13}} = \beta_{1j}^{j \in J'_1 \setminus \{k\}} \uplus (\beta_{3j}^1)^{j \in J'_{3j}} \text{ and } \beta_{23xj}^{j \in J'_{23}} = \beta_{2xj}^{j \in J'_2 \setminus \{k\}} \uplus (\beta_{3j}^2)^{j \in J'_{3j}}$$

Therefore, we have for all $j \in J'_{13}$ (recall that $J'_{13} = J'_{23}$):

$$\beta_{13j} = \beta_{23xj} \Rightarrow (j \in J'_1 \wedge \beta_{1j} = \beta_{2xj}) \vee (j \in J_3^{1'} \wedge \beta_{3j}^1 = \beta_{3j}^2)$$

(c) Considering $\beta_{3j}^1$ and $\beta_{3j}^2$ are the same (up to renaming) we have:

$$V_3^1 \uplus V_3^2 \uplus \text{vars}(t_{13}) \vdash \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \implies \bigwedge_{j \in J_3^{2'}} \beta_{3j}^1 = \beta_{3j}^2$$
Then we compose by disjunction with the following hypothesis (part of formula (\*)).

$$V_1 \oplus V_2 \oplus vars(t_1) \vdash \bigwedge_{j \in J'_{2x} \cap H} \beta_{1j} = \beta_{2xj}$$

$$ 
\begin{align*}
V_1 \oplus V_2 \oplus V_3^1 \oplus V_3^2 \oplus vars(t_{13}) \vdash \bigwedge_{v_3 \in V_3} v_3^1 &= v_3^2 &\implies \bigwedge_{j \in J'_{2x} \cap H} \beta_{1j} &= \beta_{2xj} \lor \bigwedge_{j \in J'_{3}} \beta_{3j}^1 = \beta_{3j}^2 \\
&\implies V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash \bigwedge_{v_3 \in V_3} v_3^1 &= v_3^2 &\implies \bigwedge_{j \in (J'_{2x} \cap H) \lor J'_{3}} \beta_{13j} &= \beta_{23xj} \\
&\implies V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash \bigwedge_{v_3 \in V_3} v_3^1 &= v_3^2 &\implies \bigwedge_{j \in ((J'_{2x} \cap H) \lor J'_{3}) \setminus \{k\}} \beta_{13j} &= \beta_{23xj} \\
&\implies V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash \bigwedge_{v_3 \in V_3} v_3^1 &= v_3^2 &\implies \bigwedge_{j \in (J'_{23x} \cap H')} \beta_{13j} &= \beta_{23xj}
\end{align*}
$$

We can extend the valuation context of the variables to cover the variables of the transitions $t_3$ and the variables in $V_3^1$ and $V_3^2$ in the formula (\*). By using the statements resulting from the cases (a), (b) and (c), we get:

$$V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash$$

$$ 
\begin{align*}
\mathcal{R}(s_1, s_2) \wedge (g_1 \wedge g_3^1 \wedge \alpha_3^1 = \beta_{1k}) \wedge \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 &\implies \\
\bigwedge_{x \in X} \left( \begin{array}{@{}l@{}}
\alpha_{13} = \alpha_{23x} \wedge \bigwedge_{j \in (J'_{23x} \cap H')} \beta_{13j} = \beta_{23xj} \wedge \\
g_{2x} \wedge \mathcal{R}(s'_1, s'_{2x}) \{\psi_1 \oplus \psi_{2x}\}
\end{array} \right) \wedge g_3^2 \wedge \alpha_3^2 = \beta_{2xk}
\end{align*}
$$

That can be re-written as follows:

$$V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash$$

$$ 
\begin{align*}
\mathcal{R}(s_1, s_2) \wedge g_{13} \wedge \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 &\implies \bigwedge_{x \in X} \left( \begin{array}{@{}l@{}}
\alpha_{13} = \alpha_{23x} \wedge \bigwedge_{j \in J'_{23x} \cap H'} \beta_{13j} = \beta_{23xj} \wedge \\
g_{23x} \wedge \mathcal{R}(s'_1, s'_{2x}) \{\psi_1 \oplus \psi_{2x}\}
\end{array} \right)
\end{align*}
$$

Moreover, we have for any transition $t_3$ in $A_3$ relating $s_3$ and $s'_3$ the following:

$$V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash$$

$$ \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \implies \bigwedge_{v_3 \in V_3} \psi_{13}(v_3^1) = \psi_{13}(v_3^2) \wedge s_3^{1'} = s_3^{2'} $$

Furthermore, according to the Definition 7 (reachability applied to the composed automaton $A_1[A_3/k]$) we have, for all $t_{13} \in T_{13}$:

$$ vars(t_{13}) \vdash (\check{\forall}_{A_{13}}(s_{13}) \wedge g_{13} \implies \check{\forall}_{A_{13}}(s'_{13}) \{\psi_{13}\}) $$
Thus, we get:

$$ V_{13} \oplus V_{23} \oplus vars(t_1) \cap vars(t_{13}) \vdash \\ \mathcal{R}(s_1, s_2) \wedge g_{13} \wedge \check{\wedge}_{A_{13}}(s_{13}) \wedge \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 = \\ \qquad \bigvee_{x \in X} \left( \begin{array}{l} \alpha_{13} = \alpha_{23x} \wedge \bigwedge_{j \in J'_{23x} \wedge H'} \beta_{13j} = \beta_{23xj} \wedge g_{23x} \wedge \mathcal{R}(s'_1, s'_{2x}) \{\psi_1 \oplus \psi_{2x}\} \\ \wedge \check{\wedge}_{A_{13}}(s'_{13}) \{\psi_{13}\} \wedge \bigwedge_{v_3 \in V_3} \psi_{13}(v_3^1) = \psi_{13}(v_3^2) \wedge s_3^{1'} = s_3^{2'} \end{array} \right) $$

From the two previous formulas, we get:

$$ V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash \\ \mathcal{R}(s_1, s_2) \wedge g_{13} \wedge \check{\wedge}_{A_{13}}(s_{13}) \wedge \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 = \\ \qquad \bigvee_{x \in X} \left( \begin{array}{l} \alpha_{13} = \alpha_{23x} \wedge \bigwedge_{j \in J'_{23x} \wedge H'} \beta_{13j} = \beta_{23xj} \wedge g_{23x} \wedge \check{\wedge}_{A_{13}}(s'_{13}) \{\psi_{13}\} \wedge \\ \mathcal{R}(s'_1, s'_{2x}) \{\psi_1 \oplus \psi_{2x}\} \wedge \bigwedge_{v_3 \in V_3} \psi_{13}(v_3^1) = \psi_{13}(v_3^2) \wedge s_3^{1'} = s_3^{2'} \end{array} \right) $$

Because of the independence of the substitution domains, we simplify and get the expected formula:

$$ V_{13} \oplus V_{23} \oplus vars(t_{13}) \vdash \\ \mathcal{R}'(s_{13}, s_{23}) \wedge g_{13} \implies \bigvee_{x \in X} \left( \begin{array}{l} \alpha_{13} = \alpha_{23x} \wedge \bigwedge_{j \in J'_{23x} \wedge H'} \beta_{13j} = \beta_{23xj} \wedge \\ g_{23x} \wedge \mathcal{R}'(s'_{13}, s'_{23x}) \{\psi_{13} \oplus \psi_{23x}\} \end{array} \right) $$

**Second case: Only the encompassing automaton performs a transition.** $t_{13}$ is obtained by the transition $t_1 = \frac{\beta_{1j}^{j \in J'_1}, g_1, \psi_1}{s_1 \xrightarrow{\alpha_1} s'_1}$ alone with the state $s_3^1$ unchanged, if $k \notin J'_1$

$$ t_{13} = \frac{\beta_{1j}^{j \in J'_1}, g_1, \psi_1}{(s_1, s_3^1) \xrightarrow{\alpha_1} (s'_1, s'_3^1)} $$

As stated above, from the simulation of $A_1$ by $A_2$ we get a family of OTs $t_{2x}^{x \in X}$. The composition of this family of OTs with the same transitions of $A_3$ (up to renaming) as those used to build $t_{13}$ produces a family of OTs $t_{23x}^{x \in X}$ in the form:

$$ t_{23x} = \left( \frac{\beta_{2xj}^{j \in J'_{2x}}, g_{2x}, \psi_{2x}}{(s_2, s_3^2) \xrightarrow{\alpha_{2x}} (s'_{2x}, s_3^2)} \right)^{x \in X} $$

By hypothesis we have $k \in H$, since $k \notin J'_1$, we deduce $k \notin J'_{2x}$.
∀x ∈ X we have:

$$
\begin{align*}
J'_{23x} \cap H' &= J'_{2x} \cap (J_3 \uplus H \setminus \{k\}) \\
&= (J'_{2x} \cap H) \text{ since } J'_{2x} \cap J_3 = \emptyset \wedge k \notin J'_{2x} \\
&= (J'_1 \cap H) \text{ since } J'_1 \cap H = J'_{2x} \cap H \\
&= (J'_{13} \cap H') \text{ since } J_3 \cap J'_1 = \emptyset \wedge k \notin J'_1
\end{align*}
$$

The proof of the rest of the formula follows the same steps as the previous case the only argument that change is that by composition we obtain: $g_{13}$ is the same as $g_1$ and $g_{23x}$ is the same as $g_{2x}$ and the actions of $\alpha_{13}$, resp. $\alpha_{23x}$, is the same as $\alpha_1$, resp. $\alpha_{2x}$. Similarly $\beta_{13j}$ and $\beta_{23xj}$ that are the same as $\beta_{1j}$ and $\beta_{2xj}$ respectively. We also apply the reachability definition but only on the automaton $A_1$

3. Lastly, we have to prove the satisfaction of the deadlock reduction condition, i.e., for all $(s_{13}, s_{23}) \in S_{13} \times S_{23}$

$$
V_{13} \uplus V_{23} \vdash \mathcal{R}(s_{13}, s_{23}) \wedge \neg\left(\bigvee_{t_{13} \in \mathrm{OT}(s_{13})} \mathrm{guard}(t_{13})\right) \implies \neg\left(\bigvee_{t_{23} \in \mathrm{OT}(s_{23})} \mathrm{guard}(t_{23})\right)
$$

By hypothesis the composition $A_1[A_3/k]$ is non-blocking, then according to the Definition 10 we have for all state $s_{13}$:

$$
V_{13} \uplus \biguplus_{t_1 \in \text{OT}(s_1)} \text{vars}(t_1) \vdash \left( \bigvee_{t_1 \in \text{OT}(s_1)} A_{13}(s_{13}) \wedge \bigvee \text{guard}(t_1) \right) \implies \bigvee_{t_{13} \in \text{OT}(s_{13})} \text{guard}(t_{13})
$$

From this we can infer:

$$
V_{13} \uplus \biguplus_{t_1 \in \mathrm{OT}(s_1)} \mathrm{vars}(t_1) \vdash \neg\left(\bigvee_{t_{13} \in \mathrm{OT}(s_{13})} \mathrm{guard}(t_{13})\right) \implies \neg\left(\bigvee_{t_1 \in \mathrm{OT}(s_1)} \mathrm{guard}(t_1)\right) \vee \neg\sqrt{A_{13}(s_{13})}
$$

Furthermore, from the second hypothesis stating that $A_1 \leq_H A_2$, we have for all $(s_1, s_2) \in S_1 \times S_2$

$$
V_1 \uplus V_2 \vdash \mathcal{R}(s_1, s_2) \wedge \neg(\bigvee_{t_1 \in \mathrm{OT}(s_1)} \mathrm{guard}(t_1)) \implies \neg(\bigvee_{t_2 \in \mathrm{OT}(s_2)} \mathrm{guard}(t_2))
$$

From the two previous formula can deduce:

$$
\begin{align*}
V_{13} \uplus V_2 \uplus \biguplus_{t_1 \in \mathrm{OT}(s_1)} \mathrm{vars}(t_1) \vdash \\
R(s_1, s_2) \wedge \neg\left(\bigvee_{t_{13} \in \mathrm{OT}(s_{13})} \mathrm{guard}(t_{13})\right) &\implies \neg\left(\bigvee_{t_2 \in \mathrm{OT}(s_2)} \mathrm{guard}(t_2)\right) \vee \neg\sqrt{A_{13}(s_{13})}
\end{align*}
$$

By definition of the composition of open automata, each guard of automaton $A_{23}$ is of the form $guard(t_{23}) = guard(t_2) \wedge t$, thus we have:

$$
V_{23} \vdash \neg(\bigvee_{t_1 \in \mathrm{OT}(s_2)} \mathrm{guard}(t_2)) \implies \neg(\bigvee_{t_{23} \in \mathrm{OT}(s_{23})} \mathrm{guard}(t_{23}))
$$
From the two previous formula and by introducing the following tautology

$$ \left( \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \right), \text{ we get:} $$

$$ \begin{align*} V_{13} \bowtie V_{23} &\vdash \mathcal{R}(s_1, s_2) \wedge \check{\wedge}_{A_{13}}(s_{13}) \wedge \left( \bigwedge_{v_3 \in V_3} v_3^1 = v_3^2 \wedge s_3^1 = s_3^2 \right) \wedge \neg \bigvee_{t_{13} \in \text{OT}(s_{13})} \text{guard}(t_{13}) \\ &\implies \left( \neg \bigvee_{t_{23} \in \text{OT}(s_{23})} \text{guard}(t_{23}) \vee \neg \check{\wedge}_{A_{13}}(s_{13}) \right) \wedge \check{\wedge}_{A_{13}}(s_{13}) \implies \neg \bigvee_{t_{23} \in \text{OT}(s_{23})} \text{guard}(t_{23}) \end{align*} $$

which gives the expected result. □

## C Proof of Congruence (Theorem 3)

Suppose $A_2 \leq_H A_3$ and $k \in H$. and the composition $A_1[A_2/k]$ is non-blocking. We have:

$$ A_1[A_2/k] \leq_{J_1 \bowtie H \setminus \{k\}} A_1[A_3/k] $$

Pictorially, the theorem states the following result:

<figure><img src="image_13.png" /></figure>

*Proof.* Let us denote by $A_{12}$ (resp. $A_{13}$) the OA resulting from $A_1[A_2/k]$ (resp. $A_1[A_3/k]$), to prove the theorem it is sufficient to prove that there exists a relation between states of the two OA that satisfies the conditions of the Definition 9.

We denote $A_1 = \langle S_1, s_{01}, J_1, V_1, \sigma_{01}, T_1 \rangle$ and $A_2 = \langle S_2, s_{02}, J_2, V_2, \sigma_{02}, T_2 \rangle$ and $A_3 = \langle S_3, s_{03}, J_3, V_3, \sigma_{03}, T_3 \rangle$.

Let $R$ be the refinement relation relating states of $A_2$ and $A_3$. Let us denote with $t^2$ and $t^3$ the elements of $A_2$ and $A_3$ respectively. Consider any two states $s_{12} = (s_1^1, s_2)$ and $s_{13} = (s_1^2, s_3)$ ($s_1^1$ and $s_1^2$ are the same with renaming). We define a relation $\mathcal{R}'$ relating states of $s_{12}$ and $s_{13}$ as follows:

$$ \mathcal{R}'(s_{12}, s_{13}) = \mathcal{R}(s_2, s_3) \wedge \check{\wedge}_{A_{12}}(s_{12}) \wedge \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \wedge s_1^1 = s_1^2 $$

Let us denote $H' = H \cup J_1 \setminus \{k\}$. We want to prove that $(\mathcal{R}', H')$ is a hole-tracking simulation of $A_{12}$ and $A_{13}$. As for the previous proof we deal with cases:

1. First, we have to prove the relation for initial states:

$$ \sigma_{012} \bowtie \sigma_{013} \vdash \mathcal{R}'(s_{012}, s_{013}) $$

with $\sigma_{012} = \sigma_{01}^1 \bowtie \sigma_{03}$, $\sigma_{013} = \sigma_{01}^2 \bowtie \sigma_{03}$, $s_{012} = (s_{01}^1, s_{02})$, and $s_{013} = (s_{01}^2, s_{03})$. The proof of this point is similar to that of Theorem 2.
2. Second, we need to prove for any OT $t_{12}$ in $T_{12}$ originating from $s_{12}$

$$ \frac{\beta_{12j}^{j \in J'_{12}}, g_{12}, \psi_{12}}{s_{12} \xrightarrow{\alpha_{12}} s'_{12}} \in \text{OT}(s_{12}) $$

there exists an indexed family $t_{13x}$ of OTs originating from $s_{13}$ that simulates it:

$$ \left( \frac{\beta_{13x_j}^{j \in J'_{13x}}, g_{13x}, \psi_{13x}}{s_{13} \xrightarrow{\alpha_{13x}} s'_{13x}} \in \text{OT}(s_{13}) \right)^{x \in X} $$

such that $(\forall x \in X, J'_{13x} \cap H' = J'_{12} \cap H')$ and

$$ V_{12} \oplus V_{13} \oplus \text{vars}(t_{12}) \vdash $$

$$ \mathcal{R}'(s_{12}, s_{13}) \wedge g_{12} \implies \bigvee_{x \in X} \left( \begin{array}{l} \alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J'_{13x} \cap H'} \beta_{12j} = \beta_{13xj} \wedge \\ g_{13x} \wedge \mathcal{R}'(s'_{12}, s'_{13x}) \{\psi_{12} \oplus \psi_{13x}\} \end{array} \right) $$

By definition of composition and OA refinement we have:

$$ V_{12} = V_1^1 \oplus V_3 \text{ and } V_{13} = V_1^2 \oplus V_3 $$

$$ \begin{aligned} H' &= H \oplus J_1 \setminus \{k\} \subseteq J_1 \oplus (J_2 \cap J_3) \setminus \{k\} = (J_1^1 \oplus J_2 \setminus \{k\}) \cap (J_1^2 \oplus J_3 \setminus \{k\}) \\ &= J_{12} \cap J_{13} \end{aligned} $$

We have by hypothesis $A_2 \leq_H A_3$, then for any open transition $t_2$ in $T_2$ originating from $s_2$:

$$ \frac{\beta_{2j}^{j \in J'_{2}}, g_{2}, \psi_{2}}{s_{2} \xrightarrow{\alpha_{2}} s'_{2}} \in \text{OT}(s_{2}) $$

there exists an indexed family of OTs originating from $s_3$:

$$ \left( \frac{\beta_{3x_j}^{j \in J'_{3x}}, g_{3x}, \psi_{3x}}{s_3 \xrightarrow{\alpha_{3x}} s'_{3x}} \in \text{OT}(s_3) \right)^{x \in X} $$

such that $\forall x \in X, J'_{3x} \cap H = J'_{2} \cap H$ and

$$ V_2 \oplus V_3 \oplus \text{vars}(t_2) \vdash $$

$$ \mathcal{R}(s_2, s_3) \wedge g_2 \implies \bigvee_{x \in X} \left( \begin{array}{l} \alpha_2 = \alpha_{3x} \wedge \bigwedge_{j \in J'_{3x} \cap H} \beta_{2j} = \beta_{3xj} \wedge \\ g_{3x} \wedge \mathcal{R}(s'_2, s'_{3x}) \{\psi_2 \oplus \psi_{3x}\} \end{array} \right) (*) $$

Consider any transition $t_{12}$ in $A_{12}$. Based on the definition of the composition $t_{12}$ can be obtained from two different cases, we will consider the two cases separately.
**First case: Both automata perform a transition.** The transition $t_{12}$ is obtained by the composition of transition $t_2 = \frac{\beta_{2j}^{j \in J_2'}}{s_2 \xrightarrow{\alpha_2} s_2'}$ and a transition

$$t_1^1 = \frac{(\beta_{1j}^1)^{j \in J_1'} , g_1^1, \psi_1^1}{s_1^1 \xrightarrow{\alpha_1} s_1^{1'}} \quad \text{when } k \in J_1^{1'}$$

The result:

$$t_{12} = \frac{\beta_{1j}^1 \ j \in J_1' \setminus \{k\} \ \oplus \ (\beta_{2j})^{j \in J_2'}, g_1^1 \wedge g_2 \wedge \alpha_1^1 = \beta_{2k}, \psi_1^1 \oplus \psi_2}{(s_1^1, s_2) \xrightarrow{\alpha_1^1} (s_1^{1'}, s_2')} \quad \text{where } k \in J_1^{1'}$$

We then obtain a family of OTs by the simulation of $A_2$ by $A_3$ (as stated above). By hypothesis we have $k \in H$, so in the case where $k \in J_1^{1'}$, we deduce that $k \in J_{3x}^{1'}$ we can then build a family of OTs $t_{13x}^{x \in X}$ with the same transition, up to renaming, as the one used to build $t_{12}$ (i.e., $t_1^1$), where $s_1^{2'}$ is the same as $s_1^{1'}$ up to renaming.

$$t_{13x} = \left( \frac{(\beta_{1j}^2)^{j \in J_1' \oplus \beta_{3xj}^{j \in J_{3x}'} \setminus \{k\}}, g_{3x} \wedge g_1^2 \wedge \alpha_1^2 = \beta_{3xk}, \psi_{3x} \oplus \psi_1^2}{(s_1^2, s_3) \xrightarrow{\alpha_1^2} (s_1^{2'}, s_{3x}')} \right)^{x \in X}$$

Recall that in this case $k \in J_1^{1'}$, so $\forall x \in X$ we have:

$$
\begin{align*}
J_{13x} \cap H' &= ((J_{3x}' \setminus \{k\}) \oplus J_1^{2'}) \cap (H \oplus J_1 \setminus \{k\}) \\
&= ((J_{3x}' \cap (H \oplus J_1)) \oplus (J_1^{2'} \cap (H \oplus J_1))) \setminus \{k\} \\
&= ((J_{3x}' \cap H) \oplus (J_1^{2'} \cap J_1)) \setminus \{k\} \\
&\qquad \text{since } J_1 \cap J_{3x}' = \emptyset \text{ and } H \cap J_1^{2'} = \emptyset \\
&= ((J_{3x}' \cap H) \oplus J_1^{2'}) \setminus \{k\} \text{ since } J_1^{2'} \subseteq J_1 \\
&= ((J_2' \cap H) \oplus J_1^{1'}) \setminus \{k\} \\
&\qquad \text{since } J_1^{1'} = J_1^{2'} \text{ and } J_2' \cap H = J_{3x}' \cap H \\
&= ((J_2' \cap H) \oplus (J_1^{1'} \cap J_1)) \setminus \{k\} \text{ since } J_1^{1'} \subseteq J_1 \\
&= (J_2' \cap (J_1 \oplus H)) \oplus ((J_1^{1'} \cap (J_1 \oplus H)) \setminus \{k\}) \\
&\qquad \text{since } J_1 \cap J_2' = \emptyset \text{ and } H \cap J_1^{1'} = \emptyset \\
&= ((J_2' \oplus J_1^{1'}) \setminus \{k\}) \cap ((J_1 \oplus H) \setminus \{k\}) \\
&= J_{12}' \cap H'
\end{align*}
$$

In this case the composition gives:

$$g_{12} \Leftrightarrow g_1^1 \wedge g_2 \wedge \alpha_1^1 = \beta_{2k} \text{ and } g_{13x} \Leftrightarrow g_1^2 \wedge g_{3x} \wedge \alpha_1^2 = \beta_{3xk}$$

As $k \in H$ we have $\alpha_1^1 = \alpha_1^2$ then we deduce:

$$g_1^1 \wedge \alpha_1^1 = \beta_{2k} \Leftrightarrow g_1^2 \wedge \alpha_1^2 = \beta_{3xk}$$

The proof of the rest is based on the following facts:
(a) By construction of $t_{12}$ and $t_{13x}$ we have $\alpha_{12} = \alpha_1^1$ and $\alpha_{13x} = \alpha_1^2$. Since $\alpha_1^1$ and $\alpha_1^2$ are the same (up to renaming) we deduce: $\alpha_{12} = \alpha_{13x}$.

(b) By composition we have also:

$$ \beta_{12j}^{j \in J'_{12}} = (\beta_{1j}^1)^{j \in J'_{1} \setminus \{k\}} \oplus (\beta_{2j})^{j \in J'_{2}} \text{ and } \beta_{13xj}^{j \in J'_{13}} = (\beta_{1j}^2)^{j \in J'_{1} \setminus \{k\}} \oplus \beta_{3xj}^{j \in J'_{3x} \setminus \{k\}} $$
Therefore, we have for all $j \in J'_{12}$ (recall that $J'_{12} = J'_{13}$):

$$ \beta_{12j} = \beta_{13xj} \Rightarrow (j \in J'_{1} \wedge \beta_{1j}^{1} = \beta_{1j}^{2}) \vee (j \in J'_{2} \wedge \beta_{2j} = \beta_{3xj}) $$

(c) Considering $\beta_{1j}^1$ and $\beta_{1j}^2$ are the same (up to renaming) we have:

$$ V_1^1 \oplus V_2^2 \oplus vars(t_{12}) \vdash \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \implies \bigwedge_{j \in J_1^{2'}} \beta_{1j}^1 = \beta_{1j}^2 $$

We compose by disjunction with the following hypothesis (part of formula $(*)$).

$$ V_2 \oplus V_3 \oplus vars(t_2) \vdash \bigwedge_{j \in J_{3x}^{\prime} \cap H} \beta_{2j} = \beta_{3xj} $$

$$ \begin{align*} V_2 \oplus V_3 \oplus V_1^1 \oplus V_1^2 \oplus vars(t_{12}) \vdash & \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \implies \bigwedge_{j \in J_{3x}^{\prime} \cap H} \beta_{2j} = \beta_{3xj} \vee \bigwedge_{j \in J_1^{2'}} \beta_{1j}^1 = \beta_{1j}^2 \\ & \Rightarrow V_{12} \oplus V_{13} \oplus vars(t_{12}) \vdash \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \implies \bigwedge_{j \in (J_{3x}^{\prime} \cap H) \oplus J_1^{2'}} \beta_{12j} = \beta_{13xj} \\ & \Rightarrow V_{12} \oplus V_{13} \oplus vars(t_{12}) \vdash \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \implies \bigwedge_{j \in ((J_{3x}^{\prime} \cap H) \oplus J_1^{2'}) \setminus \{k\}} \beta_{12j} = \beta_{13xj} \\ & \Rightarrow V_{12} \oplus V_{12} \oplus vars(t_{12}) \vdash \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \implies \bigwedge_{j \in (J_{13x}^{\prime} \cap H^{\prime})} \beta_{12j} = \beta_{13xj} \end{align*} $$

We can extend the valuation context of the variables to cover the variables of the transitions $t_1$ and variables $V_1^1$ and $V_1^2$ in the formula $(*)$. By using the statements resulting from the cases (a), (b) and (c), we get:

$$ V_{13} \oplus V_{13} \oplus vars(t_{12}) \vdash \begin{array}{@{}l@{}} \mathcal{R}(s_2, s_3) \wedge (g_2 \wedge g_1^1 \wedge \alpha_1^1 = \beta_{2k}) \wedge \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \\ \phantom{\mathcal{R}(s_2, s_3) \wedge (g_2 \wedge g_1^1 \wedge \alpha_1^1 = \beta_{2k}) \wedge \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2} \bigvee_{x \in X} \left( \begin{array}{@{}l@{}} \alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in (J_{13x} \cap H^{\prime})} \beta_{12j} = \beta_{13xj} \wedge \\ g_{3x} \wedge \mathcal{R}(s_2^{\prime}, s_{3x}^{\prime}) \{\psi_2 \oplus \psi_{3x}\} \end{array} \right) \wedge g_1^2 \wedge \alpha_1^2 = \beta_{3xk} \end{array} $$

That can be re-written as follows:

$$ V_{12} \oplus V_{13} \oplus vars(t_{12}) \vdash \begin{array}{@{}l@{}} \mathcal{R}(s_2, s_3) \wedge g_{12} \wedge \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \\ \phantom{\mathcal{R}(s_2, s_3) \wedge g_{12} \wedge \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2} \bigvee_{x \in X} \left( \begin{array}{@{}l@{}} \alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J_{13x}^{\prime} \cap H^{\prime}} \beta_{12j} = \beta_{13xj} \wedge \\ g_{13x} \wedge \mathcal{R}(s_2^{\prime}, s_{3x}^{\prime}) \{\psi_2 \oplus \psi_{3x}\} \end{array} \right) \end{array} $$

Moreover, we have for any transition $t_1$ in $A_1$ relating $s_1^1$ and $s_1^{1'}$ the following:

$$ V_{12} \oplus V_{13} \oplus vars(t_{12}) \vdash \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \wedge s_1^1 = s_1^2 \implies \bigwedge_{v_1 \in V_1} \psi_{12}(v_1^1) = \psi_{13x}(v_1^2) \wedge s_1^{1'} = s_1^{2'} $$
From the two previous formula, we get:

$$
\begin{align*}
& V_{12} \oplus V_{13} \oplus \mathrm{vars}(t_{12}) \vdash \\
& \phantom{V_{12} \oplus V_{13} \oplus \mathrm{vars}(t_{12}) \vdash} R(s_2, s_3) \wedge g_{12} \wedge \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \wedge s_1^1 = s_1^2 \\
& \implies \\
& \phantom{V_{12} \oplus V_{13} \oplus \mathrm{vars}(t_{12}) \vdash} \bigvee_{x \in X} \left( \begin{array}{@{}l@{}}
\alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J'_{13x} \wedge H'} \beta_{12j} = \beta_{13xj} \wedge g_{13x} \wedge \\
\phantom{\alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J'_{13x} \wedge H'} \beta_{12j} = \beta_{13xj} \wedge} R(s'_2, s'_{3x}) \{\psi_2 \oplus \psi_{3x}\} \wedge \bigwedge_{v_1 \in V_1} \psi_{12}(v_1^1) = \psi_{13x}(v_1^2) \wedge s_1^{1'} = s_1^{2'}
\end{array} \right)
\end{align*}
$$

Furthermore, according to the Definition 7 (reachability, applied to the composed automaton $A_1[A_2/k]$) we have, for all $t_{12} \in T_{12}$:

$$
\mathrm{vars}(t_{12}) \vdash (\check{\mathrm{A}}_{12}(s_{12}) \wedge g_{12} \implies \check{\mathrm{A}}_{12}(s'_{12}) \{\psi_{12}\})
$$

Thus, we get:

$$
\begin{align*}
& V_{12} \oplus V_{13} \oplus vars(t_{12}) \vdash \\
& \quad \mathcal{R}(s_2, s_3) \wedge g_{12} \wedge \check{\mathcal{A}}_{12}(s_{12}) \wedge \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \wedge s_1^1 = s_1^2 \\
& \implies \\
& \phantom{V_{12} \oplus V_{13} \oplus vars(t_{12}) \vdash} \bigvee_{x \in X} \left( \begin{array}{@{}l@{}}
\alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J'_{13x} \wedge H'} \beta_{12j} = \beta_{13xj} \wedge g_{13x} \wedge \\
\mathcal{R}(s'_2, s'_{3x}) \{\psi_2 \oplus \psi_{3x}\} \wedge \check{\mathcal{A}}_{12}(s'_{12}) \{\psi_{12}\} \\
\wedge \bigwedge_{v_1 \in V_1} \psi_{12}(v_1^1) = \psi_{13x}(v_1^2) \wedge s_1^{1'} = s_1^{2'}
\end{array} \right)
\end{align*}
$$

Because of the independence of the substitution domains, we simplify and get the expected formula:

$$
V_{12} \oplus V_{13} \oplus vars(t_{12}) \vdash \mathcal{R}'(s_{12}, s_{13}) \wedge g_{12} \implies \\
\qquad \bigvee_{x \in X} \left( \alpha_{12} = \alpha_{13x} \wedge \bigwedge_{j \in J'_{13x} \wedge H'} \beta_{12j} = \beta_{13xj} \wedge g_{13x} \wedge \mathcal{R}'(s'_{12}, s'_{13x}) \{\psi_{12} \oplus \psi_{13x}\} \right)
$$

Second case: Only the encompassing automaton performs a transition. $t_{12}$ is obtained by the transition $t_1^1 = \frac{(\beta_{1j}^1)^{j \in J_1'}}{s_1^1 \xrightarrow{\alpha_1^1} s_1'}$ alone with the state $s_2$ unchanged, if $k \notin J_1^{1'}$

$$
t_{12} = \frac{(\beta_{1j}^1)^{j \in J_1'}}{(s_1^1, s_2) \xrightarrow{\alpha_1^1} (s_1^{1'}, s_2)}
$$

The hole is not involved we can define $t_{13}$ with the same transition $t_1$ of $A_1$ (where elements of $t_1$ are the same as above modulo renaming of variables):

$$
t_{13} = \frac{(\beta_{1j}^2)^{j \in J_1''}, g_1^2, \psi_1^2}{(s_1^1, s_3) \xrightarrow{\alpha_1^2} (s_1^{2'}, s_3)}
$$
We thus take $(t_{13x})^{x \in X} = \{t_{13}\}$. $\forall x \in X$ we have $J'_{13x} = J_1^{2'}$ and trivially:

$$
\begin{align*}
J'_{13x} \cap H' &= J_1^{2'} \cap (J_1 \uplus H \setminus \{k\}) \\
&= J_1^{1'} \cap (J_1 \uplus H \setminus \{k\}) \text{ since } J_1^{2'} = J_1^{1'} \\
&= (J_{12}' \cap H')
\end{align*}
$$

Moreover, we have by definition

$$
\mathcal{R}'(s_{12}, s_{13}) = \mathcal{R}(s_{2}, s_{3}) \wedge \check{\mathcal{A}}_{A_{12}}(s_{12}) \wedge \bigwedge_{v_{1} \in V_{1}} v_{1}^{1} = v_{1}^{2} \wedge s_{1}^{1} = s_{1}^{2}
$$

Thus, because transitions $t_1^1$ and $t_1^2$ are the same:

$$
\mathcal{R}'(s_{12}, s_{13}) \implies \mathcal{R}(s_2, s_3) \wedge \check{\mathcal{A}}_{A_{12}}(s_{12}) \wedge \left( \underbrace{\bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \wedge s_1^{1'} = s_1^{2'}}_{\mathcal{R}'(s_{12}, s_{13})} \right)
$$

Moreover, we have the following:

$$
V_{12} \uplus V_{13} \uplus vars(t_{12}) \vdash \\
\quad \bigwedge_{v_1 \in V_1} v_1^1 = v_1^2 \wedge s_1^1 = s_1^2 \implies \bigwedge_{v_1 \in V_1} \psi_{12}(v_1^1) = \psi_{13}(v_1^2) \wedge s_1^{1'} = s_1^{2'}
$$

Furthermore, according to the Definition 7 (reachability, applied to the composed automa-
ton $A_1$) we have, for all $t_{12} \in T_{12}$:

$$
vars(t_{12}) \vdash (\check{\mathcal{A}}_{A_{12}}(s_{12}) \wedge g_{12} \implies \check{\mathcal{A}}_{A_{12}}(s'_{12}) \{\psi_{12}\})
$$

Because $\alpha_{12}$ and $\alpha_{13}$ are the same, and also $\beta_{12}$ and $\beta_{13}$ are the same (modulo renaming of variables), we deduce from the above the expected formula (instantiated with $X$ a singleton):

$$
V_{12} \uplus V_{13} \uplus vars(t_{12}) \vdash \mathcal{R}'(s_{12}, s_{13}) \wedge g_{12} \implies \left( \bigwedge_{j \in J'_{13} \cap H'} \beta_{12j} = \beta_{13j} \wedge g_{13} \wedge \mathcal{R}'(s'_{12}, s'_{13}) \{\psi_{12} \uplus \psi_{13}\} \right)
$$

3. Lastly, we have to prove the satisfaction of the deadlock reduction condition, i.e., for all $(s_{12}, s_{13}) \in S_{12} \times S_{13}$

$$
V_{12} \uplus V_{13} \vdash \mathcal{R}'(s_{12}, s_{13}) \wedge \neg(\bigvee_{t_{12} \in \text{OT}(s_{12})} \text{guard}(t_{12})) \implies \neg(\bigvee_{t_{13} \in \text{OT}(s_{13})} \text{guard}(t_{13}))
$$

Let's start with the hypothesis of the theorem stating that $A_2 \le_H A_3$, thus we have for all $(s_2, s_3) \in S_2 \times S_3$

$$
V_2 \uplus V_3 \vdash \mathcal{R}(s_2, s_3) \wedge \neg(\bigvee_{t_2 \in \text{OT}(s_2)} \text{guard}(t_2)) \implies \neg(\bigvee_{t_3 \in \text{OT}(s_3)} \text{guard}(t_3))
$$
By hypothesis the composition $A_1[A_2/k]$ is non-blocking, then according to the Definition 10 we have for all state $s_{12}$:

$$V_{12} \mathrel{\substack{\oplus \\ \vdash}} \bigcup_{t_1 \in \text{OT}(s_1)} vars(t_1) \quad \vdash \quad \left( \checkmark_{A_{12}(s_{12})} \wedge \bigvee_{t_1 \in \text{OT}(s_1)} guard(t_1) \right) \quad \implies \quad \bigvee_{t_{12} \in \text{OT}(s_{12})} guard(t_{12})$$

Which implies

$$V_{12} \mathrel{\substack{\oplus \\ \vdash}} vars(t_1) \quad \vdash \quad \neg \bigvee_{t_{12} \in \text{OT}(s_{12})} guard(t_{12}) \quad \implies \quad \left( \neg \checkmark_{A_{12}(s_{12})} \vee \neg \bigvee_{t_1 \in \text{OT}(s_1)} guard(t_1) \right)$$

Additionally, each transition $t_{13}$ of $\text{OT}(s_{13})$ is of the form $g_1 \wedge g_3 \wedge g$ with $g_1$ a guard of a transition $t_1$ of $\text{OT}(s_1)$. Thus we have

$$\neg \bigvee_{t_1 \in \text{OT}(s_1)} guard(t_1) \implies \neg (\bigvee_{t_{13} \in \text{OT}(s_{13})} guard(t_{13}))$$

Thus we have, as $\mathcal{R}$ contains the reachability of state $s_{12}$:

$$V_{12} \mathrel{\substack{\oplus \\ \vdash}} V_{13} \vdash \mathcal{R}'(s_{12}, s_{13}) \wedge \neg (\bigvee_{t_{12} \in \text{OT}(s_{12})} guard(t_{12})) \implies \left( \checkmark_{A_{12}(s_{12})} \wedge \left( \neg \checkmark_{A_{12}(s_{12})} \vee \neg (\bigvee_{t_{13} \in \text{OT}(s_{13})} guard(t_{13})) \right) \right) \implies \neg (\bigvee_{t_{13} \in \text{OT}(s_{13})} guard(t_{13}))$$

□
Inria

RESEARCH CENTRE
GRENOBLE - RHÔNE-ALPES

Inovallée

655 avenue de l'Europe Montbonnot

38334 Saint Ismier Cedex

Publisher

Inria

Domaine de Voluceau - Rocquencourt

BP 105 - 78153 Le Chesnay Cedex

inria.fr

ISSN 0249-6399