A framework for compositional nonblocking verification of extended finite-state machines

Abstract

This paper presents a framework for compositional nonblocking verification of discrete event systems modelled as extended finite-state machines (EFSM). Previous results are improved to consider general conflict-equivalence based abstractions of EFSMs communicating both via shared variables and events. Performance issues resulting from the conversion of EFSM systems to finite-state machine systems are avoided by operating directly on EFSMs, deferring the unfolding of variables into state machines as long as possible. Several additional methods to abstract EFSMs and remove events are also presented. The proposed algorithm has been implemented in the discrete event systems tool Supremica, and the paper presents experimental results for several large EFSM models that can be verified faster than by previously used methods.

1 Introduction

Many discrete event systems are safety-critical, where failures can result in huge financial losses or even human fatalities. Logical correctness is a crucial property of these systems, and formal verification is an important part of guaranteeing it. This paper focuses on the verification of the nonblocking property (Ramadge and Wonham 1989).

Formal verification requires a formal model, and finite-state machines (FSM) are widely used to represent discrete event systems (Ramadge and Wonham 1989). FSMs describe the behaviour of a system using states and transitions between these states. The transitions are associated to events through which the FSM can interact with other FSMs and the outside world. For systems with data dependency, it is natural to extend FSMs with variables and guards. This results in extended finite-state machines (EFSM), which interact through events and bounded discrete variables. EFSMs, also referred to as extended finite-state automata (EFA), have been similarly defined by several researchers (Cheng and Krishnakumar 1993; Chen and Lin 2000; Sköldstam et al. 2007; Zhaoa et al. 2012; Teixeira et al. 2013).

EFSMs facilitate the modelling of complex discrete event systems that include counters or other quantitative variables. The state spaces of such systems can be huge, yet they can be modelled concisely with only a few state machine diagrams. On the other hand, the formal verification of these systems remains a challenge, because technically verification must take all possible combinations of variable values into account, often resulting in state-space explosion.

Various approaches have been proposed to overcome state space explosion. With symbolic model checking, the explicit enumeration of states is avoided using a symbolic representation (Baier and Katoen 2008; McMillan 1993), typically consisting of ordered binary decision diagrams (Bryant 1992), making it possible to explore much larger state spaces (Vahidi 2004).

With compositional verification (Graf and Steffen 1990) and abstract interpretations (Dams et al. 1994), the model is simplified before or during verification in an attempt to reduce combinatorial complexity. The nonblocking property considered in this paper requires special types of abstraction for compositional verification to work. Abstraction based on conflict equivalence (Malik et al. 2006) is more effective than general abstract interpretations (Dams et al. 1994) or bisimulation equivalence (Milner 1989). While it is well-known that nonblocking verification and similar model checking problems are NP (Gohari and Wonham 2000), and the worst-case complexity of compositional verification is even worse, experimental results (Flordal and Malik 2009; Su et al. 2010; Malik and Leduc 2013) show that compositional nonblocking verification can efficiently verify several large FSM models that cannot be verified by standard monolithic verification.

Compositional verification can also be applied to systems modelled as EFSMs, after converting the EFSMs to a set of FSMs (Sköldstam et al. 2007). However, the conversion can increase the number of events significantly, and in some cases takes longer than the verification (Mohajerani et al. 2013b). Recently, a direct method for compositional verification of EFSM models has been proposed (Mohajerani et al. 2013a; 2014), which removes the need to convert EFSMs to FSMs. In (Mohajerani et al. 2013a), symbolic observation equivalence is used as the only abstraction method. This is generalised to conflict equivalence in (Mohajerani et al. 2014), where a general framework for compositional verification of EFSMs communicating only via shared variables is introduced.

This paper is an extended version of (Mohajerani et al. 2014). It proposes a framework and an algorithm for compositional nonblocking verification of systems modelled as EFSMs that do not only communicate via shared variables but also via shared events.

• Firstly, this paper introduces normalisation to treat communication via shared variables (Mohajerani et al. 2014), or via events (Flordal and Malik 2009), or combinations of these, in a uniform way. After normalisation, the conflict-preserving abstractions for FSMs (Flordal and Malik 2009; Pena et al. 2009; Su et al. 2010; Malik and Leduc 2013) can be generalised for EFSM systems. While in (Mohajerani et al. 2014), partial unfolding of variables is limited to local variables, i.e., variables used by only one component, after normalisation this can be generalised to allow unfolding of arbitrary variables, even if they are shared between several components (Proposition 8).

• Secondly, this paper proposes more ways to simplify EFSM components while preserving the nonblocking property. In addition to the FSM-based abstraction based on (Flordal and Malik 2009; Pena et al. 2009; Su et al. 2010; Malik and Leduc 2013) (Proposition 5), four further methods (Propositions 9–10) are introduced to simplify or remove events in a normalised EFSM system, which increase the possibility of abstraction.

• Lastly, this paper combines all the abstraction methods in an algorithm (Algorithm 1) for compositional nonblocking verification of EFSM systems. The algorithm is implemented in Supremica (Åkesson et al. 2006), and has been used successfully to verify several large systems. The algorithm’s performance is compared with the previously used BDD-based (Vahidi 2004) and FSM-based algorithms (Flordal and Malik 2009; Malik and Leduc 2013).

This paper is structured as follows. Section 2 introduces the notation and concepts for EFSMs, and Section 3 gives a motivating example to informally illustrate compositional nonblocking verification and abstraction of EFSM systems. Next, Section 4 explains the normalisation procedure. Then Section 5 presents the principle of compositional nonblocking verification and describes different methods to simplify EFSM systems while preserving the nonblocking property. Afterwards, Section 6 combines these results in an algorithm for compositional nonblocking verification of EFSM systems, and Section 7 presents the experimental results. Finally, Section 8 adds some concluding remarks. The A contains formal proofs of all propositions contained in the paper.

2 Preliminaries

2.1 Finite-state machines

The standard means to model discrete event systems (Ramadge and Wonham 1989) are finite-state machines (FSM), which synchronise on shared events (Hoare 1985). Events are taken from an alphabet Σ. The special silent event τ ∉ Σ is not included in Σ unless explicitly mentioned using the notation Σ _τ = Σ ∪ {τ}. Further, Σ^∗ is the set of all finite traces of events from Σ, including the empty trace ε. The concatenation of two traces s, t ∈ Σ^∗ is written as st.

Definition 1

A finite-state machine (FSM) is a tuple G = 〈Σ, Q, →, Q°, Q ^ω〉, where Σ is a set of events, Q is a finite set of states, → ⊆ Q × Σ _τ × Q is the state transition relation, Q° ⊆ Q is the set of initial states, and Q ^ω ⊆ Q is the set of marked states.

The transition relation is written in infix notation $x \overset {\sigma }{\rightarrow } y$, and is extended to traces in ${\Sigma }_{\tau }^{*}$ by $x \overset {\epsilon }{\rightarrow } x$ for all x ∈ Q, and $x \overset {s\sigma }{\rightarrow } z$ if $x \overset {s}{\rightarrow } y$ and $y \overset {\sigma }{\rightarrow } z$ for some y ∈ Q. The transition relation is also defined for state sets X ⊆ Q, for example $x \overset {s}{\rightarrow } y$ means $x \overset {s}{\rightarrow } y$ for some x ∈ X.

When two or more FSMs are brought together to interact, lock-step synchronisation in the style of (Hoare 1985) is used.

Definition 2

Let $G_{1} = \left \langle {\Sigma }_{1},Q,\rightarrow _{1},Q^{\circ }_{1},Q^{\omega }_{2}\right \rangle$ and $G_{2} = \left \langle {\Sigma }_{2},Q_{2}\rightarrow _{2},Q^{\circ }_{2},Q^{\omega }_{2}\right \rangle$ be two FSMs. The synchronous composition of G ₁ and G ₂ is

$$ G_{1} || G_{2} = \left\langle {\Sigma}_{1}\cup {\Sigma}_{2}, Q_{1}\times Q_{2},\rightarrow, Q^{\circ}_{1} \times Q^{\circ}_{2}, Q^{\omega}_{1} \times Q^{\omega}_{2} \right\rangle $$

(1)

where

$$ (x_{1},x_{2}) \overset{\sigma}{\rightarrow} (y_{1},y_{2}) \quad \text{if } \sigma \in{\Sigma}_{1} \cap {\Sigma}_{2},\ x_{1} \overset{\sigma}{\rightarrow}_{1} y_{1}, \;\text{and}\; x_{2} \overset{\sigma}{\rightarrow}_{2} y_{2} \ ; $$

(2)

$$ (x_{1},x_{2}) \overset{\sigma}{\rightarrow} (y_{1},x_{2}) \quad \text{if } \sigma \in ({\Sigma}_{1} \setminus {\Sigma}_{2})\cup\{\tau\}\ \text{and}\ x_{1} \overset{\sigma}{\rightarrow}_{1} y_{1} \ ; $$

(3)

$$ (x_{1},x_{2}) \overset{\sigma}{\rightarrow} (x_{1},y_{2}) \quad \text{if } \sigma \in ({\Sigma}_{2} \setminus {\Sigma}_{1})\cup\{\tau\}\ \text{and}\ x_{2} \overset{\sigma}{\rightarrow}_{2} y_{2} \ . $$

(4)

Hiding is the act of replacing certain events by the silent event τ.

Definition 3

Let G = 〈Σ, Q, →, Q°, Q ^ω〉 be an FSM, and let Υ ⊆ Σ. The result of hiding Υ from G is

$$ G \setminus {\Upsilon} = \langle{\Sigma}\setminus{\Upsilon}, Q,\rightarrow \setminus {\Upsilon}, Q^{\circ},Q^{\omega}\rangle, $$

(5)

where → ∖Υ is obtained from → by replacing all events in Υ with the silent event τ.

This paper concerns verification of the nonblocking property, which is commonly used in supervisory control theory of discrete event systems (Ramadge and Wonham 1989). A system is nonblocking if, from every reachable state, it is possible to reach a marked state, i.e., a state in Q ^ω.

Definition 4

An FSM G = 〈Σ, Q, →, Q°, Q ^ω〉 is nonblocking if, for every trace $s \in {\Sigma }^{\ast }_{\tau }$ and every state x ∈ Q such that $Q^{\circ } \overset {s}{\rightarrow } x$, there exists a trace $t \in {\Sigma }^{\ast }_{\tau }$ such that $x \overset {t}{\rightarrow } Q^{\omega }$.

2.2 Extended finite-state machines

Extended finite-state machines (EFSM) are similar to conventional finite-state machines, but augmented with updates associated to the transitions (Chen and Lin 2000; Sköldstam et al. 2007). Updates are formulas constructed from variables, integer constants, the Boolean literals true and false, and the usual arithmetic and logic connectives.

A variable v is an entity associated with a bounded discrete domain dom (v) and an initial value v° ∈ dom(v). Let V = {v ₀, … , v _n } be the set of variables with domain dom (V) = dom(v ₀) × … × dom(v _n ). An element of dom (V) is also called a valuation and is denoted by $\hat {v} = (\hat {v}_{0}, \ldots , \hat {v}_{n})$ with $\hat {v}_{i} \in \text {dom}(v_{i})$, and the value associated to variable v _i ∈ V is denoted $\hat {v}[v_{i}]=\hat {v}_{i}$. The initial valuation is $v^{\circ }=(v_{0}^{\circ }, \ldots , v_{n}^{\circ })$.

A second set of variables, called next-state variables and denoted by V′ = { v′∣v ∈ V } with dom(V′) = dom(V), is used to describe the values of the variables after execution of a transition. Variables in V are also referred to as current-state variables to differentiate them from the next-state variables in V′. The set of all update formulas using variables in V and V′ is denoted by π _V .

For an update p ∈ π _V , the term vars(p) denotes the set of all variables that occur in p, and vars′(p) denotes the set of all variables whose corresponding next-state variables occur in p. For example, if p ≡ x′ = y + 1 then vars(p) = {x, y} and vars′(p) = {x}. Here and in the following, the relation ≡ denotes syntactic identity of updates to avoid ambiguity when an update contains the equality symbol =. An update p without any next-state variables, vars′(p) = ∅, is called a pure guard. Usually it is understood that variables that do not appear as next-state variables remain unchanged, and the execution of a pure guards does not change any variables. To get this interpretation, the following notion of extension is used.

Definition 5

Let p ∈ π _V be an update. The extension of p to W ⊆ V is

$$ {\Xi}_{W}(p) \;\equiv\; p \land \bigwedge\nolimits_{v\in W \setminus \text{vars}^{\prime}(p)} v^{\prime}=v . $$

(6)

The extension is constructed syntactically by adding to the update p equations v′ = v for all variables v ∈ W that do not already appear as next-state variables in p. For example, Ξ_{x}(x = 1) ≡ x = 1 ∧ x′ = x and Ξ_{{x, y}}(x′ = y + 1) ≡ x′ = y + 1 ∧ y′ = y. Another important way to rewrite updates is substitution, which performs syntactic replacement of subformulas.

Definition 6

A substitution is a mapping [z ₁ ↦ a ₁, … , z _n ↦ a _n ] that maps variables z _i to terms a _i . Given an update p ∈ π _V , the substitution instance p[z ₁ ↦ a ₁, … , z _n ↦ a _n ] is the update obtained from p by simultaneously replacing each occurrence of z _i by a _i .

For example, (x′ = x + y)[x′ ↦ 1, x ↦ 0] ≡ 1 = 0 + y.

With slight abuse of notation, updates p ∈ π _V are also interpreted as predicates over their variables, and they are evaluated to F or T, i.e., p:dom(V) × dom(V′) → {F, T}. For example, if V = {x} with dom(x) = {0, 1}, then the update p ≡ x′ = x + 1 means that the value of the variable x in the next state will be increased by 1 over its current-state value. Its predicate p(x, x′) evaluates to true as p(0, 1) = T and to false as p(1, 1) = F.

Definition 7

An extended finite-state machine (EFSM) is a tuple E = 〈Σ, Q, →, Q°, Q ^ω〉, where Σ is a set of events, Q is a finite set of locations, → ⊆ Q × Σ × π _V × Q is the conditional transition relation, Q° ⊆ Q is the set of initial locations, and Q ^ω ⊆ Q is the set of marked locations.

The expression $q_{0} \overset {\sigma :p}\to q_{1}$ denotes the presence of a transition in E, from location q ₀ to location q ₁ with event σ and update p. Such a transition can occur if the EFSM is in location q ₀ and the update p evaluates to T, and when it occurs, the EFSM changes its location from q ₀ to q ₁ while updating the variables in vars′(p) in accordance with p; variables not contained in vars′(p) remain unchanged. This can be implemented by first assigning next-state variables such that the update formula p is satisfied, and after the transition assigning the values of the next-state variables to the corresponding current-state variables.

For example, let x be a variable with domain dom(x) = {0, … , 5}. A transition with update x′ = x + 1 changes the variable x by adding 1 to its current value, if it currently is less than 5. Otherwise (if x = 5) the transition is disabled and no updates are performed. The update x = 3 disables a transition unless x = 3 in the current state, and the value of x in the next state is not changed. Differently, the update x′ = 3 always enables its transition, and the value of x in the next state is forced to be 3.

Given an EFSM E = 〈Σ, Q, →, Q°, Q ^ω〉, its alphabet is also denoted by Σ _E = Σ. The variable set of E is $\text {vars}(E) = \bigcup _{(q_{0},\sigma ,p,q_{1}) \in \to } \text {vars}(p)$, and it contains all the variables that appear on some transitions of E.

Usually, reactive systems are modelled as several components interacting with each other. Such a model is called an EFSM system.

Definition 8

An EFSM system is a collection of interacting EFSMs,

$$ \mathcal{E}{E} = \{ E_{1}, \ldots, E_{n}\} . $$

(7)

The alphabet of the system$~\mathcal {E}$ is ${\Sigma }_{\mathcal {E}}=\bigcup _{E \in \mathcal {E}} {\Sigma }_{E}$, and the variable set of $\mathcal {E}$ is $\text {vars}(\mathcal {E}) = \bigcup _{E \in \mathcal {E}} \text {vars}(E)$.

In the synchronisation of EFSMs, similar to FSMs, shared events between two EFSMs are synchronised in lock-step, while other events are interleaved. In addition, the updates are combined by conjunction.

Definition 9

Given two EFSMs $E_{1} \,=\, \langle {{\Sigma }_{1},Q_{1},\!\to \!_{1},Q^{\circ }_{1},Q^{\omega }_{1}\rangle }$ and $E_{2} \,=\, \langle {{\Sigma }_{2},Q_{2}, \!\to \!_{2},Q^{\circ }_{2},Q^{\omega }_{2}\rangle }$, the synchronous composition of E ₁ and E ₂ is $E_{1} || E_{2} = \langle {\Sigma }_{1} \cup {\Sigma }_{2}, Q_{1}\times Q_{2}, \to _{2}, Q^{\circ }_{1} \times Q^{\circ }_{2}, Q^{\omega }_{1} \times Q^{\omega }_{2}\rangle$, where:

$$\begin{array}{@{}rcl@{}} (x_{1},x_{2}) {~}^{\underrightarrow{\;\;\sigma:p_{1} \wedge p_{2}\;\;}} (y_{1},y_{2}) \quad&\text{if}& \sigma \in {\Sigma}_{1} \cap {\Sigma}_{2},\ x_{1} {{~}^{\underrightarrow{\;\;\sigma:p_{1}\;\;}}}_{1} y_{1},\ \text{and}\ x_{2} {{~}^{\underrightarrow{\;\sigma:p_{2}\;}}}_{2} y_{2} \ ; \end{array} $$

(8)

$$\begin{array}{@{}rcl@{}} (x_{1},x_{2}) {~}^{\underrightarrow{\;\sigma:p_{1}\;}} (y_{1},x_{2})\quad & \text{if}& \sigma \in {\Sigma}_{1} \setminus {\Sigma}_{2}\ \text{and}\ x_{1} {{~}^{\underrightarrow{\sigma:p_{1}}}}_{1} y_{1} \ ; \end{array} $$

(9)

$$\begin{array}{@{}rcl@{}} (x_{1},x_{2}) {~}^{\underrightarrow{\sigma:p_{2}}} (x_{1},y_{2}) & \quad\!\!\!\!\!\text{if}& \sigma \in {\Sigma}_{2} \setminus {\Sigma}_{1}\ \text{and}\ x_{2} {{~}^{\underrightarrow{\sigma:p_{2}}}}_{2} y_{2} \ . \end{array} $$

(10)

Using Definition 9, the global behaviour of a system $\mathcal {E}=\{E_{1}{\ldots } E_{n}\}$ is expressed as $||\mathcal {E}=E_{1} || {\cdots } || E_{n}$.

The standard approach to verify the nonblocking property of EFSMs evaluates all variable values. This is done by flattening, which introduces states for all combinations of locations and variable values (Baier and Katoen 2008).

Definition 10

Let E = 〈Σ, Q, →, Q°, Q ^ω〉 be an EFSM with variable set vars(E) = V. The monolithic flattened FSM of E is $U(E) = \langle {\Sigma ,Q_{U},\to _{U},Q^{\circ }_{U},Q^{\omega }_{U}\rangle }$ where

• Q _U = Q × dom(V);

• $(x,\hat {v})\overset {\sigma }{\to }_{U}(y,\hat {w})$ if E contains a transition $x \overset {\sigma :p}{\to } y$ such that ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$;

• $Q^{\circ }_{U} = Q^{\circ }\times \{v^{\circ }\}$;

• $Q^{\omega }_{U} = Q^{\omega }\times \text {dom}(V)$.

The inclusion of the variable values $\hat {v}$ in the states of the monolithic flattened FSM ensures the correct sequencing of transitions. The use of Ξ _V (p) as opposed to p in the definition of → _U ensures that a variable x can only change its value if its corresponding next-state variable x′ appears in the update p. The monolithic flattened FSM of an EFSM system $\mathcal {E} = \{E_{1},\ldots ,E_{n}\}$ is $U(\mathcal {E}) = U(E_{1} || {\cdots } || E_{n})$. Using these definitions, the nonblocking property is also defined for EFSMs and EFSM systems.

Definition 11

An EFSM E or an EFSM system $\mathcal {E}$ is nonblocking if the monolithic flattened FSM U(E) or $U(\mathcal {E})$, respectively, is nonblocking.

3 Motivating example

This section demonstrates the process of EFSM-based compositional nonblocking verification using a simple manufacturing system modelled as interacting extended finite state-machines. The manufacturing system consists of four devices C B ₁, C B ₂, M ₁, and M ₂ as shown in Fig. 1. C B ₁ and C B ₂ are sections of a conveyor belt. The total capacity of the conveyor belt is given by a parameter N ≥ 1, where it is assumed that N = 2 in the remainder of this section. Workpieces are loaded onto C B ₁ (event l ₁) from outside the system, and transported over to C B ₂ (event l ₂). When workpieces enter C B ₂, a part detection sensor determines the type of workpieces (events p ₁ and p ₂). When workpieces leave C B ₂, type 1 workpieces are loaded into machine M ₁ (event s ₁), and type 2 workpieces are loaded into machine M ₂ (event s ₂). The machines M ₁ and M ₂ then process their workpieces and output them from the system ( f ₁ and f ₂).

Fig. 1

Manufacturing system example

The EFSM model consists of the EFSMs C B ₁, C B ₂, M ₁, and M ₂ as shown in Fig. 1. It uses variables v ₁ and v ₂ with domain {0, … , N} to represent the number of workpieces on conveyor section C B ₁ and C B ₂, respectively, and a variable t with domain {0, 1, 2} to keep track of the type of workpiece as determined by the sensor at C B ₂.

The update $v_{1}+v_{2}<N \land v_{1}^{\prime }=v_{1}+1$ for event l ₁ in C B ₁ enforces the capacity restriction of the conveyor belt by preventing the loading of another workpiece onto C B ₁ unless both conveyor sections combined have less than N workpieces, v ₁ + v ₂ < N, and if the event l ₁ occurs, it increases the number of workpieces on C B ₁ by 1, $v^{\prime }_{1}=v_{1}+1$. For illustration, C B ₂ contains a transition to the blocking state ⊥ to represent that conveyor section C B ₂ exceeds the capacity limit. It becomes part of the nonblocking verification to confirm that this transition is never taken.

The model in Fig. 1 is blocking, because the part recognition procedure is not implemented correctly in C B ₂. In the following, it is demonstrated how the compositional nonblocking verification algorithm finds this fault and shows that the system is blocking without exploring the full state space.

Before EFSM-based compositional nonblocking verification starts, the preprocessing step of normalisation transforms the model in such a way that each event corresponds to a unique update. This facilitates reasoning about a composed system as it shows directly what effect the execution of events has on all the variables.

In order to normalise a system, the first step is to normalise individual components. The EFSM C B ₂ is not normalised, because the event l ₂ corresponds to two different updates $v_{2}<N \land v_{2}^{\prime }=v_{2}+1$ and v ₂ = N. To normalise C B ₂, event l ₂ is replaced by two new events l ₂₁ and l ₂₂, where the update of l ₂₁ is $v_{2}<N \land v_{2}^{\prime }=v_{2}+1$ and the update of l ₂₂ is v ₂ = N. Having replaced l ₂ in C B ₂, the transition labelled with l ₂ in C B ₁ is replaced by two transitions labelled l ₂₁ and l ₂₂, both of which have the update $0<v_{1} \land v_{1}^{\prime }=v_{1}-1$ of the original l ₂-transition in C B ₁. These steps result in two EFSMs C ₁ and C ₂, shown in Fig. 2, which replace C B ₁ and C B ₂ in the system. This way of normalising components individually preserves the synchronous composition of the system except for the renaming of events.

Fig. 2

Normalised EFSMs obtained from C B ₁ and C B ₂

Now the EFSMs are individually normalised, as each event has a unique update within each EFSM. Yet, the system as a whole is not yet normalised, because s ₁ has the update t = 1 ∧ 0 < v ₂ in C ₂ and another update $t^{\prime }=0\land v^{\prime }_{2}=v_{2}-1$ in M ₁. To normalise the system, the update of each event is replaced by the conjunction of the updates of the event in all the components it occurs in. For example, after normalisation the update of event s ₁ becomes

$$ t=1 \land 0<v_{2} \land t^{\prime}=0 \land v_{2}^{\prime}=v_{2}-1\ . $$

(11)

This conjunction is well-defined for each event since, after the first step above, events have unique updates in each component. Figure 3 shows the normalised form of the system. Normalisation makes it unnecessary to write the updates on the transitions. Instead, the information about the updates of the events is given in the table in Fig. 3.

Fig. 3

Normalised manufacturing system for N = 2.

Now the EFSM system is normalised, and nonblocking verification can start. This is done by constructing an abstraction of the synchronous composition of the system in several small steps. At each step, either EFSMs are abstracted and replaced by EFSMs with less transitions or locations, or variables are unfolded, replacing them by EFSMs and producing simpler updates. Synchronous composition is computed step by step on the abstracted EFSMs. In the end, all the variables are unfolded and the final result is a single abstracted FSM, which is simpler than the result of flattening the original EFSM system would be, while it has the same property of being nonblocking or not. Then standard monolithic nonblocking verification is applied to this abstracted FSM.

After normalisation, the system is $\mathcal {E} = \{\mathcal {N}(C_{1}), \mathcal {N}(C_{2}), \mathcal {N}(M_{1}), \mathcal {N}(M_{2})\}$ as shown in Fig. 3. In the first step of compositional nonblocking verification, individual EFSMs are abstracted if possible. Event f ₁ only appears in $\mathcal {N}(M_{1})$. Such events are referred to as local events. If the update of a local event is true, then transitions labelled by that event are always executable and execution will not change the value of any variable. Thus, local events corresponding to true updates can be hidden, that is, replaced by the silent event τ. After hiding the local event f ₁ in $\mathcal {N}(M_{1})$, the two states of $\mathcal {N}(M_{1})$ can be merged using the conflict-preserving abstraction method of observation equivalence (Milner 1989). The same steps are applied to $\mathcal {N}(M_{2})$. Fig. 4 shows the EFSMs $\mathcal {N}(M_{1})\setminus \{f_{1}\}$ and $\mathcal {N}(M_{2}) \setminus \{f_{2}\}$ resulting from hiding and the resulting abstractions $\tilde {M}_{1}$ and $\tilde {M_{2}}$.

Fig. 4

Abstraction results of $\mathcal {N}(M_{1})$ and $\mathcal {N}(M_{2})$.

Events l ₁, p ₁, and p ₂ are also local. However, these events cannot yet be hidden because of their nontrivial updates. Since the abstraction methods greatly benefit from hiding, the next step is to simplify updates of some events to make hiding possible.

The only variable in the updates of p ₁ and p ₂ is t. This observation suggests to unfold the variable t, removing this variable from the updates, so that the events p ₁ and p ₂ can be hidden and more abstraction becomes possible. Partial unfolding replaces a variable by a new EFSM, called the variable EFSM, which has one location for each value in the domain of the unfolded variable, and transitions that reflect the way the variable is updated by the corresponding events. The variable EFSM T for t, shown in Fig. 5, has three locations corresponding to dom(t) = {0, 1, 2}. The variable t changes from 0 to 1 and from 0 to 2 by executing events p ₁ and p ₂, respectively, and from 1 to 0 on the occurrence of s ₁, and from 2 to 0 on the occurrence of s ₂. Now the updates of these events can be simplified as the variable EFSM T contains the effect the events have on the variable t. The results are shown in the table in Fig. 5: the updates of s ₁ and s ₂ are simplified to no longer include t, and the updates of p ₁ and p ₂ become true. However, p ₁ and p ₂ are no longer local events as they now appear in the variable EFSM T and in $\mathcal {N}(C_{2})$.

Fig. 5

The components after unfolding t.

So, now the synchronous composition $TC = T || \mathcal {N}(C_{2})$ is constructed, shown in Fig. 5, which has local events p ₁ and p ₂ that can now be hidden because of their true updates. Hiding results in the EFSM T C∖{p ₁, p ₂}, also shown in Fig. 5. All the states ⊥ can be merged since the system will be blocking if it ends up in any of these states. Also, the only states that can be reached from q ₁ are q ₂ and q ₃, and they can only be reached by the silent event τ. Such a state can be removed by the Only Silent Outgoing Rule as only the τ-successor states are relevant for conflict equivalence (Flordal and Malik 2009). The EFSM T C∖{p ₁, p ₂} can thus be simplified to $\widetilde {TC}$ in Fig. 5.

Next, the composition $\widetilde {TC} || \tilde {M}_{1} || \tilde {M_{2}}$ is found to be equal to $\widetilde {TC}$, and it results in the events s ₁ and s ₂ being local. From the table in Fig. 5, it can be observed that the updates of s ₁ and s ₂ only depend on the variable v ₂. Thus, the variable v ₂ is unfolded, which results in the variable EFSM V ₂ shown in Fig. 6. The event l ₁ with update $v_{1}+v_{2}<2 \land v_{1}^{\prime }=v_{1}+1$ does not change the value of the variable v ₂, so it appears on two selfloop transitions in EFSM V ₂. Firstly, the case v ₂ = 0 gives rise to a selfloop on state 0 with an update that simplifies to $v_{1}<2 \land v_{1}^{\prime }=v_{1}+1$, and secondly the case v ₂ = 1 gives rise to a selfloop on state 1 with simplified update $v_{1}<1 \land v_{1}^{\prime }=v_{1}+1$. To keep the system normalised after unfolding, the event l ₁ is renamed and replaced by two new events l ₁₀ and l ₁₁ each with a unique update. This renaming also affects component $\mathcal {N}(C_{1})$, where the transition labelled l ₁ is replaced by transitions with both the new events, resulting in $C^{\prime }_{1}$ in Fig. 6. The other events l ₂₁, s ₁, and s ₂ also have two transitions each, but their updates simplify to the same expression in each case, which means that there is no need for further renaming.

Fig. 6

The components after unfolding v ₂

After composition of V ₂ and $\widetilde {TC} || \tilde {M}_{1} || \tilde {M_{2}} = \widetilde {TC}$, events s ₁ and s ₂ can be hidden, resulting in T C V∖{s ₁, s ₂} shown in Fig. 6. Here, states q ₁ and q ₂ have equivalent outgoing transitions. These states can be merged using observation equivalence (Milner 1989), resulting in the abstraction $\widetilde {TC}V$ also shown in Fig. 6. The event l ₂₂ becomes always disabled after synchronisation of V ₂ and T C′, so it is removed from the model. This confirms that the transition $q_{0} {~}^{\underrightarrow {\;\;l_{2}\;\;}} \bot$ in C B ₂ never occurs.

After all these abstractions, only the EFSMs $C^{\prime }_{1}$ and $\widetilde {TC}V$ and the variable v ₁ remain. The final step is to unfold v ₁, which results in the variable EFSM V ₁ shown in Fig. 7, where all updates are true. The synchronous composition of $C^{\prime }_{1}$, $\widetilde {TC}V$, and V ₁, also shown in Fig. 7, is blocking. This essentially shows that the system blocks if a second workpiece enters C B ₂ by executing l ₂, before the previous workpiece is released by executing s ₁ or s ₂. As the final abstraction result is blocking, it is concluded that the original model in Fig. 1 is blocking. The largest component created during the compositional steps to obtain this result is TC in Fig. 5 with nine locations and ten transitions. In contrast, standard monolithic verification would have to flatten the entire system at once, which creates a blocking FSM with 44 states and 104 transitions.

Fig. 7

The final abstracted system after unfolding v ₁.

This example demonstrates how EFSM-based compositional verification works. In the sequel, Section 4 explains formally the normalisation process, and Section 5 describes the abstraction methods.

4 Normalisation

The first step of the compositional nonblocking verification algorithm proposed in this paper is normalisation, which rewrites an EFSM system in such a way that each event has its own distinct update. This makes it possible to examine directly the effect that executing an event has on the variables, greatly simplifying the processing of EFSM systems during the later steps of compositional verification.

Definition 12

An EFSM system $\mathcal {E}$ is normalised if for all transitions $x_{1} {~}^{\underrightarrow {\;\;\sigma :p_{1}\;\;}} x_{2}$ and $y_{1} {~}^{\underrightarrow {\;\sigma :p_{2}\;\;}} y_{2}$ it holds that p ₁ ≡ p ₂. An EFSM E is normalised if the EFSM system {E} is normalised.

Definition 13

For a normalised EFSM or EFSM system E, the expression Δ _E (σ) denotes the unique update associated with the event σ ∈ Σ _E . Moreover, for all σ ∈ Σ _E such that there does not exist any transition $x {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y$ in E, it is defined that Δ _E (σ) ≡ false.

If an EFSM system $\mathcal {E}$ is normalised, then each event associates to a unique update, and ${\Delta }_{\mathcal {E}}(\sigma )$ is well-defined. Then the association of updates to events can be maintained separately, and EFSMs can be represented without updates on transitions, as it is done in the figures in Section 3. In a normalised EFSM system, synchronous composition also becomes simpler, because there is no need to combine update formulas.

Definition 14

Let $E_{1} = \langle {{\Sigma }_{1},Q_{1},\to ,Q^{\circ }_{1},Q^{\omega }_{1}\rangle }$ and $E_{2} = \langle {{\Sigma }_{2},Q_{2},\to ,Q^{\circ }_{2},Q^{\omega }_{2}\rangle }$ be EFSMs. The normalised synchronous composition of E ₁ and E ₂ is $E_{1} \dot {\|} E_{2} = \langle {\Sigma }_{1} \cup {\Sigma }_{2} , Q_{1}\times Q{2} \to , Q^{\circ }_{1} \times Q^{\circ }_{2} , Q^{\omega }_{1} \times Q^{\omega }_{2} \rangle$, where:

$$\begin{array}{@{}rcl@{}} (x_{1},x_{2}) {~}^{\underrightarrow{\;\;\sigma:p\;\;}} (y_{1},y_{2}) & \quad& \text{if } \sigma \in {\Sigma}_{1} \cap {\Sigma}_{2},\ x_{1} {~}^{\underrightarrow{\;\;\sigma:p\;\;}}_{1} y_{1},\ \text{and}\ x_{2} {~}^{\underrightarrow{\;\;\sigma:p\;\;}}_{2} y_{2}; \end{array} $$

(12)

$$\begin{array}{@{}rcl@{}} (x_{1},x_{2}) {~}^{\underrightarrow{\;\;\sigma:p\;\;}} (y_{1},x_{2}) & \quad& \text{if } \sigma \in {\Sigma}_{1} \setminus {\Sigma}_{2}\ \text{and}\ x_{1} {~}^{\underrightarrow{\;\;\sigma:p\;\;}}_{1} y_{1}; \end{array} $$

(13)

$$\begin{array}{@{}rcl@{}} (x_{1},x_{2}) {~}^{\underrightarrow{\;\;\sigma:p\;\;}} (x_{1},y_{2}) & \quad& \text{if } \sigma \in {\Sigma}_{2} \setminus {\Sigma}_{1}\ \text{and}\ x_{2} {~}^{\underrightarrow{\;\;\sigma:p\;\;}}_{2} y_{2} \ . \end{array} $$

(14)

In normalised synchronous composition, events and updates are treated as one entity, and synchronisation between transitions in two EFSMs is only possible when the events and updates are the same. In a normalised system, where all updates are uniquely determined by the event, this works like synchronous composition of FSMs (Definition 2): EFSMs can be composed by considering only the events, ignoring the updates. Normalised synchronous composition of a normalised EFSM system results in a normalised EFSM that produces the same flattening result as EFSM synchronous composition (Definition 9). This is confirmed by the following proposition.

Proposition 1

Let $\mathcal {E}$ be a normalised EFSM system. Then $U(||\mathcal {E}) = U(\dot {\|}\mathcal {E})$.

By Proposition 1, if the system is normalised, the computation of the synchronous composition can be simplified using normalised synchronous composition. This paper concerns the verification of the nonblocking property of EFSM systems. As normalised synchronous composition produces the same flattening results as synchronous composition by Proposition 1, it follows in combination with Definition 11 that normalised synchronous composition preserves the nonblocking property of an EFSM system.

If a given EFSM system $\mathcal {E}$ is not normalised, it can be transformed into a normalised system by the two-step process of normalisation explained in the following. In the first step, individual EFSM components are normalised, and in the second step, the system is normalised as a whole. First, individual EFSMs are normalised by introducing new events and using a renaming.

Definition 15

Let Σ₁ and Σ₂ be two alphabets. A renaming of Σ₁ to Σ₂ is a surjective map ρ : Σ₂ → Σ₁.

If an EFSM $E\in \mathcal {E}$ is not normalised, then some event σ in E is linked to more than one update. To normalise E, new events $\sigma _{i}\notin {\Sigma }_{\mathcal {E}}$ are introduced for each update p _i associated with σ and a renaming is created that maps these new events to the original event σ, i.e., ρ(σ _i ) = σ. This results in a renamed EFSM F such that ρ : Σ _F → Σ _E and ρ(F) = E, and Δ _F (σ) is well-defined for each σ ∈ Σ _F .

Example 1

EFSM C B ₂ in Fig. 1 is not normalised since l ₂ corresponds to two different updates $v_{2}<N \land v_{2}^{\prime }=v_{2}+1$ and v ₂ = N. To normalise C B ₂, new events l ₂₁ and l ₂₂ are created, and the renaming ρ is introduced such that ρ(l ₂₁) = ρ(l ₂₂) = l ₂ and ρ(σ) = σ for all σ ∉ {l ₂₁, l ₂₂}. This results in the renamed EFSM C ₂ shown in Fig. 2, with ${\Delta }_{C_{2}}(l_{21}) \equiv v_{2}<N \land v_{2}^{\prime }=v_{2}+1$ and ${\Delta }_{C_{2}}(l_{22}) \equiv v_{2}=N$.

After applying a renaming to some component E in a system $\mathcal {E}$, a corresponding inverse renaming needs to be applied to all the remaining system components E′ ≠ E of $\mathcal {E}$, to comply with the event modification.

Definition 16

Let E = 〈Σ _E , Q, →, Q°, Q ^ω〉 be an EFSM, and let $\rho \colon {\Sigma }_{E}^{\prime } \to {\Sigma }_{E}$ be a renaming. Then $\rho ^{-1}(E) = \langle {\Sigma }_{E}^{\prime }, Q, \rho ^{-1}(\to ), Q^{\circ },Q^{\omega }\rangle$ where $\rho ^{-1}(\to ) = \{\, (x,\sigma ,p,y) \mid x {~}^{\underrightarrow {\rho (\sigma ):p}} y\,\}$.

The EFSM ρ ⁻¹(E) is obtained by replacing transitions labelled by a replaced event σ with transitions labelled by all the events replacing it.

Example 2

After normalising C B ₂ in Fig. 1, the EFSM C B ₁ is replaced by C ₁ = ρ ⁻¹(C B ₁), which is obtained by replacing the l ₂-transition by two transitions labelled l ₂₁ and l ₂₂, both of which have the update $0<v_{1} \land v_{1}^{\prime }=v_{1}-1$ of the original l ₂-transition in C B ₁. The EFSM C ₁ = ρ ⁻¹(C B ₁) is shown in Fig. 2.

The following proposition confirms that the structure of an EFSM system remains unchanged when a single EFSM is normalised using the combination of renaming and inverse renaming described above. The behaviour of the original system can be regained by applying the renaming to the synchronous composition of the renamed system.

Proposition 2

Let $\mathcal {E}$ and $\mathcal {F}$ be EFSM systems, and let $\rho : {\Sigma }_{\mathcal {F}} \to {\Sigma }_{\mathcal {E}}$ be a renaming, such that $\mathcal {E}=\{E_{1}, E_{2},\ldots , E_{n}\}$ and $\mathcal {F} = \{F_{1}\, \rho ^{-1}(E_{2}),\ldots , \rho ^{-1}(E_{n})\}$ and ρ(F ₁ ) = E ₁ . Then $\rho (||\mathcal {F}) = ||\mathcal {E}$.

The repeated application of Proposition 2 to all components of an EFSM system with appropriate renamings results in a system where each EFSM is normalised individually. Yet, the system as a whole is not necessarily normalised as events shared between different EFSMs may be associated with different updates in their EFSMs. Therefore, a second step is needed to normalise the whole system.

Definition 17

Let $\mathcal {E}=\{E_{1},\ldots , E_{n}\}$ be an EFSM system such that all $E_{i}=\langle {\Sigma }_{i},Q_{i},\to _{i},Q^{\circ }_{\omega },Q^{\omega }_{i}\rangle$ for 1 ≤ i ≤ n are individually normalised. The normalised form of $\mathcal {E}$ is $\mathcal {N}(\mathcal {E}) = \{\mathcal {N}(E_{1}),\ldots , \mathcal {N}(E_{n})\}$ where $\mathcal {N}(E_{i}) = \langle {\Sigma }_{i}, Q_{i}, {\to ^{N}_{i}}, Q^{\circ }_{i},Q^{\omega }\rangle$ and ${\to ^{N}_{i}} = \{\, (x, \sigma , {\Delta }_{\mathcal {N}(\mathcal {E})}(\sigma ), y) \mid x {~}^{\underrightarrow {\;\;\sigma :p\;\;}}_{i} y\,\}$ and ${\Delta }_{\mathcal {N}(\mathcal {E})}(\sigma ) = \bigwedge _{i:\sigma \in {\Sigma }_{i}} {\Delta }_{E_{i}}(\sigma )$.

The normalised system is obtained by assigning to each event a single update, which is the conjunction of the updates corresponding to the event in the different EFSMs. Under the assumption that the individual EFSMs in a system are individually normalised, the normalised system $\mathcal {N}(\mathcal {E})$ obtained by Definition 17 fulfils the requirement of a normalised system given in Definition 12. The update of each event after normalisation is essentially the update that would have been calculated by synchronous composition. Then, since the normalisation of individual components preserves the synchronous composition, the complete normalisation process also preserves the structure of synchronous composition of the system as a whole.

Example 3

After normalisation of the system in Section 3, the updates of the events l ₂₁ and l ₂₂ are the conjunction of the updates of these events in C ₁ and C ₂. For example, event l ₂₁ is associated with $0<v_{1} \land v^{\prime }_{1}=v_{1}-1$ in C ₁ according to Example 2 and with $v_{2}<N \land v_{2}^{\prime }=v_{2}+1$ in C ₂ according to Example 1, so its update in the normalised system is ${\Delta }_{\mathcal {N}(\mathcal {E})}(l_{21}) \equiv 0<v_{1} \land v^{\prime }_{1}=v_{1}-1 \land v_{2}<N \land v_{2}^{\prime }=v_{2}+1$ as shown in the table in Fig. 3.

The following proposition confirms that the behaviours of an EFSM system $\mathcal {E}$ and its normalised form $\mathcal {N}(\mathcal {E})$ are identical if normalised synchronous composition is used to describe the behaviour of the normalised system.

Proposition 3

Let $\mathcal {E}$ be an EFSM system such that each $E \in \mathcal {E}$ is normalised. Then $||\mathcal {E} = \dot {\|}\mathcal {N}(\mathcal {E})$.

The first step to normalise a system is to normalise individual components. Proposition 2 confirms that the behaviours of a system before and after normalisation of each component are identical up to renaming of the events. As renaming preserves the nonblocking property, normalisation of individual EFSMs does not change the nonblocking property of the system. When all individual components of a system are normalised, next the operation $\mathcal {N}(\cdot )$ is applied to associate each event with a unique update in the system. Proposition 3 guarantees that the normalised system behaviour as described using normalised synchronous composition is identical up to isomorphism to the original system behaviour. Moreover, Proposition 1 and Definition 11 together guarantee that normalised synchronous composition preserves the nonblocking property. Therefore it follows from Propositions 1–3 that the normalisation procedure preserves the nonblocking property of an EFSM system. Proofs of Proposition 1–3 are given in Appendix A.

5 EFSM-based compositional verification

The objective of compositional nonblocking verification is to determine whether a normalised EFSM system

$$ \mathcal{E}=\{E_{1} , E_{2} , {\ldots} , E_{n}\}\ . $$

(15)

is nonblocking. If a given system is not normalised, it can be normalised without affecting the nonblocking property as explained in Section 4. The straightforward approach to verify whether the system (15) is nonblocking, is to monolithically flatten the system and check for each reachable state whether it is possible to reach a marked state. However, this technique is limited by the state-space explosion problem.

In an attempt to alleviate state-space explosion, compositional verification (Flordal and Malik 2009) seeks to repeatedly rewrite individual components, and for example, replace E ₁ in (15) by an abstraction F ₁, and then to analyse the simpler system {F ₁, E ₂, … , E _n }.

The abstraction steps to simplify the individual components E _i must satisfy certain conditions to guarantee that the verification result is preserved. One equivalence to support nonblocking verification is conflict equivalence (Malik et al. 2006).

Definition 18

Two EFSMs (or FSMs) E and F are said to be conflict equivalent, written E ≃ _{c o n f} F, if for any EFSM (or FSM) T, it holds that E||T is nonblocking if and only if F||T is nonblocking.

Due to the congruence properties of conflict equivalence (Malik et al. 2006), components of an FSM system can be replaced by conflict equivalent components while preserving the nonblocking property. This follows directly from Definition 18 when T represents the rest of the system. It is straightforward to lift this result to EFSMs.

Proposition 4

Let $\mathcal {E} = \{ E_{1}, \ldots , E_{n}\}$ and $\mathcal {F} = \{ F_{1}, E_{2}, \ldots , E_{n}\}$ be EFSM systems such that E ₁ ≃ _conf F ₁ . Then $\mathcal {E}$ is nonblocking if and only if $\mathcal {F}$ is nonblocking.

If no abstraction is possible, then some components are composed to create local events or some variables are unfolded to simplify some updates. The resulting EFSMs are abstracted again, and the procedure continues until all the variables of the systems are unfolded and the system is simple enough to be verified monolithically. To ensure correctness, all these operations are performed in such a way that the nonblocking and normalisation properties of the system are preserved.

The above-mentioned abstraction methods of FSM-based abstraction, synchronous composition, and variable unfolding are described in more detail in the following Sections 5.1, 5.2, and 5.4. Section 5.3 describes the method of update simplification, which is closely linked to variable unfolding. Finally, Section 5.5 proposes four further methods to reduce the number of events and transitions in an EFSM system.

5.1 FSM-based conflict equivalence abstraction

Compositional nonblocking verification is well-developed for systems modelled as interacting finite-state machines (Flordal and Malik 2009; Malik and Leduc 2013). Several abstraction methods for FSM-based compositional nonblocking verification with efficient implementations are known. This section shows how these methods can be applied directly to EFSMs without first flattening or unfolding any variables.

Definition 19

Let E = 〈Σ, Q, →, Q°, Q ^ω〉 be a normalised EFSM. The FSM form of E is the FSM φ(E) = 〈Σ, Q,→ _φ , Q°, Q ^ω〉, where $x{{~}^{\underrightarrow {\sigma }}}_{\varphi } y$ if $x {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y$ for some x, y ∈ Q.

The FSM form of an EFSM is obtained by simply disregarding all updates. This differs from the flattened FSM (Definition 10), where variable values are expanded and updates evaluated. The conversion to FSM form and back is a straightforward operation that does not incur any blow-up, yet it makes it possible to apply FSM simplification to EFSMs. The transformation relies on the system being normalised, because in a normalised system each event has a unique update, making it possible to disregard the updates.

Most abstraction methods defined for FSMs (Flordal and Malik 2009) use local events, i.e., events that only appear in one FSM in the system. Local events can be hidden because they do not interact with other components of the system. In an EFSM system, even though local events are not shared with other components, the variables in their updates can still result in interaction; only local events with true update can be hidden. Therefore, when transforming an EFSM to an FSM, the local events with true updates are collected in a set Υ and hidden from the transformed FSM. Then the FSM is simplified based on the following result.

Proposition 5

Let $\mathcal {E}=\{E_{1}, E_{2},\ldots , E_{n}\}$ be a normalised EFSM system and let Υ ⊆ Σ ₁ such that (Σ ₂ ∪ ⋯ ∪ Σ _n ) ∩ Υ=∅ and ${\Delta }_{\mathcal {E}}(\sigma ) \equiv \textit {true}$ for all σ ∈ Υ. Let $\mathcal {F}=\{F_{1}, E_{2},\ldots , E_{n}\}$ be a normalised EFSM system such that φ(E ₁ )∖Υ ≃ _conf φ(F ₁ )∖Υ. Then $\mathcal {E}$ is nonblocking if and only if $\mathcal {F}$ is nonblocking.

To summarise Proposition 5, to apply the conflict-preserving abstraction defined for FSM on EFSM, first the set Υ is identified as the set of events with true updates that appear only in the EFSM E ₁ to be simplified. Next, the FSM form of E ₁ is obtained by disregarding all updates, and the events in Υ are hidden from the FSM form φ(E ₁). Then the conflict equivalence abstraction methods developed for FSMs are used to simplify φ(E ₁), resulting in an FSM φ(F ₁). This FSM is interpreted as an EFSM, F ₁, which is added back to the system. Proposition 5 provides a general method to simplify an EFSM in a normalised system while preserving the nonblocking property. A proof is given in Appendix B.1.

Example 4

Consider the normalised EFSM system $\mathcal {E}=\{E_{1},E_{2}\}$ in Fig. 8. It can be observed from Fig. 8 that the events α and γ only appear in the EFSM E ₁, and ${\Delta }_{\mathcal {E}}(\gamma ) \equiv \textit {true}$. Therefore, the set of local events to be hidden is chosen as Υ = {γ}. To apply the abstraction methods defined for FSMs, the EFSM E ₁ is transformed to the FSM form φ(E ₁) based on Definition 19, and event γ is hidden, resulting in φ(E ₁)∖Υ shown in Fig. 8. The two states q ₀ and q ₁ in φ(E ₁)∖Υ can now be merged using the conflict-preserving Silent Continuation Rule (Flordal and Malik 2009), resulting in the abstracted FSM $\tilde {E}_{1}$ in Fig. 8. Afterwards, the FSM $\tilde {E}_{1}$ is transformed back to an EFSM with the same structure as $\tilde {E}_{1}$ and the silent event τ is replaced by the local event γ as shown in $E^{\prime }_{1}$.

Fig. 8

Example of FSM-based conflict equivalence abstraction.

To ensure normalisation, the silent event τ is only used in FSMs and not in EFSMs. Therefore, the τ events are replaced by ordinary events when the FSM is converted back to an EFSM. Any local event with true update can be used for this replacement, and an original EFSM whose FSM form contains a τ-transition must contain at least one such event.

5.2 Partial composition

Synchronous composition is the simplest step in compositional nonblocking verification. It is always possible to replace some components of an EFSM system by their composition. This operation does not reduce the state space, but it is necessary when all other means of simplification have been exhausted. The following result follows directly from the definitions. The EFSM systems before and after normalised synchronous composition are not only equivalent with respect to nonblocking, but also identical up to isomorphism.

Proposition 6

(Partial Composition) Let $\mathcal {E} = \{E_{1}, \ldots , E_{n}\}$ be an EFSM system, and let $\mathcal {F} = \{E_{1} \dot {\|} E_{2}, E_{3}, \ldots , E_{n}\}$ . Then $\dot {\|}\mathcal {E}=\dot {\|}\mathcal {F}$.

Proposition 6 states that the composition of two EFSMs in an EFSM system does not change the behaviour of the system. It is also clear that the system stays normalised as normalised synchronous composition does not affect the updates of events. In combination with Proposition 1, it is guaranteed that the nonblocking property of the system is preserved after composing a part of a system using this operation. A proof is given in Appendix B.2.

5.3 Update simplification

An important aspect to reasoning about EFSM systems is the symbolic manipulation of updates, in order to keep the formulas as simple as possible. This is achieved by rewriting updates into logically equivalent updates, while keeping in mind that variables that do not appear as next-state variables in an update remain unchanged in a normalised system.

Definition 20

Let p, q ∈ π _V be two updates.

• p and q are logically equivalent, written p ⇔ q, if it holds that $p(\hat {v},\hat {w}) = q(\hat {v},\hat {w})$ for all valuations $\hat {v},\hat {w} \in \text {dom}(V)$.

• p and q are logically equivalent with respect to W ⊆ V, written p ⇔ _W q, if Ξ _W (p) and Ξ _W (q) are logically equivalent.

Example 5

The updates p ≡ x = 1 and q ≡ x = 1 ∧ x′ = 1 are not logically equivalent, because for valuations $\hat {v}[x]=1$ and $\hat {w}[x]=0$, e.g., it holds that $p(\hat {v},\hat {w}) = \mathbf {T}$ but $q(\hat {v},\hat {w}) = \mathbf {F}$. Yet, bearing in mind that the update p ≡ x = 1 leaves the variable x ∉ vars′(p) unchanged, these two updates have the same effect. The extension Ξ_{x}(p) ≡ x = 1 ∧ x′ = x is logically equivalent to q ≡ x = 1 ∧ x′ = 1, and therefore p and q are logically equivalent with respect to W = {x}, i.e, p ⇔ _{x} q.

Two updates being logically equivalent does not necessarily mean that they are logically equivalent with respect to W, nor does the converse hold in general.

Updates can be simplified automatically by standard methods of propositional reasoning, theorem proving, or binary decision diagrams (Huth and Ryan 2004; Bryant 1992). The following proposition confirms that replacing updates by updates logically equivalent with respect to the full variable set V does not effect the nonblocking property of the system.

Proposition 7 (Update Simplification)

Let $\mathcal {E} = \{E_{1},\ldots , E_{n}\}$ and $\mathcal {F}=\{F_{1},\ldots , F_{n}\}$ be normalised EFSM systems with $E_{i} = \langle {\Sigma }_{i}, Q_{i}, {\to _{i}^{E}}, Q^{\circ }_{i}, Q^{\omega }[i]\rangle$ and $F_{i}=\langle {\Sigma }_{i}, Q_{i}, {\to _{i}^{F}}, Q^{\circ }_{i}, Q^{\omega }_{i}\rangle$ . Let $V = \text {vars}(\mathcal {E}) = \text {vars}(\mathcal {F})$ and ${\Delta }_{\mathcal {E}}(\sigma ) \Leftrightarrow _{V} {\Delta }_{\mathcal {F}}(\sigma )$ for all $\sigma \in {\Sigma }_{\mathcal {E}} = {\Sigma }_{\mathcal {F}}$ , and ${\to _{i}^{F}} = \{\, (x,\sigma ,{\Delta }_{\mathcal {F}}(\sigma ),y) \mid x {{~}^{\underrightarrow {\;\;\sigma :{\Delta }_{\mathcal {E}(\sigma )\;\;}}}}_{i}^{E} y \,\}$ . Then $\mathcal {E}$ is nonblocking if and only if $\mathcal {F}$ is nonblocking.

The EFSMs in $\mathcal {E}$ and $\mathcal {F}$ in Proposition 7 have the same events and states, the only difference is that updates in $\mathcal {E}$ are replaced in $\mathcal {F}$ by updates logically equivalent with respect to all variables, maintaining normalisation by consistently making the same replacement for each event. A proof of Proposition 7 is given in Appendix B.3.

5.4 Variable unfolding

This section describes the abstraction that removes a variable from an EFSM system. It has been shown (Mohajerani et al. 2014) that unfolding a variable that only appears in one EFSM, called a local variable, preserves conflict equivalence. Here, this idea of partial unfolding is generalised to allow unfolding an arbitrary variable, even if it is shared between several EFSMs. In a normalised EFSM system, this can be achieved by replacing the variable with a variable EFSM that keeps track of the variable values.

Definition 21

Let z be a variable, and let Σ be a set of events. The variable alphabet of z with respect to Σ is U _z (Σ) = Σ × dom(z) × dom(z).

Definition 22

Let $\mathcal {E}$ be a normalised EFSM system. The normalised variable EFSM of $z \in \text {vars}(\mathcal {E})$ is

$$ U_{\mathcal{E}}(z) = \langle U_{z}({\Sigma}_{z}), \text{dom}(z), \to_{z}, \{z\circ\} , \text{dom}(z) \rangle $$

(16)

where

$$\begin{array}{@{}rcl@{}} {\Sigma}_{z} &=& \{\, \sigma \in {\Sigma}_{\mathcal{E}} \mid z \in \text{vars}({\Delta}_{\mathcal{E}}(\sigma)) \,\} ; \end{array} $$

(17)

$$\begin{array}{@{}rcl@{}} \to_{z} &=& \{(a,(\sigma,a,b), {\Xi}_{\{z\}}({\Delta}_{\mathcal{E}}(\sigma))[z\mapsto a,z^{\prime}\mapsto b], b)\mid \\ &&z \in \text{vars}({\Delta}_{\mathcal{E}}(\sigma)) \text{ and } a,b \in \text{dom}(z)\}. \end{array} $$

(18)

Furthermore, the variable renaming map $\rho _{z}\colon {\Sigma }_{\mathcal {E}} \cup U_{z}({\Sigma }_{z}) \to {\Sigma }_{\mathcal {E}}$ for z is defined by ρ _z (σ) = σ for all $\sigma \in {\Sigma }_{\mathcal {E}}$ and ρ _z ((σ, a, b)) = σ for all (σ, a, b) ∈ U _z (Σ _z ).

The variable EFSM uses the domain of the unfolded variable z as its set of locations. Events σ that have the variable z in their update are modified to have the form of (σ, a, b) to keep track of the value of the variable when the event is executed, where a, b ∈ dom(z) are the values of z before and after the transition, respectively. If z′ does not appear in the update ${\Delta }_{\mathcal {E}}(\sigma )$, then the extension operation Ξ_{z} adds the condition z′ = z to ensure that the value of z remains unchanged. Afterwards, the substitution [z ↦ a, z′ ↦ b] inserts the variable values corresponding to the source and target states of the transitions into the updates. The resulting updates can typically be simplified using Proposition 7.

For example, unfolding the variable v ₂ with domain {0, 1, 2} in the example of Section 3 results in the variable EFSM V ₂ with three locations 0, 1, and 2 as shown in Fig. 6. By executing l ₁ with update $v_{1}+v_{2}<2 \land v_{1}^{\prime }=v_{1}+1$, the value of v ₂ does not change. Event l ₁ is replaced by two new events (l ₁,0,0) and (l ₁, 1, 1), which are presented as l ₁₀ and l ₁₁ in Section 3. The update of (l ₁,0,0) is $(v_{1}+v_{2}<2\land v_{1}^{\prime }=v_{1}+1)[v_{2}\mapsto 0, v_{2}^{\prime }\mapsto 0] \equiv (v_{1}+0<2\land v_{1}^{\prime }=v_{1}+1)$, which can be simplified to $v_{1}<2\land v_{1}^{\prime }=v_{1}+1$ using Proposition 7.

When a variable is unfolded, updates are changed and new events are introduced. Then the following event replacement operation U _z (E) is used to ensure that the EFSMs in the system after partial unfolding use the new events. This operation replaces transitions labelled with the original events σ by new transitions labelled with each of the new events (σ, a, b), in a similar way as the inverse renaming ρ ⁻¹ in Definition 16.

Definition 23

Let E = 〈Σ _E , Q, →, Q°, Q ^ω〉 be an EFSM, and let z be a variable. The expansion of E after unfolding z is defined by

$$\begin{array}{@{}rcl@{}} U_{z}(E) &=& \langle {\Sigma}^{U}, Q, \to^{U}, Q^{\circ}, Q^{\omega}\rangle ; \end{array} $$

(19)

$$\begin{array}{@{}rcl@{}} {\Sigma}^{U} &=& U_{z}({\Sigma}_{E} \cap {\Sigma}_{z}) \cup ({\Sigma}_{E} \setminus {\Sigma}_{z})\\ \to^{U} &=&\left\{(x,(\sigma,a,b),{\Xi}_{\{z\}}({\Delta}_{\mathcal{E}}(\sigma))[z\mapsto a,z^{\prime}\mapsto b], y) \mid\right.\\ &&z \in \text{vars}({\Delta}_{\mathcal{E}}(\sigma)) \text{and} x \left.{~}^{\underrightarrow{\sigma:{\Delta}_{\mathcal{E}}(\sigma)}} y \text{and} \sigma \in {\Sigma}_{E} \cap {\Sigma}_{z}\right\}{\cup} \end{array} $$

(20)

$$\begin{array}{@{}rcl@{}} & &\{\, (x,\sigma,p,y) \mid x {~}^{\underrightarrow{\;\;\sigma:p\;\;}} y\ \text{and}\ \sigma \in {\Sigma}_{E} \setminus {\Sigma}_{z} \,\} \ . \end{array} $$

(21)

Example 6

Figure 6 in Section 3 shows the expansion $C_{1}^{\prime } = U_{v_{2}}(\mathcal {N}(C_{1}))$, which replaces the EFSM $\mathcal {N}(C_{1})$ in Fig. 3 after unfolding v ₂.

Given these definitions, a variable z is unfolded by adding the variable EFSM $U_{\mathcal {E}}(z)$ to the system, and replacing all EFSMs E by their expansions U _z (E).

Definition 24

Let $\mathcal {E} = \{E_{1},\ldots ,E_{n}\}$ be a normalised EFSM system and $z \in \text {vars}(\mathcal {E})$. The result of unfolding z in $\mathcal {E}$ is

$$ \mathcal{E} \setminus z = \{ U_{\mathcal{E}}(z), U_{z}(E_{1}), \ldots, U_{z}(E_{n})\} $$

(22)

where $U_{\mathcal {E}}(z)$ is defined as in Definition 22 and U _z (E _i ) is defined as in Definition 23.

Proposition 8

(Variable Unfolding) Let $\mathcal {E}$ be a normalised EFSM system, and let $z \in \text {vars}(\mathcal {E})$ . Then $\mathcal {E}$ is nonblocking if and only if $\mathcal {E} \setminus z$ is nonblocking.

Proposition 8 confirms that the nonblocking property of the system is preserved after unfolding a variable. A proof can be found in Appendix B.4.

Example 7

Consider the EFSM E in Fig. 9 with updates shown in the table, which is part of a normalised system $\mathcal {E}$. Assume dom(x) = dom(y) = {0, 1} and x∘ = y ∘= 0. Unfolding the variable x results in the variable EFSM $U_{\mathcal {E}}(x)$ with locations 0 and 1 in Fig. 9. The event α with update y′ = x + 1 is replaced by four new events:

$$\begin{array}{@{}rcl@{}} (\alpha,0,0) \quad \text{with update} \quad & {\Xi}_{\{x\}}&(y^{\prime}\,=\,x\,+\,1)[x\mapsto 0, x^{\prime}\mapsto 0] \!\equiv\! y^{\prime}\,=\,0\,+\,1 \land 0\,=\,0 \Leftrightarrow_{V} y^{\prime}\,=\,1 \\ (\alpha,0,1) \quad \text{with update} \quad & {\Xi}_{\{x\}}&(y^{\prime}\,=\,x\,+\,1)[x\mapsto 0, x^{\prime}\mapsto 1] \!\equiv\! y^{\prime}\,=\,0\,+\,1 \land 1\,=\,0 \Leftrightarrow_{V} \textit{false} \\ (\alpha,1,0) \quad \text{with update} \quad & {\Xi}_{\{x\}}&(y^{\prime}\,=\,x\,+\,1)[x\mapsto 1, x^{\prime}\mapsto 0] \!\equiv\! y^{\prime}\,=\,1\,+\,1 \land 0\,=\,1 \Leftrightarrow_{V} \textit{false} \\ (\alpha,1,1) \quad \text{with update} \quad & {\Xi}_{\{x\}}&(y^{\prime}\,=\,x\,+\,1)[x\mapsto 1, x^{\prime}\mapsto 1] \!\equiv\! y^{\prime}\,=\,1\,+\,1\land 1\,=\,1 \Leftrightarrow_{V} \textit{false} \end{array} $$

Fig. 9

Example of unfolding a variable x

The update of the event (α, 1, 1) is false because y′ = 2 is not possible as dom(y) = {0, 1}. Similarly, event β is replaced by four new events. The new events and their simplified updates are shown in the table in Fig. 9. Since partial unfolding introduces new events to the system, the EFSM E needs to be modified to use the new events. Thus, E is replaced by U _x (E), also shown Fig. 9.

5.5 Event Simplification

Generally, reducing the number of events in a system increases the possibility of abstraction. This section proposes four different methods to reduce the number of events.

It can happen after abstraction and simplification that the updates of some events become false. Such events can be removed from the system and their transitions deleted. This event removal is implemented by the following operation of restriction.

Definition 25

The restriction of EFSM E = 〈Σ, Q, →, Q°, Q ^ω〉 to Ω ⊆ Σ is E _|Ω = 〈Ω, Q,→_|Ω, Q°, Q ^ω〉 where

$$ \to_{|{\Omega}} = \{\, (x,\sigma,p,y) \in \to \mid \sigma \in {\Omega} \,\}\ . $$

(23)

The restriction of $\mathcal {E} = \{E_{1},\ldots ,E_{n}\}$ to Ω is $\mathcal {E}_{|{\Omega }} = \{E_{1}{}_{|{\Omega }},\ldots ,E_{n}{}_{|{\Omega }}\}$.

Proposition 9 (false-Removal)

Let $\mathcal {E}$ be a normalised EFSM system, and let ${\Lambda } \subseteq {\Sigma }_{\mathcal {E}}$ be a set of events such that for all λ ∈ Λ at least one of the following conditions holds:

• (i) ${\Delta }_{\mathcal {E}}(\lambda ) \equiv \textit {false}$;

• (ii) There exists $E \in \mathcal {E}$ such that λ ∈ Σ _E , but there does not exist any transition $x {{~}^{\underrightarrow {\lambda :p}}} y$ in E.

Then $\mathcal {E}$ is nonblocking if and only if $\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }}$ is nonblocking.

Based on Proposition 9, events with false updates can be removed from the system while preserving the nonblocking property. Likewise, events that in some EFSM do not appear on any transition and therefore are always disabled, can be removed. A proof is given in Appendix B.5.

Example 8

Consider again the EFSMs U _x (E) and $U_{\mathcal {E}}(x)$ in Fig. 9. The updates of events (α, 0, 1), (α, 1, 0), (α, 1, 1), (β, 0, 0), and (β, 1, 0) are false. Thus, these events an their transitions can be entirely removed from the system. Fig. 10 shows the simplified EFSMs X′ and E′ obtained from $U_{\mathcal {E}}(x)$ and U _x (E), respectively, by removing the events with false updates.

Fig. 10

Example of removing events with false update.

In compositional nonblocking verification of FSM systems, events that only appear on selfloops are immediately removed because no state change is possible by these transitions. This is not possible in an EFSM system. Even though no location change is possible by selfloop-only events, if the updates contain next-state variables, the execution of these events can still change the system state by changing the variable values. An event can be removed from an EFSM system if it causes no location changes, which means it appears only on selfloop transitions, and if it causes no changes of variable values, which is guaranteed if the update of the event is a pure guard, i.e., contains no primed variables.

Definition 26

An EFSM E = 〈Σ, Q, →, Q°, Q ^ω〉 is selfloop-only for λ ∈ Σ if $x{{~}^{\underrightarrow {\lambda :p}}} y$ implies x = y and $\text {vars}^{\prime }_{\mathcal {E}}(p) = \emptyset$. EFSM E is selfloop-only for Λ ⊆ Σ if E is selfloop-only for each λ ∈ Λ. An EFSM system $\mathcal {E}$ is selfloop-only for Λ ⊆ Σ if each $E\in \mathcal {E}$ is selfloop-only for Λ.

An EFSM is selfloop-only for an event, if the event appears only in selfloops and the update of the event is a pure guard. The following proposition confirms that selfloop-only events can be removed without affecting the nonblocking property of an EFSM system. A proof can be found in Appendix B.5.

Proposition 10 (Selfloop Removal)

Let $\mathcal {E}$ be a normalised EFSM system that is selfloop-only for ${\Lambda } \subseteq {\Sigma }_{\mathcal {E}}$ . Then $\mathcal {E}$ is nonblocking if and only if $\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }}$ is nonblocking.

Example 9

Consider the normalised EFSM system $\mathcal {E}=\{E_{1},E_{2}\}$ in Fig. 11, where the alphabets of E ₁ and E ₂ are Σ₁ = {α, β, γ} and Σ₂ = {β, σ}. Assume dom(x) = dom(y) = {0, 1}. The events α and β only appear on selfloops in the entire system, and the update of β is pure guard. Using Proposition 10, the event β can be removed from the system. Thus, EFSMs E ₁ and E ₂ are replaced by $E_{1}{}_{|{\Sigma }_{1}\setminus \{\beta \}}$ and $E_{2}{}_{|{\Sigma }_{2}\setminus \{\beta \}}$ shown in Fig. 11. Note that, although event α also appears only on selfloops in the entire system, its update is not a pure guard, and consequently this event cannot be removed.

Fig. 11

Example of selfloop removal.

Using Propositions 9 and 10, it is possible to remove an event from the system. The following results make it possible to combine some events and replace them by a single event.

Proposition 11 (Event Merging)

Let $\mathcal {E} = \{E_{1},\ldots , E_{n}\}$ be a normalised EFSM system with $E_{i}=\langle {\Sigma }_{i},Q_{i},\to _{i},Q^{\circ }_{\omega },Q^{\omega }_{i}\rangle$ , let $E_{k} \in \mathcal {E}$ , and let $\rho \colon {\Sigma }_{\mathcal {E}} \to {\Sigma }^{\prime }$ be a renaming such that the following conditions hold for all $\sigma _{1},\sigma _{2} \in {\Sigma }_{\mathcal {E}}$ with ρ(σ ₁ ) = ρ(σ ₂):

• (i) ${\Delta }_{\mathcal {E}}(\sigma _{1}) = {\Delta }_{\mathcal {E}}(\sigma _{2})$;

• (ii) for all i ≠ k, it holds that σ ₁ ∈ Σ _i if and only if σ ₂ ∈ Σ _i , and for all x,y ∈ Q _i it holds that $x {{~}^{\underrightarrow {\sigma _{1}:{\Delta }_{\mathcal {E}}(\sigma _{1})}}}_{i} y$ if and only if $x {{~}^{\underrightarrow {\sigma _{2}:{\Delta }_{\mathcal {E}}(\sigma _{2})}}}_{i} y$.

Then $\mathcal {E}$ is nonblocking if and only if $\rho (\mathcal {E})$ is nonblocking.

By Proposition 11, all events with the same update can be merged and replaced by the same event if they appear on transitions with the same source and target states in all the EFSMs of the system except for one EFSM E _k . A proof is given in Appendix B.5.

One of the applications of event merging, Proposition 11, is after variable unfolding as events introduced by variable unfolding appear on different transitions only in the variable EFSM. For example, after unfolding the variable v ₂ in Fig. 6 in Section 3, event s ₂ is replaced by two new events (s ₂, 1, 0) and (s ₂, 2, 1) both with the same update true. Using Proposition 11, these events can be merged back into s ₂. Therefore, there is no need to introduce new events in the first place, and only s ₂ is used in Fig. 6.

Example 10

Consider again the EFSMs E′ and X′ in Fig. 10. The updates of events (β, 0, 1) and (β, 1, 1) are the same, and these events appear on different transitions only in the EFSM X′. Thus, the renaming ρ is introduced such that ρ((β, 0, 1)) = ρ((β, 1, 1)) = β and ρ(σ) = σ for all σ ∉ {(β, 0, 1), (β, 1, 1)}. The resulting simplified EFSMs ρ(E′) and ρ(X′) are shown in Fig. 12.

Fig. 12

Example of event merging

Proposition 12

(Update Merging) Let $\mathcal {E} = \{E_{1},\ldots , E_{n}\}$ be a normalised EFSM system with $E_{i} = \langle {\Sigma }_{i},Q_{i},\to _{i},Q^{\circ }_{\omega },Q^{\omega }_{i}\rangle$ . Let ρ be a renaming such that the following conditions hold for all $\sigma _{1},\sigma _{2} \in {\Sigma }_{\mathcal {E}}$ with ρ(σ ₁ ) = ρ(σ ₂):

• (i) $\text {vars}^{\prime }({\Delta }_{\mathcal {E}}(\sigma _{1})) = \text {vars}^{\prime }({\Delta }_{\mathcal {E}}(\sigma _{2}))$,

• (ii) for all i = 1, … , n it holds that σ ₁ ∈ Σ _i if and only if σ ₂ ∈ Σ _i , and for all x,y ∈ Q _i it holds that $x {{~}^{\underrightarrow {{\sigma _{1}:{\Delta }_{\mathcal {E}}(\sigma _{1})}}}}_{i} y$ if and only if $x {{~}^{\underrightarrow {\sigma _{2}:{\Delta }_{\mathcal {E}}(\sigma _{2})}}}_{i} y$

Further let $\mathcal {F}=\{F_{1},\ldots , F_{n}\}$ such that $F_{i} = \langle \rho ({\Sigma }_{i}), Q_{i}, {\to _{i}^{F}} , Q^{\circ }_{i}, Q^{\omega }_{i}\rangle$ where ${\to _{i}^{F}} =\, \{ (x,\rho (\sigma ), {\Delta }_{\mathcal {F}}(\rho (\sigma )), y) \mid x {~}^{\underrightarrow {\sigma :{\Delta }_{\mathcal {E}}(\sigma )}} y \,\}$ and ${\Delta }_{\mathcal {F}}(\mu ) \equiv \bigvee _{\sigma \in \rho ^{-1}(\mu )} {\Delta }_{\mathcal {E}}(\sigma )$ for all $\mu \in {\Sigma }_{\mathcal {F}}$ . Then $\mathcal {E}$ is nonblocking if and only if $\mathcal {F}$ is nonblocking.

By Proposition 12, two events with the same next-state variables in their updates that appear on transitions with the same source and target states in the entire system can be replaced by a single new event. The update of the new event is the disjunction of the updates of the replaced events. The condition on the next-state variables ensures that the set of unchanged variables, i.e., variables not occurring as next-state variables, is preserved. A proof can be found in Appendix B.5.

Example 11

Consider the normalised EFSM system $\mathcal {E}=\{E_{1},E_{2}\}$ in Fig. 13 with dom(x) = dom(y) = {0, 1}. Events α ₁ and α ₂ appear on the same transitions throughout $\mathcal {E}$, and $\text {vars}^{\prime }_{\mathcal {E}}(\alpha _{1}) = \text {vars}^{\prime }_{\mathcal {E}}(\alpha _{2}) = \emptyset$. In order to use Proposition 12, the new event α and the renaming ρ are introduced such that ρ(α ₁) = ρ(α ₂) = α, ρ(β) = β, and ρ(γ) = γ. The update of the merged event α is y = 0∨y = 1 ⇔ _V true, and as a result the EFSM E ₁ can be replaced by F ₁ in Fig. 13.

Fig. 13

Example of update merging

6 Algorithm

This section applies the results from the previous sections to give an algorithm for compositional nonblocking verification of EFSM systems. An overview of the approach is shown as Algorithm 1. Given an EFSM system, the algorithm repeatedly unfolds variables, composes EFSMs, and applies abstraction to the resultant EFSMs. While doing this, it maintains an event tree data structure to keep track of the events and their updates, and the renamings generated by partial unfolding.

The first step of Algorithm 1 is to normalise the system. The normalise() procedure in line 2 performs the normalisation and initialises the event tree, which at the beginning only links each event to its unique update. Then the main loop in lines 3–18 repeatedly unfolds variables or composes EFSMs, and simplifies EFSMs, until only a single EFSM is left. In each iteration, the selectCandidate() procedure in line 4 heuristically selects a candidate representing a subsystem to simplify, which consists of a set V _c of variables and a set $\mathcal {E}_{c}$ of EFSMs, the composition or unfolding of which is predicted to have potential for the most simplification. If the selected subsystem contains variables, then the selectVariable() procedure in line 6 heuristically identifies the best variable to unfold, which is then removed from the system and unfolded by the unfold() procedure in lines 7–8. If the selected candidate contains no variables, then it consists of only EFSMs, which are removed from the system and composed in lines 10–11. In both cases, the EFSM E resulting from unfolding or composition is sent for abstraction in lines 13–17.

Abstraction starts by calling the procedure removeEvents() in line 13, which applies update simplification (Proposition 7), removes events with false updates (Proposition 9), removes selfloop-only events (Proposition 10), and merges events (Propsosition 11 and 12). These steps can change both the EFSM E and the remaining components of $\mathcal {E}$, while at the same time updating the event tree. Afterwards, the simplify() procedure called in line 15 computes a conflict-preserving abstraction of E according to Proposition 5. As abstraction may change or remove transitions, it may result that some events only appear as selfloops or that there are groups of events on transitions with the same source and target states. Therefore, the removeEvents() procedure is applied again to the abstracted EFSM in an attempt to remove more events.

The loop terminates when $\mathcal {E}$ contains only one EFSM and all the variables are unfolded. The final EFSM can be considered as an FSM as there are no more variables in the system, so it is passed to standard FSM-based nonblocking verification in line 19. In the following, each of the procedures mentioned above is explained in more detail.

The selectCandidate() method in line 4 uses the following steps to select the most promising candidate, which consists of a set V _c of variables and a set $\mathcal {E}_{c}$ of EFSMs to be composed or unfolded.

• (i) The first step is to search the system for variables that appear only as (primed) next-state variables or only as (unprimed) current-state variables in the entire system. If a variable only appears as next-state variable then all states in the variable EFSM are bisimilar (Milner 1989), so the variable EFSM can immediately be simplified to a single-location EFSM. If a variable only appears as current-state variable, then it never changes its value. Then all locations except the initial locations are unreachable in the variable EFSM, which again can be simplified to a single-location EFSM. If the system contains variables that only appear as current-state or only as next-state variables, then the selectCandidate() procedure returns all these variables in V _c , while $\mathcal {E}_{c}$ is an empty set.

• (ii) The second step is to search for local variables, i.e., for variables that appear in the updates of only one EFSM. As the system is normalised, events with a local variable in their updates appear in only one EFSM. Unfolding local variables simplifies their updates, which may result in some updates becoming true, increasing the possibility of hiding and abstractions in later steps. Yet, after unfolding a local variable, its events in the EFSM are shared with the variable EFSM.

  If the system contains local variables, the selectCandidate() procedure returns the local variables in V _c , while $\mathcal {E}_{c}$ is an empty set. Subsequently, one of these variables will be unfolded in line 8. To exploit the benefit of this unfolding, the selectCandidate() procedure also ensures that, in the next iteration of the main loop after unfolding a local variable and simplifying the resultant EFSM, the next candidate only consists of the variable EFSM and the EFSM that has the local variable.

• (iii) If there are no variables that appear only primed or only unprimed, and no local variables, the final step is to use a strategy called mustL (Flordal and Malik 2009), which tries to improve the potential of abstraction by making events local. For each event σ, all EFSMs with σ in the alphabet and all variables in the update of σ are selected, so that σ becomes a local event if the selected EFSMs and variables were to be composed. This gives several candidates, one for each event, and the following heuristics are used to select the best candidate among them.

  • minF selects the candidate with the smallest number of other EFSMs and variables linked via events to the candidate’s EFSMs and variables (Mohajerani et al. 2014). This heuristic attempts to minimise event sharing between the candidate and the rest of the system.

  • minS selects the candidate with the smallest estimated number of states in its synchronous composition. The number of states in the synchronous composition is estimated as the product of the sizes of the domains of the variables and the numbers of locations of the EFSMs, multiplied by the ratio of the number of events the candidate shares with the rest of the system over the total number of events of the candidate (Flordal and Malik 2009).

  The selectCandidate() procedure first employs the minF heuristic, and if minF gives equal preference to two candidates, then the minS heuristic is used to break the tie.

If the candidate returned by the selectCandidate() procedure contains variables, only one of these variables will be unfolded. Line 6 calls the selectVariable() procedure, which uses another set of heuristics to identify the most promising variable:

• maxE selects a variable that appears in the update of the largest number of events.

• maxS selects a variable that appears in the largest number of selfloops.

• minD selects a variable with the smallest domain.

The maxE heuristic enables more update simplification, which increases the chance of updates becoming true and thus the possibility of hiding. As the contributions of the conflict equivalence abstraction methods are high in simplifying the system, and they are greatly dependent on hiding, maxE is the first heuristic that is applied. If maxE gives equal preference to two variables, then the maxS heuristic is used to break the tie. maxS attempts to boost the performance of selfloop removal, which also may increase the performance of conflict equivalence abstraction. In the case that both maxE and maxS give equal preference to two variables, the minD heuristic is used in order to create the smallest possible variable EFSM.

Example 12

Consider the EFSM system $\mathcal {E}=\{E_{1},E_{2}\}$ in Fig. 14. Normalisation produces $\mathcal {N}(E_{1})$ and $\mathcal {N}(E_{2})$ with the updates shown in the table. As variable x only appears unprimed and variable y only appears primed in the updates, the selectCandidate() procedure returns V _c = {x, y} and $\mathcal {E}_{c} = \emptyset$ as the selected candidate. As this candidate has variables, next the selectVariable() procedure is called in line 6 to select a variable, which starts by evaluating the maxE heuristic. In this case, x only occurs in the update of β, while y occurs in the updates of both α and β, so y is selected for unfolding.

Fig. 14

Normalisation and initial event tree

According to Definition 22, partial unfolding by the unfold() procedure in line 8 generates for each event σ with the variable v in its update, several new events of the form (σ, a, b). Subsequently, all the components of the system need to be changed by replacing σ with these new events according to Definition 24. To improve performance, this replacement is done by modifying the event tree only. The new events (σ, a, b) are added with their updates to the event tree as children of the original event σ. Other EFSMs using σ remain unchanged, with the interpretation that any transition labelled σ represents transitions with all the descendants of σ stored in the event tree. In this way, the replacement of events and the associated blow-up in the number of transitions is postponed until the synchronous composition of EFSMs containing σ with the variable EFSM. Often, the replacement can be avoided altogether, as some of the new events can be removed or merged before they are needed in synchronous composition.

Example 13

Consider the normalised EFSM system $\mathcal {E}=\{\mathcal {N}(E_{1}),\mathcal {N}(E_{2})\}$ in Fig. 14 with dom(x) = {0, 1}, x∘ = 0, dom(y) = {1, 2}, and y∘ = 1. Normalisation produces $\mathcal {N}(E_{1})$ and $\mathcal {N}(E_{2})$ with the updates stored separately in an event tree that initially consists of two root nodes with the two events α and β and their updates, as shown in Fig. 14. Unfolding of the variable y produces events of the form (α, a, b) and (β, a, b), which are added as children of α and β to the event tree. Figure 15 shows the variable EFSM $U_{\mathcal {E}}(y)$ and the updated event tree. At this point, the EFSMs $\mathcal {N}(E_{1})$ and $\mathcal {N}(E_{2})$ are left unchanged.

Fig. 15

Result of unfolding y and associated event tree

The removeEvents() procedure called in line 13 attempts to simplify the EFSMs and the event tree as much as possible before proceeding further with simplification. It first simplifies all the updates according to Proposition 7 and removes all events with false updates according to Proposition 9. Next, selfloop removal is applied, which removes events that have pure guards as updates and that only appear as selfloops in the entire system (Proposition 10). Afterwards, the removeEvents() procedure merges events and updates using Propostions 11 and 12. An exact implementation of these propositions requires a search of transitions of all the EFSMs. To improve performance, the removeEvents() uses the event tree. Only events that have the same parent and no children in the event tree are considered for merging. By the construction of the event tree, the children of an event σ are implicitly present in all EFSMs containing the parent event σ, but they appear on exactly the same transitions as the parent event, so these EFSMs do not need to be checked to determine whether merging is possible according to Propositions 11 and 12. More precisely, the removeEvents() procedure first searches for childless events with the same parent and the same next-state variables in their updates. Each group of such events becomes a merge candidate. Within a merge candidate, all events with the same update p are replaced by a single event with update p (Proposition 11), and the remaining events that appear on transitions with the same source and target states are replaced by a new event with an update that is the disjunction of the updates of the replaced events (Proposition 12).

Example 14

Consider the EFSM system $\mathcal {E}=\{\mathcal {N}(E_{1}),\mathcal {N}(E_{2}),U_{\mathcal {E}}(y)\}$ with the EFSMs shown in Figs. 14 and 15, where dom(x) = {0, 1} and x∘ = 0. First, the removeEvents() procedure removes events (α, 1, 2) and (α, 2, 2) as their updates are false. Next, events (α, 1, 1) and (α, 2, 1) both have the parent α and the update true. These events can be merged according to Proposition 11, and as they are the only children of α they are replaced by their parent α with update true. Further, the events (β, 1, 1) and (β, 2, 1), and (β, 1, 2) and (β, 2, 2) have the same update and the same parent. The removeEvents() procedure merges events (β, 1, 1) and (β, 2, 1) into a new event β ₀, and merges (β, 1, 2) and (β, 2, 2) into a new event β ₁. Then β is assigned as the parent of β ₀ and β ₁ in the event tree. Figure 16 shows the EFSM Y that results from $U_{\mathcal {E}}(y)$ and the event tree after these modifications.

Fig. 16

Result of the removeEvents() procedure applied to $U_{\mathcal {E}}(y)$

After event removal and update merging, the simplify() procedure called in line 15 attempts to simplify the EFSM E based on conflict equivalence. First, the getLocalEvents() procedure called in line 14 computes the set Υ of events to be hidden. According to Proposition 5, these are events with true update that only appear in E. Then the EFSM is converted to FSM form while hiding these events. As the updates are stored separately from the EFSM E in the event tree, E is simply considered as an FSM and the events in Υ are replaced by τ. Then the conflict preserving abstraction methods (Flordal and Malik 2009) are applied to this FSM. Using the event tree, the resultant FSM can again be considered as an EFSM.

The synchronise() procedure, called in line 11, performs normalised synchronous composition, ignoring updates, and taking the event relationships in the event tree into account. If the set $\mathcal {E}_{c}$ of EFSMs to be composed contains an EFSM containing a parent event and an EFSM containing its children, then the procedure replaces all occurrences of the parent event with its children while computing the normalised synchronous composition.

Example 15

Consider the normalised EFSM system $\mathcal {E}=\{\mathcal {N}(E_{1}),\mathcal {N}(E_{2}),Y\}$ with the EFSMs shown in Figs.14 and 16, and assume that the EFSMs Y and $\mathcal {N}(E_{1})$ are to be composed. During synchronous composition, based on the event tree, event β in $\mathcal {N}(E_{1})$ is replaced by β ₀ and β ₁, resulting in EFSM $E_{1}^{\prime }$, while Y remains unchanged. Figure 17 shows the EFSM $E^{\prime }_{1}$ and the result $E^{\prime }_{1} || Y$ of normalised synchronous composition.

Fig. 17

Synchronous composition of $\mathcal {N}(E_{1})$ and Y using event tree

7 Experimental results

The EFSM-based compositional nonblocking verification has been implemented in the discrete event systems tool Supremica (Åkesson et al. 2006). It has been tested on some large EFSM models and compared to an FSM-based compositional algorithm (Malik and Leduc 2013) and a BDD-based algorithm (Vahidi 2004). This section shows the results of the experiments.

The following list gives an overview of the test cases used to compare the algorithms. These include complex industrial models and case studies, and some scalable models with very large state spaces.

• series pml3 A system consisting of three parallel manufacturing lines each processing workpieces of a particular type (Mohajerani et al. 2014). Each line has 49 serially connected machines. The parallel lines share 50 buffers with capacity 2 or 3.

• series prime-sieve A distributed version of the Sieve of Eratosthenes for generating prime numbers (Mohajerani et al. 2013b). The models considered here contain filters for the first 4, 6, or 8 prime numbers, enabling them to find prime numbers less or equal to 120, 288, or 528, respectively. prime-sieve4b is a faulty blocking version of the program, while the others are correct and nonblocking.

• series production-cell A model of part of a metal-processing plant consisting of seven manufacturing devices (Fabian et al. 2014).

• series profisafe-ihost-b Part of the PROFIsafe protocol for fail-safe communication (Malik and Mühlfeld 2003). Considered here are two EFSM models of a blocking version of the PROFIsafe input-host with sequence numbers ranging from 0 to 127 or 255.

• series psl An assembly cell for toy cars, which are built up from seven parts (Parsaeian 2014). The cell has three robots, which pick up parts from two intakes, assemble them in a fixture, and thereafter place the complete car at an outlet. psl-big is a model of the uncontrolled plant, psl-n is the nonblocking system with supervisor updates added to the EFSMs. psl-b is a blocking version obtained from psl-n by removing some of the supervisor updates, psl-restart is an uncontrolled plant with additional transitions to facilitate resynchronisation of the system.

• series round-robin EFSM model of a token-passing resource allocation protocol with a ring of 300 or 400 processes (Graf and Steffen 1990).

• series tline A scalable version of the transfer line with rework cycles (Teixeira et al. 2013). The system consists of 500 serially connected cells linked by buffers. Each cell has three machines and a test unit that can reject workpieces up to 3 or 4 times.

Table 1 shows experimental results for nonblocking verification of the above models using the EFSM-based compositional nonblocking verification algorithm proposed in Section 6 and two other methods. The table shows for each model the number of EFSMs ($|\mathcal {E}|$), the number of variables ( |V|), the size of the largest variable domain ( |dom|), whether or not the model is nonblocking (Nbl), and the performance data for the different algorithms. The experiments were run on a standard desktop computer using a single core 3.3 GHz CPU and not more than 2 GB of RAM. Runtime was limited to 20 minutes: if this time was exceeded, or the process ran over the limit of 2 GB RAM, the attempt was aborted and the table entries left blank.

Table 1 Experimental results for different nonblocking verification algorithms

The EFSM column shows the runtimes of the EFSM-based compositional nonblocking verification and the total number of EFSM transitions encountered during the run. The implementation proceeds as described in Section 6 and selects the subsystems to compose and the variables to unfold following the heuristics in the order presented. That is, candidates for composition are selected according to the minF heuristic, and if this gives the same priority for two candidates, then the minS heuristic is used to break the tie. Likewise, the order for the variable selection heuristics is first maxE, then maxS, and finally minD. The number of transitions shown in the table is the sum of the transition numbers of the EFSMs E encountered in line 13 of Algorithm 1, before abstraction, plus the number of transitions of the final EFSM in line 19.

For comparison, the table also contains runtimes for the following two alternative algorithms from previous work, which are also implemented in Supremica.

• FSM The FSM-based compositional algorithm converts the EFSM model to a set of FSMs and then applies the compositional algorithm (Flordal and Malik 2009). The EFSM model is modularly flattened by creating a collection of location FSMs and variable FSMs (Mohajerani et al. 2013a). Location FSMs use the EFSM locations as states but replace the updates with events. The variable FSMs use the domain of a variable as their states space and keep track of the value of that variable. Differently from Section 5.4 above, the flattened FSM system has events of the form $(\sigma ;\hat {v};\hat {w})$ for each update p of event σ in EFSM E and all valuations $\hat {v}\in \text {dom}(\text {vars}(p))$ and $\hat {w}\in \text {dom}(\text {vars}^{\prime }(p))$ such that $p(\hat {v},\hat {w}) = \mathbf {T}$. In the worst case, the number of events created for an update is the product of the sizes of the domains of its variables. Table 1 shows the total number of transitions encountered during verification, obtained in the same way as for the EFSM column, and in two further columns the times spent to flatten the system (Flatten) and to verify the flattened FSM system (Verify). The total runtime is the sum of these two columns.

• BDD The BDD-based algorithm converts the EFSM model to a symbolic representation in the form of Binary Decision Diagrams (BDDs) (Bryant 1992) and explores the full state space symbolically (McMillan 1993). The implementation includes several performance improvements, most importantly an initial variable ordering based on the FORCE heuristics (Aloul et al. 2003) and a disjunctive partitioning of the transition relation in a form optimised for discrete event systems (Vahidi 2004). Table 1 shows the total runtime of BDD-based verification and the total number of BDD nodes encountered. BDD nodes require a similar amount of memory as transitions, so that their number gives a measure of the memory requirements similar to the numbers of transition encountered by the other two algorithms.

Table 1 shows that the EFSM-based compositional algorithms successfully verifies all the examples in this experiment, in most cases faster than the two other algorithms. The transition numbers encountered by the EFSM-based algorithm are usually smaller than those encountered by the FSM-based algorithm, as is to be expected from the deferred unfolding and event tree techniques.

However, the EFSM algorithm needs to perform symbolic computation and can take more time even with fewer numbers. For examples like pml3 〈2〉, production-cell, and round-robin the runtimes of the FSM-based and EFSM-based algorithms are similar. These models have got simple updates, so that the number of events in the flattened FSM system is small and the flattening times are small, and as a result, the FSM-based and EFSM-based algorithms verify the models in similar ways.

This effect can also be observed with the psl models. The models psl-b and psl-n are obtained by calculating a supervisor and attaching some or all its updates to psl-big, resulting in EFSMs with a large number of extremely complicated updates. As it can be observed from the table, the psl-big and psl-restart models, which have much fewer and simpler updates, can be flattened significantly faster than psl-b and psl-n. In these cases, the FSM-based algorithm encounters fewer transitions than the EFSM-based algorithm, suggesting that the FSM-based method can perform more accurate simplification for these simple models. For psl-b and psl-n, the large large number of events in the flattened FSM system causes the FSM-based compositional algorithm to perform poorly, while both the EFSM-based compositional and the BDD algorithm cope well with the complicated updates.

The BDD algorithm is not impeded by complicated update formulas, as these only cause a moderate increase in the complexity of the symbolic model. However, it is limited by the size and search depth of the state space, and fails to verify large scaled-up models such as pml, round-robin and tline.

The nonblocking verification algorithms have also been applied to a scalable version of the manufacturing system example in Section 3. The system consists of M serially connected cells linked by conveyor belts. Each cell m for 1 ≤ m ≤ M has two conveyor belt sections $C{B^{m}_{1}}$ and $C{B^{m}_{2}}$ and two machines ${M^{m}_{1}}$ and ${M^{m}_{2}}$. Initially workpieces are picked up by the conveyor belt $C{B^{1}_{1}}$ to enter cell 1, and completed workpieces from ${M^{m}_{1}}$ or ${M^{m}_{2}}$ in cell m are placed on the next conveyor $CB^{m+1}_{1}$. Fig. 18 shows the runtimes for instances with 1–1000 serially connected cells and fixed conveyor belt capacity N = 10, and Fig. 19 shows the runtimes for instances with conveyor belt capacity 2–100 and a fixed number of 100 serially connected cells.

Fig. 18

Runtimes for manufacturing systems with conveyor capacity N = 10 and increasing number of cells

Fig. 19

Runtimes for manufacturing systems with 100 cells and increasing conveyor belt capacity N

The EFSM-based compositional algorithm successfully reveals the blocking conditions of manufacturing systems with up to 1000 serially connected cells and conveyor belt capacity up to 100. However, the runtime does not grow linearly in the number of connected cells because of the complexity of the MustL and MinF heuristics. The preselection heuristic MustL produces up to |Σ| candidates, and the evaluation of MinF takes time proportional to the number of events of the candidate. Therefore, the complexity of the component selection heuristic is quadratic in the number of events. The FSM-based algorithm has more events to process and therefore suffers more from this effect, and in addition most of its runtime is taken up by the flattening process. The difference is more noticeable when the conveyor belt capacity increases than when the number of cells increases, because the number of events grows quadratically in the size of the domain of the variable N and only linearly in the number of cells. The BDD algorithm cannot handle more than 60 serially connected cells and therefore is not shown in these figures.

Table 2 shows the runtimes of the EFSM-based compositional nonblocking verification algorithm using different heuristics for the selection of composition candidates and variables. In this experiment, the standard ordering of the heuristics is changed such that the indicated heuristic is used first. In the maxS columns, the order of variable selection heuristics is first maxS, then maxE, and finally minD; and in the minD columns, the order is first minD, then maxE, and finally maxS.

Table 2 Runtimes with different composition candidate and variable selection heuristics

The results suggest that, in many cases the variable ordering heuristics have little or no effect on the runtime. On the other hand, while the algorithm fails to verify some of the models using minS, it successfully verifies all the examples using minF. It appears that the minF heuristic is better at increasing the number of local events and thus the possibility of abstraction.

8 Conclusions

A general framework for compositional nonblocking verification of extended finite-state machines (EFSMs) has been presented, which supports the verification of large models consisting of several EFSMs that interact both via shared events and shared variables. Normalisation is introduced, which makes it possible to unfold arbitrary variables and apply abstraction methods developed previously for ordinary finite-state machines to EFSMs, without the need to flatten the system and the associated overhead. Various methods of abstraction are presented that simplify individual system components while preserving the nonblocking property of the whole system.

These results are combined in an algorithm for compositional nonblocking verification of EFSM systems. This algorithm gradually composes the system and applies conflict equivalence abstraction to the components, unfolds variables, and removes events if possible. The algorithm has been implemented and its performance compared with two other well-developed algorithms. The experimental results suggest that the EFSM-based algorithm can outperform FSM-based and BDD-based methods for large systems with complex update formulas on their transitions.

In future work, the authors would like to improve the algorithm using better symbolic abstractions and considering special properties of updates. Another area of interest is to extend the method and apply it to the compositional synthesis of supervisors for EFSM systems.

Appendix: A Normalisation

This appendix contains the proofs of the propositions concerning normalisation presented in Section 4. First Proposition 1 confirms that EFSMs obtained by normalised synchronous composition in Definition 14 and by standard synchronous composition in Definition 9 produce identical flattened FSMs. Next, Proposition 2 confirms that the structure of an EFSM system is preserved after normalisation of individual components. Finally, Proposition 3 confirms that the normalised system is identical to the original system.

Proposition 1

Let $\mathcal {E}$ be a normalised EFSM system. Then $U(||\mathcal {E}) = U(\dot {\|}\mathcal {E})$.

Proof

It follows from Definitions 9, 10, and 14 that $U(||\mathcal {E})$ and $U(\dot {\|}\mathcal {E})$ have the same event and state sets, including initial and marked states. It remains to be shown that they also have the same transitions.

To show this, write $\mathcal {E} = \{E_{1},\ldots ,E_{n}\}$, and ${\Sigma }_{i} = {\Sigma }_{E_{i}}$ and ${\Delta }_{i} = {\Delta }_{E_{i}}$ for 1 ≤ i ≤ n.

First let $(x_{1},\ldots ,x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n},\hat {w})$ in $U(||\mathcal {E})$. By Definition 10 this means $(x_{1},\ldots ,x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},\ldots ,y_{n})$ in $||\mathcal {E}$ such that ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$, where $p \equiv \bigwedge _{i:\sigma \in {\Sigma }_{i}} {\Delta }_{\mathcal {E}}(\sigma )$ by Definition 9 and by the fact that $\mathcal {E}$ is normalised. Consider two cases for each E _i : either σ ∈ Σ _i or σ ∉ Σ _i . If σ ∈ Σ _i , then $x_{i} {~}^{\underrightarrow {\sigma :{\Delta }_{\mathcal {E}}(\sigma )}} y_{i}$ in E _i . If σ ∉ Σ _i , then x _i = y _i . Then $(x_{1}, \ldots , x_{n}) {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}}(\sigma )\,\,}} (y_{1}, \ldots , y_{n})$ in $\dot {\|}\mathcal {E}$ by Definition 14, and as ${\Xi }_{V}(\bigwedge _{i:\sigma \in {\Sigma }_{i}} {\Delta }_{\mathcal {E}}(\sigma ))(\hat {v},\hat {w}) = {\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$, it holds that ${\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma ))(\hat {v},\hat {w}) = \mathbf {T}$. Thus, $(x_{1}, \ldots , x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1}, \ldots , y_{n},\hat {w})$ in $U(\dot {\|}\mathcal {E})$ by Definition 10.

Conversely, assume $(x_{1},\ldots ,x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\dot {\|}\mathcal {E})$. By Definition 10 this means $(x_{1},\ldots ,x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},\ldots ,y_{n})$ in $\dot {\|}\mathcal {E}$ such that ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$. Consider two cases for each E _i : either σ ∈ Σ _i or σ ∉ Σ _i . If σ ∈ Σ _i , then by Definition 14 it follows that $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ in E _i . If σ ∉ Σ _i , then x _i = y _i . By Definition 9, it follows that $(x_{1}, \ldots , x_{n}) {~}^{\underrightarrow {\,\,\sigma :\bigwedge _{i:\sigma \in {\Sigma }_{i}} p\,\,}} (y_{1}, \ldots , y_{n})$ in $||\mathcal {E}$, and as ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$, it follows that ${\Xi }_{V}(\bigwedge _{i:\sigma \in {\Sigma }_{i}} p) (\hat {v},\hat {w}) = \mathbf {T}$. Thus, $(x_{1}, \ldots , x_{n},\hat {v}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1}, \ldots , y_{n},\hat {w})$ in $U(||\mathcal {E})$ by Definition 10. □

Proposition 2

Let $\mathcal {E}$ and $\mathcal {F}$ be EFSM systems, and let $\rho : {\Sigma }_{\mathcal {F}} \to {\Sigma }_{\mathcal {E}}$ be a renaming, such that $\mathcal {E}=\{E_{1}, E_{2},\ldots , E_{n}\}$ and $\mathcal {F} = \{F_{1}\, \rho ^{-1}(E_{2}),\ldots , \rho ^{-1}(E_{n})\}$ and ρ(F ₁ ) = E ₁ . Then $\rho (||\mathcal {F}) = ||\mathcal {E}$.

Proof

Let

$$\begin{array}{@{}rcl@{}} E = ||\mathcal{E} &=& E_{1} || {\cdots} || E_{n} ; \end{array} $$

(24)

$$\begin{array}{@{}rcl@{}} F = ||\mathcal{F} &=& F_{1} || F_{2} || {\cdots} || F_{n} = F_{1} || \rho^{-1}(E_{2}) || {\cdots} || \rho^{-1}(E_{n}) \ . \end{array} $$

(25)

Clearly ${\Sigma }_{E} = {\Sigma }_{\mathcal {E}} = \rho ({\Sigma }_{\mathcal {F}}) = \rho ({\Sigma }_{F})$, and from ρ(F ₁) = E ₁ it follows that E and ρ(F) have the same state sets, including initial and marked states. It remains to be shown that E and ρ(F) have the same transitions.

First assume $(x_{1}, x_{2},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1}, y_{2}, \ldots , y_{n})$ in E = E ₁||⋯||E _n . By Definition 9 it holds that $p = \bigwedge _{i:\sigma \in {\Sigma }_{E_{i}}} p_{i}$ where $x_{i} {~}^{\underrightarrow {\,\,\sigma :p_{i}\,\,}} y_{i}$ in E _i whenever $\sigma \in {\Sigma }_{E_{i}}$. Consider two cases.

• If $\sigma \in {\Sigma }_{E_{1}}$ then $x_{1} \overset {\sigma :p_{1}}{\to } y_{1}$ in E ₁. Since ρ(F ₁) = E ₁, there exists $\mu \in {\Sigma }_{F_{1}}$ such that ρ(μ) = σ and $x_{1} {~}^{\underrightarrow {\,\,\mu :p_{1}\,\,}} y_{1}$ in F ₁. Now consider two cases for each 2 ≤ i ≤ n: either $\sigma \in {\Sigma }_{E_{i}}$ or $\sigma \notin {\Sigma }_{E_{i}}$. If $\sigma \in {\Sigma }_{E_{i}}$ then $x_{i} {~}^{\underrightarrow {\,\,\sigma :p_{i}\,\,}} y_{i}$ in E _i , and since ρ(μ) = σ it holds by Definition 16 that $x_{i} {~}^{\underrightarrow {\,\,\mu :p_{i}\,\,}} y_{i}$ in ρ ⁻¹(E _i ). If $\sigma \notin {\Sigma }_{E_{i}}$ then $\mu \notin \rho ^{-1}({\Sigma }_{E_{i}}) = {\Sigma }_{\rho ^{-1}(E_{i})}$ and x _i = y _i . Combining the above observations for all i, it follows by Definition 9 that $(x_{1}, x_{2},\ldots , x_{n}) {~}^{\underrightarrow {\,\,\mu :p\,\,}}(y_{1}, y_{2},\ldots , y_{n})$ in F, which implies $(x_{1}, x_{2},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1}, y_{2},\ldots , y_{n})$ in ρ(F).

• If $\sigma \notin {\Sigma }_{E_{1}}$ then x ₁ = y ₁. As ρ is surjective by Definition 15, there exists $\mu \in {\Sigma }_{\mathcal {F}}$ such that ρ(μ) = σ. Then since $\rho ({\Sigma }_{F_{1}}) = {\Sigma }_{E_{1}}$, it holds that $\mu \notin {\Sigma }_{F_{1}}$. Now consider two cases for each 2 ≤ i ≤ n: either $\sigma \in {\Sigma }_{E_{i}}$ or $\sigma \notin {\Sigma }_{E_{i}}$. If $\sigma \in {\Sigma }_{E_{i}}$ then $x_{i} {~}^{\underrightarrow {\,\,\sigma :p_{i}\,\,}} y_{i}$ in E _i , and since ρ(μ) = σ it holds by Definition 16 that $x_{i} {~}^{\underrightarrow {\,\,\mu :p_{i}\,\,}} y_{i}$ in ρ ⁻¹(E _i ). If $\sigma \notin {\Sigma }_{E_{i}}$ then $\mu \notin \rho ^{-1}({\Sigma }_{E_{i}}) = {\Sigma }_{\rho ^{-1}(E_{i})}$ and x _i = y _i . Combining the above observations for all i, it follows by Definition 9 that $(x_{1}, x_{2},\ldots , x_{n}) {~}^{\underrightarrow {\,\,\mu :p\,\,}}(y_{1}, y_{2},\ldots , y_{n})$ in F, which implies $(x_{1}, x_{2},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1}, y_{2},\ldots , y_{n})$ in ρ(F).

Conversely assume $(x_{1}, x_{2},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1}, y_{2},\ldots , y_{n})$ in ρ(F). Then there exists $\mu \in {\Sigma }_{\mathcal {F}}$ such that ρ(μ) = σ and $(x_{1}, x_{2},\ldots , x_{n}) {~}^{\underrightarrow {\,\,\mu :p\,\,}} (y_{1}, y_{2},\ldots , y_{n})$ in F. By Definition 9 it holds that $p \equiv \bigwedge _{i:\mu \in {\Sigma }_{F_{i}}} p_{i}$ where $x_{i} {~}^{\underrightarrow {\,\,\mu :p_{i}\,\,}} y_{i}$ in F _i whenever $\mu \in {\Sigma }_{F_{i}}$. Consider two cases for E ₁:

• If $\mu \in {\Sigma }_{F_{1}}$ then $x_{1} {~}^{\underrightarrow {\,\,\mu :p_{1}\,\,}} y_{1}$ in F ₁. Since ρ(μ) = σ, it follows that $x_{1} \overset {\sigma :p_{1}}{\to } y_{1}$ in ρ(F ₁) = E ₁.

• If $\mu \notin {\Sigma }_{F_{1}}$ then $\sigma = \rho (\mu ) \notin \rho ({\Sigma }_{F_{1}}) = {\Sigma }_{E_{1}}$ and x ₁ = y ₁.

Now consider two cases for each 2 ≤ i ≤ n:

• If $\sigma \in {\Sigma }_{E_{i}}$ then $\mu \in \rho ^{-1}({\Sigma }_{E_{i}}) = {\Sigma }_{F_{i}}$ and therefore $x_{i} {~}^{\underrightarrow {\,\,\mu :p_{i}\,\,}} y_{i}$ in F _i = ρ ⁻¹(E _i ). Since ρ(μ) = σ, it holds by Definition 16 that $x_{i} {~}^{\underrightarrow {\,\,\sigma :p_{i}\,\,}} y_{i}$ in E _i .

• If $\sigma \notin {\Sigma }_{E_{i}}$ then $\mu \notin \rho ^{-1}({\Sigma }_{E_{i}}) = {\Sigma }_{F_{i}}$ and x _i = y _i .

Combining the above observations for 1 ≤ i ≤ n, it follows by Definition 9 that $(x_{1}, x_{2},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1}, y_{2},\ldots , y_{n})$ in E ₁||⋯||E _n = E. □

Proposition 3

Let $\mathcal {E}$ be an EFSM system such that each $E \in \mathcal {E}$ is normalised. Then $||\mathcal {E} = \dot {\|}\mathcal {N}(\mathcal {E})$.

Proof

It follows from Definitions 9, 14, and 17 that $||\mathcal {E}$ and $\dot {\|}\mathcal {N}(\mathcal {E})$ have the same event and state sets, including initial and marked states. It remains to be shown that they also have the same transitions.

To show this, write $\mathcal {E} = \{E_{1},\ldots ,E_{n}\}$, and ${\Sigma }_{i} = {\Sigma }_{E_{i}}$ and ${\Delta }_{i} = {\Delta }_{E_{i}}$ for 1 ≤ i ≤ n.

First assume $(x_{1}, \ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}}(y_{1}, \ldots , y_{n})$ in $||\mathcal {E}$. Then by Definitions 9 and 17, it holds that $p \equiv \bigwedge _{i:\sigma \in {\Sigma }_{i}} {\Delta }_{i}(\sigma ) \equiv {\Delta }_{\mathcal {N}(\mathcal {E})}(\sigma )$. Consider two cases for each E _i : either σ ∈ Σ _i or σ ∉ Σ _i . If σ ∈ Σ _i , then $x_{i} {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{i}(\sigma )\,\,}} y_{i}$ in E _i , and since E _i and $\mathcal {N}(E_{i})$ by Definition 17 have the same alphabet, it holds that $x_{i} {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {N}(\mathcal {E})}(\sigma )\,\,}} y_{i}$ in $\mathcal {N}(E_{i})$. If σ ∉ Σ _i , then σ is not in the alphabet of $\mathcal {N}(E_{i})$ and x _i = y _i . Then $(x_{1}, \ldots , x_{n}) {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {N}(\mathcal {E})}(\sigma )\,\,}} (y_{1}, \ldots , y_{n})$ in $\dot {\|}\mathcal {N}(\mathcal {E})$ by Definition 14, and as ${\Delta }_{\mathcal {N}(\mathcal {E})}(\sigma ) \equiv p$, it holds that $(x_{1}, \ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1}, \ldots , y_{n})$ in $\dot {\|}\mathcal {N}(\mathcal {E})$.

Conversely, assume $(x_{1}, \ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1}, \ldots , y_{n})$ in $\dot {\|}\mathcal {N}(\mathcal {E})$ where $p \equiv {\Delta }_{\mathcal {N}(\mathcal {E})}(\sigma ) \equiv \bigwedge _{i:\sigma \in {\Sigma }_{i}} {\Delta }_{i}(\sigma )$. Consider two cases for each E _i : either σ ∈ Σ _i or σ ∉ Σ _i . If σ ∈ Σ _i , then by Definition 14 it follows that $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ in $\mathcal {N}(E_{i})$, and since E _i and $\mathcal {N}(E_{i})$ have the same alphabet, it holds that $x_{i} {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{i}(\sigma )\,\,}} y_{i}$ in E _i . If σ ∉ Σ _i , then σ is not in the alphabet of E _i and x _i = y _i . By Definition 14, it follows that $(x_{1}, \ldots , x_{n}) {~}^{\underrightarrow {\,\,\sigma :\bigwedge _{i:\sigma \in {\Sigma }_{i}} {\Delta }_{i}(\sigma )\,\,}} (y_{1}, \ldots , y_{n})$ in $||\mathcal {E}$, and as $\bigwedge _{i:\sigma \in {\Sigma }_{i}} {\Delta }_{i}(\sigma ) \equiv p$, it holds that $(x_{1}, \ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1}, \ldots , y_{n})$ in $||\mathcal {E}$. □

1.1 B EFSM-based compositional verification

This appendix contains the proofs of the results concerning abstraction methods presented in Section 5. Each of the following subsections contains the proofs for the propositions in the corresponding subsection of Section 5.

1.2 B.1 FSM-based conflict equivalence abstraction

This section contains the proof of Proposition 5 in Section 5.1, which states that the nonblocking property of an EFSM system is preserved when the FSM form of a single component is simplified subject to conflict equivalence of FSMs. This proof requires modular reasoning about the unfolded EFSM system to exploit the conflict equivalence of FSM forms.

This reasoning is facilitated using an alternative way to unfold an EFSM system, called modular unfolding, where the variables are unfolded to a single variable FSM while the EFSMs are only replaced by their FSM forms.

Definition 27

Let $\mathcal {E}$ be a normalised EFSM system with variable set $V = \text {vars}(\mathcal {E})$. The variable FSM for $\mathcal {E}$ is $V_{\mathcal {E}} = \langle {\Sigma }_{\mathcal {E}}, \text {dom}(V), \to _{V}, \{v\circ \}, \text {dom}(V) \rangle$ where $\hat {v} \overset {\sigma }{\rightarrow }_{V} \hat {w}$ if ${\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma ))(\hat {v},\hat {w}) = \mathbf {T}$.

Definition 28

Let $\mathcal {E} = \{E_{1},\ldots ,E_{n}\}$ be a normalised EFSM system. The modular unfolding of $\mathcal {E}$ is

$$ \varphi(E_{1}) ||\cdots|| \varphi(E_{n}) || V_{\mathcal{E}} \ . $$

(26)

The variable FSM $V_{\mathcal {E}}$ has all possible valuations of the variables of $\mathcal {E}$ as its states and in its transitions encodes all the constraints imposed by the updates. This makes it possible to replace each EFSM E _i by its FSM form φ(E _i ) according to Definition 19, resulting in the system (26) of FSMs that interact in standard FSM synchronous composition (Definition 2). The following Lemma 13 shows that this modular unfolding is isomorphic to the EFSM system unfolding $U(\mathcal {E})$. Then the modular unfolding can be used to decompose an EFSM system into FSMs and prove Proposition 5.

Lemma 13

Let $\mathcal {E}=\{E_{1},\ldots , E_{n}\}$ be a normalised EFSM system. Then $U(\mathcal {E}) = \varphi (E_{1})|| \cdots || \varphi (E_{n})|| V_{\mathcal {E}}$.

Proof

Let $\mathcal {E} = \{E_{1}, \ldots , E_{n}\}$ with $E_{i}=\langle {\Sigma }_{i},Q_{i},\to _{i},Q^{\circ }_{\omega },Q^{\omega }_{i}\rangle$, let $E = U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$ by Proposition 1, and let $F = \varphi (E_{1})|| \cdots || \varphi (E_{n})|| V_{\mathcal {E}}$. Since E _i and φ(E _i ) have the same alphabet Σ _i , it follows that φ(E ₁)||⋯||φ(E _n ) and $\mathcal {E}$ also have the same alphabet ${\Sigma }_{\mathcal {E}} = \bigcup _{i=1}^{n} {\Sigma }_{i}$. The alphabet of $V_{\mathcal {E}}$ also is ${\Sigma }_{\mathcal {E}}$, which implies that ${\Sigma }_{E}={\Sigma }_{\mathcal {E}}={\Sigma }_{F}$. Moreover, by Definition 27 it holds that Q _E = Q ₁ × … × Q _n × dom(V) = Q _F , $Q\circ _{E}=Q\circ _{1}\times \ldots \times Q\circ _{n}\times \{\hat {v}\circ \}=Q\circ _{F}$, and $Q^{\omega }_{E}=Q^{\omega }_{1}\times \ldots \times Q^{\omega }_{n}\times \text {dom}(V) = Q^{\omega }_{F}$. It is left to show that → _E = → _F .

First let $(x_{1}, \ldots , x_{n}, \hat {v}) \overset {\sigma }{\rightarrow } (y_{1}, \ldots , y_{n}, \hat {w})$ in $E = U(\dot {\|}\mathcal {E})$. This means by Definition 10 that $(x_{1}, \ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1}, \ldots , y_{n})$ in $\dot {\|}\mathcal {E}$ where $p \equiv {\Delta }_{\mathcal {E}}(\sigma )$ and ${\Xi }_{V}(p)(\hat {v}, \hat {w}) = \mathbf {T}$. The latter means by Definition 27 that $\hat {v} \overset {\sigma }{\rightarrow }_{V} \hat {w}$ in $V_{\mathcal {E}}$. Now consider two cases for each E _i : either σ ∈ Σ _i or σ ∉ Σ _i . If σ ∈ Σ _i , it follows by Definition 14 that $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ in E _i , which implies $x_{i}{~}^{\underrightarrow {\,\,\sigma \,\,}}y_{i}$ in φ(E _i ). If σ ∉ Σ _i then x _i = y _i . Thus, $(x_{1},\ldots ,x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n},\hat {w})$ in $\varphi (E_{1})|| \cdots || \varphi (E_{n}) || V_{\mathcal {E}} = F$.

Conversely, let $(x_{1},\ldots ,x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n},\hat {w})$ in $F = \varphi (E_{1}) ||\cdots || \varphi (E_{n}) || V_{\mathcal {E}}$. This means $(x_{1},\ldots ,x_{n}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n})$ in φ(E ₁)||…||φ(E _n ) and $\hat {v} \overset {\sigma }{\rightarrow } \hat {w}$ in $V_{\mathcal {E}}$. Consider two cases for each E _i : either σ ∈ Σ _i or σ ∉ Σ _i . If σ ∈ Σ _i then by Definition 2 it follows that $x_{i}\overset {\sigma }{\rightarrow }y_{i}$ in φ(E _i ). Then by Definition 19 it holds that $x_{i}{~}^{\underrightarrow {\,\,\sigma :p\,\,}}y_{i}$ in E _i , where $p \equiv {\Delta }_{E_{i}}(\sigma ) \equiv {\Delta }_{\mathcal {E}}(\sigma )$ as $\mathcal {E}$ is normalised. If σ ∉ Σ _i then x _i = y _i . Thus, $(x_{1},\ldots ,x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}}(y_{1},\ldots ,y_{n})$ in $\dot {\|}\mathcal {E}$ by Definition 14. Furthermore, as $\hat {v} \overset {\sigma }{\rightarrow } \hat {w}$ in $V_{\mathcal {E}}$, it holds by Definition 27 that ${\Xi }_{V}(p)(\hat {v},\hat {w}) = {\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma ))(\hat {v},\hat {w}) = \mathbf {T}$. It follows by Definition 10 that $(x_{1},\ldots ,x_{n},\hat {v})\overset {\sigma }{\rightarrow }(y_{1},\ldots ,y_{n},\hat {w})$ in $U(\dot {\|}\mathcal {E}) = E$. □

Proposition 5

Let $\mathcal {E}=\{E_{1}, E_{2},\ldots , E_{n}\}$ be a normalised EFSM system and let Υ ⊆ Σ ₁ such that (Σ ₂ ∪ ⋯ ∪ Σ _n ) ∩ Υ=∅ and ${\Delta }_{\mathcal {E}}(\sigma ) \equiv \textit {true}$ for all σ ∈ Υ. Let $\mathcal {F}=\{F_{1}, E_{2},\ldots , E_{n}\}$ be a normalised EFSM system such that φ(E ₁ )∖Υ ≃ _conf φ(F ₁ )∖Υ. Then $\mathcal {E}$ is nonblocking if and only if $\mathcal {F}$ is nonblocking.

Proof

Let

$$ \varphi(E_{1}) \setminus {\Upsilon}\simeq_{conf} \varphi(F_{1}) \setminus {\Upsilon}\ . $$

(27)

Because of symmetry it is enough to show that, if $\mathcal {E}$ is nonblocking then $\mathcal {F}$ is nonblocking. Therefore assume that $\mathcal {E}$ is nonblocking, which means that $U(\mathcal {E})$ is nonblocking. By Lemma 13,

$$ U(\mathcal{E}) = \varphi(E_{1}) || {\cdots} ||\varphi(E_{n}) || V_{\mathcal{E}} $$

(28)

is nonblocking. As ${\Delta }_{\mathcal {E}}(\upsilon ) \equiv \textit {true}$ for all υ ∈ Υ, it holds by Definition 27 that $\hat {v} {~}^{\underrightarrow {\,\,\upsilon \,\,}} \hat {v}$ in $V_{\mathcal {E}}$ for all $\hat {v} \in \text {dom}(\text {vars}(\mathcal {E}))$ and all υ ∈ Υ, and these events appear on no other transitions in $V_{\mathcal {E}}$. These events are pure selfloop events in $V_{\mathcal {E}}$ and can be removed (Wonham), i.e.,

$$ U(\mathcal{E}) = \varphi(E_{1}) || {\cdots} ||\varphi(E_{n}) || V_{\mathcal{E}} = \varphi(E_{1}) || {\cdots} ||\varphi(E_{n}) || {V_{\mathcal{E}}}_{|{\Omega}} $$

(29)

is nonblocking, where ${\Omega } = {\Sigma }_{\mathcal {E}} \setminus {\Upsilon }$. Now consider $T=\varphi (E_{2})||\ldots || \varphi (E_{n})|| {V_{\mathcal {E}}}_{|{\Omega }}$. Then it follows from (Σ₂ ∪ ⋯ ∪ Σ _n ) ∩ Υ = ∅ and Ω ∩ Υ = ∅ that

$$ (\varphi(E_{1}) \setminus {\Upsilon}) || \varphi(E_{2})||\ldots|| \varphi(E_{n}) || {V_{\mathcal{E}}}_{|{\Omega}} $$

(30)

is nonblocking. Note that $V_{\mathcal {E}} = V_{\mathcal {F}}$. Since φ(E ₁)∖Υ and φ(F ₁)∖Υ are conflict equivalent (27), it follows that

$$ (\varphi(F_{1}) \setminus {\Upsilon}) || \varphi(E_{2})||\ldots|| \varphi(E_{n}) || {V_{\mathcal{F}}}_{|{\Omega}} $$

(31)

is nonblocking. Again since (Σ₂ ∪ ⋯ ∪ Σ _n ) ∩ Υ = ∅ and Ω ∩ Υ = ∅ and the events in Υ are pure selfloops in $V_{\mathcal {E}} = V_{\mathcal {F}}$, it follows that

$$ \varphi(F_{1})|| \varphi(E_{2})||\ldots|| \varphi(E_{n})|| {V_{\mathcal{F}}}_{|{\Omega}} = \varphi(F_{1})|| \varphi(E_{2})||\ldots|| \varphi(E_{n})|| V_{\mathcal{F}} = U(\mathcal{F}) $$

(32)

is nonblocking, i.e., $\mathcal {F}$ is nonblocking. □

1.3 B.2 Partial composition

This section proves that the synchronous composition of two components in an EFSM system preserves the nonblocking property of the system as stated in Proposition 6 in Section 5.2. In this proof, it is shown that the results of unfolding before and after partial synchronous composition are not only equivalent but identical.

Proposition 6

(Partial Composition) Let $\mathcal {E} = \{E_{1}, \ldots , E_{n}\}$ be an EFSM system, and let $\mathcal {F} = \{E_{1} \dot {\|} E_{2}, E_{3}, \ldots , E_{n}\}$ . Then $\dot {\|}\mathcal {E}=\dot {\|}\mathcal {F}$.

Proof

It follows from Definition 14 that $\dot {\|}\mathcal {E}$ and $\dot {\|}\mathcal {F}$ have the same event and state sets, including initial and marked states. It remains to be shown that they also have the same transitions. Throughout the proof, let ${\Sigma }_{i} = {\Sigma }_{E_{i}}$ for 1 ≤ i ≤ n.

First, let

$$ (x_{1},\ldots,x_{n}) {~}^{\underrightarrow{\;\;\sigma:p\;\;}} (y_{1},\ldots,y_{n}) $$

(33)

in $\dot {\|}\mathcal {E}$. By Definition 14, this means for each 1 ≤ i ≤ n that either σ ∈ Σ _i and $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ or σ ∉ Σ _i and x _i = y _i . Consider four cases for E ₁ and E ₂.

• If σ ∈ Σ₁ ∩ Σ₂, then $x_{1}{~}^{\underrightarrow {\;\;\sigma :p\;\;}}y_{1}$ in E ₁ and $x_{2}{~}^{\underrightarrow {\;\;\sigma :p\;\;}}y_{2}$ in E ₂, and by Definition 14 it holds that $(x_{1},x_{2}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},y_{2})$ in $E_{1} \dot {\|} E_{2}$.

• If σ ∈ Σ₁∖Σ₂, then $x_{1} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{1}$ in E ₁ and x ₂ = y ₂, and by Definition 14 it holds that $(x_{1},x_{2}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},x_{2}) = (y_{1},y_{2})$ in $E_{1} \dot {\|} E_{2}$.

• If σ ∈ Σ₂∖Σ₁, then x ₁ = y ₁ and $x_{2} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{2}$ in E ₂, and by Definition 14 it holds that $(x_{1},x_{2}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (x_{1},y_{2}) = (y_{1},y_{2})$ in $E_{1} \dot {\|} E_{2}$.

• If σ ∉ Σ₁ ∪ Σ₂, then σ is not in the alphabet of $E_{1} \dot {\|} E_{2}$ and (x ₁, x ₂) = (y ₁, y ₂).

Combining the above observations for $E_{1} \dot {\|} E_{2}$ and E ₃, … , E _n , it follows by Definition 14 that $((x_{1},x_{2}), x_{3},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} ((y_{1},y_{2}), y_{3},\ldots , y_{n})$ in $\dot {\|}\mathcal {F}$.

Conversely, let

$$ ((x_{1},x_{2}),x_{3},\ldots,x_{n}) {~}^{\underrightarrow{\;\;\sigma:p\;\;}} ((y_{1},y_{2}),y_{3},\ldots,y_{n}) $$

(34)

in $\dot {\|}\mathcal {F}$. Consider four cases for E ₁ and E ₂.

• If σ ∈ Σ₁ ∩ Σ₂, then by Definition 14 it holds that $(x_{1},x_{2}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},y_{2})$ in $E_{1}\dot {\|} E_{2}$, and furthermore $x_{1} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{1}$ in E ₁ and $x_{2} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{2}$ in E ₂.

• If σ ∈ Σ₁∖Σ₂, then by Definition 14 it holds that $(x_{1},x_{2}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},y_{2})$ in $E_{1}\dot {\|} E_{2}$, and furthermore $x_{1} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{1}$ in E ₁ and σ ∉ Σ₂ and x ₂ = y ₂.

• If σ ∈ Σ₂∖Σ₁, then by Definition 14 it holds that $(x_{1},x_{2}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},y_{2})$ in $E_{1}\dot {\|} E_{2}$, and furthermore σ ∉ Σ₁ and x ₁ = y ₁ and $x_{2} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{2}$ in E ₂ and

• if σ ∉ Σ₁ ∪ Σ₂, then by Definition 14 it holds that x ₁ = x ₂ and y ₁ = y ₂.

Furthermore, for 3 ≤ i ≤ n it follows from (34) by Definition 14 that either σ ∈ Σ _i and $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ or σ ∉ Σ _i and x _i = y _i . Combining the above observations for E ₁, … , E _n , it follows by Definition 14 that $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\mathcal {F}$. □

1.4 B.3 Update simplification

This section proves the correctness of update simplification as stated in Proposition 7 in Section 5.3. The proof uses the following lemma, which shows two EFSM systems with logically equivalent updates with respect to all variables have isomorphic monolithic flattening results.

Lemma 14

Let $\mathcal {E} = \{E_{1},\ldots , E_{n}\}$ and $\mathcal {F}=\{F_{1},\ldots , F_{n}\}$ be normalised EFSM systems with $E_{i} = \langle {\Sigma }_{i}, Q_{i}, {\to _{i}^{E}}, Q^{\circ }_{i}, Q^{\omega }_{i}\rangle$ and $F_{i}=\langle {\Sigma }_{i}, Q_{i}, {\to _{i}^{F}}, Q^{\circ }_{i}, Q^{\omega }_{i}\rangle$ . Let $V = \text {vars}(\mathcal {E}) = \text {vars}(\mathcal {F})$ and ${\Delta }_{\mathcal {E}}(\sigma ) \Leftrightarrow _{V} {\Delta }_{\mathcal {F}}(\sigma )$ for all $\sigma \in {\Sigma }_{\mathcal {E}} = {\Sigma }_{\mathcal {F}}$ , and ${\to _{i}^{F}} = \{\, (x,\sigma ,{\Delta }_{\mathcal {F}}(\sigma ),y) \mid x {{~}^{\underrightarrow {\;\;\sigma :{\Delta }_{\mathcal {E}(\sigma )\;\;}}}}_{i}^{E} y \,\}$ . Then $U(\mathcal {E}) = U(\mathcal {F})$.

Proof

Clearly, $U(\mathcal {E})$ and $U(\mathcal {F})$ by construction both have the same event alphabet ${\Sigma }_{\mathcal {E}}$, and they have the same state sets, including initial and marked states. Also note that $\mathcal {E}$ and $\mathcal {F}$ are normalised, so $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$ and $U(\mathcal {F}) = U(\dot {\|}\mathcal {F})$ by Proposition 1. It remains to be shown that $U(\mathcal {E})$ and $U(\mathcal {F})$ have the same transitions. Because of symmetry it is enough to show that, if $(x_{1},\ldots , x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n}, \hat {w})$ in $U(\mathcal {E})$ then $(x_{1},\ldots , x_{n}, \hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n}, \hat {w})$ in $U(\mathcal {F})$.

Assume $(x_{1}, \ldots , x_{n}, \hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n}, \hat {w})$ in $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$. By Definition 10, this means $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}}(\sigma )\,\,}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\mathcal {E}$ and ${\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma )) (\hat {v},\hat {w}) = \mathbf {T}$. Then by construction, $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {F}}(\sigma )\,\,}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\mathcal {F}$ and ${\Delta }_{\mathcal {E}}(\sigma ) \Leftrightarrow _{V} {\Delta }_{\mathcal {F}}(\sigma )$. The latter means ${\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma )) \Leftrightarrow {\Xi }_{V}({\Delta }_{\mathcal {F}}(\sigma ))$ by Definition 20, i.e., ${\Xi }_{V}({\Delta }_{\mathcal {F}}(\sigma )) (\hat {v},\hat {w}) = {\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma )) (\hat {v},\hat {w}) = \mathbf {T}$. It follows by Definition 10 that $(x_{1}, \ldots , x_{n}, \hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n}, \hat {w})$ in $U(\dot {\|}\mathcal {F}) = U(\mathcal {F})$. □

Proposition 7 (Update Simplification)

Let $\mathcal {E} = \{E_{1},\ldots , E_{n}\}$ and $\mathcal {F}=\{F_{1},\ldots , F_{n}\}$ be normalised EFSM systems with $E_{i} = \langle {\Sigma }_{i}, Q_{i}, {\to _{i}^{E}}, Q^{\circ }_{i}, Q^{\omega }[i]\rangle$ and $F_{i}=\langle {\Sigma }_{i}, Q_{i}, {\to _{i}^{F}}, Q^{\circ }_{i}, Q^{\omega }_{i}\rangle$ . Let $V = \text {vars}(\mathcal {E}) = \text {vars}(\mathcal {F})$ and ${\Delta }_{\mathcal {E}}(\sigma ) \Leftrightarrow _{V} {\Delta }_{\mathcal {F}}(\sigma )$ for all $\sigma \in {\Sigma }_{\mathcal {E}} = {\Sigma }_{\mathcal {F}}$ , and ${\to _{i}^{F}} = \{\, (x,\sigma ,{\Delta }_{\mathcal {F}}(\sigma ),y) \mid x {{~}^{\underrightarrow {\;\;\sigma :{\Delta }_{\mathcal {E}(\sigma )\;\;}}}}_{i}^{E} y \,\}$ . Then $\mathcal {E}$ is nonblocking if and only if $\mathcal {F}$ is nonblocking.

Proof

By Definition 11, $\mathcal {E}$ is nonblocking if and only if $U(\mathcal {E})$ is nonblocking, and $\mathcal {F}$ is nonblocking if and only if $U(\mathcal {F})$ is nonblocking; and by Lemma 14, it holds that $U(\mathcal {E}) = U(\mathcal {F})$. It follows that $\mathcal {E}$ is nonblocking if and only if $\mathcal {F}$ is nonblocking. □

1.5 B.4 Variable unfolding

This section proves that unfolding of a variable in an EFSM system preserves the nonblocking property of the system as stated in Proposition 8 in Section 5.4. The key step to prove this result is contained in Lemma 15, which shows that the FSMs obtained from completely unfolding the system before and after partial unfolding have essentially the same transition relations. The link between these transition relations is established by extending or restricting valuations to add or remove the variable to be unfolded. The following two definitions are needed for this purpose.

Definition 29

Let $\hat {v}\colon V \to D$ be a valuation. For a variable set W ⊆ V, the restriction $\hat {v}_{|W}\colon W \to D$ is defined by $\hat {v}_{|W}[v] = \hat {v}[v]$ for all v ∈ W.

Definition 30

Let $V = V_{1} \dot {\cup } V_{2}$ be a variable set, and let $\hat {v}_{1} \colon V_{1} \to D_{1}$ and $\hat {v}_{2} \colon V_{2} \to D_{2}$ be two valuations. The extension $\hat {v}_{1} \oplus \hat {v}_{2}\colon V \to D_{1} \cup D_{2}$ is defined by

$$ (\hat{v}_{1} \oplus \hat{v}_{2})[v] = \left\{\begin{array}{ll} \hat{v}_{1}[v], & \text{if}\ v \in V_{1}\ ; \\ \hat{v}_{2}[v], & \text{if}\ v \in V_{2}\ . \end{array}\right. $$

(35)

Lemma 15

Let $\mathcal {E}=\{E_{1},\ldots , E_{n}\}$ be a normalised EFSM system and $z \in \text {vars}(\mathcal {E})$ . Then $(a,x_{1},\ldots ,x_{n},\check {v}) \overset {\sigma }{\rightarrow } (b,x_{1},\ldots ,x_{n},\check {w})$ in $\rho _{z}(U(\mathcal {E} \setminus z))$ if and only if $(x_{1},\ldots ,x_{n},\check {v} \oplus \{z \mapsto a\}) \overset {\sigma }{\rightarrow } (x_{1},\ldots ,x_{n}, \check {w} \oplus \{z \mapsto b\})$ in $U(\mathcal {E})$.

Proof

Let $V = \text {vars}(\mathcal {E})$, and let $\hat {v} = \check {v} \oplus \{z \mapsto a\}$ and $\hat {w} = \check {w} \oplus \{z \mapsto b\}$, which means $\hat {v}[z]=a$ and $\hat {w}[z] = b$. Also write $E_{i} = \langle {{\Sigma }_{i},Q_{i},\to _{i},Q^{\circ }_{i},Q^{\omega }_{i}}\rangle$ for 1 ≤ i ≤ n. Note that $\mathcal {E}$ and $\mathcal {E}\setminus z$ are normalised, so by Proposition 1 it holds that $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$ and $U(\mathcal {E} \setminus z) = U(\dot {\|}(\mathcal {E} \setminus z))$.

First let $(a,x_{1},\ldots ,x_{n},\check {v}) \overset {\sigma }{\rightarrow } (b,y_{1},\ldots ,y_{n},\check {w})$ in $\rho _{z}(U(\mathcal {E} \setminus z)) = \rho _{z}(U(\dot {\|}\mathcal {E} \setminus z))$. Note that $\mathcal {E} \setminus z =\{ U_{\mathcal {E}}(z), U_{z}(E_{1}),\cdots , U_{z}(E_{n})\}$ by Definition 24. Consider two cases.

• (i) σ ∈ Σ _z . Then $z \in \text {vars}({\Delta }_{\mathcal {E}}(\sigma ))$ by Definition 22, and $(a,x_{1},\ldots ,x_{n},\check {v}) {~}^{\underrightarrow {\,\,(\sigma ^{\prime },a^{\prime },b^{\prime })\,\,}} (b,y_{1},\ldots ,y_{n},\check {w})$ in $U(\mathcal {E} \setminus z) = U(\dot {\|}(\mathcal {E} \setminus z))$ for some (σ′, a′, b′) ∈ U _z (Σ _z ) such that ρ _z ((σ′, a′, b′)) = σ. By definition of ρ _z it holds that σ′ = σ. By Definition 10, it holds that

  $$\begin{array}{@{}rcl@{}} &&(a, x_{1},\ldots, x_{n}) {~}^{\underrightarrow{\,\,(\sigma,a^{\prime},b^{\prime})\,:\,{\Delta}_{\mathcal{E}\setminus z}((\sigma,a^{\prime},b^{\prime}))\,\,}} (b, y_{1},\ldots, y_{n}) \quad\text{in}\ \dot{\|}(\mathcal{E} \setminus z) \\&&= U_{\mathcal{E}}(z) \dot{\|} U_{z}(E_{1}) \dot{\|}\cdots\dot{\|} U_{z}(E_{n}) \end{array} $$

  (36)

  and ${\Xi }_{V \setminus \{z\}}({\Delta }_{\mathcal {E}\setminus z}((\sigma ,a^{\prime },b^{\prime }))) (\check {v},\check {w}) = \mathbf {T}$. As (σ, a′, b′) = (σ′, a′, b′) ∈ U _z (Σ _z ) is in the alphabet of $U_{\mathcal {E}}(z)$, it follows that

  $$\begin{array}{@{}rcl@{}} a {~}^{\underrightarrow{\,\,(\sigma,a^{\prime},b^{\prime})\,:\,{\Delta}_{\mathcal{E}\setminus z}((\sigma,a^{\prime},b^{\prime}))\,\,}} b \quad\text{in}\ U_{\mathcal{E}}(z) \ . \end{array} $$

  (37)

  Then it follows from Definition 22 that a′ = a and b′ = b, and ${\Delta }_{\mathcal {E}\setminus z}((\sigma ,a,b)) \equiv {\Xi }_{\{z\}}({\Delta }_{\mathcal {E}}(\sigma ))[z\mapsto a , z^{\prime }\mapsto b]$. Note that

  $$\begin{array}{@{}rcl@{}} {\Xi}_{V}({\Delta}_{\mathcal{E}}(\sigma))(\hat{v},\hat{w}) &=& {\Xi}_{V}({\Delta}_{\mathcal{E}}(\sigma))(\check{v} \oplus \{z \mapsto a\}, \check{w} \oplus \{z \mapsto b\}) \\ &=& {\Xi}_{V \setminus \{z\}}({\Xi}_{\{z\}}({\Delta}_{\mathcal{E}}(\sigma))) (\check{v} \oplus \{z \mapsto a\}, \check{w} \oplus \{z \mapsto b\}) \\ &=& {\Xi}_{V \setminus \{z\}}({\Xi}_{\{z\}}({\Delta}_{\mathcal{E}}(\sigma))) [z \mapsto a, z^{\prime} \mapsto b] (\check{v}, \check{w}) \\ &=& {\Xi}_{V \setminus \{z\}}({\Xi}_{\{z\}}({\Delta}_{\mathcal{E}}(\sigma)) [z \mapsto a, z^{\prime} \mapsto b]) (\check{v}, \check{w}) \\ &=& {\Xi}_{V \setminus \{z\}}({\Delta}_{\mathcal{E}\setminus z}((\sigma,a,b))) (\check{v}, \check{w}) \\ &=& {\Xi}_{V \setminus \{z\}}({\Delta}_{\mathcal{E}\setminus z}((\sigma,a^{\prime},b^{\prime}))) (\check{v}, \check{w}) \\ &=& \mathbf{T} \ . \end{array} $$

  Now consider some E _i with 1 ≤ i ≤ n. If σ ∈ Σ _i then since σ ∈ Σ _z also (σ, a′, b′) ∈ U _z (Σ _i ) so that (σ, a′, b′) is in the alphabet of U _z (E _i ) by Definition 23. It follows from (36) that $x_{i} {~}^{\underrightarrow {\,\,(\sigma ,a^{\prime },b^{\prime }):{\Delta }_{\mathcal {E}\setminus z}((\sigma ,a^{\prime },b^{\prime }))\,\,}} y_{i}$ in U _z (E _i ), which implies $x_{i} {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}}(\sigma )\,\,}} y_{i}$ in E _i by Definition 23. Otherwise, if σ ∉ Σ _i then (σ, a′, b′) is not in the alphabet of U _z (E _i ) and x _i = y _i . Having shown the above for all 1 ≤ i ≤ n, it can be concluded by Definition 14 that $(x_{1},\ldots ,x_{n}) {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}}(\sigma )\,\,}} (y_{1},\ldots ,y_{n})$ in $E_{1} \dot {\|} {\cdots } \dot {\|} E_{n} = \dot {\|}\mathcal {E}$.

• (ii) σ ∉ Σ _z . Then $z \notin \text {vars}({\Delta }_{\mathcal {E}}(\sigma ))$ by Definition 22, and $(a,x_{1},\ldots ,x_{n},\check {v}) {~}^{\underrightarrow {\,\,\sigma ^{\prime }\,\,}} (b,y_{1},\ldots ,y_{n},\check {w})$ in $U(\mathcal {E} \setminus z) = U(\dot {\|}(\mathcal {E} \setminus z))$ for some $\sigma ^{\prime } \in {\Sigma }_{\mathcal {E} \setminus z} \setminus U_{z}({\Sigma }_{z})$ such that ρ _z (σ′) = σ. By definition of ρ _z it holds that $\sigma ^{\prime } = \sigma \in {\Sigma }_{\mathcal {E}}$. By Definition 10, it holds that

  $$ (a, x_{1},\ldots, x_{n}) {~}^{\underrightarrow{\,\,\sigma:{\Delta}_{\mathcal{E}\setminus z}(\sigma)\,\,}} (b, y_{1},\ldots, y_{n}) \quad\text{in}\ \dot{\|}(\mathcal{E} \setminus z) = U_{\mathcal{E}}(z) \dot{\|} U_{z}(E_{1}) \dot{\|}\cdots\dot{\|} U_{z}(E_{n}) $$

  (38)

  and ${\Xi }_{V \setminus \{z\}}({\Delta }_{\mathcal {E} \setminus z}(\sigma )) (\check {v}, \check {w}) = \mathbf {T}$. As $\sigma \in {\Sigma }_{\mathcal {E}}$, it is clear that σ ∉ U _z (Σ _z ) and thus σ is not in the alphabet of $U_{\mathcal {E}}(z)$, which implies a = b. Also by (38), there must exist i such that $x_{i} {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}\setminus z}(\sigma )\,\,}} y_{i}$ in U _z (E _i ), which given $\sigma \in {\Sigma }_{\mathcal {E}}$ implies $x_{i} {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}\setminus z}(\sigma )\,\,}} y_{i}$ in E _i by Definition 23 where ${\Delta }_{\mathcal {E}\setminus z}(\sigma ) \equiv {\Delta }_{\mathcal {E}}(\sigma )$ as $\mathcal {E}$ is normalised. As $z \notin \text {vars}({\Delta }_{\mathcal {E}}(\sigma ))$, it holds that ${\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma ))(\hat {v},\hat {w}) = {\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma ))(\check {v} \oplus \{z \mapsto a\}, \check {w} \oplus \{z \mapsto b\}) = {\Xi }_{V \setminus \{z\}}({\Delta }_{\mathcal {E}}(\sigma ))(\check {v}, \check {w}) = {\Xi }_{V \setminus \{z\}}({\Delta }_{\mathcal {E} \setminus z}(\sigma )) (\check {v}, \check {w}) = \mathbf {T}$.

  Now consider some E _i with 1 ≤ i ≤ n. If σ ∈ Σ _i then since σ ∉ Σ _z it follows from (38) that $x_{i} {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E} \setminus z}(\sigma )\,\,}} y_{i}$ in U _z (E _i ), which implies $x_{i} {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}}(\sigma )\,\,}} y_{i}$ in E _i by Definition 23. Otherwise, if σ ∉ Σ _i then σ is not in the alphabet of U _z (E _i ) and x _i = y _i . Having shown the above for all 1 ≤ i ≤ n, it can be concluded by Definition 14 that $(x_{1},\ldots ,x_{n}) {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}}(\sigma )\,\,}} (y_{1},\ldots ,y_{n})$ in $E_{1} \dot {\|} {\cdots } \dot {\|} E_{n} = \dot {\|}\mathcal {E}$.

In both cases, it has been shown that $(x_{1},\ldots ,x_{n}) {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}}(\sigma )\,\,}} (y_{1},\ldots ,y_{n})$ in $\dot {\|}\mathcal {E}$ and ${\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma ))(\hat {v},\hat {w}) = \mathbf {T}$. Then it follows by Definition 10 that $(x_{1},\ldots ,x_{n},\check {v} \oplus \{z \mapsto a\}) = (x_{1},\ldots ,x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n},\hat {w}) = (y_{1},\ldots ,y_{n},\check {w} \oplus \{z \mapsto b\})$ in $U(\dot {\|}\mathcal {E}) = U(\mathcal {E})$.

Conversely let $(x_{1},\ldots ,x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$. Then it holds by Definition 10 that

$$ (x_{1},\ldots, x_{n}) {~}^{\underrightarrow{\;\;\sigma:p\;\;}} (y_{1},\ldots, y_{n}) \qquad\text{in}\ \dot{\|}\mathcal{E} = E_{1} \dot{\|} {\cdots} \dot{\|} E_{n} $$

(39)

where $p \equiv {\Delta }_{\mathcal {E}}(\sigma )$ and ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$. Consider two cases.

• (i) σ ∈ Σ _z . Note that $z \in \text {vars}({\Delta }_{\mathcal {E}}(\sigma )) = \text {vars}(p)$. Then by Definition 22 it holds that $a {~}^{\underrightarrow {\,\,(\sigma ,a,b):p^{\prime }\,\,}} b$ in $U_{\mathcal {E}}(z)$ where p′ ≡ Ξ_{z}(p)[z ↦ a, z′ ↦ b] and ρ _z ((σ, a, b)) = σ. Note that ${\Xi }_{V\setminus \{z\}}(p^{\prime })(\check {v},\check {w}) = {\Xi }_{V\setminus \{z\}}({\Xi }_{\{z\}}(p))[z\mapsto a, z^{\prime }\mapsto b]) (\check {v},\check {w}) = ({\Xi }_{V}(p)[z\mapsto a, z^{\prime }\mapsto b]) (\check {v},\check {w}) = {\Xi }_{V}(p)(\check {v} \oplus \{z \mapsto b\},\check {w} \oplus \{z \mapsto b\}) = {\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$.Now consider some E _i with 1 ≤ i ≤ n. If σ ∈ Σ _i , it follows from (39) that $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ in E _i , which implies $x_{i} {~}^{\underrightarrow {\,\,(\sigma ,a,b):p^{\prime }\,\,}} y_{i}$ in U _z (E _i ) by Definition 23 as σ ∈ Σ _z . Otherwise, if σ ∉ Σ _i then σ is not in the alphabet of E _i and x _i = y _i . Having shown the above for all 1 ≤ i ≤ n, it can be concluded by Definition 14 that

  $$\begin{array}{@{}rcl@{}} (a,x_{1},\ldots,x_{n}) & \!\!\!{~}^{\underrightarrow{\,\,(\sigma,a,b):p^{\prime}\,\,}} (b,y_{1},\ldots,y_{n})~ \text{in}\ U_{\mathcal{E}}(z) \dot{\|} U_{z}(E_{1}) \dot{\|} {\cdots} || U_{z}(E_{n}) \,=\, \dot{\|}(\mathcal{E} \setminus z) \ .\\ \end{array} $$

  (40)

  Since ${\Xi }_{V\setminus \{z\}}(p^{\prime })(\check {v},\check {w}) = \mathbf {T}$, it follows by Definition 10 that $(a,x_{1},\ldots ,x_{n},\check {v}) {~}^{\underrightarrow {\,\,(\sigma ,a,b):p^{\prime }\,\,}} (b,y_{1},\ldots ,y_{n},\check {w})$ in $U(\dot {\|}(\mathcal {E} \setminus z)) = U(\mathcal {E} \setminus z)$, which implies $(a,x_{1},\ldots ,x_{n},\check {v}) \overset {\sigma }{\rightarrow } (b,y_{1},\ldots ,y_{n},\check {w})$ in $\rho _{z}(U(\mathcal {E} \setminus z))$.

• (ii) σ ∉ Σ _z . In this case, by Definition 22 it holds that $z \notin \text {vars}({\Delta }_{\mathcal {E}}(\sigma )) = \text {vars}(p)$ and $\rho _{z}(\sigma ) = \sigma \in {\Sigma }_{\mathcal {E}}$ is not in the alphabet of $U_{\mathcal {E}}(z)$. Consider some E _i with 1 ≤ i ≤ n. If σ ∈ Σ _i , it follows from (39) that $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ in E _i , which implies $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ in U _z (E _i ) by Definition 23 as σ ∈ Σ _i ∖Σ _z . Otherwise, if σ ∉ Σ _i then σ is not in the alphabet of E _i and x _i = y _i . Having shown the above for all 1 ≤ i ≤ n, it can be concluded by Definition 14 that

  $$\begin{array}{@{}rcl@{}} (a,x_{1},\ldots,x_{n}) & {~}^{\underrightarrow{\;\;\sigma:p\;\;}} (a,y_{1},\ldots,y_{n})\quad \text{in}\ U_{\mathcal{E}}(z) \dot{\|} U_{z}(E_{1}) \dot{\|} {\cdots} \dot{\|} U_{z}(E_{n}) = \dot{\|}(\mathcal{E} \setminus z) \ .\\ \end{array} $$

  (41)

  From ${\Xi }_{V}(p)(\hat {v}, \hat {w}) = \mathbf {T}$ and z ∉ vars(p)⊇vars′(p), it follows that $(z^{\prime }=z)(\hat {v}, \hat {w}) = \mathbf {T}$. This means $a = \hat {v}[z] = \hat {w}[z] = b$ and ${\Xi }_{V \setminus \{z\}}(p)(\check {v}, \check {w}) = {\Xi }_{V}(p)(\hat {v}, \hat {w}) = \mathbf {T}$. Then by Definition 10, it holds that $(a, x_{1}, \ldots , x_{n}, \check {v}) \overset {\sigma }{\rightarrow } (a, y_{1}, \ldots , y_{n}, \check {w}) = (b, y_{1}, \ldots , y_{n}, \check {w})$ in $U(\dot {\|}(\mathcal {E} \setminus z)) = U(\mathcal {E} \setminus z)$, which given ρ _z (σ) = σ implies $(a, x_{1}, \ldots , x_{n}, \check {v}) \overset {\sigma }{\rightarrow } (b, y_{1}, \ldots , y_{n}, \check {w})$ in $\rho _{z}(U(\mathcal {E} \setminus z))$.

□

Proposition 8 (Variable Unfolding)

Let $\mathcal {E}$ be a normalised EFSM system, and let $z \in \text {vars}(\mathcal {E})$ . Then $\mathcal {E}$ is nonblocking if and only if $\mathcal {E} \setminus z$ is nonblocking.

Proof

Let $\mathcal {E} = \{E_{1},\ldots , E_{n}\}$, let $\mathcal {E} \setminus z = \{U_{\mathcal {E}}(z), U_{z}(E_{1}),\ldots , U_{z}(E_{n})$, according to Definition 24, and let $\rho _{z}\colon {\Sigma }_{\mathcal {E}} \cup U_{z}({\Sigma }_{z}) \to {\Sigma }_{\mathcal {E}}$ be the variable renaming map according to Definition 22.

First assume $\mathcal {E}$ is nonblocking, which implies $U(\mathcal {E})$ is nonblocking. It will be shown that $\rho _{z}(U(\mathcal {E}\setminus z))$ is nonblocking. Assume $(a^{0}, {x^{0}_{1}},\ldots ,{x_{n}^{0}},\check {v}^{0}) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} (a^{l}, {x^{l}_{1}},\ldots , {x_{n}^{l}},\check {v}^{l})$ in $\rho _{z}(U(\mathcal {E}\setminus z))$. From Lemma 15 it follows that $({x^{0}_{1}},\ldots , {x_{n}^{0}},\check {v}^{0} \oplus \{z \mapsto a^{0}\}) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} ({x^{l}_{1}},\ldots , {x_{n}^{l}}, \check {v}^{l} \oplus \{z \mapsto a^{l}\})$ in $U(\mathcal {E})$. Since $U(\mathcal {E})$ is nonblocking, there exists a path $({x^{l}_{1}},\ldots , {x_{n}^{l}},\hat {v}^{l}) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} ({x^{m}_{1}},\ldots , {x_{n}^{m}},\hat {v}^{m})$ in $U(\mathcal {E})$ such that $({x^{m}_{1}},\ldots , {x_{n}^{m}}) \in Q_{1}^{\omega } \times {\cdots } \times Q_{n}^{\omega }$. From Lemma 15 it follows that $(a^{l}, {x^{l}_{1}},\ldots , {x_{n}^{l}},\check {v}^{l}) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} \cdots {~}^{\underrightarrow {\,\,\sigma _{l}\,\,}} (a^{m}, {x^{m}_{1}},\ldots , {x_{n}^{m}},\check {v}^{m})$ in $\rho _{z}(U(\mathcal {E}\setminus z))$ such that $({x^{m}_{1}},\ldots , {x_{n}^{m}}) \in Q_{1}^{\omega } \times {\cdots } \times Q_{n}^{\omega }$ and $\hat {v}^{i} = \check {v}^{i} \oplus \{z \mapsto a^{i}\}$ for l + 1 ≤ i ≤ m. Since $({x^{l}_{1}},\ldots , {x_{n}^{l}},\hat {v}^{l})$ was chosen arbitrarily, it holds that $\rho _{z}(U(\mathcal {E}\setminus z))$ is nonblocking. Since renaming preserves nonblocking, it holds that $U(\mathcal {E}\setminus z)$ is nonblocking, which implies that $\mathcal {E}\setminus z$ is nonblocking.

Conversely assume $\mathcal {E} \setminus z$ is nonblocking. Then $U(\mathcal {E}\setminus z)$ is nonblocking, which implies $\rho _{z}(U(\mathcal {E}\setminus z))$ is nonblocking. It will be shown that $U(\mathcal {E})$ is nonblocking. Assume $({x^{0}_{1}},\ldots , {x_{n}^{0}},\hat {v}^{0}) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} ({x^{l}_{1}},\ldots , {x_{n}^{l}},\hat {v}^{l})$ in $U(\mathcal {E})$. From Lemma 15, it follows that $(a^{0}, {x^{0}_{1}},\ldots , {x_{n}^{0}},\check {v}^{0}) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} \cdots {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} (a^{l}, {x^{l}_{1}},\ldots , {x_{n}^{l}},\check {v}^{l})$ in $\rho _{z}(U(\mathcal {E}\setminus z))$, where $\hat {v}^{i} = \check {v}^{i} \oplus \{z \mapsto a^{i}\}$ for 0 ≤ i ≤ l. Since $\rho _{z}(U(\mathcal {E}\setminus z))$ is nonblocking, there exists a path $(a^{l}, {x^{l}_{1}},\ldots , {x_{n}^{l}},\check {v}^{l}) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} (a^{m}, {x^{m}_{1}},\ldots , {x_{n}^{m}},\check {v}^{m})$ in $\rho _{z}(U(\mathcal {E} \setminus z))$ such that $({x^{m}_{1}},\ldots , {x_{n}^{m}}) \in Q_{1}^{\omega } \times {\cdots } \times Q_{n}^{\omega }$. From Lemma 15 it follows that $({x^{l}_{1}},\ldots , {x_{n}^{l}}, \check {v}^{l} \oplus \{z \mapsto a^{l}\}) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} ({x^{m}_{1}},\ldots , {x_{n}^{m}},\check {v}^{m} \oplus \{z \mapsto a^{m}\})$ in $U(\mathcal {E})$ such that $({x^{m}_{1}},\ldots , {x_{n}^{m}}) \in Q_{1}^{\omega } \times {\cdots } \times Q_{n}^{\omega }$. Since $({x^{l}_{1}},\ldots , {x_{n}^{l}},\hat {v}^{l})$ was chosen arbitrarily, it follows that $U(\mathcal {E})$ is nonblocking, which implies that $\mathcal {E}$ is nonblocking. □

1.6 B.5 Event simplification

This section contains proofs of correctness of the event removal and merging operations in Propositions 9–12 in Section 5.5. The common approach to prove that abstractions such as these preserve the nonblocking property of an EFSM system, is to show that for each path in the EFSM system before abstraction there exists a corresponding path after abstraction, and vice versa.

First, to prove Prop. 9, which states that false-removal preserves the nonblocking property, it is shown in Lemma 16 that every path in any EFSM system resulting from restriction can be lifted to a path in the original system, and conversely it is shown in Lemma 17 that paths in an EFSM system also exist in a system resulting from false-removal.

Lemma 16

Let $\mathcal {E} = \{E_{1},\ldots ,E_{n}\}$ be a normalised EFSM system, let ${\Omega } \subseteq {\Sigma }_{\mathcal {E}}$ , and let $\hat {u} \in \text {dom}(\text {vars}(\mathcal {E}) \setminus \text {vars}(\mathcal {E}_{|{\Omega }}))$ . Then $(x_{1},\ldots , x_{n}, \hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n}, \hat {w})$ in $U(\mathcal {E}_{|{\Omega }})$ implies $(x_{1},\ldots , x_{n}, \hat {v} \oplus \hat {u}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n}, \hat {w} \oplus \hat {u})$ in $U(\mathcal {E})$.

Proof

Let $\mathcal {F} = \mathcal {E}_{|{\Omega }}$ and $V = \text {vars}(\mathcal {E})$ and $W = \text {vars}(\mathcal {E}_{|{\Omega }}) \subseteq \text {vars}(\mathcal {E}) = V$.

Assume $(x_{1},\ldots , x_{n}, \hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n}, \hat {w})$ in $U(\mathcal {F}) = U(\dot {\|}\mathcal {F})$. Then σ ∈ Ω, and by Definition 10 it holds that $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\mathcal {F}$ with $p \equiv {\Delta }_{\mathcal {F}}(\sigma )$ and ${\Xi }_{W}(p)(\hat {v},\hat {w}) = \mathbf {T}$. By Definition 14, it holds that $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ in E _{i |Ω} for each i such that 1 ≤ i ≤ n and $\sigma \in {\Sigma }_{E_{i}}$, with $p \equiv {\Delta }_{\mathcal {F}}(\sigma )$ and $\text {vars}(p) \subseteq \text {vars}(\mathcal {F}) = \text {vars}(\mathcal {E}_{|{\Omega }}) = W$. As →_|Ω ⊆ →, it follows that $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ in E _i for each i such that $\sigma \in {\Sigma }_{E_{i}}$. This shows $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\mathcal {E}$ by Definition 14. As furthermore ${\Xi }_{W}(p)(\hat {v},\hat {w}) = \mathbf {T}$ and vars′(p) ⊆ vars(p) ⊆ W, it holds that ${\Xi }_{V}(p)(\hat {v}\oplus \hat {u},\hat {w}\oplus \hat {u}) = \mathbf {T}$. Thus, $(x_{1},\ldots , x_{n}, \hat {v}\oplus \hat {u}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n}, \hat {w}\oplus \hat {u})$ in $U(\dot {\|}\mathcal {E}) = U(\mathcal {E})$ by Definition 10. □

Lemma 17

Let $\mathcal {E}$ be a normalised EFSM system, and let ${\Lambda } \subseteq {\Sigma }_{\mathcal {E}}$ be a set of events such that for all λ ∈ Λ at least one of the following conditions holds:

• (i) ${\Delta }_{\mathcal {E}}(\lambda ) \equiv \textit {false}$;

• (ii) There exists $E \in \mathcal {E}$ such that λ ∈ Σ _E , but there does not exist any transition $x {{~}^{\underrightarrow {\lambda :p}}} y$ in E.

Also let $W = \text {vars}(\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }})$ . Then $(x_{1},\ldots , x_{n},\hat {v}) \overset {\sigma }{\rightarrow }(y_{1},\ldots , y_{n},\hat {w})$ in $U(\mathcal {E})$ implies $(x_{1},\ldots , x_{n},\hat {v}_{|W}) \overset {\sigma }{\rightarrow }(y_{1},\ldots , y_{n},\hat {w}_{|W})$ in $U(\mathcal {E}_{|{\Sigma }_{\mathcal {E}}\setminus {\Lambda }})$.

Proof

Let $\mathcal {E} = \{E_{1},\ldots ,E_{n}\}$ and ${\Omega } = {\Sigma }_{\mathcal {E}} \setminus {\Lambda }$ and $\mathcal {F} = \mathcal {E}_{|{\Omega }}$ and $V=\text {vars}(\mathcal {E})$. It is clear that $W = \text {vars}(\mathcal {E}_{|{\Omega }}) \subseteq \text {vars}(\mathcal {E}) = V$.

Assume $(x_{1},\ldots , x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n},\hat {w})$ in $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$. By Definition 10, it follows that $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\mathcal {E}$ with $p \equiv {\Delta }_{\mathcal {E}}(\sigma )$ and ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$. Note that σ ∈ Λ cannot hold, because if σ ∈ Λ, then either (i) $p \equiv {\Delta }_{\mathcal {E}}(\sigma ) \equiv \textit {false}$ in contradiction to ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$, or (ii) there exists $E = E_{k} \in \mathcal {E}$ such that σ ∈ Σ _E and $x_{k} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{k}$ in E = E _k does not hold, in contradiction to $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\mathcal {E}$ by Definition 9. Thus σ ∈ Ω and $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\mathcal {E}_{|{\Omega }} = \dot {\|}\mathcal {F}$. As also ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$ and $\text {vars}^{\prime }(p) \subseteq \text {vars}(p) \subseteq \text {vars}(\mathcal {E}_{|{\Omega }}) = W$, it follows that ${\Xi }_{W}(p)(\hat {v}_{|W},\hat {w}_{|W}) = \mathbf {T}$. Thus, by Definition 10 it holds that $(x_{1},\ldots , x_{n},\hat {v}_{|W}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n}, \hat {w}_{|W})$ in $U(\dot {\|}\mathcal {F}) = U(\mathcal {F}) = U(\mathcal {E}_{|{\Omega }})$. □

Proposition 9 (false-Removal)

Let $\mathcal {E}$ be a normalised EFSM system, and let ${\Lambda } \subseteq {\Sigma }_{\mathcal {E}}$ be a set of events such that for all λ ∈ Λ at least one of the following conditions holds:

• (i) ${\Delta }_{\mathcal {E}}(\lambda ) \equiv \textit {false}$;

• (ii) There exists $E \in \mathcal {E}$ such that λ ∈ Σ _E , but there does not exist any transition $x {{~}^{\underrightarrow {\lambda :p}}} y$ in E.

Proof

Note that $\mathcal {E}$ and thus $\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }}$ are normalised, so $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$ and $U(\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }}) = U(\dot {\|}\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }})$ by Proposition 1.

Assume $\mathcal {E}$ is nonblocking, which means that $U(\mathcal {E})$ is nonblocking. It will be shown that $U(\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }})$ is nonblocking. Let $(x\circ _{1},\ldots ,x^{\circ }_{n},\hat {v}^{\circ }) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} ({x^{1}_{1}},\ldots ,{x^{1}_{n}},\hat {v}^{1}) {~}^{\underrightarrow {\,\,\sigma _{2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{l}\,\,}}({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$ in $U(\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }}) = U(\dot {\|}\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }})$ where $(x^{\circ }_{1},\ldots ,x^{\circ }_{n}) \in Q^{\circ }_{1} \times \cdots \times Q^{\circ }_{n}$. By Lemma 16, it follows that $({x^{0}_{1}},\ldots ,{x^{0}_{n}}, \hat {v}\circ \oplus \hat {u}^{\circ }) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} ({x^{1}_{1}},\ldots ,{x^{1}_{n}}, \hat {v}^{1}\oplus \hat {u}^{\circ }) {~}^{\underrightarrow {\,\,\sigma _{2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{l}\,\,}} ({x^{l}_{1}},\ldots ,{x^{l}_{n}}, \hat {v}^{l}\oplus \hat {u}^{\circ })$ in $U(\dot {\|}\mathcal {E})$. Since $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$ is nonblocking, there exists a path $({x^{l}_{1}},\ldots ,{x^{l}_{n}}, \hat {v}^{l}\oplus \hat {u}^{\circ }) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} (x^{l+1}_{1},\ldots ,x^{l+1}_{n}, \hat {w}^{l+1}) {~}^{\underrightarrow {\,\,\sigma _{l+2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} ({x^{m}_{1}},\ldots ,{x^{m}_{n}},\hat {w}^{m})$ in $U(\dot {\|}\mathcal {E})$ such that $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. From Lemma 17 and as $(\hat {v}^{l}\oplus \hat {u}\circ )_{|W}=\hat {v}^{l}$, it follows that $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} (x^{l+1}_{1},\ldots ,x^{l+1}_{n}, \hat {w}^{l+1}_{|W}) {~}^{\underrightarrow {\,\,\sigma _{l+2}\,\,}} \cdots {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} ({x^{m}_{1}},\ldots ,{x^{m}_{n}},\hat {v}^{m}_{|W})$ in $U(\dot {\|}\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }})$ and $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. Since $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$ was chosen arbitrarily, it follows that $U(\dot {\|}\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }}) = U(\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }})$ is nonblocking, i.e., $\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }}$ is nonblocking.

Conversely assume $\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }}$ is nonblocking, which means that $U(\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }})$ is nonblocking. Let $(x^{\circ }_{1},\ldots ,x^{\circ }_{n}, \hat {v}^{\circ }) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} ({x^{1}_{1}},\ldots , {x^{1}_{n}}, \hat {v}^{1}) {~}^{\underrightarrow {\,\,\sigma _{2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{l}\,\,}} ({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$ in $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$ where $(x^{\circ }_{1},\ldots ,x^{\circ }_{n}) \in Q^{\circ }_{1} \times \cdots \times Q^{\circ }_{n}$. By Lemma 17, it holds that $(x^{\circ }_{1},\ldots ,x^{\circ }_{n},\hat {v}^{\circ }_{|W}) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} ({x^{1}_{1}},\ldots , {x^{1}_{n}},\hat {v}^{1}_{|W}) {~}^{\underrightarrow {\,\,\sigma _{2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{l}\,\,}} ({x^{l}_{1}},\ldots , {x^{l}_{n}},\hat {v}^{l}_{|W})$ in $U(\dot {\|}\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }})$. As $U(\dot {\|}\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }}) = U(\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }})$ is nonblocking, there exists a path $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}_{|W}) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} (x^{l+1}_{1},\ldots ,x^{l+1}_{n},\hat {w}^{l+1}) {~}^{\underrightarrow {\,\,\sigma _{l+2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} ({x^{m}_{1}},\ldots , {x^{m}_{n}},\hat {w}^{m})$ in $U(\dot {\|}\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }})$ such that $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. By Lemma 16, it follows that $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}) = ({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}_{|W}\oplus \hat {v}^{l}_{|V\setminus W}) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} (x^{l+1}_{1},\ldots ,x^{l+1}_{n}, \hat {w}^{l+1}\oplus \hat {v}^{l}_{|V\setminus W}) {~}^{\underrightarrow {\,\,\sigma _{l+2}\,\,}} \cdots {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} ({x^{m}_{1}},\ldots ,{x^{m}_{n}}, \hat {w}^{m}\oplus \hat {v}^{l}_{|V\setminus W})$ in $U(\dot {\|}\mathcal {E})$ and $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. As $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$ was chosen arbitrarily, it follows that $U(\dot {\|}\mathcal {E}) = U(\mathcal {E})$ is nonblocking, i.e., $\mathcal {E}$ is nonblocking. □

As selfloop removal is also defined using restriction, the proof of Proposition 10 again uses Lemma 16 to lift paths from an abstracted system to the original system. For the converse, the following Lemma 18 shows that a path in the original system also exists in the abstracted system after selfloop removal, except possibly for the deletion of some selfloops.

Lemma 18

Let $\mathcal {E} = \{E_{1},\ldots ,E_{n}\}$ be a normalised EFSM system with event alphabet ${\Sigma }_{\mathcal {E}} = {\Omega } \dot {\cup } {\Lambda }$ , which is selfloop-only for Λ. Then $(x_{1},\ldots , x_{n}, \hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n}, \hat {w})$ in $U(\mathcal {E})$ implies $(x_{1},\ldots , x_{n}, \hat {v}_{|W}) {~}^{\underrightarrow {\,\,P_{\Omega }(\sigma )\,\,}} (y_{1},\ldots , y_{n}, \hat {w}_{|W})$ in $U(\mathcal {E}_{|{\Omega }})$ where $W = \text {vars}(\mathcal {E}_{|{\Omega }})$.

Proof

Let $V = \text {vars}(\mathcal {E})$. Clearly $W = \text {vars}(\mathcal {E}_{|{\Omega }}) \subseteq \text {vars}(\mathcal {E}) = V$.

Assume that $(x_{1},\ldots , x_{n}, \hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n}, \hat {w})$ in $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$. Then by Definition 10 it holds that $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\mathcal {E}$ with $p \equiv {\Delta }_{\mathcal {E}}(\sigma )$ and ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$. By Definition 14 it holds that $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ for each i such that 1 ≤ i ≤ n and $\sigma \in {\Sigma }_{E_{i}}$, and x _i = y _i for each i such that 1 ≤ i ≤ n and $\sigma \notin {\Sigma }_{E_{i}}$. Consider two cases for σ: either σ ∈ Λ or σ ∉ Λ.

• If σ ∈ Λ then P _Ω(σ) = ε, and since each E _i is selfloop-only for σ ∈ Λ, it follows from $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ in E _i that x _i = y _i and vars′(p) = ∅. From vars′(p) = ∅ and ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$ it follows that $\hat {v} = \hat {w}$, which implies $\hat {v}_{|W}=\hat {w}_{|W}$. Given P _Ω(σ) = ε, it follows that $(x_{1},\ldots , x_{n}, \hat {v}_{|W}) {~}^{\underrightarrow {\,\,P_{\Omega }(\sigma )\,\,}} (x_{1},\ldots , x_{n}, \hat {v}_{|W}) = (y_{1},\ldots , y_{n}, \hat {w}_{|W})$ in $U(\dot {\|}\mathcal {E}_{|{\Omega }}) = U(\mathcal {E}_{|{\Omega }})$.

• If σ ∉ Λ then P _Ω(σ) = σ. In this case, it follows from $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ in E _i that $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ in E _{i |Ω}, and thus $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\mathcal {E}_{|{\Omega }}$. As this transition is in $\dot {\|}\mathcal {E}_{|{\Omega }}$, it holds that $\text {vars}^{\prime }(p) \subseteq \text {vars}(p) \subseteq \text {vars}(\dot {\|}\mathcal {E}_{|{\Omega }}) = \text {vars}(\mathcal {E}_{|{\Omega }}) = W$, so it follows from ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$ that ${\Xi }_{W}(p) (\hat {v}_{|W},\hat {w}_{|W}) = \mathbf {T}$. By Definition 10, it follows that $(x_{1},\ldots , x_{n},\hat {v}_{|W}) {~}^{\underrightarrow {\,\,P_{\Omega }(\sigma )\,\,}} (y_{1},\ldots , y_{n}, \hat {w}_{|W})$ in $U(\dot {\|}\mathcal {E}_{|{\Omega }}) = U(\mathcal {E}_{|{\Omega }})$.

□

Proposition 10 (Selfloop Removal)

Let $\mathcal {E}$ be a normalised EFSM system that is selfloop-only for ${\Lambda } \subseteq {\Sigma }_{\mathcal {E}}$ . Then $\mathcal {E}$ is nonblocking if and only if $\mathcal {E}_{|{\Sigma }_{\mathcal {E}} \setminus {\Lambda }}$ is nonblocking.

Proof

Let $\mathcal {E} = \{E_{1},\ldots ,E_{n}\}$ and ${\Omega } = {\Sigma }_{\mathcal {E}} \setminus {\Lambda }$ and $V = \text {vars}(\mathcal {E})$ and $W = \text {vars}(\mathcal {E}_{|{\Omega }})$.

Assume $\mathcal {E}$ is nonblocking, which means that $U(\mathcal {E})$ is nonblocking. It will be shown that $U(\mathcal {E}_{|{\Omega }})$ is nonblocking. Let $(x^{\circ }_{1},\ldots , x^{\circ }_{n}, \hat {v}^{\circ }) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} ({x^{1}_{1}},\ldots , {x^{1}_{n}}, \hat {v}^{1}) {~}^{\underrightarrow {\,\,\sigma _{2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{l}\,\,}} ({x^{l}_{1}},\ldots , {x^{l}_{n}}, \hat {v}^{l})$ in $U(\mathcal {E}_{|{\Omega }}) = U(\dot {\|}\mathcal {E}_{|{\Omega }})$ where $(x^{\circ }_{1},\ldots , x^{\circ }_{n}) \in Q^{\circ }_{1} \times \cdots \times Q^{\circ }_{n}$. By Lemma 16, it follows that $({x^{0}_{1}},\ldots ,{x^{0}_{n}}, \hat {v}\circ \oplus \hat {u}^{\circ }) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} ({x^{1}_{1}},\ldots ,{x^{1}_{n}}, \hat {v}^{1}\oplus \hat {u}^{\circ }) {~}^{\underrightarrow {\,\,\sigma _{2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{l}\,\,}} ({x^{l}_{1}},\ldots ,{x^{l}_{n}}, \hat {v}^{l}\oplus \hat {u}^{\circ })$ in $U(\dot {\|}\mathcal {E})$. Since $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$ is nonblocking, there exists a path $({x^{l}_{1}},\ldots ,{x^{l}_{n}}, \hat {v}^{l}\oplus \hat {u}^{\circ }) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} (x^{l+1}_{1},\ldots ,x^{l+1}_{n}, \hat {w}^{l+1}) {~}^{\underrightarrow {\,\,\sigma _{l+2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} ({x^{m}_{1}},\ldots ,{x^{m}_{n}},\hat {w}^{m})$ in $U(\dot {\|}\mathcal {E})$ such that $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. From Lemma 18 and since $(\hat {v}^{l}\oplus \hat {u}^{\circ })_{|W}=\hat {v}^{l}$, it follows that $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}) {~}^{\underrightarrow {\,\,P_{\Omega }(\sigma _{l+1})\,\,}} (x^{l+1}_{1},\ldots ,x^{l+1}_{n}, \hat {w}^{l+1}_{|W}) {~}^{\underrightarrow {\,\,P_{\Omega }(\sigma _{l+2})\,\,}} {\cdots } {~}^{\underrightarrow {\,\,P_{\Omega }(\sigma _{m})\,\,}} ({x^{m}_{1}},\ldots ,{x^{m}_{n}},\hat {v}^{m}_{|W})$ in $U(\dot {\|}\mathcal {E}_{|{\Omega }})$ and $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. Since $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$ was chosen arbitrarily, it follows that $U(\dot {\|}\mathcal {E}_{|{\Omega }}) = U(\mathcal {E}_{|{\Omega }})$ is nonblocking, i.e., $\mathcal {E}_{|{\Omega }}$ is nonblocking.

Conversely assume $\mathcal {E}_{|{\Omega }}$ is nonblocking, which means that $U(\mathcal {E}_{|{\Omega }})$ is nonblocking.Let$(x^{\circ }_{1},\ldots , x^{\circ }_{n}, \hat {v}^{\circ }) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} ({x^{1}_{1}},\ldots , {x^{1}_{n}}, \hat {v}^{1}) {~}^{\underrightarrow {\,\,\sigma _{2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{l}\,\,}} ({x^{l}_{1}},\ldots , {x^{l}_{n}}, \hat {v}^{l})$ in $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$ where $(x\circ _{1},\ldots , x\circ _{n}) \in Q^{\circ }_{1} \times \cdots \times Q^{\circ }_{n}$. By Lemma 18, it holds that $(x^{\circ }_{1},\ldots , x^{\circ }_{n}, \hat {v}^{\circ }_{|W}) {~}^{\underrightarrow {\,\,P_{\Omega }(\sigma _{1})\,\,}} ({x^{1}_{1}},\ldots , {x^{1}_{n}},\hat {v}^{1}_{|W}) {~}^{\underrightarrow {\,\,P_{\Omega }(\sigma _{2})\,\,}} \cdots {~}^{\underrightarrow {\,\,P_{\Omega }(\sigma _{l})\,\,}} ({x^{l}_{1}},\ldots , {x^{l}_{n}},\hat {v}^{l}_{|W})$ in $U(\dot {\|}\mathcal {E}_{|{\Omega }})$. Since $U(\dot {\|}\mathcal {E}_{|{\Omega }}) = U(\mathcal {E}_{|{\Omega }})$ is nonblocking, there exists a path $({x^{l}_{1}},\ldots , {x^{l}_{n}}, \hat {v}^{l}_{|W}) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} (x^{l+1}_{1},\ldots , x^{l+1}_{n}, \hat {w}^{l+1}) {~}^{\underrightarrow {\,\,\sigma _{l+2}\,\,}} \cdots {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} ({x^{m}_{1}},\ldots , {x^{m}_{n}},\hat {w}^{m})$ in $U(\dot {\|}\mathcal {E}_{|{\Omega }})$ such that $({x^{m}_{1}},\ldots , {x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. By Lemma 16, it follows that $({x^{l}_{1}},\ldots , {x^{l}_{n}},\hat {v}^{l}) \!\!\!\!\!\!\,=\,\!\!\!\!\!\! ({x^{l}_{1}},\ldots , {x^{l}_{n}},\hat {v}^{l}_{|W}\oplus \hat {v}^{l}_{|V\setminus W}) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} (x^{l+1}_{1},\ldots ,x^{l+1}_{n}, \hat {w}^{l+1}\oplus \hat {v}^{l}_{|V\setminus W}) {~}^{\underrightarrow {\,\,\sigma _{l+2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} ({x^{m}_{1}},\ldots ,{x^{m}_{n}}, \hat {w}^{m}\oplus \hat {v}^{l}_{|V\setminus W})$ in $U(\dot {\|}\mathcal {E})$ and $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. As $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$ was chosen arbitrarily, it follows that $U(\dot {\|}\mathcal {E}) = U(\mathcal {E})$ is nonblocking, i.e., $\mathcal {E}$ is nonblocking. □

The next result to prove is Proposition 11, which states that the nonblocking property of an EFSM system is preserved by event merging. Again, it needs to be established that for each path in the EFSM system before abstraction there exists a corresponding path after abstraction, and vice versa. First, Lemma 19 shows that every path in an EFSM system can be found again after renaming, and afterwards Lemma 20 shows how to lift a path from the abstracted system after event merging back to the original system.

Lemma 19

Let $\mathcal {E} = \{E_{1},\ldots ,E_{n}\}$ be an EFSM system, and let $\rho \colon {\Sigma }_{\mathcal {E}} \to {\Sigma }^{\prime }$ be an arbitrary renaming. Then $(x_{1},\ldots ,x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\mathcal {E})$ implies $(x_{1},\ldots ,x_{n},\hat {v}) {~}^{\underrightarrow {\,\,\rho (\sigma )\,\,}} (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\rho (\mathcal {E}))$.

Proof

Write V = vars(E) and ${\Sigma }_{i} = {\Sigma }_{E_{i}}$ for 1 ≤ i ≤ n. Assume $(x_{1},\ldots ,x_{n},\hat {v})\overset {\sigma }{\rightarrow }(y_{1},\ldots ,y_{n},\hat {w})$ in $U(\mathcal {E})$. By Definition 10, this means $(x_{1},\ldots ,x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},\ldots ,y_{n})$ in $||\mathcal {E}$ where ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$. By Definition 9, it holds that $x_{i} {~}^{\underrightarrow {\,\,\sigma :p_{i}\,\,}} y_{i}$ for each E _i such that σ ∈ Σ _i , and x _i = y _i for each E _i such that σ ∉ Σ _i , and $p \equiv \bigwedge _{\sigma \in {\Sigma }_{i}} p_{i}$. For σ ∈ Σ _i it follows that $x_{i} {~}^{\underrightarrow {\,\,\rho (\sigma ):p_{i}\,\,}} y_{i}$ in ρ(E _i ), and therefore $(x_{1},\ldots ,x_{n}) {~}^{\underrightarrow {\rho (\sigma ):p}} (y_{1},\ldots ,y_{n})$ in $||\rho (\mathcal {E})$. As ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$ and $\text {vars}(\rho (\mathcal {E})) = \text {vars}(\mathcal {E}) = V$, it follows by Definition 10 that $(x_{1},\ldots ,x_{n},\hat {v}){~}^{\underrightarrow {\,\,\rho (\sigma )\,\,}}(y_{1},\ldots ,y_{n},\hat {w})$ in $U(\rho (\mathcal {E}))$. □

Lemma 20

Let $\mathcal {E} = \{E_{1},\ldots , E_{n}\}$ be a normalised EFSM system with $E_{i}=\langle {\Sigma }_{i},Q_{i},\to _{i},Q^{\circ }_{\omega },Q^{\omega }_{i}\rangle$ , let $E_{k} \in \mathcal {E}$ , and let $\rho \colon {\Sigma }_{\mathcal {E}} \to {\Sigma }^{\prime }$ be a renaming such that the following conditions hold for all $\sigma _{1},\sigma _{2} \in {\Sigma }_{\mathcal {E}}$ with ρ(σ ₁ ) = ρ(σ ₂):

• (i) ${\Delta }_{\mathcal {E}}(\sigma _{1}) = {\Delta }_{\mathcal {E}}(\sigma _{2})$;

• (ii) for all i ≠ k, it holds that σ ₁ ∈ Σ _i if and only if σ ₂ ∈ Σ _i , and for all x,y ∈ Q _i it holds that $x {{~}^{\underrightarrow {\sigma _{1}:{\Delta }_{\mathcal {E}}(\sigma _{1})}}}_{i} y$ if and only if $x {{~}^{\underrightarrow {\sigma _{2}:{\Delta }_{\mathcal {E}}(\sigma _{2})}}}_{i} y$.

Then $(x_{1},\ldots ,x_{n},\hat {v}) {~}^{\underrightarrow {\mu }} (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\rho (\mathcal {E}))$ implies $(x_{1},\ldots ,x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\mathcal {E})$ for some $\sigma \in {\Sigma }_{\mathcal {E}}$ such that ρ(σ) = μ.

Proof

First note that $\mathcal {E}$ is normalised, which implies by assumption (i) that $\rho (\mathcal {E})$ is normalised. Therefore, it holds by Proposition 1 that $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$ and $U(\rho (\mathcal {E})) = U(\dot {\|}\rho (\mathcal {E}))$.

Assume $(x_{1},\ldots ,x_{n},\hat {v}) {~}^{\underrightarrow {\mu }} (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\rho (\mathcal {E})) = U(\dot {\|}\rho (\mathcal {E}))$. Then it holds by Definition 10 that $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\,\,\mu :p\,\,}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\rho (\mathcal {E})$ where $p \equiv {\Delta }_{\rho (\mathcal {E})}(\mu )$ and ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$ where $V = \text {vars}(\rho (\mathcal {E})) = \text {vars}(\mathcal {E})$. Consider two cases: either μ ∈ ρ(Σ _k ) or μ ∉ ρ(Σ _k ).

• If μ ∈ ρ(Σ _k ), then $x_{k} {~}^{\underrightarrow {\,\,\mu :p\,\,}} y_{k}$ in ρ(E _k ) by Definition 14. Then there exists σ ∈ Σ _k such that ρ(σ) = μ and $x_{k} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{k}$ in E _k .

• If μ ∉ ρ(Σ _k ), then x _k = y _k by Definition 14. As ρ is surjective by Definition 15, there exists $\sigma \in {\Sigma }_{\mathcal {E}}$ such that ρ(σ) = μ. Note that σ ∉ Σ _k as otherwise μ = ρ(σ) ∈ ρ(Σ _k ).

In both cases there exists $\sigma \in {\Sigma }_{\mathcal {E}}$ with ρ(σ) = μ, with other properties mentioned in each case. Now consider two cases for each i ≠ k: either σ ∈ Σ _i or σ ∉ Σ _i .

• If σ ∈ Σ _i , then μ = ρ(σ) ∈ ρ(Σ _i ) and thus $x_{i} {~}^{\underrightarrow {\,\,\mu :p\,\,}} y_{i}$ in ρ(E _i ) by Definition 14. Then there exists σ _i ∈ Σ _i such that ρ(σ _i ) = μ and $x_{i} {~}^{\underrightarrow {\,\,\sigma _{i}:p\,\,}} y_{i}$ in E _i . As i ≠ k and ρ(σ _i ) = μ = ρ(σ), it follows by assumption (ii) that σ ∈ Σ _i and $x_{i} {~}^{\underrightarrow {\;\;\sigma :p\;\;}} y_{i}$ in E _i .

• If σ ∉ Σ _i , then μ = ρ(σ) ∉ ρ(Σ _i ) and thus x _i = y _i by Definition 14.

Combining the above observations for k and all i ≠ k, it follows by Definition 14 that $(x_{1},\ldots ,x_{n}) {~}^{\underrightarrow {\;\;\sigma :p\;\;}} (y_{1},\ldots ,y_{n})$ in $\dot {\|}\mathcal {E}$. As furthermore ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$, it follows by Definition 10 that $(x_{1},\ldots ,x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\dot {\|}\mathcal {E}) = U(\mathcal {E})$. □

Proposition 11 (Event Merging)

Let $\mathcal {E} = \{E_{1},\ldots , E_{n}\}$ be a normalised EFSM system with $E_{i}=\langle {\Sigma }_{i},Q_{i},\to _{i},Q^{\circ }_{\omega },Q^{\omega }_{i}\rangle$ , let $E_{k} \in \mathcal {E}$ , and let $\rho \colon {\Sigma }_{\mathcal {E}} \to {\Sigma }^{\prime }$ be a renaming such that the following conditions hold for all $\sigma _{1},\sigma _{2} \in {\Sigma }_{\mathcal {E}}$ with ρ(σ ₁ ) = ρ(σ ₂):

• (i) ${\Delta }_{\mathcal {E}}(\sigma _{1}) = {\Delta }_{\mathcal {E}}(\sigma _{2})$;

• (ii) for all i ≠ k, it holds that σ ₁ ∈ Σ _i if and only if σ ₂ ∈ Σ _i , and for all x,y ∈ Q _i it holds that $x {{~}^{\underrightarrow {\sigma _{1}:{\Delta }_{\mathcal {E}}(\sigma _{1})}}}_{i} y$ if and only if $x {{~}^{\underrightarrow {\sigma _{2}:{\Delta }_{\mathcal {E}}(\sigma _{2})}}}_{i} y$.

Then $\mathcal {E}$ is nonblocking if and only if $\rho (\mathcal {E})$ is nonblocking.

Proof

First assume $\mathcal {E}$ is nonblocking, which means that $U(\mathcal {E})$ is nonblocking. It will be shown that $\mathcal {E}$ is nonblocking. Let $U(\rho (\mathcal {E})) {~}^{\underrightarrow {\mu _{1}}} ({x^{1}_{1}},\ldots ,{x^{1}_{n}},\hat {v}^{1}) {~}^{\underrightarrow {\mu _{2}}} \cdots {~}^{\underrightarrow {\mu _{l}}}({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$. By Lemma 20, there exist events σ ₁, … , σ _l such that $U(\mathcal {E}) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} ({x^{1}_{1}},\ldots ,{x^{1}_{n}},\hat {v}^{1}) {~}^{\underrightarrow {\,\,\sigma _{2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{l}\,\,}} ({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$. Since $U(\mathcal {E})$ is nonblocking, there exists a path $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} {\cdots } {~}^{\underrightarrow {\;\;\sigma _{m}\;\;}} ({x^{m}_{1}},\ldots ,{x^{m}_{n}},\hat {v}^{m})$ in $U(\mathcal {E})$ such that $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }[1] \times \cdots \times Q^{\omega }[n]$. From Lemma 19, it follows that $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}) {~}^{\underrightarrow {\;\;\rho (\sigma _{l+1})\;\;}} {\cdots } {~}^{\underrightarrow {\,\,\rho (\sigma _{m})\,\,}} ({x^{m}_{1}},\ldots ,{x^{m}_{n}},\hat {v}^{m})$ in $U(\rho (\mathcal {E}))$ and $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. Since $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$ was chosen arbitrarily, it follows that $U(\rho (\mathcal {E}))$ is nonblocking, i.e., $\mathcal {E}$ is nonblocking.

Conversely assume $\mathcal {F}$ is nonblocking, which means that $U(\mathcal {F})$ is nonblocking. Let $U(\mathcal {E}) {~}^{\underrightarrow {\,\,\sigma _{1}\,\,}} ({x^{1}_{1}},\ldots , {x^{1}_{n}}, \hat {v}^{1}) {~}^{\underrightarrow {\,\,\sigma _{2}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{l}\,\,}} ({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$. By Lemma 19, it holds that $U(\mathcal {F}) {~}^{\underrightarrow {\,\,\rho (\sigma _{1})\,\,}} ({x^{1}_{1}},\ldots , {x^{1}_{n}},\hat {v}^{1}) {~}^{\underrightarrow {\,\,\rho (\sigma _{2})\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\rho (\sigma _{l})\,\,}} ({x^{l}_{1}},\ldots , {x^{l}_{n}},\hat {v}^{l})$. As $U(\mathcal {F})$ is nonblocking, there exists a path $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}) {~}^{\underrightarrow {\,\,\mu _{l+1}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\mu _{m}\,\,}} ({x^{m}_{1}},\ldots , {x^{m}_{n}},\hat {v}^{m})$ in $U(\mathcal {F})$ such that $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. By Lemma 20, there exist events σ ₁₊₁, … , σ _m such that $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}) {~}^{\underrightarrow {\,\,\sigma _{l+1}\,\,}} {\cdots } {~}^{\underrightarrow {\,\,\sigma _{m}\,\,}} ({x^{m}_{1}},\ldots ,{x^{m}_{n}},\hat {v}^{m})$ in $U(\mathcal {E})$ and $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. As $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$ was chosen arbitrarily, it follows that $U(\mathcal {E})$ is nonblocking, i.e., $\mathcal {E}$ is nonblocking. □

Similar to event merging, to prove that update merging preserves the nonblocking property of an EFSM system as stated in Proposition 12, the relationship between the paths in the system before and after abstraction is first established. Lemma 21 shows how to construct a path in the abstracted system after update merging from a path in the original system, and Lemma 22 shows how to do the converse.

Lemma 21

Let $\mathcal {E}\hspace *{-3pt} \!\!\,=\,\!\!\hspace *{-3pt} \{E_{1},\ldots ,\hspace *{-3pt} E_{n}\}$ beanormalisedEFSMsystemwith $E_{i} = \langle {\Sigma }_{i},Q_{i},\to _{i},Q^{\circ }_{\omega },Q^{\omega }_{i}\rangle$ . Let ρ be a renaming such that the following conditions hold for all $\sigma _{1},\sigma _{2} \in {\Sigma }_{\mathcal {E}}$ with ρ(σ ₁ ) = ρ(σ ₂):

• (i) $\text {vars}^{\prime }({\Delta }_{\mathcal {E}}(\sigma _{1})) = \text {vars}^{\prime }({\Delta }_{\mathcal {E}}(\sigma _{2}))$,

• (ii) for all i = 1, … , n it holds that σ ₁ ∈ Σ _i if and only if σ ₂ ∈ Σ _i , and for all x,y ∈ Q _i it holds that $x {{~}^{\underrightarrow {{\sigma _{1}:{\Delta }_{\mathcal {E}}(\sigma _{1})}}}}_{i} y$ if and only if $x {{~}^{\underrightarrow {\sigma _{2}:{\Delta }_{\mathcal {E}}(\sigma _{2})}}}_{i} y$

Further let $\mathcal {F}=\{F_{1},\ldots , F_{n}\}$ such that $F_{i} = \langle \rho ({\Sigma }_{i}), Q_{i}, {\to _{i}^{F}} , Q^{\circ }_{i}, Q^{\omega }_{i}\rangle$ where ${\to _{i}^{F}} =\, \{ (x,\rho (\sigma ), {\Delta }_{\mathcal {F}}(\rho (\sigma )), y) \mid x {~}^{\underrightarrow {\sigma :{\Delta }_{\mathcal {E}}(\sigma )}} y \,\}$ and ${\Delta }_{\mathcal {F}}(\mu ) \equiv \bigvee _{\sigma \in \rho ^{-1}(\mu )} {\Delta }_{\mathcal {E}}(\sigma )$ for all $\mu \in {\Sigma }_{\mathcal {F}}$ . Then $(x_{1},\ldots , x_{n}, \hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots , y_{n}, \hat {w})$ in $U(\mathcal {E})$ implies $(x_{1},\ldots , x_{n}, \hat {v}) {~}^{\underrightarrow {\,\,\rho (\sigma )\,\,}} (y_{1},\ldots , y_{n}, \hat {w})$ in $U(\mathcal {F})$.

Proof

Note that $\mathcal {E}$ and $\mathcal {F}$ are normalised, so $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$ and $U(\mathcal {F}) = U(\dot {\|}\mathcal {F})$ by Proposition 1.

Let $(x_{1},\ldots ,x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$. This means by Definition 10 that $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}}(\sigma )\,\,}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\mathcal {E}$ and ${\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma ))(\hat {v},\hat {w}) = \mathbf {T}$ where $V = \text {vars}(\mathcal {E}) = \text {vars}(\mathcal {F})$. Consider two cases for each E _i : either σ ∈ Σ _i or σ ∉ Σ _i .

• If σ ∈ Σ _i , then it follows by Definition 14 that $x_{i} {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}}(\sigma )\,\,}} y_{i}$ in E _i . In this case, ρ(σ) ∈ ρ(Σ _i ), and it follows by construction of ${\to _{i}^{F}}$ that $x_{i} {~}^{\underrightarrow {\,\,\rho (\sigma ):{\Delta }_{\mathcal {F}}(\sigma )\,\,}} y_{i}$ in F _i .

• If σ ∉ Σ _i then x _i = y _i by Definition 14, and ρ(σ) ∉ ρ(Σ _i ).

Combining these observations for all i, it follows by Definition 14 that $(x_{1},\ldots ,x_{n}) {~}^{\underrightarrow {\,\,\rho (\sigma ):{\Delta }_{\mathcal {F}}(\rho (\sigma ))\,\,}} (y_{1},\ldots ,y_{n})$ in $F_{1} \dot {\|} {\cdots } \dot {\|} F_{n} = \dot {\|}\mathcal {F}$. Furthermore, note that by construction ${\Delta }_{\mathcal {F}}(\rho (\sigma )) = \bigvee _{\sigma ^{\prime } \in \rho ^{-1}(\rho (\sigma ))} {\Delta }_{\mathcal {E}}(\sigma ^{\prime })$, which implies ${\Xi }_{V}({\Delta }_{\mathcal {F}}(\rho (\sigma ))) \Leftrightarrow \bigvee _{\sigma ^{\prime } \in \rho ^{-1}(\rho (\sigma ))} {\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma ^{\prime }))$ by assumption (i). Then it follows from σ ∈ ρ ⁻¹(ρ(σ)) and ${\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma ))(\hat {v},\hat {w}) = \mathbf {T}$ that ${\Xi }_{V}({\Delta }_{\mathcal {F}}(\rho (\sigma )))(\hat {v},\hat {w}) = \mathbf {T}$. Then it follows from Definition 10 that $(x_{1},\ldots ,x_{n},\hat {v}) {~}^{\underrightarrow {\,\,\rho (\sigma )\,\,}} (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\dot {\|}\mathcal {F}) = U(\mathcal {F})$. □

Lemma 22

Let $\mathcal {E} = \{E_{1},\ldots , E_{n}\}$ be a normalised EFSM system with $E_{i} = \langle {\Sigma }_{i},Q_{i},\to _{i},Q^{\circ }_{\omega },Q^{\omega }_{i}\rangle$ . Let ρ be a renaming such that the following conditions hold for all $\sigma _{1},\sigma _{2} \in {\Sigma }_{\mathcal {E}}$ with ρ(σ ₁ ) = ρ(σ ₂):

• (i) $\text {vars}^{\prime }({\Delta }_{\mathcal {E}}(\sigma _{1})) = \text {vars}^{\prime }({\Delta }_{\mathcal {E}}(\sigma _{2}))$,

• (ii) for all i = 1, … , n it holds that σ ₁ ∈ Σ _i if and only if σ ₂ ∈ Σ _i , and for all x,y ∈ Q _i it holds that $x {{~}^{\underrightarrow {{\sigma _{1}:{\Delta }_{\mathcal {E}}(\sigma _{1})}}}}_{i} y$ if and only if $x {{~}^{\underrightarrow {\sigma _{2}:{\Delta }_{\mathcal {E}}(\sigma _{2})}}}_{i} y$

Further let $\mathcal {F}=\{F_{1},\ldots , F_{n}\}$ such that $F_{i} = \langle \rho ({\Sigma }_{i}), Q_{i}, {\to _{i}^{F}} , Q^{\circ }_{i}, Q^{\omega }_{i}\rangle$ where ${\to _{i}^{F}} =\, \{ (x,\rho (\sigma ), {\Delta }_{\mathcal {F}}(\rho (\sigma )), y) \mid x {~}^{\underrightarrow {\sigma :{\Delta }_{\mathcal {E}}(\sigma )}} y \,\}$ and ${\Delta }_{\mathcal {F}}(\mu ) \equiv \bigvee _{\sigma \in \rho ^{-1}(\mu )} {\Delta }_{\mathcal {E}}(\sigma )$ for all $\mu \in {\Sigma }_{\mathcal {F}}$ . Then $(x_{1},\ldots ,x_{n},\hat {v}) {~}^{\underrightarrow {\mu }} (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\mathcal {F})$ implies $(x_{1},\ldots ,x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\mathcal {E})$ for some $\sigma \in {\Sigma }_{\mathcal {E}}$ such that ρ(σ) = μ.

Proof

Note that $\mathcal {E}$ and $\mathcal {F}$ are normalised, so $U(\mathcal {E}) = U(\dot {\|}\mathcal {E})$ and $U(\mathcal {F}) = U(\dot {\|}\mathcal {F})$ by Proposition 1.

Assume $(x_{1},\ldots ,x_{n},\hat {v}) {~}^{\underrightarrow {\mu }} (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\mathcal {F}) = U(\dot {\|}\mathcal {F})$. Then it holds that by Definition 10 that $(x_{1},\ldots , x_{n}) {~}^{\underrightarrow {\,\,\mu :p\,\,}} (y_{1},\ldots , y_{n})$ in $\dot {\|}\mathcal {F}$ where $p \equiv {\Delta }_{\mathcal {F}}(\mu ) \equiv \bigvee _{\sigma \in \rho ^{-1}(\mu )}{\Delta }_{\mathcal {E}}(\sigma )$, and ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$ where $V = \text {vars}(\mathcal {F})$. As $p \equiv \bigvee _{\sigma \in \rho ^{-1}(\mu )}{\Delta }_{\mathcal {E}}(\sigma )$ and ${\Xi }_{V}(p)(\hat {v},\hat {w}) = \mathbf {T}$, there exists σ ∈ ρ ⁻¹(μ) such that ${\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma ))(\hat {v},\hat {w}) = \mathbf {T}$. Note, as σ ∈ ρ ⁻¹(μ) it holds that ρ(σ) = μ. Consider two cases for each E _i : either σ ∈ Σ _i or σ ∉ Σ _i .

• If σ ∈ Σ _i then μ = ρ(σ) ∈ ρ(Σ _i ), which by Definition 14 implies $x_{i} {~}^{\underrightarrow {\,\,\mu :p\,\,}} y_{i}$ in F _i . By construction of ${\to ^{F}_{i}}$, this means $x_{i} {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}}(\sigma )\,\,}} y_{i}$ in E _i .

• If σ ∉ Σ _i , then μ ∉ ρ(Σ _i ) and x _i = y _i by Definition 14.

Combining the above observations for all i, it follows by Definition 14 that $(x_{1},\ldots ,x_{n}) {~}^{\underrightarrow {\,\,\sigma :{\Delta }_{\mathcal {E}}(\sigma )\,\,}} (y_{1},\ldots ,y_{n})$ in $\dot {\|}\mathcal {E}$. As ${\Xi }_{V}({\Delta }_{\mathcal {E}}(\sigma ))(\hat {v},\hat {w}) = \mathbf {T}$, it follows that $(x_{1},\ldots ,x_{n},\hat {v}) \overset {\sigma }{\rightarrow } (y_{1},\ldots ,y_{n},\hat {w})$ in $U(\dot {\|}\mathcal {E}) = U(\mathcal {E})$. □

Proposition 12 (Update Merging)

Let $\mathcal {E} = \{E_{1},\ldots , E_{n}\}$ be a normalised EFSM system with $E_{i} = \langle {\Sigma }_{i},Q_{i},\to _{i},Q^{\circ }_{\omega },Q^{\omega }_{i}\rangle$ . Let ρ be a renaming such that the following conditions hold for all $\sigma _{1},\sigma _{2} \in {\Sigma }_{\mathcal {E}}$ with ρ(σ ₁ ) = ρ(σ ₂):

• (i) $\text {vars}^{\prime }({\Delta }_{\mathcal {E}}(\sigma _{1})) = \text {vars}^{\prime }({\Delta }_{\mathcal {E}}(\sigma _{2}))$,

• (ii) for all i = 1, … , n it holds that σ ₁ ∈ Σ _i if and only if σ ₂ ∈ Σ _i , and for all x,y ∈ Q _i it holds that $x {{~}^{\underrightarrow {{\sigma _{1}:{\Delta }_{\mathcal {E}}(\sigma _{1})}}}}_{i} y$ if and only if $x {{~}^{\underrightarrow {\sigma _{2}:{\Delta }_{\mathcal {E}}(\sigma _{2})}}}_{i} y$

Further let $\mathcal {F}=\{F_{1},\ldots , F_{n}\}$ such that $F_{i} = \langle \rho ({\Sigma }_{i}), Q_{i}, {\to _{i}^{F}} , Q^{\circ }_{i}, Q^{\omega }_{i}\rangle$ where ${\to _{i}^{F}} =\, \{ (x,\rho (\sigma ), {\Delta }_{\mathcal {F}}(\rho (\sigma )), y) \mid x {~}^{\underrightarrow {\sigma :{\Delta }_{\mathcal {E}}(\sigma )}} y \,\}$ and ${\Delta }_{\mathcal {F}}(\mu ) \equiv \bigvee _{\sigma \in \rho ^{-1}(\mu )} {\Delta }_{\mathcal {E}}(\sigma )$ for all $\mu \in {\Sigma }_{\mathcal {F}}$ . Then $\mathcal {E}$ is nonblocking if and only if $\mathcal {F}$ is nonblocking.

Proof

First assume $\mathcal {E}$ is nonblocking, which means that $U(\mathcal {E})$ is nonblocking. It will be shown that $\mathcal {F}$ is nonblocking. Let $U(\mathcal {F}) {~}^{\underrightarrow {\mu _{1}}} ({x^{1}_{1}},\ldots ,{x^{1}_{n}},\hat {v}^{1}) {~}^{\underrightarrow {\mu _{2}}} \cdots {~}^{\underrightarrow {\mu _{1}}}({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$. By Lemma 22, there exist events σ ₁, … , σ _l such that $U(\mathcal {E}) {~}^{\underrightarrow {\sigma _{1}}} ({x^{1}_{1}},\ldots ,{x^{1}_{n}},\hat {v}^{1}) {~}^{\underrightarrow {\sigma _{2}}} {\cdots } {~}^{underrightarrow{\sigma _{l}}} ({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$. Since $U(\mathcal {E})$ is nonblocking, there exists a path $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}) {~}^{\underrightarrow {\sigma _{l+1}}} {\cdots } {~}^{\underrightarrow {\sigma _{m}}} ({x^{m}_{1}},\ldots ,{x^{m}_{n}},\hat {v}^{m})$ in $U(\mathcal {E})$ such that $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. From Lemma 21, it follows that $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}) {~}^{\underrightarrow {\rho (\sigma _{l+1})}} {\cdots } {~}^{\underrightarrow {\rho (\sigma _{m})}} ({x^{m}_{1}},\ldots ,{x^{m}_{n}},\hat {v}^{m})$ in $U(\mathcal {F})$ and $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. Since $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$ was chosen arbitrarily, it follows that $U(\mathcal {F})$ is nonblocking, i.e., $\mathcal {F}$ is nonblocking.

Conversely assume $\mathcal {F}$ is nonblocking, which means that $U(\mathcal {F})$ is nonblocking. Let $U(\mathcal {E}) {~}^{\underrightarrow {\sigma _{1}}} ({x^{1}_{1}},\ldots , {x^{1}_{n}}, \hat {v}^{1}) {~}^{\underrightarrow {\sigma _{2}}} {\cdots } {~}^{\underrightarrow {\sigma _{l}}} ({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$. By Lemma 21, it holds that $U(\mathcal {F}) {~}^{\underrightarrow {\rho (\sigma _{1})}} ({x^{1}_{1}},\ldots , {x^{1}_{n}},\hat {v}^{1}) {~}^{\underrightarrow {\rho (\sigma _{2})}} {\cdots } {~}^{\underrightarrow {\rho (\sigma _{l})}} ({x^{l}_{1}},\ldots , {x^{l}_{n}},\hat {v}^{l})$. As $U(\mathcal {F})$ is nonblocking, there exists a path $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}) {~}^{\underrightarrow {\mu _{l+1}}} {\cdots } {~}^{\underrightarrow {\mu _{m}}} ({x^{m}_{1}},\ldots , {x^{m}_{n}},\hat {v}^{m})$ in $U(\mathcal {F})$ such that $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. By Lemma 22, there exist events σ ₁₊₁, … , σ _m such that $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l}) {~}^{\underrightarrow {\sigma _{l+1}}} {\cdots } {~}^{\underrightarrow {\sigma _{m}}} ({x^{m}_{1}},\ldots ,{x^{m}_{n}},\hat {v}^{m})$ in $U(\mathcal {E})$ and $({x^{m}_{1}},\ldots ,{x^{m}_{n}}) \in Q^{\omega }_{1} \times \cdots \times Q^{\omega }_{n}$. As $({x^{l}_{1}},\ldots ,{x^{l}_{n}},\hat {v}^{l})$ was chosen arbitrarily, it follows that $U(\mathcal {E})$ is nonblocking, i.e., $\mathcal {E}$ is nonblocking. □