Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions

TL;DR

This paper presents a new predicate abstraction approach for max-plus linear systems, enabling efficient bounded model checking of time-difference specifications and providing explicit bounds on verification completeness.

Contribution

It introduces an automatic predicate abstraction method for MPL systems and enhances BMC with explicit completeness bounds based on system properties.

Findings

Predicate abstractions improve verification efficiency.

Explicit bounds on completeness threshold are derived.

Experimental results show superiority over existing algorithms.

Abstract

This paper introduces the abstraction of max-plus linear (MPL) systems via predicates. Predicates are automatically selected from system matrix, as well as from the specifications under consideration. We focus on verifying time-difference specifications, which encompass the relation between successive events in MPL systems. We implement a bounded model checking (BMC) procedure over a predicate abstraction of the given MPL system, to verify the satisfaction of time-difference specifications. Our predicate abstractions are experimentally shown to improve on existing MPL abstractions algorithms. Furthermore, with focus on the BMC algorithm, we can provide an explicit upper bound on the completeness threshold by means of the transient and the cyclicity of the underlying MPL system.

Tables

Table 1. Table 1: Average and maximal running times of abstraction procedures

$n$	Tropical Abstractions from [29]	Predicate Abstractions (this work)
3	$\{0.15,0.21\}\left[\text{ms}\right]$	$\{0.27,0.38\}\left[\text{ms}\right]$
4	$\{0.26,0.35\}\left[\text{ms}\right]$	$\{0.49,0.72\}\left[\text{ms}\right]$
5	$\{0.41,0.44\}\left[\text{ms}\right]$	$\{0.79,0.88\}\left[\text{ms}\right]$
6	$\{1.12,1.20\}\left[\text{ms}\right]$	$\{1.92,2.10\}\left[\text{ms}\right]$
7	$\{2.68,3.74\}\left[\text{ms}\right]$	$\{3.19,4.60\}\left[\text{ms}\right]$
8	$\{8.78,10.02\}\left[\text{ms}\right]$	$\{9.13,13.74\}\left[\text{ms}\right]$
9	$\{32.12,36.66\}\left[\text{ms}\right]$	$\{30.38,42.02\}\left[\text{ms}\right]$
10	$\{0.12,0.14\}\left[\text{sec}\right]$	$\{0.11,0.17\}\left[\text{sec}\right]$
11	$\{0.57,0.66\}\left[\text{sec}\right]$	$\{0.54,0.81\}\left[\text{sec}\right]$
12	$\{3.82,4.67\}\left[\text{sec}\right]$	$\{2.58,4.19\}\left[\text{sec}\right]$
13	$\{23.71,28.28\}\left[\text{sec}\right]$	$\{15.80,28.52\}\left[\text{sec}\right]$
14	$\{1.39,1.59\}\left[\text{min}\right]$	$\{0.89,1.27\}\left[\text{min}\right]$
15	$\{27.73,31.06\}\left[\text{min}\right]$	$\{4.68,8.40\}\left[\text{min}\right]$

Table 2. Table 2: The comparison of completeness thresholds.

$n$	$\#\mathrm{𝚜𝚝𝚏}$		$\#\left({\mathrm{𝚌𝚝}}_1={\mathrm{𝚌𝚝}}_2\right)$	$\#\left({\mathrm{𝚌𝚝}}_1>{\mathrm{𝚌𝚝}}_2\right)$
3	$14$	$0$	1	13
4	$15$	$1$	0	14
5	$14$	$0$	0	14

Equations

$$[A\oplus B](i,j)$$

$$[A\otimes C](i,j)$$

$$\text{x}(k+1)=A\otimes \text{x}(k),$$

$$\text{x}(k+1)=\left[\begin{array}{cc}2& \text{leavevmode}5\\ 3& \text{leavevmode}3\end{array}\right]\otimes \text{x}(k).$$

$${\mathsf{R}}_{\text{g}}=\bigcap _{i=1}^n\bigcap _{j=1}^n\left\{\text{x}\in {\mathbb{R}}^n|x_{g_i}-x_j\ge A(i,j)-A(i,g_i)\right\}.$$

$$x_i(k+1)=x_{g_i}(k)+A(i,g_i),\text{leavevmode}\text{leavevmode}i=1,\dots ,n.$$

$$t_i(k)$$

$$\phi :=\text{true}\text{leavevmode}|\text{leavevmode}a\text{leavevmode}|\text{leavevmode}{\phi }_1\wedge {\phi }_2\text{leavevmode}|\text{leavevmode}\neg \phi \text{leavevmode}|\text{leavevmode}◯\phi \text{leavevmode}|\text{leavevmode}{\phi }_1\text{leavevmode}\mathsf{U}\text{leavevmode}{\phi }_2,$$

$$[A^{\otimes (k+c)}\text{x}-A^{\otimes k}\otimes \text{x}{]}_i=\sum _{j=1}^c[A^{\otimes (k+j)}\text{x}-A^{\otimes (k+j-1)}\otimes \text{x}{]}_i\ge c\alpha$$

Full text

1 Introduction

Max-Plus-Linear (MPL) systems are a class of discrete-event systems, with dynamics based on two binary operations (maximisation and addition) over a max-plus semiring. MPL systems are used to model synchronisation phenomena without concurrency. These systems have been used in many areas, such as manufacturing [27], transportation [24], and biological systems [10, 18].

Classical analysis of MPL systems is conducted using algebraic approaches [4, 24]. Recently, an alternative take based on formal abstractions has been developed to verify MPL systems against quantitative specifications [1] that are general and expressive. The performance and scalability of the abstraction approach has been later improved by employing tropical operations [29] that are native to the max-plus semiring.

This work pushes the envelop on scalability of formal abstractions of MPL systems. We newly apply predicate abstractions (PA) and bounded model checking (BMC) for the verification of MPL systems over time-difference specifications. Predicate abstractions are an abstraction approach that leverage a set of predicates, and have been classically used for software and hardware verification [21, 16], for the abstraction of programs [15, 6], and for reachability analysis of hybrid systems [3].

BMC is a symbolic model checking approach that leverages SAT solvers. The basic idea is to attempt finding counterexamples with a length bounded by some integer. If no counterexamples are found, the length is greedily increased. The approach is sound (counterexamples are correct), and complete (no counterexamples are admitted) whenever a completeness threshold (CT) for the length is reached [8, 9]. Whilst there exist results on correct upper-bounds on the CT, in practice BMC is run until the underlying problem becomes intractable.

This paper has two specific contributions. The first contribution is related to the abstraction approach. Moving beyond [1, 29], where the abstraction procedures are based on the translation of MPL systems into piecewise affine (PWA) systems, in this work we newly employ PA. Namely, we determine a set of predicates such that the dynamics within each partitioning region is affine. In other words, there is no need to compute PWA systems anymore.

The second contribution is related to the model-checking approach. [1] employs standard model checking to verify the abstract transition system. In this paper, we leverage BMC: notice that PA naturally yield Boolean encodings that can be relevant for the SAT-based BMC procedure. We focus on time-difference specifications. Since we are working on abstractions, counterexample generated by the BMC procedure needs to be checked for spuriousness (cf. Algorithm 5 and Algorithm 6). Whenever a counterexample is spurious, we refine the abstract transition using the procedure in [2], combined with lazy abstraction [26]. Finally, for the considered time-difference specifications, we show that the CT can be upper-bounded by means of the transient and cyclicity of the concrete MPL system - such bounds are in general tighter than those obtained working on the abstract transition system. As a side result, we provide a few instance of “direct verification”, where the model checking of MPL models can be performed straightforwardly for time-difference specifications.

The paper is organised as follows. Section 2 describes the basics of models, abstraction techniques and temporal logic formulae used in this work. It also contains the notion of time-difference over MPL systems. The contributions of this paper are contained in Sections 3 and 4. The comparison of abstraction procedures is presented in Section 5, with PA implemented in C++ and model checking run over NuSMV [11]. We also compare the completeness threshold w.r.t. transient and cyclicity of MPL systems with those that are computed by NuSMV. The paper is concluded in Section 6.

2 Model and Preliminaries

2.1 Max-Plus Linear Systems

By max-plus semiring we understand an algebraic structure $(\mathbb{R}_{\max},\oplus,\otimes)$ where $\mathbb{R}_{\max}:=\mathbb{R}\cup\{\varepsilon:=-\infty\}$ and $a\oplus b:=\max\{a,b\},\leavevmode\nobreak\ a\otimes b:=a+b\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \forall a,b\in\mathbb{R}_{\max}.$ The set of $n\times m$ matrices over max-plus semiring is denoted as $\mathbb{R}_{\max}^{n\times m}$. Two binary operations of a max-plus semiring can be extended to matrices as follows

[TABLE]

where $A,B\in\mathbb{R}_{\max}^{n\times m},C\in\mathbb{R}_{\max}^{m\times p}$. Given $r\in\mathbb{N}$, the max-plus algebraic power of $A\in\mathbb{R}_{\max}^{n\times n}$ is denoted by $A^{\otimes r}$ and corresponds to $A\otimes\ldots\otimes A$ ($r$ times).

A Max-Plus Linear (MPL) system is defined as

[TABLE]

where $A\in\mathbb{R}_{\max}^{n\times n}$ is the system matrix and $\textbf{x}(k)=[x_{1}(k)\ldots x_{n}(k)]^{\top}$ is the state variables [4]. In particular, for $i\in\{1,\ldots,n\}$, $x_{i}(k+1)=\max\{A(i,1)+x_{1}(k),\ldots,A(n,i)+x_{n}(k)\}$. In applications, x represents the time stamps of the discrete events, while $k$ corresponds to the event counter. Therefore, it is more convenient to take $\mathbb{R}^{n}$ (instead of $\mathbb{R}_{\max}^{n}$) as the state space.

Definition 1 (Precedence Graph [4]).

The precedence graph of $A$, denoted by $\mathcal{G}(A)$, is a weighted directed graph with nodes $1,\ldots,n$ and an edge from $j$ to $i$ with weight $A(i,j)$ if $A(i,j)\neq\varepsilon$. $\square$

Definition 2 (Regular Matrix [24]).

A matrix $A\in\mathbb{R}_{\max}^{n\times n}$ is called regular if there is at least one finite element in each row. $\square$

Definition 3 (Irreducible Matrix [4]).

A matrix $A\in\mathbb{R}_{\max}^{n\times n}$ is called irreducible if the corresponding precedence graph $\mathcal{G}(A)$ is strongly connected. $\square$

Recall that a directed graph is strongly connected if for two different nodes $i,j$ of the graph, there exists a path from $i$ to $j$ [4, 20]. The weight of a path $p=i_{1}i_{2}\ldots i_{k}$ is equal to the total weight of the corresponding edges i.e. $|p|=A(i_{2},i_{1})+\ldots+A(i_{k},i_{k-1})$. A circuit, namely a path that begins and ends at the same node, is called critical if it has maximum average weight, which is the weight divided by the length of path [4].

Every irreducible matrix $A\in\mathbb{R}_{\max}^{n\times n}$ admits a unique max-plus eigenvalue $\lambda\in\mathbb{R}$, which corresponds to the weight of critical circuit in $\mathcal{G}(A)$. Furthermore, by 1 next, $A$ satisfies the so-called transient condition:

Proposition 1 (Transient Condition[4]).

For an irreducible matrix $A\in\mathbb{R}_{\max}^{n\times n}$ and its corresponding max-plus eigenvalue $\lambda\in\mathbb{R}$, there exist $k_{0},c\in\mathbb{N}$ such that $A^{\otimes(k+c)}=\lambda c\otimes A^{\otimes k}$ for all $k\geq k_{0}$. The smallest such $k_{0}$ and $c$ are called the transient and the cyclicity of $A$, respectively. $\square$

Example 1.

Consider a $2\times 2$ MPL system that represents a simple railway network [24]:

[TABLE]

Its max-plus eigenvalue is $\lambda=4$, whereas the transient and cyclity for the matrix are $k_{0}=c=2$. $\square$

Any given MPL system can be translated into a Piece-Wise Affine (PWA) system [23]. A PWA system comprises of spatial regions with corresponding PWA dynamics. The regions are generated from all possible coefficients $\textbf{g}=(g_{1},\ldots,g_{n})\in\{1,\ldots,n\}^{n}$, which satisfies $A(i,g_{i})\neq\varepsilon$ for $1\leq i\leq n$. As shown in [1], the region corresponding to g is

[TABLE]

One could check that for each non-empty $\mathsf{R}_{\textbf{g}}$ and $\textbf{x}(k)\in\mathsf{R}_{\textbf{g}}$, the MPL system (1) can be rewritten as the following affine dynamics:

[TABLE]

Notice that (4) can be expressed as $\textbf{x}(k+1)=A_{\textbf{g}}\otimes\textbf{x}(k)$, where $A_{\textbf{g}}$ is a region matrix [29] for the coefficient g.

2.2 Time Differences in MPL Systems

We consider delays occurring between events governed by (1). Delays can describe the difference of two events corresponding to the same event counter but at different variable indices (i.e. $x_{i}(k)-x_{j}(k)$), or the difference of two consecutive events for the same index (i.e. $x_{i}(k+1)-x_{i}(k)$). This paper focuses on the later case although, in general, the results of this paper can be applied to the former case.

We write the $(k+1)^{\text{th}}$ time difference for the $i^{\text{th}}$ component as $t_{i}(k)=x_{i}(k+1)-x_{i}(k)$. One can see that

[TABLE]

where $\texttt{fin}_{i}$ is the set containing the indices of finite elements of $A(i,\cdot)$.111For the sake of simplicity, we write the elements of $\texttt{fin}_{i}$ in a strictly increasing order.

2.3 Transition Systems and Linear Temporal Logic

Definition 4 (Transition System [5]).

A transition system is formulated by a tuple $(S,T,I,\mathcal{AP},L)$, where

• $\bullet$

$S$ is a set of states,

• $\bullet$

$T\subseteq S\times S$ is a transition relation,

• $\bullet$

$I\subseteq S$ is a set of initial states,

• $\bullet$

$\mathcal{AP}$ is a set of atomic propositions, and

• $\bullet$

$L:S\rightarrow 2^{\mathcal{AP}}$ is a labelling function. $\square$

A path of $TS$ is defined as a sequence of states $\pi=s_{0}s_{1}\ldots$, where $s_{0}\in I$ and $(s_{i},s_{i+1})\in T$ for all $i\geq 0$. We denote $\pi[i]=s_{i-1}$ as the $i^{\text{th}}$ state of $\pi$. Furthermore, $|\pi|$ represents the number of transitions in $\pi$.

Linear temporal logic (LTL) is one of the predominant logics that are used for specifying properties over the set of atomic propositions [5]. LTL formulae are recursively defined as follows.

Definition 5 (Syntax of LTL [5]).

LTL formulae over the set of atomic propositions $\mathcal{AP}$ are constructed according to the following grammar:

[TABLE]

where $a\in\mathcal{AP}$. $\square$

The symbol $\bigcirc$ (next) and $\mathsf{U}$ (until) are called temporal operators. Two additional operators, $\lozenge$ (eventually) and $\square$ (always), are generated via the until operators: $\lozenge\varphi=\text{true}\leavevmode\nobreak\ \mathsf{U}\leavevmode\nobreak\ \varphi\leavevmode\nobreak\ \leavevmode\nobreak\ \text{and}\leavevmode\nobreak\ \leavevmode\nobreak\ \square\varphi=\neg\lozenge\neg\varphi$. We refer to [5] for the semantics of LTL formulae including the satisfaction relation $\models$ over transition systems.

2.4 Abstractions and Predicate Abstractions

Abstractions are techniques to generate a finite and smaller model from a large or even infinite-space (i.e., a continuous-space model, e.g., an MPL system) model. Abstractions can reduce the verification of a temporal property $\varphi$ over the original model (a concrete model with state space $S$), to checking a related property on a simpler abstract model (over $\hat{S}$) [5]. The mapping from $S$ to $\hat{S}$ is called abstraction function.

From a (concrete) transition system $TS=(S,T,I,\mathcal{AP},L)$ and an abstraction function $f:S\rightarrow\hat{S}$, the (abstract) transition system $TS_{f}=(\hat{S},T_{f},I_{f},\mathcal{AP},L_{f})$ is generated from $TS$ as follows: i) $I_{f}=\{f(s)\mid s\in I\}$, ii) $(f(s)$,$f(s^{\prime}))\in T_{f}$ if $(s,s^{\prime})\in T$, and iii) $L_{f}(f(s))=L(s)$, for all $s\in S$.

The important relation between $TS$ and $TS_{f}$ is that the former is simulated by the latter (which is denoted by $TS\preceq TS_{f})$. In detail, all behaviour on concrete transition system occur on the abstract one. The formal definition of simulation relation can be found in [5, Definition 7.47]. Furthermore, given an LTL formula $\varphi$, $TS_{f}\models\varphi$ implies $TS\models\varphi$ [5, 13].

Predicate abstractions [22, 17, 13, 19] denote abstraction methods that use a set of predicates $P=\{p_{1},\ldots,p_{k}\}$ to characterise the abstract states. Predicates are identified from the concrete model, and possibly from the specification(s) under consideration. Each predicate $p_{i}$ corresponds to a Boolean variable $b_{i}$ and each abstract state $\hat{s}\in\hat{S}$ corresponds to a Boolean assignment of these $k$ Boolean variables [13]. Therefore, we obtain that $|\hat{S}|\leq 2^{k}$. An abstract state will be labelled with predicate $p_{i}$ if the corresponding $b_{i}$ is true in that state. For this reason, predicates also serve as atomic propositions [13].

The predicates are also used to define an abstraction function between the concrete and abstract state spaces. A concrete state $s\in S$ will be related to an abstract state $\hat{s}\in\hat{S}$ iff the truth value of $p_{i}$ on $s$ equals the value of $b_{i}$ on $\hat{s}$. The abstraction function for predicate abstractions is defined as $f(s)=\bigwedge_{i=1}^{k}\text{val}(s,p_{i})$, where $\text{val}(s,p_{i})=b_{i}$ if $p_{i}$ is satisfied in $s$, otherwise $\neg b_{i}$.

3 Predicate Abstractions of MPL Systems

3.1 Related Work

The notion of abstractions of an MPL system has been first introduced in [1]: there, it leverages translation of an MPL system into the corresponding PWA system. The resulting abstract states are expressed as Difference-Bound Matrices (DBM). A more efficient procedure for MPL abstractions via max-plus algebraic operations is later discussed in [29].

3.2 Generation of the Predicates

Considering an abstraction via a set of predicates, the first issue is to find appropriate predicates. Recall that related abstraction techniques [1, 29] explore the connection between MPL and PWA systems and use DBMs to represent the abstract states. Similarly, predicates here are chosen such that the dynamics in the resulting abstract states are affine as in (3) and can be expressed as DBMs. Following these considerations, the predicates are defined as an inequality $p\equiv x_{i}-x_{j}\sim c$ where $\sim\hskip 4.30554pt\in\{>,\geq\},c\in\mathbb{R}$222In this paper, we always use $p\equiv x_{i}-x_{j}\geq c$ as a predicate.. For simplicity, we may write a predicate as a tuple $p\equiv(i,j,c,s)$ where $s=1$ if $\sim\leavevmode\nobreak\ =\leavevmode\nobreak\ \geq$, otherwise $s=0$. The negation of $p$ then can be written as $\neg p\equiv(j,i,-c,1-s)$.

From the PWA region in (3), $c$ can be chosen from the difference of two finite elements of the state matrix $A\in\mathbb{R}_{\max}^{n\times n}$ at the same row. In detail, if $A(k,j)\neq\varepsilon$ and $A(k,i)\neq\varepsilon$ with $i<j$ and $1\leq k\leq n$, then we get a predicate $(i,j,A(k,j)-A(k,i),1)$.

Algorithm 1 shows a procedure to generate the predicates from an MPL system. For each $k\in\{1,\ldots,n\}$, $P_{k}$ is a set of predicates generated from $A(k,\cdot)$. If there are exactly $m>1$ finite elements at each row of $A$ then $|P_{k}|=\binom{m}{2}$ and in general $|\bigcup_{k=1}^{n}P_{k}|\leq n\binom{m}{2}$: indeed, it is possible to get the same predicate from two different rows when $A(k_{1},j)-A(k_{1},i)=A(k_{2},j)-A(k_{2},i)$ for $k_{1}\neq k_{2}$.

As mentioned before, predicates can also be associated to given specifications. In this paper, we focus on time-difference specifications that are generated from a set of time-difference propositions. For $\alpha\in\mathbb{R}$, we define a time-difference proposition ‘$t_{i}\sim\alpha$’ to reason the condition that $x_{i}^{\prime}-x_{i}\sim\alpha$. We remove the counter event $k$ for the sake of simplicity.

One can rewrite (5) as $t_{i}=\max_{{j^{\ast}}\in\texttt{fin}_{i}}\{x_{{j^{\ast}}}+A(i,{{j^{\ast}}})\}-x_{i}$. Therefore, from $t_{i}\sim\alpha$ for $\sim\hskip 4.30554pt\in\{>,\geq,<,\leq\}$ we have $\max_{{j^{\ast}}\in\texttt{fin}_{i}}\{x_{{j^{\ast}}}+A(i,{{j^{\ast}}})\}-x_{i}\sim\alpha$. The number of predicates corresponding to ‘$t_{i}\sim\alpha$’ is bounded by $|\texttt{fin}_{i}|$. For each $j^{\ast}\in\texttt{fin}_{i}$ we get a predicate $x_{j^{\ast}}-x_{i}\sim\alpha-A(i,j^{\ast})$. However, in case of $i\in\texttt{fin}_{i}$, or in other words $A(i,i)\neq\varepsilon$, $x_{i}-x_{i}\sim\alpha-A(i,j^{\ast})$ is not a predicate. Algorithm 2 shows how to generate the predicates w.r.t. a time-difference proposition.

3.3 Generation of Abstract States

This section starts by describing the procedure to generate abstract states via a set of predicates. We denote $P$ as the set of predicates generated by Algorithm 1 and Algorithm 2, i.e. $P=P_{mat}\cup P_{time}=\{p_{1},\ldots,p_{k}\}$. Let $\hat{S}$ be a set of abstract states defined over Boolean variables $B=\{b_{1},\ldots,b_{k}\}$, where the truth value of $b_{i}$ depends on that of $p_{i}$. For each Boolean variable $b_{i}$, we define the corresponding DBM as follows: $\texttt{DBM}(b_{i})=\{\textbf{x}\in\mathbb{R}^{n}\mid p_{i}\leavevmode\nobreak\ \text{is true in}\leavevmode\nobreak\ \textbf{x}\}$ and $\texttt{DBM}(\neg b_{i})=\{\textbf{x}\in\mathbb{R}^{n}\mid p_{i}\leavevmode\nobreak\ \text{is false in}\leavevmode\nobreak\ \textbf{x}\}$. One can show that $\texttt{DBM}(b_{i}\wedge b_{j})=\texttt{DBM}(b_{i})\cap\texttt{DBM}(b_{j})$.

Algorithm 3 shows the steps to generate the abstract states of an MPL system given a set of predicates $P$. For each $i\in\{1,\ldots,|P|\}$, we manipulate DBMs: the complexity of Algorithm 3 depends on emptiness checking of DBM (line 11), which runs in $\mathcal{O}(n^{3})$, where $n$ is the dimension of the state matrix [1]. Therefore, the worst-case complexity of Algorithm 3 is $\mathcal{O}(2^{|P|}n^{3})$.

3.4 Generation of Abstract Transitions

Having obtained the abstract states, one needs to generate the abstract transitions, which can be obtained via one-step reachability, as described in [1]. Namely, there is a transition from $\hat{s}_{i}$ to $\hat{s}_{j}$ if $\mathsf{Im}(\texttt{DBM}(\hat{s}_{i}))\cap\texttt{DBM}(\hat{s}_{j})\neq\emptyset$, where $\texttt{Im}(\texttt{DBM}(\hat{s}_{i}))=\{A\otimes\textbf{x}\mid\textbf{x}\in\texttt{DBM}(\hat{s}_{i})\}$. The computation of $\texttt{Im}(\texttt{DBM}(\hat{s}_{i}))$ corresponds to the image of $\texttt{DBM}(\hat{s}_{i})$ w.r.t. the affine dynamics of $\hat{s}_{i}$ which has complexity $\mathcal{O}(n^{2})$ [29].

However, unlike [29, Algorithm 2], Algorithm 3 does not produce the affine dynamics for each abstract state. For each $\hat{s}\in\hat{S}$, we need to find g as in (4). One can generate the affine dynamics for $\hat{s}\in\hat{S}$ from the value (either true or false) of $p\in P_{mat}$ on $\hat{s}$. Given a predicate $p\equiv(i,j,c,s)$, we call $i$ and $j$ as the left and right index of $p$ (as $x_{i}\sim x_{j}+c$) and denoted them by $\texttt{left}(p)$ and $\texttt{right}(p)$, respectively.

If $p\equiv(i,j,A(k,j)-A(k,i),1)$ is true in $\hat{s}$, we have $x_{i}+A(k,i)\geq x_{j}+A(k,j)$, otherwise $x_{j}+A(k,j)>x_{i}+A(k,i)$. Hence, the left index of predicates can be used to determine the affine dynamics. Algorithm 4 provides the procedure to find the affine dynamic associated to $\hat{s}\in\hat{S}$.

For each $k$, $\texttt{fin}_{k}$ is computed. Initially, the elements of $\texttt{fin}_{k}$ are in strictly increasing order. Then, for each predicate $p\in P_{k}$, we swap the location of $\texttt{left}(p)$ and $\texttt{right}(p)$ whenever $p$ is false on $\hat{s}$. Suppose $i$ is the first element of $\texttt{fin}_{k}$ after swapping. One could show that $x_{i}+A(k,i)\sim x_{j}+A(k,j)$ for all $j\in\texttt{fin}_{k}\setminus\{i\}$.

3.5 Model Checking MPL Systems over Time-Difference Specifications: Direct Verification

This section discusses the verification of MPL systems over time-difference specifications. First, we define a (concrete) transition system w.r.t. a given MPL system.

Definition 6 (Transition system associated with MPL system).

A transition system $TS$ for an MPL system in (1) is a tuple $(S,T,\mathcal{X},\mathcal{AP},L)$ where

• $\bullet$

the set of states $S$ is $\mathbb{R}^{n}$,

• $\bullet$

$(\textbf{x},\textbf{x}^{\prime})\in T$ if $\textbf{x}^{\prime}=A\otimes\textbf{x}$,

• $\bullet$

$\mathcal{X}\subseteq\mathbb{R}^{n}$ is a set of initial conditions,

• $\bullet$

$\mathcal{AP}$ is a set of time-difference propositions,

• $\bullet$

the labelling function $L:S\rightarrow 2^{\mathcal{AP}}$ is defined as follows: a state $\textbf{x}\in S$ is labeled by ‘$t_{i}\sim\alpha$’ if $[A\otimes\textbf{x}-\textbf{x}]_{i}\sim\alpha$, where $\sim\leavevmode\nobreak\ \in\{>,\geq,<,\leq\}$. $\square$

We express the time-difference specifications as LTL formulae over a set of time-difference propositions.333Notice that, in 6 we consider $\mathcal{AP}$ as a set of time-difference propositions. For instance, $\bigcirc(t_{i}\leq\alpha)$ represents ‘the next time difference for the $i^{\text{th}}$ component is $\leq\alpha$’ while $\lozenge\square(t_{i}\leq\alpha)$ corresponds to ‘after some finite executions, the time difference for the $i^{\text{th}}$ component is always $\leq\alpha$’. To check the satisfaction of these specifications, we generate the abstract version of MPL system.

The abstract transition system $TS_{f}=(\hat{S},T_{f},I_{f},P_{mat}\cup P_{time},L_{f})$ for an MPL system is generated via predicate abstraction where $P_{mat}$ and $P_{time}$ is the set of predicates generated by Algorithm 1 and Algorithm 2, respectively. The (abstract) labelling function $L_{f}$ is defined over predicates $p\in P_{mat}\cup P_{time}$: for $\hat{s}\in\hat{S}$, $p\in L_{f}(\hat{s})$ iff $p$ is true in $\hat{s}$. We show the relation between predicates in $P_{time}$ and a time-difference proposition in $\mathcal{AP}$.

Proposition 2.

Suppose $P_{time}$ is a set of predicates corresponding to a time-difference proposition ‘$t_{i}\sim\alpha$’ and an abstract state $\hat{s}\in\hat{S}$.

• i.

For $\sim\{>,\geq\}$. A (concrete) state $\textbf{x}\in\texttt{DBM}(\hat{s})$ is labeled by ‘$t_{i}\sim\alpha$’ iff at least one predicate in $P_{time}$ is true in $\hat{s}$.

• ii.

For $\sim\{<,\leq\}$. A (concrete) state $\textbf{x}\in\texttt{DBM}(\hat{s})$ is labeled by ‘$t_{i}\sim\alpha$’ iff all predicates in $P_{time}$ are true in $\hat{s}$.

Proof. We only need to show the proof for $\sim\leavevmode\nobreak\ =\leavevmode\nobreak\ \geq$ and $\sim\leavevmode\nobreak\ =\leavevmode\nobreak\ \leq$.

• i.

Notice that $[A\otimes\textbf{x}-\textbf{x}]_{i}\geq\alpha$ is equivalent to $\max_{{j^{\ast}}\in\texttt{fin}_{i}}\{x_{{j^{\ast}}}+A(i,{{j^{\ast}}})\}\geq x_{i}+\alpha.$ This inequality is satisfied iff at least one of $x_{{j^{\ast}}}+A(i,{{j^{\ast}}})\geq x_{i}+\alpha$ for $j^{\ast}\in\texttt{fin}_{i}$ is true. It is indeed equivalent to a predicate $x_{{j^{\ast}}}-x_{i}\geq\alpha-A(i,{{j^{\ast}}})\in P_{time}$.

• ii.

Now for $[A\otimes\textbf{x}-\textbf{x}]_{i}\leq\alpha$ we have $\max_{{j^{\ast}}\in\texttt{fin}_{i}}\{x_{{j^{\ast}}}+A(i,{{j^{\ast}}})\}\leq x_{i}+\alpha$. This inequality is satisfied iff all inequality $x_{{j^{\ast}}}+A(i,{{j^{\ast}}})\leq x_{i}+\alpha$ are true. Hence, the corresponding predicates are all true. $\square$

Example 2.

Suppose we have an MPL system (2) and $\mathcal{AP}=\{t_{1}\leq 5\}$. We consider two time-difference specifications $\lozenge(t_{1}\leq 5)$ and $\lozenge\square(t_{1}\leq 5)$ and a set of initial conditions $\mathcal{X}=\mathbb{R}^{2}$. By Algorithm 1 and Algorithm 2, we have $P_{mat}=\{(1,2,3,1),(1,2,0,1)\}$ and $P_{time}=\{(1,2,0,1)\}$. Thus, $P=\{p_{1},p_{2}\}$ where $p_{1}\equiv(1,2,3,1)$ and $p_{2}\equiv(1,2,0,1)$.

The resulting abstract transition is depicted in Figure 1. All abstract states are initial. The corresponding LTL formulae for the time-difference specifications are $\lozenge p_{2}$ and $\lozenge\square p_{2}$.

It is clear that $TS_{1}\models\lozenge p_{2}$. Therefore, the underlying MPL system satisfies $\lozenge(t_{1}\leq 5)$. However, $TS_{1}\not\models\lozenge\square p_{2}$ and we can not conclude whether $\lozenge\square(t_{1}\leq 5)$ is false. We will show how to deal with this problem in Section 4. $\square$

3.5.1 Direct Verification

In some cases, it is possible to check the satisfaction of time-difference specifications directly, namely without generating the abstraction of the MPL system. We call a time-difference proposition $t_{i}\sim\alpha$ is a contradiction if there is no $\textbf{x}\in\mathbb{R}^{n}$ such that $[A\otimes\textbf{x}-\textbf{x}]_{i}\sim\alpha$. One the other hand, $t_{i}\sim\alpha$ is a tautology if all $\textbf{x}\in\mathbb{R}^{n}$ satisfy $[A\otimes\textbf{x}-\textbf{x}]_{i}\sim\alpha$.

Proposition 3.

Given an MPL (1) with $A(i,i)=\beta\in\mathbb{R}$.

• i.

For $\sim\{>,\geq\}$, $t_{i}\sim\alpha$ is a tautology if $\beta\sim\alpha$.

• ii.

For $\sim\{<,\leq\}$, $t_{i}\sim\alpha$ is a contradiction if $\alpha<\beta$.

Proof. One could show that the time difference for the $i^{\text{th}}$ element is never smaller than the corresponding diagonal element. In other words, for all $\textbf{x}\in\mathbb{R}$ we have $[A\otimes\textbf{x}-\textbf{x}]_{i}\geq A(i,i)$. Hence, $t_{i}\geq\beta$ is indeed a tautology.

• i.

The condition $\beta\sim\alpha$ implies $t_{i}\sim\alpha$ is also a tautology.

• ii.

Because $t_{i}\geq\beta$ is a tautology then its negation $t_{i}<\beta$ is a contradiction. It is clear that in case of $\alpha<\beta$, $t_{i}\sim\alpha$ is also a contradiction. $\square$

The consequence of 3 is that any time-difference specification defined from a tautology (resp., contradiction) time-difference proposition, is guaranteed to be true (resp., false). For instance, from 2, the specification $(t_{1}\geq 2)\mathsf{U}(t_{2}\geq 3)$ is satisfied, while $\lozenge(t_{2}\leq 2)$ is not. As a second instance of direct verification, in the case of irreducible MPL systems, the dissatisfaction of specifications in the form of $\lozenge\square(t_{i}\sim\alpha)$ is related to the eigenvalue of the corresponding MPL matrix.

Proposition 4.

Consider an MPL system characterised by an irreducible matrix $A\in\mathbb{R}_{\max}^{n\times n}$ and a time-difference specification $\lozenge\square(t_{i}\sim\alpha)$. Suppose $\lambda$ is the max-plus eigenvalue of $A$. The following holds:

• i.

For $\sim\{>,\geq\}$, if $\lambda<\alpha$ then $\lozenge\square(t_{i}\sim\alpha)$ is false.

• ii.

For $\sim\{<,\leq\}$, if $\lambda>\alpha$ then $\lozenge\square(t_{i}\sim\alpha)$ is false.

Proof.

• i.

We proof by contradiction. Let assume $\lozenge\square(t_{i}\geq\alpha)$ is true. Thus, there is an $l\geq 0$ such that $[A^{\otimes(k+1)}\textbf{x}-A^{\otimes k}\otimes\textbf{x}]_{i}\geq\alpha,\leavevmode\nobreak\ \leavevmode\nobreak\ \forall k\geq l.$ On the other hand, by 1, there exists $k_{0},c$ such that $A^{\otimes(k+c)}=c\lambda\otimes A^{\otimes k}$ for all $k\geq k_{0}$. For all $k\geq\max\{k_{0},l\}$ we have

[TABLE]

One could find that the LHS is equal to $c\lambda$. Hence, we have $\lambda\geq\alpha$ which contradicts $\lambda<\alpha$. From the fact that $\lozenge\square(t_{i}\geq\alpha)$ is false, it is clear that the strict version of the formula is also false.

• ii.

Similar proof of part (i).

4 Bounded Model Checking of MPL Systems

In this section, we implement bounded model checking (BMC) algorithm to check the satisfaction of time-difference specifications over MPL system. The basic idea of BMC is to find a bounded counterexample of a given length $k$. If no such counterexample is found, then one increases $k$ by one until a pre-known completeness threshold is reached, or until the problem becomes intractable. The readers are referred to [8, 9, 7] for a more detailed description of BMC.

We use NuSMV 2.6.0 [11] via command check_ltlspec_bmc_onepb to apply BMC. It performs non-incremental BMC to find a counterexample with length $k$. If no such bug is present then the command is reapplied for length $k+1$, otherwise we apply spurious checking (cf. Section 4.1). In case of non-spurious witness, one can conclude that the time-difference specification is false. Otherwise, we refine the transition system (cf. Section 4.2) such that the counterexample is removed and then reapply BMC command for length $k$. This procedure is repeated until we reach a completeness threshold (cf. Section 4.3).

4.1 Checking Spuriousness of Counterexamples

There are two types of $k$-length bounded abstract counterexamples $\pi=\hat{s}_{0}\hat{s}_{1}\ldots\hat{s}_{k}$ in BMC: either no-loop or lasso-shaped paths. The former one can be used to express the violation of invariant properties $\square p$. A lasso-shaped path is $\pi=\hat{s}_{0}\hat{s}_{1}\ldots\hat{s}_{k}$ such that there exists $1\leq l\leq k$ where $s_{l-1}=s_{k}$ [8, 9]. Although it is finite, it can represent an infinite path $\overline{\pi}=(\hat{s}_{0}\hat{s}_{1}\hat{s}_{l-1})(\hat{s}_{l}\ldots\hat{s}_{k})^{\omega}$ where $\hat{s}_{l-1+m}=\hat{s}_{k+m}$ for $m\geq 0$. It can be used to represent the counterexample of LTL formulae with eventuality, such as $\lozenge p$ and $\lozenge\square p$.

From now, we write a lasso-shaped path as $(\pi_{stem})(\pi_{loop})^{\omega}$, where $\pi_{stem}=\hat{s}_{0}\ldots\hat{s}_{l-1}$ and $\pi_{loop}=\hat{s}_{l}\ldots\hat{s}_{k}$. To avoid ambiguity, we consider that the length of a lasso-shaped path is equal to $|\pi_{stem}|+|\pi_{loop}|$.444Notice a loop-back transition from $\hat{s}_{k}$ to $\hat{s}_{l}$ in $\pi_{loop}$. Furthermore, any no-loop path cannot be expressed as a lasso-shaped one. That is, if $\pi$ is a no-loop path then the states in $\pi$ are all different.

The spuriousness of no-loop paths can be checked via forward-reachability analysis. In detail, $\pi=\hat{s}_{0}\hat{s}_{1}\ldots\hat{s}_{k}$ is not spurious iff the sequence of DBMs $D_{1},\ldots,D_{k+1}$ where $D_{1}=\texttt{DBM}(\hat{s}_{0})$ and $D_{i+1}=\mathsf{Im}(D_{i})\cap\texttt{DBM}(\hat{s}_{i})$ for $1\leq i\leq k$, are not empty. Simply put, there exists $\textbf{x}(0)\in\texttt{DBM}(\hat{s}_{0})$ such that $\textbf{x}(i+1)=A\otimes\textbf{x}(i)\in\texttt{DBM}(\hat{s}_{i+1})$ for $0\leq i\leq k$. Algorithm 5 summarises the procedure of spuriousness checking for no-loop paths.

The spuriousness checking for lasso-shaped paths is computed via Algorithm 6. We use periodicity checking to deal with the infinite suffix $(\pi_{loop})^{\omega}$. In lines 14-22, we check the spuriousness of $(\pi_{stem})(\pi_{loop})^{it}$ where $\pi_{loop}$ is repeated $it$ times. If it is not spurious then we check the periodicity of the DBM (line 25). We can conclude that $(\pi_{stem})(\pi_{loop})^{\omega}$ is not spurious if the periodicity is found. In case of an irreducible MPL system, by 1, the periodicity is no greater than its cyclicity. On the other hand, after 1000 iterations, if the periodicity cannot be found then the algorithm is stopped with an ‘undecided’ result.

One can see that the spuriousness checking for no-loop paths (Algorithm 5) is guaranteed to be complete. However, this is not the case for Algorithm 6. In the case of irreducible MPL systems, it is complete due to the fact that the periodicity is related to 1. However for reducible MPL systems, it is incomplete as it may provide undecided results.

1 relates the spuriousness of an abstract path, either no-loop or lasso-shaped path, with the value of transient and cyclicity of an irreducible matrix.

Lemma 1.

Consider an irreducible $A\in\mathbb{R}_{\max}^{n\times n}$ with transient $k_{0}$ and cyclicity $c$ and the resulting abstract transition system $TS_{f}=(\hat{S},T_{f},I_{f},P_{mat}\cup P_{time},L_{f})$. Suppose that $\pi$ is a path over $TS_{f}$. Then,

• i.

If $\pi$ is a no-loop path with $|\pi|\geq k_{0}+c$, then it is spurious.

• ii.

If $\pi=(\pi_{stem})(\pi_{loop})^{\omega}$ with $|\pi_{stem}|+|\pi_{loop}|>k_{0}+c$, then it is spurious.

Proof.

• i.

Let assume $\pi=\hat{s}_{0}\ldots\hat{s}_{k_{0}+c}$ is not spurious. Thus, there exists $\textbf{x}(0)\in\texttt{DBM}(\hat{s}_{0})$ such that $\textbf{x}(i+1)=A\otimes\textbf{x}(i)=A^{\otimes i+1}\otimes\textbf{x}(0)\in\texttt{DBM}(\hat{s}_{i+1})$ for $0\leq i\leq k_{0}+c$. By 1, we have $A^{\otimes k_{0}+c}=\lambda c\otimes A^{\otimes k_{0}}$ which implies $\textbf{x}(k_{0}+c)=\lambda c\otimes\textbf{x}(k_{0})$. One could show that $\textbf{x}(k_{0}+c)$ and $\textbf{x}(k_{0})$ belong to the same DBM.555Given a non-empty DBM $D$ and $\alpha\in\mathbb{R}$, if $\textbf{x}\in D$ then so is $\alpha\otimes\textbf{x}$. Consequently $\texttt{DBM}(\hat{s}_{k_{0}})=\texttt{DBM}(\hat{s}_{k_{0}+c})$ and then $\hat{s}_{k_{0}}=\hat{s}_{k_{0}+c}$. This contradicts the fact that the states in $\pi$ must be all different.

• ii.

Likewise, we assume $\pi=(\pi_{stem})(\pi_{loop})^{\omega}$ where $\pi_{stem}=\hat{s}_{0}\ldots\hat{s}_{l-1}$ and $\pi_{loop}=\hat{s}_{l}\ldots\hat{s}_{k}$ is not spurious. Consequently, there exists $\textbf{x}(0)\in\texttt{DBM}(\hat{s}_{0})$ such that $\textbf{x}(i+1)=A\otimes\textbf{x}(i)=A^{\otimes i+1}\otimes\textbf{x}(0)\in\texttt{DBM}(\hat{s}_{i+1})$ for $i\geq 0$. Again by 1, we have $\textbf{x}(i+c)=\lambda c\otimes\textbf{x}(i)$ for $i\geq k_{0}$. This implies, for $i\geq 0$, $\hat{s}_{k_{0}+i}=\hat{s}_{k_{0}+c+i}$. Thus $\pi$ can be rewritten as $(\hat{s}_{0}\ldots\hat{s}_{k_{0}})(\hat{s}_{k_{0}+1}\ldots\hat{s}_{k_{0}+c})^{\omega}$. Therefore, the maximum length for $\pi_{stem}$ and $\pi_{loop}$ is $k_{0}$ and $c$, respectively. This contradicts $|\pi_{stem}|+|\pi_{loop}|>k_{0}+c$. $\square$

4.2 Refinement Procedure

Provided that the counterexample is spurious, one needs to refine the abstract transition. Instead of adding new predicates as in CEGAR [12], we are inspired by the refinement procedure described in [2, Sec. 3.3]: for each abstract state $\hat{s}$ with more than one outgoing transitions, it partitions $\texttt{DBM}(\hat{s})$ according to its successors.

Our approach for the refinement procedure is slightly different. We refine the abstract transition based on a spurious counterexample $\pi=\hat{s}_{0}\ldots\hat{s}_{k}$ using the concept of lazy abstraction [26]. This starts by finding a pivot state, namely a state in which the spuriousness starts. Then, it splits the pivot state using the procedure in [2].

Notice that, from Algorithm 5, the pivot state can be found from the number of DBMs we have in $D$. One could find that $\hat{s}_{|D|-1}$ is a pivot state. On the other hand, from Algorithm 6, a pivot state is $\hat{s}_{i}$ where $i=|D|-1$, if $|D|<|\pi_{stem}|+1$ (the spuriousness is found in $\pi_{stem}$), otherwise $i=|\pi_{stem}|+1+\texttt{mod}(D-|\pi_{stem}|-1,|\pi_{loop}|)$.

With regards to the refined abstract transitions, the labels and affine dynamics for the new abstract states are equal to those of the pivot state. Furthermore, the outgoing (resp. ingoing) transitions from (resp. to) new abstract states are determined similarly using one-step reachability.

Example 3.

We use abstract transition in Figure 1 with specification $\lozenge\square p_{2}$. The NuSMV model checker reports a counterexample of length 2: $\pi=\hat{s}_{1}(\hat{s}_{0}\hat{s}_{1})^{\omega}$. By Algorithm 6, it is spurious and the pivot state is $\hat{s}_{1}$. The resulting post-refinement abstract transition is depicted in Figure 2. $\square$

4.3 Upper-Bound on the Completeness Threshold

Given a transition system $TS$ and a specification $\varphi$, a completeness threshold is a bound $k$ such that, if no counterexample of $\varphi$ with length $k$ or less can be found in $TS$, then $\varphi$ is satisfied by $TS$ [8, 9].

We recall from above that for specific formulae, the completeness threshold is related to the structure of the underlying transition system. For instance, the CT for safety properties of the form $\square p$ is equal to the diameter of transition system: the length of longest shortest distance between two states [7]. Likewise, the CT for liveness specifications in the form of $\lozenge p$ is given by the recurrent diameter (the length of loop-free path) [14]. Computing the completeness threshold for general LTL formulae is still an open problem [14].

We show that the CT for (abstract) transition system that generated from an irreducible MPL system is related to the transient and cyclicity of the corresponding matrix.

Lemma 2.

Consider an irreducible $A\in\mathbb{R}_{\max}^{n\times n}$ with transient $k_{0}$ and cyclicity $c$ and the resulting abstract transition system $TS_{f}=(\hat{S},T_{f},I_{f},P_{mat}\cup P_{time},L_{f})$. The CT for $TS_{f}$ and for any LTL formula $\varphi$ over $P_{mat}\cup P_{time}$ is bounded by $k_{0}+c$. $\square$

Proof. By 1, any counterexample of $\varphi$ with length greater than $k_{0}+c$ (if any) is guaranteed to be spurious.

2 ensures that the CT is not greater than the sum of the transient and cyclicity of the MPL systems. Looking back to the transition system in Figure 1, the completeness threshold for $\lozenge p_{2}$ is 2. In comparison, the transient and cyclicity of matrix in (2) are $k_{0}=c=2$.

By 2, one could say that the BMC algorithm for irreducible MPL systems is complete for any LTL formula. However, this is not the case for reducible MPL systems, due to the incompleteness of Algorithm 6.

5 Computational Benchmarks

We compare the run-time of the predicate abstractions in this paper with related abstraction procedures in [29], which use max-plus algebraic operations (“tropical abstractions”) and are enhanced versions of the earlier work in [1]. For increasing $n$, we generate matrices $A\in\mathbb{R}_{\max}^{n\times n}$ with two finite elements in each row, each with values ranging between 1 and 10. Location and value of the finite elements are chosen randomly. The computational benchmark has been implemented on an Intel(R) Xeon(R) CPU E5-1660 v3, 16 cores, 3.0GHz each, and 16GB of RAM.

We run the experiments for both procedures using C++. Over 10 independents experiments for each dimension, Table 1 shows the running time to generate (specification-free) abstractions of MPL systems, where entry represents the average and maximal values. We do not compare the running time for the generation of abstract transitions because both methods apply the same algorithm.

As we can see in Table 1, for large dimensions (beyond 8), the average running time of predicate abstractions is faster than that of tropical abstractions. We recall that the (specification-free) predicate abstractions of MPL systems are computed by Algorithm 1, Algorithm 2, and Algorithm 4. Whereas for tropical abstractions, they are computed by [29, Algorithm 2].

We also provide a comparison over values of CT. NuSMV is able to compute CT via an incremental BMC command $\texttt{check}\_\texttt{ltlspec}\_\texttt{sbmc}\_\texttt{inc}\leavevmode\nobreak\ \texttt{-c}$. For each bound $k$, in addition to counterexample searching, it generates a SAT (i.e. boolean satisfiability) problem to verify whether the LTL formula can be concluded to hold. This method of computation of completeness check can be found in [25, 28].

Table 2 shows the comparison of the CT values specified by 2 and those computed by NuSMV. For dimension of $n\in\{3,4,5\}$, we generate 20 random irreducible matrices $A\in\mathbb{R}_{\max}^{n\times n}$ with two finite elements in each row. We use the same time-difference specification $\lozenge\square(t_{1}\leq 10)$ for all experiments.

The $2^{\text{nd}}$ column of Table 2 represents the number of experiments whose the specification $\lozenge\square(t_{1}\leq 10)$ is satisfied. The last three columns describe the comparison of CT. We use $\mathtt{ct}_{1}$ and $\mathtt{ct}_{2}$ to respectively denote the CT that computed by NuSMV and 2. As we can see, the CT upper bounds specified by 2 are relatively smaller than those computed by NuSMV.

6 Conclusions

This paper has introduced a new technique to generate the abstractions of MPL systems via a set of predicates. The predicates are chosen automatically from system matrix and the time-difference specifications under consideration. Having obtained the abstract states and transition, this paper has implemented bounded model checking to check the satisfaction of time-difference specifications.

The abstraction performance has been tested on a numerical benchmark, which has displayed an improvement over existing procedures. The comparison for completeness thresholds suggests that the cyclicity and transient of MPL systems can be used as an upper bound. Yet, this bound is relatively smaller than the CT bounds computed by NuSMV.

Acknowledgements

The first author is supported by Indonesia Endowment Fund for Education (LPDP), while the third acknowledges the support of the Alan Turing Institute, London, UK.