Model abstraction for discrete-event systems by binary linear programming with applications to manufacturing systems

Abstract

Model abstraction for finite state automata is helpful for decreasing computational complexity and improving comprehensibility for the verification and control synthesis of discrete-event systems (DES). Supremal quasi-congruence equivalence is an effective method for reducing the state space of DES and its effective algorithms based on graph theory have been developed. In this paper, a new method is proposed to convert the supremal quasi-congruence computation into a binary linear programming problem which can be solved by many powerful integer linear programming and satisfiability (SAT) solvers. Partitioning states to cosets is considered as allocating states to an unknown number of cosets and the requirement of finding the coarsest quasi-congruence is equivalent to using the least number of cosets. The novelty of this paper is to solve the optimal partitioning problem as an optimal state-to-coset allocation problem. The task of finding the coarsest quasi-congruence is equivalent to the objective of finding the least number of cosets. Then the problem can be solved by optimization methods, which are respectively implemented by mixed integer linear programming (MILP) in MATLAB and binary linear programming (BLP) in CPLEX. To reduce the computation time, the translation process is first optimized by introducing fewer decision variables and simplifying constraints in the programming problem. Second, the translation process formulates a few techniques of converting logic constraints on finite automata into binary linear constraints. These techniques will be helpful for other researchers exploiting integer linear programming and SAT solvers for solving partitioning or grouping problems. Third, the computational efficiency and correctness of the proposed method are verified by two different solvers. The proposed model abstraction approach is applied to simplify the large-scale supervisor model of a manufacturing system with five automated guided vehicles. The proposed method is not only a new solution for the coarsest quasi-congruence computation, but also provides us a more intuitive understanding of the quasi-congruence relation in the supervisory control theory. A future research direction is to apply more computationally efficient solvers to compute the optimal state-to-coset allocation problem.

Introduction

Discrete-event (dynamic) systems are a typical class of computer-integrated man-made system with discrete state spaces and event-driven characteristics. They can be modeled by a state-transition structure such as deterministic or non-deterministic finite automata (DFAs or NFAs) and Petri nets. Both formalisms are used for designing supervisory controllers of a DES.^1–5 On the one hand, the supervisory control theory developed in Wonham and Cai, ¹ Ramadge and Wonham ³ is regarded as a seminal work for the treatment of supervisor synthesis for a DES such that the closed-loop behavior is observable,^6,7 controllable, nonblocking, ⁸ and maximally permissive. On the other hand, a Petri net (PN) is also a common mathematical tool for modeling and analyzing a DES, which often avoids explicit state exploration but derives certain network properties through the net structure.^9–14 Both methods are popular for synthesizing satisfactory supervisors.

Due to the theoretical maturity, DES have received much attention from academy and industry communities.^15–22 However, DES control methods have not yet been extensively applied to industrial scale problems, owing to the state explosion problem: the number of reachable states increases exponentially with that of concurrent components and variables. ²³ The intractable number of states may quickly deplete the computer memory and terminate the computation if the given system is structurally complex. Therefore, effectively exploring the huge state space with limited memory and time is a significant and persistent research subject.

To tackle the state explosion problem, many reduction methods have been developed, including equivalence reduction^24,25 and process equivalence, ²⁶ model abstraction, ²⁷ symbolic computation and state tree structures,^28,29 and partial order reduction, ³⁰ which all benefit from the proper design and analysis of the system architecture.

Model abstraction based on equivalence relations is an efficient way to reduce the state size of finite state automata. An equivalence relation on the state set of a finite state automaton partitions the state set as a collection of equivalence classes (or cosets). The set of cosets defines a simpler finite state automaton with fewer states, which is called the quotient automaton^31,32 of the original one with respect to the equivalence relation. In many applications, the observable language of the quotient automaton must be equivalent to the original automaton. The identity implies that if two states of the original automaton are equivalent, the same observable event sequences must be defined at both states. This property is guaranteed by the quasi-congruence equivalence, ¹ which is similar to the concept of bi-simulation. ³³

It is necessary to thoroughly investigate the results on the quasi-congruence relation of DES in references,^1,2,34,35 and use them to effectively reduce the computational complexity of the formal verification and control synthesis of DES. Most contemporary approaches^{31,32,36–39} are based on graph theory. However, we adopt a new approach to the quasi-congruence relations by binary linear programming in the paper, and apply it to reduce the state space.

Wong and Wonham ³¹ solve the problem on how to design an observer by modifying the given causal reporter map that is not an observer. The method is to compute the coarsest equivalence relation, which is finer than that of the given map. A polynomial-time algorithm is developed to compute an observer of an automaton, and it can also be used to verify the observer property of natural projection. However, this algorithm cannot be applied to natural projection directly.

Feng and Wonham ³² adopt the algorithm in Wong and Wonham ³¹ to the natural projection, where the minimum event extension is particularly interesting, whose computation, however, is shown to be NP-hard. In this case, an acceptable event extension can be found by developing a polynomial-time algorithm.

These methods are based on graph theory and state-transition data structure. The novelty of this paper is to solve the optimal partitioning problem as an optimal state-to-coset allocation problem. Partitioning states to cosets is considered as allocating states to an unknown number of cosets and the requirement of finding the coarsest quasi-congruence is equivalent to using the least number of cosets. Then the problem can be solved by optimization methods, which leverage many powerful and easy-to-use software tools, such as CPLEX (the CPLEX optimizer can be available on the website https://www.ibm.com/analytics/cplex-optimizer) ⁴⁰ and SAT solvers (the SAT solvers can be available on the website https://www.satlive.org/solvers). ⁴¹ These computation tools exploit modern computing technologies, such as graphics processing unit (GPU) computing, ⁴² parallel computing, ⁴³ and cloud computing. ⁴⁴ Large scale problems of finding the coarsest quasi-congruence may be solved by modern optimization technologies.

To this end, this paper formalizes the problem of finding the coarsest quasi-congruence as a binary linear programming problem. The design variables form a binary allocation matrix between the states and cosets. The constraints are relationships between states and cosets, and the objective function is to minimize the number of cosets. The main contributions of this paper are summarized below.

1. The number of design variables determines the computational complexity. In Section 4, a property of the allocation problem is discovered and proved to remove around half of the binary design variables.

2. A novel approach on how to compute the supremal quasi-congruence is proposed, which is based on a combination of propositional logic and binary representation in Section 5.

3. The method proposed in Section 5 is converted to a binary linear programming problem, so as to save computing time. In this transformation, we formulate a few techniques of converting logic constraints on finite automata into binary linear constraints which are formalized and proved to be correct in Section 6.

4. The correctness and efficiency of our method are verified by different solvers and examples in Section 8.

Compared with existing studies, the motivation of this work is to propose an optimization method for quasi-congruence computation of DFAs, and to increase the generality of optimal quasi-congruence computation algorithms. The computational results of this method are the same as that of using the computation software TCT (the software TCT can be available on the website https://www.control.utoronto.ca/DES/Research). ⁴⁵ for supervisory control design.

The work is structured as follows. The preliminaries pertaining to automata and natural projection are recalled in the following section. Some functions and concepts that are necessary for the quasi-congruence calculation, and the coarsest quasi-congruence are reported in Section 3. Section 7 touches on the main algorithm implementation of the proposed approach. Finally, Section 9 concludes this research.

Preliminaries

This section recalls some basic concepts of deterministic finite automata used in the paper. Then we review the definition of quasi-congruence relation and some operations on it. More details on automata can be found in references.^{1,2,31,32,46–48}

Fundamental of automata

A deterministic finite automaton (DFA) ¹ is represented as a five-tuple,

$$G=(Q,\Sigma ,\delta ,q_1,Q_m)$$

(1)

• $Q=\{q_1,q_2,\dots ,q_n\}$ is the finite state set and $n=\left|Q\right|$ is the number of states in the automaton.

• $\Sigma$ is a nonempty finite event set with $\Sigma ={\Sigma }_o\cup {\Sigma }_u$ , where ${\Sigma }_o$ is the observable event set and ${\Sigma }_u$ is the unobservable event set of $G$ .

• $\delta :Q\times \Sigma \to Q$ is the state transition function which is considered as a partial function. For an event $\sigma \in \Sigma$ , if the function $\delta (q,\sigma )$ is defined, we write it as $\delta (q,\sigma )!$ .

• $q_1\in Q$ is the initial state.

• $Q_m$ is the set of marker states with $Q_m\subseteq Q$ .

Note that the set of all finite strings over $\Sigma$ is denoted as ${\Sigma }^{*}$ . The empty string $\epsilon$ denotes the string with length 0.

Natural projection

Given two event sets: $\Sigma$ is a finite alphabet and ${\Sigma }_o$ is the set of observable events with ${\Sigma }_o\subseteq \Sigma$ , the corresponding natural projection function is $P:{\Sigma }^{*}\to {\Sigma }_o^{*}$ , such that $P(\epsilon )=\epsilon$ and

$$P(\sigma )=\{\begin{array}{c}\epsilon ,\sigma \in \Sigma -{\Sigma }_o\hfill \\ \sigma ,\sigma \in {\Sigma }_o\hfill \end{array}$$

(2)

$$P(s\sigma )=P(s)P(\sigma ),s\in {\Sigma }^{*},\sigma \in \Sigma$$

(3)

Next, the natural projection $P$ can be extended to the image function, ³² $P:P_{\mathrm{wr}}({\Sigma }^{*})\to P_{\mathrm{wr}}({\Sigma }_o^{*})$ such that

$$\forall L\subseteq {\Sigma }^{*},P(L):=\{P(s)|s\in L\}.$$

(4)

Note that $P_{\mathrm{wr}}(A)$ is the power set of set $A$ . Mathematically, the inverse function of natural projection $P$ does not exist. Here, the notation of the function $P^{-1}$ is expressed as the inverse image function, which can be defined as $P^{-1}:P_{\mathrm{wr}}({\Sigma }_o^{*})\to P_{\mathrm{wr}}({\Sigma }^{*})$ such that

$$\forall L_o\subseteq {\Sigma }_o^{*},P^{-1}(L_o):=\{s\in {\Sigma }^{*}|P(s)\in L_o\}.$$

(5)

Equivalence relation and quasi-congruence relation

This section defines three important functions and some concepts associated with the quasi-congruence computation.

Equivalence relation

Suppose that $E(Q)$ is the lattice of equivalence relations on the state set $Q$ . Given an equivalence relation $\pi \in E(Q)$ , it must meet the following properties.^1,49

1. $(\forall q\in Q)q\pi q$ ( $\pi$ is reflexive.)

2. $(\forall q,q\prime \in Q)q\pi q\prime \Rightarrow q\prime \pi q$ ( $\pi$ is symmetric.)

3. $(\forall q,q\prime ,q″\in Q)q\pi q\prime \wedge q\prime \pi q″\Rightarrow q\pi q″$ ( $\pi$ is transitive.)

In this paper, $q\pi q\prime$ is also written as $q\equiv q\prime (\mathrm{mod}\pi )$ . For any state $q\in Q$ , the coset (or equivalence class) of $q$ with respect to the equivalence relation $\pi$ is denoted as $[q{]}_{\pi }$ .

$$[q{]}_{\pi }:=\{q\prime \in Q|q\prime \pi q\}\subseteq Q$$

(6)

By reflexivity $q\in [q{]}_{\pi }$ , every coset is nonempty. In this paper, $Q/\pi$ represents the set of all cosets.

Functions

In a DFA $G$ , we can decide the possibly reachable states from any state $q_i\in Q$ based only on observation of the events in ${\Sigma }_o$ .

• Definition 1. Let $s_o\in {\Sigma }_o^{*}$ be an observable string and $q_i\in Q$ a state. The function $\mathrm{\Delta }$ is defined as

$$\mathrm{\Delta }:Q\times {\Sigma }_o^{*}\to P_{\mathrm{wr}}(Q)$$

(7)

and

$$\mathrm{\Delta }(q_i,s_o):=\{q\prime \in Q|(\exists s\in {\Sigma }^{*})P(s)=s_o\wedge q\prime =\delta (q_i,s)\}.$$

Note that if $\delta (q_i,s)$ is undefined for every string $s$ with $P(s)=s_o$ , then $\mathrm{\Delta }(q_i,s_o)=Ø$ . In addition, if $s_o=\sigma \in {\Sigma }_o$ , we can simplify the notation of $\mathrm{\Delta }(q_i,\sigma )$ to ${\mathrm{\Delta }}_{\sigma }(q_i)$ , which denotes the set of reachable states from state $q_i\in Q$ via an observable event $\sigma$ . Similarly, if $s_o=\epsilon$ , it can be written as ${\mathrm{\Delta }}_{\epsilon }(q_i)$ which denotes the set of all reachable states from state $q_i\in Q$ via a sequence of unobservable events in $\Sigma -{\Sigma }_o$ . Moreover, the set of all reachable marker states can be computed by ${\mathrm{\Delta }}_m(q_i)={\mathrm{\Delta }}_{\epsilon }(q_i)\cap Q_m$ .

For concise presentation, we define a new event $\mu \notin \Sigma$ , and define ${\mathrm{\Delta }}_{\mu }$ as ${\mathrm{\Delta }}_m$ and $\Sigma {\prime }_o={\Sigma }_o\cup \{\mu \}$ . In addition, we denote $\mathbf{n}=\{1,2,\cdots ,n\}$ .

• Definition 2. Let $\pi$ be an equivalence relation, $q_i\in Q$ and $\sigma \in {\Sigma }_o$ . Denote the canonical projection function as $P_{\pi }:Q\to Q/\pi :q_i\to [q_i{]}_{\pi }$ . We can further define its extension projection function as

$$P_{\pi }:P_{\mathrm{wr}}(Q)\to P_{\mathrm{wr}}(Q/\pi ).$$

(8)

• Definition 3. Function $P_{\pi }°{\mathrm{\Delta }}_{\sigma }$ is the composition function of ${\mathrm{\Delta }}_{\sigma }$ and $P_{\pi }$ ,

$$P_{\pi }°{\mathrm{\Delta }}_{\sigma }:Q\to P_{\mathrm{wr}}(Q/\pi ).$$

(9)

At a state $q_i\in Q$ , this composed function $P_{\pi }°{\mathrm{\Delta }}_{\sigma }$ can be further expressed as $P_{\pi }({\mathrm{\Delta }}_{\sigma }(q_i)):=\{[q{]}_{\pi }|q\in {\mathrm{\Delta }}_{\sigma }(q_i)\}$ .

The composite $\pi °{\mathrm{\Delta }}_{\sigma }$ ( $\sigma \in {\Sigma }_o^{\prime }$ ) defines an equivalence relation on $Q$ as follows. Suppose $i\ne j$ and $i,j\in \mathbf{n}$ .

$$(\forall q_i,q_j\in Q)q_i\equiv q_j(\mathrm{mod}\pi °{\mathrm{\Delta }}_{\sigma })\iff$$

$$\{\begin{array}{c}(\forall x\in {\mathrm{\Delta }}_{\sigma }(q_i))(\exists x\prime \in {\mathrm{\Delta }}_{\sigma }(q_j))x\equiv x\prime (\mathrm{mod}\pi );\hfill \\ \multicolumn{1}{c}{(\forall x\prime \in {\mathrm{\Delta }}_{\sigma }(q_j))(\exists x\in {\mathrm{\Delta }}_{\sigma }(q_i))x\prime \equiv x(\mathrm{mod}\pi ).}\end{array}$$

(10)

Quasi-congruence relation

Assume that $(Q,\mathrm{\Delta })$ is a nondeterministic dynamic system where $Q$ is the set of system states and $\mathrm{\Delta }:Q\to P_{\mathrm{wr}}(Q)$ is its state transition function. According to references,^1,31,32 we can define the quasi-congruence relation as follows.

• Definition 4. An equivalence relation $\pi$ on $Q$ is a quasi-congruence for $(Q,\mathrm{\Delta })$ , if it satisfies the following three equivalent conditions.

• (1)  $\pi \le \pi °\mathrm{\Delta }$ .

• (2)  $(\forall q_i,q_j\in Q)P_{\pi }(q_i)=P_{\pi }(q_j)\Rightarrow P_{\pi }°\mathrm{\Delta }(q_i)=P_{\pi }°\mathrm{\Delta }(q_j).$

• (3)  $(\forall q_i,q_j\in Q)q_i\equiv q_j(\mathrm{mod}\pi )\Rightarrow q_i\equiv q_j(\mathrm{mod}\pi °\mathrm{\Delta }).$

The coarsest quasi-congruence

• Definition 5. Given a DFA $G$ and the observable event set ${\Sigma }_o\subseteq \Sigma$ , the coarsest quasi-congruence ^31,50,51 with respect to $Q$ and ${\Sigma }_o\prime$ is

$$\rho :=\sup \{\pi \in E(Q)|\pi \le ({\wedge }_{\sigma \in {\Sigma }_o\prime }(\pi °{\mathrm{\Delta }}_{\sigma }))\}.$$

(11)

Quotient automaton

For a state set $Q$ and the coarsest quasi-congruence relation $\rho \in E(Q)$ , we have the canonical projection $P_{\rho }:Q\to Q/\rho$ as defined in Definition 2. Renaming the cosets in $Q/\rho$ , we get a new state set $Q\prime$ and a bijection $r:Q/\rho \cong Q\prime$ . The composition of $P_{\rho }$ and $r$ is denoted as a function $g=r°P_{\rho }$ , with equivalence kernel $\ker g=\rho$ .

• Definition 6. Given a DFA $G=(Q,\Sigma ,\delta ,q_1,Q_m)$ , an observable event set ${\Sigma }_o\subseteq \Sigma$ , and an equivalence relation $\rho \in E(Q)$ , the quotient automaton ^1,51 is

$$G\prime =(Q\prime ,{\Sigma }_o,\eta ,q{\prime }_1,Q{\prime }_m)=G/({\Sigma }_o,\rho )$$

(12)

where $Q\prime \cong Q/\rho$ , $q{\prime }_1:=g(q_1)$ , $Q{\prime }_m:=g(Q_m)$ . Here, the transition function is $\eta :Q\prime \times ({\Sigma }_o\cup \{\epsilon \})\to P_{\mathrm{wr}}(Q\prime )$ as follows.

$$\eta (q\prime ,\sigma )\mapsto \{\begin{array}{c}g°\delta (g^{-1}(q\prime ),\sigma ),\mathrm{if}\sigma \in {\Sigma }_o\hfill \\ \multicolumn{1}{c}{g°\delta (g^{-1}(q\prime ),\Sigma -{\Sigma }_o)-\{q\prime \},\mathrm{if}\sigma =\epsilon }\end{array}$$

The quotient automaton may be nondeterministic.

Matrix representations

Define the reachable matrix of each event $\sigma$ ( $\sigma \in {\Sigma }_o\prime$ ) as a Boolean matrix $R_{\sigma }$ , which is an $n\times n$ square matrix and $n=|Q|$ . For any $i,j\in \mathbf{n}$ ,

$$R_{\sigma }(i,j)=\{\begin{array}{c}1,q_j\in {\mathrm{\Delta }}_{\sigma }(q_i);\hfill \\ \multicolumn{1}{c}{0,\mathrm{otherwise}.}\end{array}$$

(13)

Let $\pi \in E(Q)$ be a quasi-congruence relation on the state set $Q$ . Assume that $\pi$ partitions $Q$ into $m\le n$ cosets, then $Q/\pi =\{C_1,C_2,\cdots ,C_m\}$ and $C_j$ represents a coset.

The quasi-congruence relation $\pi$ is representable by an allocation matrix $X_{n\times m}$ , which is also Boolean, that is, $x_{\mathrm{ij}}=1$ iff $q_i\in C_j$ , $i\in \mathbf{n}$ , $j\in \mathbf{m}$ . To decrease the number of unknown variables, we show that through permutation of the cosets, the allocation matrix is reducible to a lower triangular matrix as formalized in Proposition 1.

• Proposition 1. There must exist a permutation of the cosets $\{C_1,C_2,\cdots ,C_m\}$ such that the allocation matrix $X_{n\times m}$ is lower triangular, namely

$$(\forall i\in \mathbf{n})(\forall j\in \mathbf{m})i<j\to x_{\mathrm{ij}}=0.$$

(14)

Proof. According to the definition of the allocation matrix $X_{n\times m}$ , if $m=1$ , then there is only one coset $C_1$ , so the proposition is true.

If $1<m\le n$ , then we perform the following operations iteratively for each state $q_i\in Q$ in an ascending order of $i\in n$ . If $q_i\in C_j$ and $i\ge j$ , then we need not any permutation of columns, that is, $x_{\mathrm{ij}}=1$ , and the rest of the elements in the $i$ -th row are 0. Otherwise, if $q_i\in C_j$ and $i<j$ , then $x_{\mathrm{ii}}=0$ and $x_{\mathrm{ij}}=1$ . In this case, since the previous operations have ensured that $(\forall s\in \mathbf{i}-1)(\forall t\in \mathbf{m})s<t\to x_{\mathrm{st}}=0$ , the first $i-1$ rows of the allocation matrix is already lower triangular.

Now that the $i$ -th row violates the lower triangular property, we permute cosets $C_i$ and $C_j$ and denote the new allocation matrix as $X\prime$ . After the permutation, $x{\prime }_{\mathrm{ii}}=1$ and $x{\prime }_{\mathrm{ij}}=0$ . The $i$ -th row satisfies the lower-triangular property. We need to further prove that the first $i-1$ rows of the new allocation matrix still satisfy the lower triangular property.

For all $s\in \mathbf{i}-1$ and $t\in \mathbf{m}$ , if $t\notin \{i,j\}$ , then $x{\prime }_{\mathrm{st}}=x_{\mathrm{st}}$ . Under the same condition of $s$ , if $t=i$ , then $x{\prime }_{\mathrm{si}}=x_{\mathrm{sj}}=0$ ; if $t=j$ , then $x{\prime }_{\mathrm{sj}}=x_{\mathrm{si}}=0$ . These arguments prove that the first $i-1$ rows of $X\prime$ indeed satisfy the lower triangular property.

Set $X=X\prime$ and iterate the operations from the next state $q_{i+1}$ . The procedure terminates when the allocation of state $q_m$ also satisfies the lower-triangular property.

Finally, we can construct the lower triangle allocation matrix $X_{n\times m}$ as shown in Table 1.

Table 1.

Lower triangular allocation matrix $X_{n\times m}$ .

$X_{n\times m}$	$C_1$	$C_2$	…	$C_m$
$q_1$	$x_{11}$	0	0	0
$q_2$	$x_{21}$	$x_{22}$	0	0
⋮	⋮	⋮	⋱	0
$q_m$	$x_{m1}$	$x_{m2}$	…	$x_{\mathrm{mm}}$
⋮	⋮	⋮	⋮	⋮
$q_n$	$x_{n1}$	$x_{n2}$	…	$x_{\mathrm{nm}}$

Quasi-congruence calculation

In this part, we propose a new approach of calculating the supremal quasi-congruence using the Boolean allocation matrix and logical propositions.

Let $\pi$ be an equivalence relation on the state set $Q$ , $n=\left|Q\right|$ . Suppose that the number of cosets is $m$ , $m\le n$ . Since the minimal number of cosets is unknown, we define the Boolean variable $y_j$ to represent if coset $C_j$ is not empty, where $j\in \mathbf{m}$ .

$$y_j=\{\begin{array}{c}1,\exists q\in C_j;\hfill \\ \multicolumn{1}{c}{0,\forall q\notin C_j.}\end{array}$$

(15)

Then the decision variables are

$$\{\begin{array}{c}{x}_{\mathrm{ij}}\in \{0,1\},1\le i\le n,1\le j\le m,j\le i;\hfill \\ \multicolumn{1}{c}{y_k\in \{0,1\},1\le k\le m.}\end{array}$$

(16)

In total, there are $\frac{m·(2·n-m+1)}{2}+m$ decision variables.

The objective is to find the coarsest quasi-congruence, which has the least number of cosets among all quasi-congruences of the given DFA $G$ based on an observable event set ${\Sigma }_o$ . Therefore the objective function for the optimization problem is:

$$\underset{x_{\mathrm{ij}},y_k}{min}\sum _{k=1}^m{y}_k.$$

(17)

To represent quasi-congruences, these decision variables must satisfy the following constraints from C1 to C3.

• C1: For each coset $C_k$ , $y_k=1$ iff at least one state is allocated to it, that is,

$$y_k={\vee }_{i=k}^n{x}_{\mathrm{ik}},1\le k\le m.$$

(18)

• C2: Each state must belong to one and only one coset, that is,

$$\sum _{j=1}^{min(i,m)}{x}_{\mathrm{ij}}=1,1\le i\le n.$$

(19)

• C3: For all the state pairs $q_i,q_j\in Q$ and all $\sigma \in {\Sigma }_o\prime$ ,

$$q_i\equiv q_j(\mathrm{mod}\pi )\to P_{\pi }°{\mathrm{\Delta }}_{\sigma }(q_i)=P_{\pi }°{\mathrm{\Delta }}_{\sigma }(q_j).$$

(20)

If two states $q_i$ , $q_j$ belong to the same coset $C_k$ ( $1\le k\le m$ ), then they must meet the above constraints C3. Equation (20) is further transformed into propositions consisting of binary variables in two steps.

• Step 1: The reachable state sets of states $q_i$ and $q_j$ can be obtained by standard algorithms, assuming that they are represented as

$${\mathrm{\Delta }}_{\sigma }(q_i)=\{q_{i_1},q_{i_2},\dots ,q_{i_p}\},,\mathrm{where}{q}_{i_p}\in Q,1\le i_p\le n$$

$${\mathrm{\Delta }}_{\sigma }(q_j)=\{q_{j_1},q_{j_2},\dots ,q_{j_t}\},\mathrm{where}{q}_{j_t}\in Q,1\le j_t\le n.$$

Based on the definition of reachable matrix in (13), the two state subsets are equivalent to two row vectors of length $n$ , namely $R_{\sigma }(i,:)$ and $R_{\sigma }(j,:)$ , respectively. By (13), $R_{\sigma }(i,k)=1$ if and only if $q_k\in {\mathrm{\Delta }}_{\sigma }(q_i)$ . In the special case ${\mathrm{\Delta }}_{\sigma }(q_i)=Ø$ , the row vector $R_{\sigma }(i,:)=0_{1\times n}$ holds.

• Step 2: we need to compute $P_{\pi }°{\mathrm{\Delta }}_{\sigma }(q_i)$ and $P_{\pi }°{\mathrm{\Delta }}_{\sigma }(q_j)$ . The formulas can be simply implemented by Boolean matrix multiplication, denoted by ⋀. The rule is the same as normal matrix multiplication, but replaces multiplication by logic ∧ and addition by logic ∨. Given a state $q_i\in Q$ , $\sigma \in {\Sigma }_o\prime$ , $P_{\pi }°{\mathrm{\Delta }}_{\sigma }(q_i)$ can be represented as

$$R_{\sigma }(i,:)\bigwedge X_{n\times m}=X(i_1,:)\vee X(i_2,:)\vee \dots \vee X(i_p,:).$$

Similarly, $P_{\pi }°{\mathrm{\Delta }}_{\sigma }(q_j)$ is equivalent to the row vector

$$R_{\sigma }(j,:)\bigwedge X_{n\times m}=X(j_1,:)\vee X(j_2,:)\vee \dots \vee X(j_t,:).$$

Thus, it follows that the equality $P_{\pi }°{\mathrm{\Delta }}_{\sigma }(q_i)=P_{\pi }°{\mathrm{\Delta }}_{\sigma }(q_j)$ is equivalent to the new vector equality as follows.

$$R_{\sigma }(i,:)\bigwedge X_{n\times m}=R_{\sigma }(j,:)\bigwedge X_{n\times m}.$$

(21)

• Remark 1. $R_{\sigma }(i,:)$ is a $1\times n$ row vector and $X$ is an $n\times m$ matrix, then the Boolean multiplication is a $1\times m$ row vector. The notation of $X(i_p,:)$ means that all the elements of the row correspond to state $q_{i_p}$ in the allocation matrix $X_{n\times m}$ .

Therefore, we can further get the logical formulas of this constraint C3:

• If $R_{\sigma }(i,:)=R_{\sigma }(j,:)$ , then the vector equality (21) is always true. So the two states $q_i$ and $q_j$ must belong to the same coset, that is, $X(i,:)=X(j,:)$ .

• If $R_{\sigma }(i,:)\ne R_{\sigma }(j,:)$ , then we further consider two cases.

• One case is that one of the two row vectors $R_{\sigma }(i,:)$ and $R_{\sigma }(j,:)$ is zero but not both. Then $q_i$ and $q_j$ cannot belong to the same coset. Consequently, $X(i,:)\ne X(j,:)$ . For all $k\le min(i,j,m)$ ,

$$\neg (x_{\mathrm{ik}}=1\wedge x_{\mathrm{jk}}=1)\iff x_{\mathrm{ik}}=0\vee x_{\mathrm{jk}}=0.$$

(22)

• • When neither of the two reachable state sets is empty, that is, both $R_{\sigma }(i,:)$ and $R_{\sigma }(j,:)$ are not zero, the following condition derived from (20) must be satisfied.

$$\begin{array}{c}\multicolumn{1}{c}{[X(i,:)=X(j,:)]\to \{{\wedge }_{\sigma \in {\Sigma }_o\prime }[R_{\sigma }(i,:)\bigwedge X_{n\times m}=R_{\sigma }(j,:)\bigwedge X_{n\times m}]\}.}\end{array}$$

(23)

Transforming logical propositions to linear constraints

Many constraints in Section 5 are logical constraints. Solving this problem is a Constraint Satisfaction Problem (CSP) or SAT problem.^52,53 A well-known solution to the CSP is to convert the logical constraints into binary linear constraints and to solve the problem by binary linear programming. ⁵⁴ There are three main logical propositions that need to be converted equivalently. In this section, we will show how to convert them into equivalent linear inequalities.

• Proposition 2. If $y\in \{0,1\}$ and $x_i\in \{0,1\}$ ( $i\in \mathbf{n}$ ) are binary variables, then the following two expressions are equivalent.

$$y={\vee }_{i=1}^n{x}_i\iff \frac{y}{n}\le \sum _{i=1}^n{x}_i\le n·y$$

(24)

Proof. (⇒) For the logic proposition, we need to consider two scenarios: If $y=0$ , then all $x_i=0$ , $i\in \mathbf{n}$ . Then these values satisfy the linear inequalities, because $\frac{y}{n}=0$ , $n·y=0$ , and $\sum _{i=1}^n{x}_i=0$ .

If $y=1$ , then there exists at least one $x_i=1$ . Therefore, $\frac{y}{n}=\frac{1}{n}$ and $n·y=n$ , and $1\le \sum _{i=1}^n{x}_i\le n$ . Since $\frac{1}{n}\le 1$ and $y=1$ , $\frac{1}{n}\le 1\le \sum _{i=1}^n{x}_i\le n\Rightarrow \frac{y}{n}\le \sum _{i=1}^n{x}_i\le n·y$ .

(⇐) If the linear inequalities on the right-hand side hold, then we need to prove that the left logical proposition is also true.

If $y=1$ , then $\frac{1}{n}\le \sum _{i=1}^n{x}_i\le n$ . Since $\frac{1}{n}>0$ , $\sum _{i=1}^n{x}_i\ge \frac{1}{n}>0$ . Thus, there exists at least one $x_i=1$ in this case. Therefore ${\vee }_{i=1}^n{x}_i=1$ .

On the other hand, if $y=0$ , then $\sum _{i=1}^n{x}_i=0$ . Under this condition, all $x_i=0$ , $i=\{1,2,\dots ,n\}$ , thus ${\vee }_{i=1}^n{x}_i=0$ .

Clearly, it can be seen from the above derivation that the logic proposition is also satisfied in the two cases.

Accordingly, we can conclude that this equivalent transformation is always true. □

• Proposition 3. If $x_i\in \{0,1\}$ ( $i\in \mathbf{m}$ ), and $y_j\in \{0,1\}$ ( $j\in \mathbf{n}$ ) are binary variables, then the following equivalence holds, where $N\ge max(m,n)$ is a positive integer.

$${\vee }_{i=1}^m{x}_i={\vee }_{j=1}^n{y}_j\iff \frac{1}{N}·\sum _{i=1}^m{x}_i\le \sum _{j=1}^n{y}_j\le N·\sum _{i=1}^m{x}_i$$

(25)

Proof. (⇒) The proof is a simple extension of the proof of Proposition 2. For the left logical formula, we also need to consider two scenarios:

If the logical expressions are 1, at least one $x_i$ and at least one $y_j$ are 1. Then $1\le \sum _{i=1}^m{x}_i\le m$ , and $1\le \sum _{j=1}^n{y}_j\le n\le N$ . Therefore, $\frac{1}{N}·\sum _{i=1}^m{x}_i\le \frac{m}{N}\le 1$ and $N·\sum _{i=1}^m{x}_i\ge N$ . The two linear inequalities at the right-hand side are both true.

If the logical expressions are 0, then all $x_i$ and all $y_j$ are 0. Then the linear inequalities are also obviously true.

(⇐) If the right-hand side of Proposition 3 holds, then we need to prove that the left logical formula is also true. There are two cases as below.

• 1. If all $y_j=0$ , then

$$\sum _{j=1}^n{y}_j=0\Rightarrow \frac{1}{N}·\sum _{i=1}^m{x}_i\le 0\le N·\sum _{i=1}^m{x}_i$$

Since $\frac{1}{N}>0$ and $x_i\in \{0,1\}$ ( $i\in \mathbf{m}$ ), we have $\sum _{i=1}^m{x}_i=0$ , i.e., all $x_i=0$ . Obviously, in this case, the logical formula ${\vee }_{i=1}^m{x}_i={\vee }_{j=1}^n{y}_j$ is satisfied.

• (2) If there exists at least one $y_j=1$ , then

$$1\le \sum _{j=1}^n{y}_j\le N·\sum _{i=1}^m{x}_i\Rightarrow 1\le N·\sum _{i=1}^m{x}_i$$

Since $x_i\in \{0,1\}$ ( $i\in \mathbf{m}$ ) and $N\ge max(m,n)$ is a positive integer. Thus, $\sum _{i=1}^m{x}_i\ge \frac{1}{N}>0$ , i.e., there must exist at least one $x_i=1$ . Clearly, these values also satisfy the logical formula ${\vee }_{i=1}^m{x}_i={\vee }_{j=1}^n{y}_j$ .

Therefore, it can be seen from the above derivation that the Proposition 3 is always true. □

Next, we introduce the following lemma for establishing Proposition 4.

• Lemma 1. Let $A$ , $B$ and $C$ be logical propositions. The logical equivalence $A\to (B\wedge C)\iff (A\to B)\wedge (A\to C)$ is always valid.

• Proposition 4. If $z_1$ , $z_2$ , $x_i\in \{0,1\}$ ( $i\in \mathbf{m}$ ), and $y_j\in \{0,1\}$ ( $j\in \mathbf{n}$ ) are all binary variables, where $m$ , $n$ are both positive integers, then the following logical implication formula is equivalent to the given inequalities, where $N\ge max(m,n)$ is a positive integer.

$$\begin{array}{c}(z_1=1\wedge z_2=1)\to ({\vee }_{i=1}^m{x}_i={\vee }_{j=1}^n{y}_j)\hfill \\ \iff \{\begin{array}{c}{z}_1+z_2-2\le \sum _{j=1}^n{y}_j-\frac{1}{N}·\sum _{i=1}^m{x}_i\hfill \\ \multicolumn{1}{c}{N·(z_1+z_2-2)\le N·\sum _{i=1}^m{x}_i-\sum _{j=1}^n{y}_j}\end{array}\hfill \end{array}$$

(26)

Proof. (⇒) According to Proposition 3, we can first equivalently convert the logical implication into the statement as below.

$$(z_1=1\wedge z_2=1)\to \frac{1}{N}·\sum _{i=1}^m{x}_i\le \sum _{j=1}^n{y}_j\le N·\sum _{i=1}^m{x}_i$$

(27)

Second, based on Lemma 1, we can translate the logical implication (27) into the following form.

$$\{\begin{array}{c}(z_1=1\wedge z_2=1)\to \frac{1}{N}·\sum _{i=1}^m{x}_i\le \sum _{j=1}^n{y}_j\hfill \\ \multicolumn{1}{c}{(z_1=1\wedge z_2=1)\to \sum _{j=1}^n{y}_j\le N·\sum _{i=1}^m{x}_i}\end{array}$$

(28)

The next step is to show that if the two propositions in (28) hold, then the two inequalities of (26) also hold. The proof has two cases.

1. If both $z_1$ and $z_2$ are 1, then $z_1=1\wedge z_2=1$ is true, and (28) yields the inequalities $\frac{1}{N}·\sum _{i=1}^m{x}_i\le \sum _{j=1}^n{y}_j\le N·\sum _{i=1}^m{x}_i$ . Since $z_1+z_2-2=0$ , the two inequalities of (26) obviously hold.

2. Otherwise, then $z_1+z_2-2\le -1$ . Since $x_i\in \{0,1\}$ , $y_j\in \{0,1\}$ and $m$ , $n$ are both positive integers, then we can derive the following inequality set.

$$\{\begin{array}{c}0\le \sum _{i=1}^m{x}_i\le m\hfill \\ \multicolumn{1}{c}{0\le \sum _{j=1}^n{y}_j\le n}\end{array}$$

(29)

Because $N$ is a positive integer, $-\frac{1}{N}<0$ . Further, we can transform the above inequality set (29) into the following two inequality pairs.

$$\{\begin{array}{c}-\frac{m}{N}\le -\frac{1}{N}·\sum _{i=1}^m{x}_i\le 0\hfill \\ 0\le \sum _{j=1}^n{y}_j\le N\hfill \end{array}$$

(30)

$$\{\begin{array}{c}0\le N·\sum _{i=1}^m{x}_i\le N·m\hfill \\ \multicolumn{1}{c}{-n\le -\sum _{j=1}^n{y}_j\le 0}\end{array}$$

(31)

Summing the inequality pairs in (30) and (31), we have the following two inequalities.

$$\{\begin{array}{c}-\frac{m}{N}\le (\sum _{j=1}^n{y}_j-\frac{1}{N}·\sum _{i=1}^m{x}_i)\le N\hfill \\ -n\le (N·\sum _{i=1}^m{x}_i-\sum _{j=1}^n{y}_j)\le N·m\hfill \end{array}$$

(32)

Since $m,n>0$ and $N\ge max(m,n)$ , we have $-1\le -\frac{m}{N}$ and $-N\le -n$ . From this we derive the following pairs.

$$\{\begin{array}{c}-1\le (\sum _{j=1}^n{y}_j-\frac{1}{N}·\sum _{i=1}^m{x}_i)\le N\hfill \\ -1·N\le (N·\sum _{i=1}^m{x}_i-\sum _{j=1}^n{y}_j)\le N·m\hfill \end{array}$$

(33)

Recalling $z_1+z_2-2\le -1$ , then both inequalities in (26) are also satisfied, regardless of the values of $x_i$ and $y_j$ .

(⇐) We prove this direction in two cases.

1. If $z_1=0$ or $z_2=0$ , the proposition $z_1=1\wedge z_2=1$ is always false. The logical proposition at the left-hand side is always true regardless of the values of $x_i$ and $y_j$ in this case.

2. If $z_1=1\wedge z_2=1$ , then $z_1+z_2-2=0$ . In this case, we can convert the set of inequalities in Proposition 4 into the set of inequalities below.

$$\{\begin{array}{c}\multicolumn{1}{c}{0\le \sum _{j=1}^n{y}_j-\frac{1}{N}·\sum _{i=1}^m{x}_i}\\ \multicolumn{1}{c}{0\le N·\sum _{i=1}^m{x}_i-\sum _{j=1}^n{y}_j}\end{array}$$

(34)

$$\iff \frac{1}{N}·\sum _{i=1}^m{x}_i\le \sum _{j=1}^n{y}_j\le N·\sum _{i=1}^m{x}_i$$

(35)

The inequalities (35) are equivalent to the right-hand side inequalities by Proposition 3.

Therefore, we can know that the equivalent conversion of Proposition 4 is always true. □

The main algorithm and procedure of model abstraction

Main algorithm

According to Proposition 2, it is easy to convert the constraints of C1 into the following pairs of linear inequalities. For any $k\in \mathbf{m}$ ,

$$\{\begin{array}{c}\multicolumn{1}{c}{\frac{1}{n}·y_k-\sum _{i=k}^n{x}_{\mathrm{ik}}\le 0}\\ \multicolumn{1}{c}{\sum _{i=k}^n{x}_{\mathrm{ik}}-n·y_k\le 0}\end{array}$$

(36)

Moreover, the constraints of C2 are already linear equality constraints. Finally, all linear inequality constraints of C3 are obtained by Algorithm 1.

Algorithm 1:Computation of the constraints C3
Input: $n$ , $m$ , $(R_{\sigma }{)}_{n\times n}$ for each event $\sigma \in \Sigma {\prime }_o$ , and $X_{n\times m}$ ( $m\le n$ ).
Output: List of linear inequalities corresponding to the constraints C3.
1 for $i=1\mathrm{to}n-1$ do
2  for $j=i+1\mathrm{to}n$ do
3   forall $\sigma \in \Sigma {\prime }_o$
4    if $R_{\sigma }(i,:)=0_{1\times n}\wedge R_{\sigma }(j,:)\ne 0_{1\times n}$ or $R_{\sigma }(i,:)\ne 0_{1\times n}\wedge R_{\sigma }(j,:)=0_{1\times n}$ then
5     for $k=1\mathrm{to}min(i,m)$ do
6       $x_{\mathrm{ik}}+x_{\mathrm{jk}}\le 1$
7     end
8     goto line 25; /*Iterate to the next $j$ */
9    end
10   end
11   forall $\sigma \in {{\Sigma }^{\prime }}_o$ do
12    if $R_{\sigma }(i,:)==R_{\sigma }(j,:)$ then
13     continue; /*Iterate to the next event*/
14    else
15      $\mathrm{co}{l}_i=\{s\in \mathbf{n}|R_{\sigma }(i,s)=1\}$
16      $\mathrm{co}{l}_j=\{s\prime \in \mathbf{n}|R_{\sigma }(j,s\prime )=1\}$
17     for $k=1\mathrm{to}min(i,m)$ do
18      for $t=1\mathrm{to}m$ do
19        $x_{\mathrm{ik}}+x_{\mathrm{jk}}+\frac{1}{n}·\sum _{s\in \mathrm{co}{l}_i}{x}_{\mathrm{st}}-\sum _{s\prime \in \mathrm{co}{l}_j}{x}_{s\prime t}\le 2$
20        $n·x_{\mathrm{ik}}+n·x_{\mathrm{jk}}-n·\sum _{s\in \mathrm{co}{l}_i}{x}_{\mathrm{st}}+\sum _{s\prime \in \mathrm{co}{l}_j}{x}_{s\prime t}\le 2·n$
21      end
22     end
23    end
24   end
25  end
26 end

In the following Algorithm 1, $n$ is the number of states, $m$ is the maximal number of cosets, $(R_{\sigma }{)}_{n\times n}$ represents the reachable matrices for each event $\sigma \in \Sigma {\prime }_o$ , and $X_{n\times m}$ ( $m\le n$ ) is the allocation matrix we supposed.

This algorithm computes the linear inequalities for all pairs of states $q_i$ and $q_j$ according to (20). Line 4 determines whether the two states cannot be equivalent. In that case, the algorithm adds the inequalities specified by lines 5–7, skips the remaining part, and iterates to the next value of $j$ . Otherwise, the algorithm continues into the loop of lines 11–24. Lines 12–13 check whether the reachable state sets from both states $q_i$ and $q_j$ are equivalent. If they are, no constraint is added; otherwise, the algorithm continues to execute lines 15–22 and output the linear inequalities of lines 17–22.

In the algorithm, line 6 corresponds to formula (22) in Section 5. Line 12 represents case (a) of the constraints C3. Lines 14–23 implement the second case in case (b) of C3. Finally, lines 17–22 correspond to the linear inequalities from the transformation of the logical formula (23) according to Proposition 4.

Model abstraction

This section presents the complete procedure of computing the model abstraction.

Input: A finite automaton $G=(Q,\Sigma ,\delta ,q_1,Q_m)$ and an observable event set ${\Sigma }_o\subseteq \Sigma$ .

• Step 1: Compute the reachable state set function ${\mathrm{\Delta }}_{\sigma }$ for all $\sigma \in {\Sigma }_o\prime$ . According to the definition of reachable matrix in (13), the reachable matrix of each event $\sigma$ can be obtained as $(R_{\sigma }{)}_{n\times n}$ .

• Step 2: Compute the coarsest quasi-congruence by solving the optimization problem (17)–(20) using the proposed method in the paper, based on all the reachable matrices $(R_{\sigma }{)}_{n\times n}$ and $\sigma \in {\Sigma }_o\prime$ .

• Step 3: Compute the quotient automaton for $G$ with the coarsest quasi-congruence, according to Definition 6.

Output: The quotient automaton is the abstraction of $G$ .

Computational examples

An illustrative example

This section elaborates the complete calculation process of the method with the simple example in Figure 1. The automaton M2 has the state set $Q=\{q_1,q_2,\dots ,q_6\}$ , the event set $\Sigma =\{\alpha ,\beta ,\gamma \}$ , the initial state $q_1$ and the marker state set $\{q_6\}$ . Given an observable event set ${\Sigma }_o=\{\alpha ,\gamma \}$ , we calculate the coarsest quasi-congruence through the following steps. First, we need to calculate its reachable matrices for all observable events, including $(R_{\alpha }{)}_{6\times 6}$ , $(R_{\gamma }{)}_{6\times 6}$ , and $(R_{\mu }{)}_{6\times 6}$ as in Tables 2 to 4. Second, let $m=6$ and the corresponding lower triangular allocation matrix $X_{6\times 6}$ is in Table 5. Third, on the basis of Propositions 2–4 and the constraints C1–C3 in Section 5, we can list all linear inequalities constraints for M2 as follows. Here, $n=6$ and $m=6$ .

• C1: $y_k={\vee }_{i=k}^n{x}_{\mathrm{ik}},(k\in \mathbf{m})\iff$

$$\{\begin{array}{c}\frac{1}{n}·y_k-x_{\mathrm{kk}}-x_{(k+1)k}-\cdots -x_{\mathrm{nk}}\le 0\hfill \\ \multicolumn{1}{c}{x_{\mathrm{kk}}+x_{(k+1)k}+\cdots +x_{\mathrm{nk}}-n·y_k\le 0}\end{array}$$

• C2: $\sum _{j=1}^{\min (i,m)}{x}_{\mathrm{ij}}=1,(i\in \mathbf{n})\iff$

$$\{\begin{array}{c}{x}_{i1}+x_{i2}+\cdots +x_{\mathrm{ii}}=1,i<m\hfill \\ \multicolumn{1}{c}{x_{i1}+x_{i2}+\cdots +x_{\mathrm{im}}=1,i\ge m}\end{array}$$

• C3: For all pairs of $i\in \mathbf{n}-1$ and $i+1\le j\le n$ , for all $\sigma \in \Sigma {\prime }_o$ , we need to consider the following three cases in turn. Firstly, if one of the two row vectors $R_{\sigma }(i,:)$ and $R_{\sigma }(j,:)$ is zero but not both, then states $q_i$ and $q_j$ cannot belong to the same coset. Then we add the following inequalities.

$$x_{\mathrm{ik}}+x_{\mathrm{jk}}\le 1,1\le k\le min(i,m)$$

(37)

Figure 1.

Automaton M2, and an observable event set ${\Sigma }_o=\{\alpha ,\gamma \}$ .

Table 2.

Reachable matrix $(R_{\alpha }{)}_{6\times 6}$ of M2.

$(R_{\alpha }{)}_{6\times 6}$	$q_1$	$q_2$	$q_3$	$q_4$	$q_5$	$q_6$
$q_1$	0	1	0	0	0	0
$q_2$	0	0	1	0	1	1
$q_3$	0	1	0	0	0	0
$q_4$	0	0	0	0	0	0
$q_5$	0	0	0	0	0	0
$q_6$	0	0	0	0	0	0

Table 3.

Reachable matrix $(R_{\gamma }{)}_{6\times 6}$ of M2.

$(R_{\gamma }{)}_{6\times 6}$	$q_1$	$q_2$	$q_3$	$q_4$	$q_5$	$q_6$
$q_1$	0	0	0	0	0	0
$q_2$	0	0	0	1	0	1
$q_3$	0	0	0	0	0	0
$q_4$	0	1	0	0	0	0
$q_5$	0	0	0	0	0	0
$q_6$	0	0	0	0	0	0

Table 4.

Reachable matrix $(R_{\mu }{)}_{6\times 6}$ of M2.

$(R_{\mu }{)}_{6\times 6}$	$q_1$	$q_2$	$q_3$	$q_4$	$q_5$	$q_6$
$q_1$	0	0	0	0	0	1
$q_2$	0	0	0	0	0	0
$q_3$	0	0	0	0	0	1
$q_4$	0	0	0	0	0	1
$q_5$	0	0	0	0	0	1
$q_6$	0	0	0	0	0	1

Table 5.

Supposed matrix $X_{6\times 6}$ of M2.

$X_{6\times 6}$	$C_1$	$C_2$	$C_3$	$C_4$	$C_5$	$C_6$
$q_1$	$x_{11}$	0	0	0	0	0
$q_2$	$x_{21}$	$x_{22}$	0	0	0	0
$q_3$	$x_{31}$	$x_{32}$	$x_{33}$	0	0	0
$q_4$	$x_{41}$	$x_{42}$	$x_{43}$	$x_{44}$	0	0
$q_5$	$x_{51}$	$x_{52}$	$x_{53}$	$x_{54}$	$x_{55}$	0
$q_6$	$x_{61}$	$x_{62}$	$x_{63}$	$x_{64}$	$x_{65}$	$x_{66}$

For example, we find $R_{\alpha }(q_2,:)\ne 0_{1\times n}$ and $R_{\alpha }(q_4,:)=0_{1\times n}$ in Table 2. According to (37), we have $i=2$ , $j=4$ , and $k\in \{1,2\}$ . The following two inequalities must be added.

$$\{\begin{array}{c}{x}_{21}+x_{41}\le 1\hfill \\ \multicolumn{1}{c}{x_{22}+x_{42}\le 1}\end{array}$$

Secondly, if the condition $R_{\sigma }(i,:)=R_{\sigma }(j,:)$ is true for all reachable matrices ( $\sigma \in \Sigma {\prime }_o$ ), then the two states $q_i$ and $q_j$ must belong to a coset, and no constraint needs to be added. From Tables 2 to 4, we can see that $[R_{\alpha }(1,:)=R_{\alpha }(3,:)]\wedge [R_{\gamma }(1,:)=R_{\gamma }(3,:)]\wedge [R_{\mu }(1,:)=R_{\mu }(3,:)]$ , so we can determine that $q_1$ and $q_3$ must belong to a coset, and there are no constraints to be added in this case. The final case is that $R_{\sigma }(i,:)\ne R_{\sigma }(j,:)$ and both are not zero vectors. Since M2 is simple, the third case does not exist in this example. If there is such a case in more complex automata, we also need to add the following pairs of linear inequalities according to (23).

$$\{\begin{array}{c}{x}_{\mathrm{ik}}+x_{\mathrm{jk}}+\frac{1}{n}\sum _{t=1}^m{Z}_{\sigma }(i,t)-\sum _{t=1}^m{Z}_{\sigma }(j,t)\le 2\hfill \\ \multicolumn{1}{c}{n(x_{\mathrm{ik}}+x_{\mathrm{jk}})-n\sum _{t=1}^m{Z}_{\sigma }(i,t)+\sum _{t=1}^m{Z}_{\sigma }(j,t)\le 2n}\end{array}$$

(38)

Note that the symbol $Z_{\sigma }(i,t)$ in the formula (38) represents the new vector multiplication, which can be calculated according to formula (21) and expressed as follows.

$$Z_{\sigma }(i,t)=R_{\sigma }(i,:)\bigwedge X(:,t)$$

(39)

$$={\vee }_{s=1}^n[R_{\sigma }(i,s)\wedge X(s,t)]$$

(40)

Here, $\sigma \in \Sigma {\prime }_o$ , $i\in \mathbf{n}$ and $t\in \mathbf{m}$ . On this basis, we can compute the corresponding product matrix $(Z_{\sigma }{)}_{n\times m}$ . For example,

$$Z_{\alpha }(2,3)={\vee }_{s=1}^6[R_{\sigma }(2,s)\wedge X(s,3)]=x_{33}\vee x_{53}\vee x_{63}.$$

Thus, if $k\in \mathbf{m}$ , then

$$Z_{\alpha }(2,:)=R_{\alpha }(2,:)\bigwedge X(:,k)={\left[\begin{array}{c}{x}_{31}\vee x_{51}\vee x_{61}\hfill \\ \multicolumn{1}{c}{x_{32}\vee x_{52}\vee x_{62}}\\ \multicolumn{1}{c}{x_{33}\vee x_{53}\vee x_{63}}\\ \multicolumn{1}{c}{x_{54}\vee x_{64}}\\ \multicolumn{1}{c}{x_{55}\vee x_{65}}\\ \multicolumn{1}{c}{x_{66}}\end{array}\right]}_{6\times 1.}^{\mathrm{T}}$$

Therefore, this example is formalized as the following binary linear programming problem. The objective function for the optimization problem is:

$$\underset{x_{\mathrm{ij}},y_k}{min}\sum _{k=1}^m{y}_k,n=m=6$$

(41)

subject to the following constraints.

$$\frac{1}{n}·y_k-x_{\mathrm{kk}}-x_{(k+1)k}-\cdots -x_{\mathrm{nk}}\le 0,k\in \mathbf{m}$$

(42)

$$x_{\mathrm{kk}}+x_{(k+1)k}+\cdots +x_{\mathrm{nk}}-n·y_k\le 0,k\in \mathbf{m}$$

(43)

$$x_{i1}+x_{i2}+\cdots +x_{\mathrm{ii}}=1,i\in \mathbf{n}$$

(44)

$$x_{2k}+x_{\mathrm{jk}}\le 1,j\in \{1,3,4,5,6\},1\le k\le min(2,j)$$

(45)

$$x_{4k}+x_{\mathrm{jk}}\le 1,j\in \{1,2,3,5,6\},1\le k\le min(4,j)$$

(46)

$$x_{\mathrm{ij}}\in \{0,1\},i\le j\in \mathbf{n}$$

(47)

$$y_k\in \{0,1\},k\in \mathbf{m}$$

(48)

In total, this simple example has 27 variables, 6 linear equalities and 35 linear inequalities. The number of linear inequalities obtained by C3 is 23. The problem is solved by MATLAB with a PC with Intel(R) i7-4600U CPU @2.10 GHz, 2.70 GHz, and 16.0 GB installed memory (RAM). The computation time is 0.0135 s. Table 6 shows the final result of the coarsest quasi-congruence relation for M2, and its state partition is $\pi =\{\{q_1,q_3\},\{q_2\},\{q_4\},\{q_5,q_6\}\}$ , as shown in Figure 2. All the states in a dotted box represent a coset. Figure 3 further illustrates the simplified quotient automaton of M2. The abstracted model is a nondeterministic finite automaton, because there are unobservable transitions from states 0 and 2 to state 3. This suggests that the selected observable event set is not proper for simplifying the original DFA as a smaller DFA. In this case, we may need to consider re-selecting an observable event set. ³² Finally, the coarsest quasi-congruence is also computed by the standard method in TCT and the result confirms the correctness of the new BLP approach.

Table 6.

Allocation matrix $X_{6\times 6}$ of M2.

$X_{6\times 6}$	$C_1$	$C_2$	$C_3$	$C_4$	$C_5$	$C_6$
$q_1$	1	0	0	0	0	0
$q_2$	0	1	0	0	0	0
$q_3$	1	0	0	0	0	0
$q_4$	0	0	1	0	0	0
$q_5$	0	0	0	1	0	0
$q_6$	0	0	0	1	0	0

Figure 2.

M2 model abstraction based on ${\Sigma }_o=\{\alpha ,\gamma \}$ .

Figure 3.

The quotient automaton of M2 with respect to ${\Sigma }_o=\{\alpha ,\gamma \}$ .

Comparisons of computation methods

This section compares the computation results of three different methods: the classical graph-partition method^1,45 implemented in TCT, and the binary linear programming method proposed in this paper which are respectively implemented by mixed integer linear programming (MILP) ⁵⁵ in MATLAB and binary linear programming in CPLEX (BLP).

Table 7 is a comparison of computing the supremal quasi-congruence relations on the basis of different observable event sets of the automaton M2 by using the stated three methods. Column 1 lists different sets of observable events. Column 2 lists the result using the graph-based partition method implemented in TCT ⁴⁵ for each ${\Sigma }_o$ . Column 3 lists the assumed $m$ value, where each $m$ is equal to 6 for comparison of calculation results. Column 4 shows the size of the linear inequalities C3 obtained by Algorithm 1. Since the size of constraints C3 (Number of linear inequalities × Number of variables) is the main factor that affects the computation time of the method proposed in the paper, it is necessary to analyze the relationship between its size and running time. Columns 5–6 show the running time using two different methods, the MILP method in MATLAB and the BLP method implemented by calling CPLEX Studio 12.8 in MATLAB. Note that when the running time of BLP method is less than 0.01 s, the system automatically reduces it to 0.00 s. The computation results are summarized as follows.

• The computational results using MILP and BLP methods are the same as that of using the computation software TCT.

• On different sets of observable events, when $m$ is invariant, the scale of linear inequalities C3 is not necessarily the same.

• In general, however, the smaller the constraint size is, the shorter the run time will be. Moreover, the smaller the number of observable events is, the smaller the number of cosets will be.

Table 7.

Computation results of M2 based on different ${\Sigma }_o$ .

${\Sigma }_o$	TCT	$m$	Size of C3	Time/s
				MILP	BLP
$\{\alpha ,\beta ,\gamma \}$	5	6	$34\times 27$	0.0171	0.01
$\{\alpha ,\beta \}$	4	6	$193\times 27$	0.0237	0.01
$\{\beta ,\gamma \}$	4	6	$169\times 27$	0.0304	0.01
$\{\alpha ,\gamma \}$	4	6	$29\times 27$	0.0135	0.01
$\{\alpha \}$	2	6	$104\times 27$	0.0142	0.00
$\{\beta \}$	3	6	$135\times 27$	0.0159	0.00
$\{\gamma \}$	2	6	$92\times 27$	0.0151	0.00

Table 8 summarizes the computation results for a few large examples. Column 1 lists the automata of different sizes, including the corresponding size of state space $n$ , the size of event set $|\Sigma |$ and different observable event sets ${\Sigma }_o$ . Columns 2–3 respectively list the real number of cosets of the coarsest quasi-congruence $|\mathrm{QC}|$ and the number of cosets assumed $m$ ( $m\le n$ ). Column 4 shows the size of constraints C3 (Number of linear inequalities × Number of variables). Columns 5–6 show the calculation time for two different methods: MILP method and BLP method. Each line represents the results of different $m$ assumed for the same automaton. In the first column of Table 8, M3 and M4 are created by ourselves to test the algorithm. M3 has 21 states, 22 events, and 26 transitions. M4 has 54 states, 53 events, and 100 transitions. We have the following observations from Table 8.

• For the same automaton and the same observable event set, a tight estimate of $m$ is important. A smaller $m$ generally results in less computation time. On the other hand, if $m$ is less than the real minimum, the binary linear programming problem is infeasible.

• As the state space increases, the calculation time and memory consumption of MILP method also increase, mainly due to the increase of the number of linear inequality constraints C3. When the automaton is not large, the MILP method is efficient.

• The BLP method is more efficient than MILP method under the same conditions.

Table 8.

Comparison of calculation results.

Example	$|\mathrm{QC}|$	$m$	Size of C3	Time/s
				MILP	BLP
SMALLFACT 32		12	$157\times 90$	0.0503	0.02
$n=12$ , $|\Sigma |=9$	3	6	$129\times 63$	0.0302	0.02
${\Sigma }_o=\{12,22,32\}$		3	$78\times 36$	0.0204	0.00
M3		21	$1261\times 252$	73.0757	0.06
$n=21$ , $|\Sigma |=22$	8	10	$1092\times 175$	8.5508	0.05
${\Sigma }_o=\{13,31,53,71,81\}$		8	$975\times 148$	1.6661	0.03
M3		21	$3312\times 252$	55.7098	1.66
$n=21$ , $|\Sigma |=22$	8	10	$1620\times 175$	10.6396	0.42
${\Sigma }_o=\{15,33,55,75\}$		8	$1310\times 148$	2.4277	0.25
M3		21	$995\times 252$	0.1757	0.02
$n=21$ , $|\Sigma |=22$	3	10	$905\times 175$	0.1579	0.01
${\Sigma }_o=\{51\}$		3	$387\times 63$	0.0249	0.01
M4		54	$8121\times 1539$	1.7758	0.19
$n=54$ , $|\Sigma |=53$	3	27	$6750\times 1134$	1.4337	0.17
${\Sigma }_o=\{15,25,35,45\}$		3	$1002\times 162$	0.0248	0.02
M4		54	$10446\times 1539$	35.7073	0.38
$n=54$ , $|\Sigma |=53$	4	10	$3885\times 505$	0.9188	0.11
${\Sigma }_o=\{28,38,48\}$		4	$1662\times 214$	0.1867	0.05
M4		54	$19519\times 1539$	7209.08	1.05
$n=54$ , $|\Sigma |=53$	10	27	$16969\times 1134$	7200.51	0.90
${\Sigma }_o=\{10,16,41,50,52\}$		10	$9350\times 505$	7199.90	0.66
FMS 50
$n=180$ , $|\Sigma |=13$
${\Sigma }_o=\{211,231,241\}$	3	3	$276732\times 540$	328.5743	102.05
${\Sigma }_o=\{230,251,371\}$	6	6	$877048\times 1071$	10,138.733	901.29
PRODCELL 28
$n=2478$ , $|\Sigma |=23$	2	2	$1503438\times 4957$	18.3476	0.94
${\Sigma }_o=\{610\}$

An application

The proposed model abstraction method is applied to simplify the supremal nonblocking supervisor of a manufacturing system with five automated guided vehicles (AGVs),^1,51 as shown in Figure 4. The simplified supervisor model exposes the control logic hidden in the original large automaton model. The manufacturing system has two input stations IPS1 and IPS2 for parts of types 1, 2; three workstations WS1, WS2, and WS3, each containing a conveyor belt; one completed parts station CPS; and five AGVs. The five AGVs alternately load and unload parts on their own fixed circular routes.

Figure 4.

The AGVs system.

The system model consists of five automaton models of the five AGVs, eight automaton models of control specifications.

• Figure 5 shows the automaton models of the five AGVs. The states corresponding to the physical zones are illustrated as gray rectangles. The solid and dotted lines represent the loading and unloading of each AGV respectively.

• Each of the four shared zones is modeled as an automaton ( $\mathbf{Zon}{\mathbf{e}}_j$ , $j=1,\cdots ,4$ ) that restricts only one AGV in the zone.

• Each of the three workstations is modeled as an automaton ( $\mathbf{W}{\mathbf{S}}_k$ , $k=1,\cdots ,3$ ). WS1 receives type 1 parts via AGV3 and type 2 parts via AGV4, and assembles both into the complete products, which are transferred to CPS via AGV5. WS2 receives type 1 parts via AGV1 and processes them. The finished type 1 parts are transferred to WS1 via AGV3. WS3 receives type 2 parts via AGV2 and processes them. The finished type 2 parts are transferred to WS1 via AGV4.

• The dotted zone of $\mathbf{IPS}$ is modeled as an automaton, which restricts only one AGV inside the zone.

Figure 5.

The automaton models for the five AGVs.

More details of the AGVs system can be found in Wonham and Cai, ¹ Feng and Wonham. ⁵¹ The plant model is the synchronous product of the five AGV models. Note that the two values in parentheses respectively represent the number of states and transitions in the automaton model obtained by each calculation.

$$\mathbf{AGV}:=\mathbf{AG}{\mathbf{V}}_1||\mathbf{AG}{\mathbf{V}}_2||\cdots ||\mathbf{AG}{\mathbf{V}}_5(3072,15360).$$

Compute the specification model ZWISPEC for the whole system by the synchronous product of all individual spec models in Figure 6.

Figure 6.

Eight specification automaton models for the AGVs system.

On this basis, the supremal nonblocking supevisor of the AGVs system is

$$\mathbf{ZWISUP}:=\mathrm{Supcon}(\mathbf{AGV},\mathbf{ZWISUP})(4406,11338).$$

Namely, the full AGVs system consists of 4406 states and 11338 transitions.

The automaton model of the supervisor is too complex to be comprehended. We apply the proposed model abstraction method to simplify the supervisor model so that the control logic becomes clearer. Deadlock arises in many manufacturing systems when the number of being-processed parts in the system is more than a limit. We investigate this limit through the model abstraction method. Type 1 parts enter the system via event $\{11\}$ and type 2 parts via event $\{21\}$ . The completed products exit the system via event $\{51\}$ . So we choose the observable event set as $\{11,21,51\}$ , then compute the supremal quasi-congruence of the supervisor model $\mathbf{ZWISUP}$ using the method proposed in the paper. Finally, we obtain a simplified supervisor model for AGVs system with 22 cosets and 45 transitions.

Figure 7 shows the quotient automaton of $\mathbf{ZWISUP}$ with respect to an observable event set $\{11,21,51\}$ . The simplified model reveals a constraint between events 11 and 21. Event 11 (21) can successively occur at most three times before an occurrence of event 12 (11). The reason is that after three successive occurrences of event 11 (12), there are three type 1 (2) parts in the manufacturing system. One is in WS1 waiting for the assembly with the other type of part, one is in AGV3 (AGV4) waiting to be transferred to WS1, and the last one is in WS2 (WS3). If event 11 (12) would occur once more before the other event occurs, AGV1 (AGV2) would have to park within the shared zone IPS, because WS2 (WS3) is full. Then AGV2 (AGV1) cannot enter the input station IPS2 (IPS1). The final product can never be assembled at WS1 and deadlock thus arises.

Figure 7.

The quotient automaton of $\mathbf{ZWISUP}$ with respect to $\{11,21,51\}$ .

Conclusions

In this paper, an optimization process is designed to automatically convert the computation of the coarsest quasi-congruence into a binary linear problem. Partitioning states to cosets is formalized as a binary allocation matrix $X_{n\times m}$ , where $n$ is the number of states, $m$ is an estimated number of cosets. Evidently $m\le n$ . The task of finding the coarsest quasi-congruence is equivalent to the objective of finding the least number of cosets. To reduce the computation time, the translation process is also optimized by introducing fewer decision variables and simplifying constraints in the formulas. The computational efficiency and correctness of this method are verified by two different solvers. Therefore, the proposed method is not only a new solution for the coarsest quasi-congruence computation, but also provides us a more intuitive understanding of the quasi-congruence relation in the supervisory control theory.

A future direction is to apply more computationally efficient solvers, such as satisfiability modulo theories (SMT) and SAT, to compute the optimal state-to-coset allocation problem. Another direction is to apply the same method to compute model abstraction of finite automata with variables, namely the extended finite automata which are easily applicable to the real industrial scale problems.