11institutetext: University of Colorado Boulder

# Closure Certificates

Vishnu Murali (✉) 11 Ashutosh Trivedi 11 Majid Zamani 11

###### Abstract

A _barrier certificate_ , defined over the states of a dynamical system, is a
real-valued function whose zero level set characterizes an inductively
verifiable state invariant separating reachable states from unsafe ones. When
combined with powerful decision procedures—such as sum-of-squares programming
(SOS) or satisfiability-modulo-theory solvers (SMT)— barrier certificates
enable an automated deductive verification approach to safety. The barrier
certificate approach has been extended to refute $\omega$-regular
specifications by separating consecutive transitions of $\omega$-automata in
the hope of denying all accepting runs. Unsurprisingly, such tactics are bound
to be conservative as refutation of _recurrence properties_ requires reasoning
about the well-foundedness of the transitive closure of the transition
relation. This paper introduces the notion of _closure certificates_ as a
natural extension of barrier certificates from state invariants to transition
invariants. We provide SOS and SMT based characterization for automating the
search of closure certificates and demonstrate their effectiveness via a
paradigmatic case study.

sec:keywords Discrete-Time Dynamical Systems, Formal Verification, Barrier
Certificates, Transition Invariants, Automated Deductive Verification

##  1 Introduction

As cyber-physical systems and internet-of-things continue to proliferate
within critical infrastructure, the need for practical verification algorithms
for infinite-state dynamical systems is ever-present. Structural induction
over the transition structure of dynamical systems provides a lightweight yet
powerful proof method to establish safety and invariance guarantees. However,
when the invariant is not inductive, human ingenuity is required in
strengthening the invariant to an inductive one. The notion of barrier
certificates [25], when combined with automatic decision procedures automate
the search for an inductive state invariant. This paper presents _closure
certificates_ as a generalization of barrier certificates to capture the
transitive closure of transition relations to automate verification of
$\omega$-regular specifications of discrete-time dynamical systems.

Intuitively, a barrier certificate [25] is a real-valued function over the
state space that is negative over the initial states, positive over the unsafe
states, and it does not increase with transitions. From this definition and
the principle of structural induction, it follows that the zero level set of
the barrier certificate over-approximate the set of reachable states. This,
together with the positivity requirement over the unsafe states, provide a
separation between reachable and unsafe states, guaranteeing safety. The
results in [33] extended the barrier certificate based approach to refute
violation of temporal specifications given in the form of $\omega$-automata.
In this approach, that we dub the _state-triplet_ approach, barrier
certificates provide separation between consecutive transitions (involving
three states) of the given $\omega$-automaton in such a way that denies
accepting runs. The approach has been extended for verification and synthesis
for more general dynamical systems [14, 15, 1, 2]. These state-triplet
approach are bound to suffer from conservatism as the verification of a
general $\omega$-regular property requires refutation of infinitely many
visits to some state and that in turn requires a well-founded argument [23, 6]
over transitive closure of transition relation.

Podelski and Rybalchenko, in an influential paper [23], introduced
disjunctively well-founded _transition invariants_ to verify programs against
$\omega$-regular properties. They defined the transition invariant as an over-
approximation of the transitive closure of the transition relation, restricted
to the set of reachable states. If the transition invariant restricted to
pairs of accepting states is disjunctively well-founded, then they showed that
no execution can visit these accepting states infinitely often, refuting the
$\omega$-regular specification. We define closure certificates as a functional
analog of _transition invariants_ and enable the use of SOS programming and
SMT solvers to search for these certificates.

Intuitively, a closure certificate
$\mathcal{T}:\mathcal{X}\times\mathcal{X}\to\mathbb{R}$ is a real-valued
function over the Cartesian product of the state set and itself (state pairs),
such that $\mathcal{T}(x,x^{\prime})\geq 0$ if $x^{\prime}$ is reachable from
$x$. The closure certificate characterizes a transition invariant
$T\subseteq\mathcal{X}\times\mathcal{X}$ such that:

$T=\\{(x,x^{\prime}):\mathcal{T}(x,x^{\prime})\geq 0\text{ and
}\mathcal{T}(x_{0},x)\geq 0\text{ for some $x_{0}\in\mathcal{X}_{0}$}\\}.$ (1)

$0$$1$$2$$3$$4$$5$

Barrier vs. Closure. While the existence of a barrier certificate implies the
existence of a closure certificate, there are systems (see figure on the left)
that permit considerably simpler closure certificates than barrier
certificates. In this example, there is no polynomial barrier certificate of
degree $2$ that demonstrates the safety of the system, but there exists a
linear closure certificate that does so. This example can be modified to show
the absence of barrier certificate for any fixed degree. Here,
$\mathcal{X}_{0}=\\{1,3,5\\}$ are initial states, $\mathcal{X}_{u}=\\{2,4\\}$
are unsafe states, and the transition function is as shown in the figure. Note
that the system is trivially safe.

Let us suppose there exists a polynomial barrier certificate $\mathcal{B}$ of
degree $2$ that acts as a proof of safety. We need $\mathcal{B}(x)\leq 0$ for
every state $x\in\mathcal{X}_{0}$, and $\mathcal{B}(x)>0$ for every state
$x\in\mathcal{X}_{u}$. Applying intermediate value theorem, the function
$\mathcal{B}$ needs to change signs in at least $3$ points and must therefore
have at least $3$ roots. This supports our claim that there is no barrier
certificate that is a polynomial of degree $2$. On the other hand, the linear
function $\mathcal{T}:\mathcal{X}\times\mathcal{X}\to\mathbb{R}$ defined as
$\mathcal{T}(x,y)=-y$ is a closure certificate for this system. While we defer
the details to later sections, from (1), it follows that this function
corresponds to the transition invariant $T=\\{(1,0),(3,0),(5,0),(0,0)\\}$, and
has no intersection with the set $\mathcal{X}_{0}\times\mathcal{X}_{u}$. This
ensures the safety of the system.

Contributions. In summary, we propose a novel notion of closure certificates
that act as a functional analog to transition invariants. We present SOS
programming as well as SMT characterizations to search for a closure
certificates within a given template (function class). We show that even when
traditional barrier certificates of a some template fail to ensure safety, one
can find closure certificates of the same template. We demonstrate how to use
closure certificates to verify dynamical systems against $\omega$-regular
properties in a case study. We show how closure certificates subsume existing
barrier certificate based approaches to verify continuous-space dynamical
systems against $\omega$-regular properties.

Related works. Prajna and Jadbabaie proposed the notion of barrier
certificates [25] as a discretization-free approach to give guarantees of
safety or reachability [27] for dynamical and hybrid systems. The results in
[33] presented a state triplet approach that uses barrier certificates to
verify $\omega$-regular properties. This approach has since been used in the
the verification and synthesis of stochastic and interconnected continuous-
space systems against $\omega$-regular properties [14, 15, 1, 2].
Unfortunately, the above approach is conservative in the sense that it treats
the nondeterministic Büchi automaton corresponding to the negation of the
$\omega$-regular specification as a finite automaton and then searches for
barrier certificates to disallow the transitions along accepting paths to show
the accepting state is not visited. Thus, even if a system satisfies the
property but visits the accepting state, then one cannot make use of the above
approaches to verify the system. We show (cf. Section 5) that our approach
subsumes this current approach. Podelski and Rybalchenko [23], proposed a
notion of transition invariants and demonstrated their use in verifying the
liveness properties of programs as well as in verifying programs against
$\omega$-regular properties. Transition invariants have also been used in [24]
to give guarantees of stability for hybrid systems. Here, they make use of a
reachability analysis tool to determine the overapproximation of reachable
states and then establish a Lyapunov guarantee on the transition invariant to
ensure the stability of the system. The results in [30] consider a notion of
relational abstraction that is similar to transition invariants to give
guarantees for safety. While transition invariants must be irreflexive to
demonstrate well-foundedness, relational abstractions are defined to be
reflexive and have mainly been used in the context of verifying safety.

While this paper focuses on abstraction-free approaches to verify
$\omega$-regular properties, we note that abstraction-based techniques have
been used in the verification and synthesis of continuous-space dynamical
systems against $\omega$-regular properties such as the results in [13, 20,
28, 17]. These results rely on building a finite state abstraction and then
making use of model checking and synthesis techniques [32, 3].

##  2 Preliminaries

We use $\mathbb{N}$ and $\mathbb{R}$ to denote the set of natural numbers and
reals. For $a\in\mathbb{R}$, we use $\mathbb{R}_{\geq a}$ and
$\mathbb{R}_{>a}$ to denote the intervals $[a,\infty)$ and $(a,\infty)$,
respectively, and similarly, for any natural number $n\in\mathbb{N}$, we use
$\mathbb{N}_{\geq n}$ to denote the set of natural numbers greater than or
equal to $n$. Given a set $A$, sets $A^{*}$ and $A^{\omega}$ denote the set of
finite and countably infinite sequences of elements in $A$, while $|A|$
denotes the cardinality of the set. If $A\subseteq B$, and the set $B$ can be
inferred from the context, we denote the complement $B\setminus A$ simply as
$\overline{A}$. We call a function $f:A\to\mathbb{R}$ bounded if there exists
$l,u\in\mathbb{R}$, such that $l\leq f(a)\leq u$ for every $a\in A$.

Given a relation $R\subseteq A\times B$, and an element $a\in A$, let $R(a)$
denote the set $\\{b\mid(a,b)\in R\\}$. We use the notation
$(a_{1},a_{2},\ldots,a_{n})\in A^{*}$ for finite length sequences and $\langle
a_{0},a_{1},\ldots,\rangle\in A^{\omega}$ for $\omega$-sequences. Let
$\mathsf{Inf}(s)$ be the set of elements that occur infinitely often in the
sequence $s$.

Discrete-time Dynamical System. A (discrete-time dynamical) system
$\mathfrak{S}$ is a tuple $(\mathcal{X},\mathcal{X}_{0},f)$, where
$\mathcal{X}$ (possibly infinite) denotes the state set,
$\mathcal{X}_{0}\subseteq X$ denotes a set of initial states, and
$f\subseteq\mathcal{X}\times\mathcal{X}$ is the state transition relation. The
state evolution of the system is given by

$\mathfrak{S}:x(t+1)\in f(x(t)).$ (2)

If for every $x\in\mathcal{X}$, we have $|f(x)|=1$, then we consider the
transition relation $f$ to be a _state transition function_ that uniquely
determines the next state. Abusing notation, we use $f$ for both a set-valued
map when it is a relation, and a transition function when it is a function.
Throughout the paper, we assume that state sets of the systems under
consideration are compact.

A _state sequence_ is an infinite sequence $\langle
x_{0},x_{1},\ldots,\rangle\in\mathcal{X}^{\omega}$ where
$x_{0}\in\mathcal{X}_{0}$, and $x_{i+1}\in f(x_{i})$, for all
$i\in\mathbb{N}$. We associate a labelling function
$\mathcal{L}:\mathcal{X}\to\Sigma$ which maps each state of the system to a
letter in a finite alphabet $\Sigma$. This naturally generalizes to mapping a
state sequence of the system $\langle
x_{0},x_{1},\ldots,\rangle\in\mathcal{X}^{\omega}$ to a trace or word
$w=\langle\mathcal{L}(x_{0}),\mathcal{L}(x_{1}),\ldots,\rangle\in\Sigma^{\omega}$.
For notational convenience, given a state $x\in\mathcal{X}$, we use $x^{+}$ to
indicate a state in $f(x)$. Let $TR(\mathfrak{S},\mathcal{L})$ denote the set
of all traces of $\mathfrak{S}$ under the labeling map $\mathcal{L}$.

Barrier Certificates. A system $\mathfrak{S}$ is safe with respect to a set of
unsafe states $\mathcal{X}_{u}$, if no state sequence reaches
$\mathcal{X}_{u}$, i.e., for every state sequence $\langle
x_{0},x_{1},\ldots,\rangle$, we have $x_{i}\notin\mathcal{X}_{u}$ for every
$i\geq 0$.

######  Definition 1 (Barrier Certificate)

A function $\mathcal{B}:\mathcal{X}\to\mathbb{R}$ is a barrier certificate for
$\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$ with respect to a set of unsafe
states $\mathcal{X}_{u}$ if:

$\displaystyle\mathcal{B}(x)\leq 0$ $\displaystyle\text{ for all
}x\in\mathcal{X}_{0}$ (3) $\displaystyle\mathcal{B}(x)>0$ $\displaystyle\text{
for all }x\in\mathcal{X}_{u}$ (4) $\displaystyle\big{(}\mathcal{B}(x)\leq
0\big{)}\implies\big{(}\mathcal{B}(x^{+})\leq 0\big{)}$ $\displaystyle\text{
for all }x\in\mathcal{X},\text{ and }x^{+}\in f(x)$ (5)

######  Theorem 2.1 (Barrier certificates imply safety [25])

For a system $\mathfrak{S}$ with unsafe states $\mathcal{X}_{u}$, the
existence of a barrier certificate $\mathcal{B}$ implies its safety.

##  3 Closure Certificates

A set $Inv\subseteq\mathcal{X}$ is said to be an _inductive state invariant_
if $x_{0}\in Inv$, $\forall x_{0}\in\mathcal{X}_{0}$, and for any state $x\in
Inv$, every state $x^{+}\in f(x)$ is also in the set $Inv$. Similarly, a set
$Tinv\subseteq\mathcal{X}\times\mathcal{X}$ is an _inductive transition
invariant_ [23] if for every state $x\in\mathcal{X}$ and $x^{+}\in f(x)$, the
pair $(x,x^{+})\in Tinv$; and for any state $y\in\mathcal{X}$ such that
$(x^{+},y)\in Tinv$, the pair $(x,y)$ is also in the set $Tinv$. Barrier
certificates act as functional analogs to indutive state invariants in the
following way: all the initial states are within the zero level set of the
barrier certificate, and, given any state that is within the zero level set,
its successor according to the transition relation is also in the zero level
set. In this section, we propose closure certificates as functional analogs to
inductive transition invaraints and study their use in the verification of
safety, persistence (refuting recurrence), and $\omega$-regular
specifications.

###  3.1 Closure Certificates for Safety

We first show how one may use closure certificates to show that a system is
safe.

######  Definition 2 (Closure Certificate for Safety)

A bounded function $\mathcal{T}:\mathcal{X}{\times}\mathcal{X}{\to}\mathbb{R}$
is a Closure Certificate (CC) for
$\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$ with set of unsafe states
$\mathcal{X}_{u}$ if there exists a value $\delta\in\mathbb{R}_{>0}$ such
that:

$\displaystyle\mathcal{T}(x,x^{+})\geq 0$ $\displaystyle\text{ for all
}x\in\mathcal{X},x^{+}\in f(x),$ (6)
$\displaystyle\big{(}\mathcal{T}(x^{+},y)\geq
0\big{)}\implies\big{(}\mathcal{T}(x,y)\geq 0\big{)}$ $\displaystyle\text{ for
all }x,y\in\mathcal{X},x^{+}\in f(x),\text{ and }$ (7)
$\displaystyle\mathcal{T}(x_{0},x_{u})\leq-\delta$ $\displaystyle\text{ for
all }x_{0}\in\mathcal{X}_{0},\text{ and }x_{u}\in\mathcal{X}_{u}.$ (8)

######  Theorem 3.1 (Closure Certificate imply Safety)

Consider a system $\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$. The
existence of a function
$\mathcal{T}:\mathcal{X}\times\mathcal{X}\to\mathbb{R}$ that satisfies
conditions (6)-(8) implies that no trace of the system reaches
$\mathcal{X}_{u}$.

###### Proof

Let us assume that there exists a trace of the system $\langle
x_{0},\ldots,x_{u},\ldots\rangle$ that reaches an unsafe state
$x_{u}\in\mathcal{X}_{u}$ from some initial state $x_{0}$. From condition (6),
we have $\mathcal{T}(x_{i},x_{i+1})\geq 0$ for all $i\in\mathbb{N}$, and from
condition (7) and induction, we have $\mathcal{T}(x_{0},x_{i})\geq 0$ for all
$i\in\mathbb{N}$. Thus we must have $\mathcal{T}(x_{0},x_{u})\geq 0$ as
$x_{j}=x_{u}$ for some $j\in\mathbb{N}$. According to condition (8),
$\mathcal{T}(x_{0},x_{u})\leq-\delta$, where $\delta\in\mathbb{R}_{>0}$, which
is in contradiction to the previous inequality. ∎

Observe that closure certificates are defined over pairs of states of the
system rather than just over the states of the system. Hence, searching for a
closure certificate suffers computationally more than a search for a barrier
certificate. On the other hand, for a certain template of functions (e.g.,
linear or quadratic), one might be able to find closure certificates, even
when barrier certificates of the same template do not exist. In particular, we
have the following result:

######  Theorem 3.2 (Simplicity of Closure Certificates)

For any natural number $d\in\mathbb{N}$, there exists a system
$\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$ with unsafe set of states
$\mathcal{X}_{u}$ that cannot be shown to be safe by a polynomial barrier
certificate of degree $d$ but can be shown to be safe by a linear closure
certificate.

###### Proof

Consider a system $\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$, with
$\mathcal{X}=[0,(2d+2)]$ as the state set,
$\mathcal{X}_{0}=\\{1,3,\ldots,(2d+1)\\}$ as the initial set of states, and a
constant transition relation $f(x)=\\{0\\}$ for every state $x\in\mathcal{X}$.
Let the set of unsafe states be $\mathcal{X}_{u}=\\{2,4,\ldots,(2d+2)\\}$. We
observe that the system is trivially safe. Let us suppose there exists a
polynomial barrier certificate $\mathcal{B}:\mathcal{X}\to\mathbb{R}$ of
degree $d$ that acts as a proof of safety. From conditions (3) and (4), we
have $\mathcal{B}(x)\leq 0$ for every state $x\in\mathcal{X}_{0}$, and
$\mathcal{B}(x)>0$ for every state $x\in\mathcal{X}_{u}$. Applying
intermediate value theorem, the function $\mathcal{B}$ needs to change signs
in at least $(d+1)$ points and must therefore have at least $(d+1)$ roots.
This contradicts our assumption that $\mathcal{B}$ is a polynomial of degree
$d$. Consider the function
$\mathcal{T}:\mathcal{X}\times\mathcal{X}\to\mathbb{R}$ defined as
$\mathcal{T}(x,y)=-y$. Observe that $0\in f(x)$ for all $x\in\mathcal{X}$, and
that $\mathcal{T}(x,y)\geq 0$ only when $y\leq 0$. This implies conditions (6)
and (7) are satisfied. Further for every state $x_{u}\in X_{u}$ and every
state $x_{0}\in X_{0}$, we have $\mathcal{T}(x_{0},x_{u})\leq-2$. Thus
condition (8) also holds. We conclude that the function $\mathcal{T}$ is a
closure certificate and acts as a proof that the system is safe. ∎

Previously, we discussed how one can use closure certificates even when
barrier certificates fail. We now show that if a system can be guaranteed to
be safe via barrier certificates, then it can be guaranteed via closure
certificates as well.

######  Theorem 3.3 (Expressiveness)

Consider a system $\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$, with unsafe
set of states $\mathcal{X}_{u}$. Given a barrier certificate
$\mathcal{B}:\mathcal{X}\to\mathbb{R}$ (Definition 1), one can compute a
closure certificate $\mathcal{T}:\mathcal{X}\times\mathcal{X}\to\mathbb{R}$.

###### Proof

Let $\gamma\in\mathbb{R}_{>0}$. We define the function
$\mathcal{T}:\mathcal{X}\times\mathcal{X}\to\mathbb{R}$ as:

$\mathcal{T}(x,y)=\begin{cases}0&\text{ if }\mathcal{B}(x)>0\text{ or
}\mathcal{B}(y)\leq 0,\\\ -\gamma&\text{otherwise}.\end{cases}$

We now show that $\mathcal{T}$ is a CC with $\delta=\gamma$. Let us suppose
that $\mathcal{T}(x,x^{+})<0$ for some $x\in\mathcal{X}$. For this to be true,
we must have $\mathcal{B}(x)\leq 0$, and $\mathcal{B}(x^{+})>0$, however, this
contradicts condition (5) and so $\mathcal{T}$ must satisfy condition (6).
Second, suppose $\mathcal{T}(x^{+},y)\geq 0$, and $\mathcal{T}(x,y)<0$. Then
$\mathcal{B}(x)\leq 0$, $\mathcal{B}(y)>0$, and one of $\mathcal{B}(x^{+})>0$
or $\mathcal{B}(y)\leq 0$. Since both $\mathcal{B}(y)\leq 0$ and
$\mathcal{B}(y)>0$ cannot be true, we must have $\mathcal{B}(x)\leq 0$, and
$\mathcal{B}(x^{+})>0$, which again contradicts condition (5), and so
condition (7) must hold. Finally, consider $\mathcal{T}(x_{0},x_{u})$. From
conditions (3) and (4), we have $\mathcal{B}(x_{0})\leq 0$, and
$\mathcal{B}(x_{u})>0$, and, hence, by definition
$\mathcal{T}(x_{0},x_{u})=-\delta$ satisfies condition (8). ∎

###  3.2 Closure Certificates for Persistence

Similar to how closure certificates are used to guarantee safety, one may use
closure certificates to show a region is visited finitely often. This relies
on showing that the closure certificate is well-founded, similar to the
condition used in [24].

######  Definition 3 (Closure Certificates for Persistence)

Consider a system $\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$. A bounded
function $\mathcal{T}:\mathcal{X}\times\mathcal{X}\to\mathbb{R}$ is a Closure
Certificate (CC) for $\mathfrak{S}$ with set of states
$\mathcal{X}_{VF}\subseteq\mathcal{X}$, that must be visited finitely often if
there exists a value $\delta\in\mathbb{R}_{>0}$ such that:

$\displaystyle\mathcal{T}(x,x^{+})\geq 0$ $\displaystyle\text{ for all
}x\in\mathcal{X},x^{+}\in f(x)$ (9)
$\displaystyle\big{(}\mathcal{T}(x^{+},y)\geq
0\big{)}\implies\big{(}\mathcal{T}(x,y)\geq 0\big{)}$ $\displaystyle\text{ for
all }x,y\in\mathcal{X},x^{+}\in f(x),\text{ and }$ (10)
$\displaystyle\big{(}\mathcal{T}(x_{0},y)\geq
0\big{)}\wedge\big{(}\mathcal{T}(y,y^{\prime})\geq 0\big{)}\implies$
$\displaystyle\qquad\big{(}\mathcal{T}(x_{0},y^{\prime})\leq\mathcal{T}(x_{0},y)-\delta\big{)}$
$\displaystyle\text{ for all }x_{0}\in\mathcal{X}_{0},\text{ and
}y,y^{\prime}\in\mathcal{X}_{VF}$ (11)

######  Theorem 3.4 (Closure Certificates imply Persistence)

Consider a system $\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$. The
existence of a function
$\mathcal{T}:\mathcal{X}\times\mathcal{X}\to\mathbb{R}$ that satisfies
conditions (9)-(11) implies that the traces of the system visit the set
$\mathcal{X}_{VF}$ finitely often.

###### Proof

Let us suppose that there is some trajectory $\langle
x_{0},x_{1},\ldots,\rangle$ of the system that starts from state
$x_{0}\in\mathcal{X}_{0}$ and visits $\mathcal{X}_{VF}$ infinitely often. Let
the infinite sequence $\langle y_{0},y_{1},\ldots,\rangle$ denote the states
that are visited in $\mathcal{X}_{VF}$ in that order, i.e., the trajectory is
$\langle x_{0},\ldots,y_{0},\ldots,y_{1},\ldots\rangle$. From conditions (9)
and (10), we have $\mathcal{T}(x_{0},y_{i})\geq 0$ and
$\mathcal{T}(y_{i},y_{j})\geq 0$ for all indices $j>i$, $i,j\in\mathbb{N}$. As
we assume the function $\mathcal{T}$ to be bounded, there exists some
$\mathcal{T}^{*}\in\mathbb{R}$, such that
$\mathcal{T}(x,y)\leq\mathcal{T}^{*}$ for every pair of states
$x,y\in\mathcal{X}$. Note that $\mathcal{T}(x_{0},y_{0})\leq T^{*}$. From
condition (11), and induction, we have
$\mathcal{T}(x,y_{i})\leq\mathcal{T}(x_{0},y_{0})-i\delta\leq T^{*}-i\delta$.
As this is true for all $i\in\mathbb{N}$, and we have
$\delta\in\mathbb{R}_{>0}$, there must exist some $j\in\mathbb{N}$ such that
$\mathcal{T}(x_{0},y_{j})<0$. This is a contradiction. ∎

###  3.3 Closure Certificates for Büchi Objectives

A Nondeterministic Büchi Automaton (NBA) $\mathcal{A}$ is a tuple
$(\Sigma,Q,Q_{0},\delta,Q_{Acc})$, where $\Sigma$ denotes a finite alphabet,
$Q$ a finite set of states, $Q_{0}\subseteq Q$ an initial set of states,
$\delta\subseteq Q\times\Sigma\times Q$ the transition relation, and
$Q_{Acc}\subseteq Q$ denotes a set of accepting states. A run of the automaton
$\mathcal{A}=(\Sigma,Q,q_{0},\delta,Q_{Acc})$ over a word
$w=\langle\sigma_{0},\sigma_{1},\sigma_{2}\ldots,\rangle\in\Sigma^{\omega}$,
is an infinite sequence of states $\rho=\langle
q_{0},q_{1},q_{2},\ldots,\rangle\in Q^{\omega}$ with $q_{0}\in Q_{0}$ and
$q_{i+1}\in\delta(q_{i},\sigma_{i})$. An NBA
$\mathcal{A}=(\Sigma,Q,Q_{0},\delta,Q_{Acc})$ is said to accept a word $w$, if
there exists a run $\rho$ over $w$ where $\mathsf{Inf}(\rho)\cap
Q_{Acc}\neq\emptyset$. We denote the set of words accepted by an NBA
$\mathcal{A}$ (the language of the NBA) as $L(\mathcal{A})$. It is well known
that NBAs are closed under complementation [29]: given an NBA
$\mathcal{A}=(\Sigma,Q,Q_{0},\delta,Q_{Acc})$, there exists an NBA
$\mathcal{A}^{\prime}=(\Sigma,Q^{\prime},Q^{\prime}_{0},\delta^{\prime},Q^{\prime}_{Acc})$
such that $L(\mathcal{A}^{\prime})=\overline{L(\mathcal{A})}$. Finally, we say
that a Büchi automaton is _determinstic_ if or all $q\in Q$, and
$\sigma\in\Sigma$, we have $|\delta(q,\sigma)|\leq 1$.

Let the NBA $\mathcal{A}=(Q,Q_{0},\delta,Q_{Acc})$ denote the complement of an
$\omega$-regular specification. Then the system $\mathfrak{S}$ under labeling
map $\mathcal{L}$ satisfies the $\omega$-regular property if
$TR(\mathfrak{S},\mathcal{L})\cap L(\mathcal{A})=\emptyset$, i.e., no trace of
the system under the labeling map is accepted by $\mathcal{A}$. Observe that
$\mathcal{A}$ has a finite set of states, and so each state can be represented
as a number in $\\{0,\ldots,|Q|-1\\}$. To verify whether the system satisfies
the $\omega$-regular property, we first construct the product
$\mathfrak{S}\otimes\mathcal{A}=(\mathcal{X}^{\prime},\mathcal{X}_{0}^{\prime},f^{\prime})$
of the system $\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$ with the NBA
$\mathcal{A}=(Q,Q_{0},\delta,Q_{Acc})$ representing the complement of the
specification, where
$\mathcal{X}^{\prime}=\mathcal{X}\times\\{0,\ldots,|Q|-1\\}$ indicates the
state set, and
$\mathcal{X}^{\prime}_{0}=\mathcal{X}_{0}^{\prime}\times\\{j\mid q_{j}\in
Q_{0}\\}$ is the initial set of states. We define the state transition
relation $f^{\prime}$ as :

$f^{\prime}((x,i))=\big{\\{}(x^{+},j)\mid
q_{j}\in\delta(q_{i},\mathcal{L}(x)),\text{ and }x^{+}\in f(x)\big{\\}}.$

To ensure the satisfaction of an $\omega$-regular property, we make use of a
closure certificate on the product system $\mathfrak{S}\otimes\mathcal{A}$.

######  Definition 4 (Closure Certificate for Büchi Objectives)

Consider a system $\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$ and NBA
$\mathcal{A}=(Q,Q_{0},\delta,Q_{Acc})$ representing the complement of an
$\omega$-regular specification. A bounded function
$\mathcal{T}:(\mathcal{X}\times\mathbb{N})\times(\mathcal{X}\times\mathbb{N})\to\mathbb{R}$
is a closure certificate for $\mathfrak{S}$ under labeling map
$\mathcal{L}:\mathcal{X}\to\Sigma$, and NBA $\mathcal{A}$ if there exists a
value $\delta\in\mathbb{R}_{>0}$ such that for all $x,y\in\mathcal{X}$,
$x^{+}\in f(x)$, and states $q_{i}\in Q$, $q_{l}\in Q$, and
$q_{j}\in\delta(q_{i},\mathcal{L}(x))$, we have:

$\displaystyle\mathcal{T}(x,i,x^{+},j)\geq 0,$ (12)
$\displaystyle\big{(}\mathcal{T}(x^{+},j,y,\ell)\geq
0\big{)}\implies\big{(}\mathcal{T}(x,i,y,\ell)\geq 0\big{)},\text{ and }$ (13)

for all $x\in\mathcal{X}_{0}$, $q_{i}\in Q_{0}$, and every
$y,y^{\prime}\in\mathcal{X}$, $q_{j},q_{j^{\prime}}\in Q_{Acc}$, there exists
a $\delta\in\mathbb{R}_{>0}$ such that:

$\displaystyle\big{(}\mathcal{T}(x,i,y,j)\geq
0\big{)}\wedge\big{(}\mathcal{T}(y,j,y^{\prime},j^{\prime})\geq
0\big{)}\implies$
$\displaystyle\qquad\big{(}(\mathcal{T}(x,i,y^{\prime},j^{\prime})\leq\mathcal{T}(x,i,y,j)-\delta\big{)}$
(14)

Now, we provide the next result of the paper on the verification of
$\omega$-regular properties using closure certificates on
$\mathfrak{S}\otimes\mathcal{A}$.

######  Theorem 3.5 (Closure Certificates imply Büchi objectives)

Consider a system $\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$ and NBA
$\mathcal{A}=(Q,Q_{0},\delta,Q_{Acc})$ representing the complement of an
$\omega$-regular specification. The existence of a CC satisfying conditions
(12)-(14) implies that $TR(\mathfrak{S},\mathcal{L})\cap
L(\mathcal{A})=\emptyset$.

###### Proof

Observe that a CC $\mathcal{T}$ satisfying conditions (12) to (14) is a CC for
the product of $\mathfrak{S}$ and $\mathcal{A}$. From Theorem 3.4, we observe
that the product system visits accepting states finitely often and so we infer
that no trace of the system is in the language of the NBA $\mathcal{A}$.∎

##  4 Synthesizing Closure Certificates

This section presents two approaches to synthesize closure certificates when
the dynamical systems under study have state sets which are subsets of
$\mathbb{R}^{n}$, i.e., $\mathcal{X}\subseteq\mathbb{R}^{n}$, and the
transition function $f$ is a polynomial. The first approach we consider is
using a counterexample guided approach via Satisfiability Modulo Theory (SMT)
solvers [4], while the second makes use of standard sum-of-squares (SOS) [22]
approaches to find closure certificates similar to barrier certificates.

###  4.1 SMT-based Approach

The method of Counterexample-guided Inductive Synthesis (CEGIS) [31] has seen
significant use in the synthesis of barrier certificates. We show how one may
use CEGIS to find closure certificates. To find a CC as in Definition 3, we
first fix the template of the CC to be a linear combination of user-defined
basis functions, i.e. $\mathcal{T}(x,y)=\sum_{m=1}^{z}c_{m}p_{m}(x,y)$ where
functions $p_{m}$ are user-defined analytical basis functions over the state
variables $x$ and $y$ and $c_{1},\ldots,c_{z}$ are the coefficients. As an
example, we can consider $c_{1},\ldots,c_{z}$ to be real values, and
$\mathcal{T}(x,y)$ to be a polynomial. In such a case, the functions
$p_{1},\ldots,p_{m}$ are monomials over $x$ and $y$. Note that if the values
of $x,y\in\mathcal{X}$ are fixed, then the only decision variables in
$\mathcal{T}(x,y)$ are the coefficients $c_{m}$, $m\in\\{1,\ldots,z\\}$. We
sample $2N$ points from the state set $\mathcal{X}$ of the system to create
the sets $S_{1}=\\{x_{1},\ldots,x_{N}\\}$, and
$S_{2}=\\{y_{1},\ldots,y_{N}\\}$, and sample $3N$ points from
$\mathcal{X}_{0}$, $\mathcal{X}_{VF}$, and $\mathcal{X}_{VF}$, respectively,
to create sets $S_{3}=\\{x^{\prime}_{1},\ldots,x^{\prime}_{N}\\}$,
$S_{4}=\\{z_{1},\ldots,z_{N}\\}$,
$S_{5}=\\{z^{\prime}_{1},\ldots,z^{\prime}_{N}\\}$, respectively. We then
encode the constraints of the closure certificate for every pair of points as
an SMT-query over the theory of linear real arithmetic (LRA) [7] using z3 [21]
as follows:

$\displaystyle\underset{}{\bigwedge}\Big{(}\mathcal{T}(x_{i},x_{i}^{+})\geq
0\Big{)},$ (15)
$\displaystyle\underset{}{\bigwedge}\Big{(}\big{(}\mathcal{T}(x_{i}^{+},y_{j})\geq
0\big{)}\implies\big{(}\mathcal{T}(x_{i},y_{j})\geq 0\big{)}\Big{)},$ (16)
$\displaystyle\underset{}{\bigwedge}\Big{(}\big{(}\mathcal{T}(x^{\prime}_{j},z_{j})\geq
0\big{)}\wedge\big{(}\mathcal{T}(x^{\prime}_{j},z^{\prime}_{k})\geq
0\big{)}\implies\big{(}\mathcal{T}(x^{\prime}_{j},z^{\prime}_{k})\leq\mathcal{T}(x^{\prime}_{j},z_{j})-\delta\big{)}\Big{)},$
(17)

where $x_{i}^{+}=f(x_{i})$ indicates the next state from $x_{i}$ following the
transition function. We lastly add a constraint of $\delta$ being larger than
some small positive value and then find values $c_{1},\ldots,c_{z}$ for the
coefficients and substitute them as a candidate CC $\mathcal{T}(x,y)$. To
determine if this candidate is in fact a CC, we now try to find elements
$x,y,x^{\prime},z,z^{\prime}\in\mathcal{X}$ such that one of the conditions
(9)-(11) does not hold. We do this by encoding the negation of these
conditions as an SMT query. If such a counterexample is found, we add them to
the respective set and repeat the process. If no such counterexample is found,
then we conclude that this function is indeed a CC.

Instead of using an SMT solver to find a CC, we can instead run our CEGIS loop
quicker by strengthening conditions (10)-(11) as inequalities of the form:

$\displaystyle\tau_{1}\mathcal{T}(x^{+},y)\leq\mathcal{T}(x,y)$
$\displaystyle\forall x,y\in\mathcal{X},$ (18)
$\displaystyle\mathcal{T}(x_{0},y)\\!-\\!\delta\\!-\\!\mathcal{T}(x_{0},y^{\prime})\\!\geq\\!\tau_{2}\mathcal{T}(x_{0},y)\\!+\\!\tau_{3}\mathcal{T}(y,y^{\prime})$
$\displaystyle\forall x_{0}\in\mathcal{X}_{0},\forall
y,y^{\prime}\in\mathcal{X}_{VF},$ (19)

where $\tau_{1},\tau_{2},\tau_{3}\in\mathbb{R}_{>0}$ are fixed positive
values. The satisfaction of conditions (18) and (19) implies the satisfaction
of conditions (10) and (11), and the search for a candidate CC can be cast as
a linear program instead. This allows one to use a linear programming solver
(such as Gurobi [11]) to find a candidate CC instead. We then find a
counterexample via SMT queries similar to the earlier approach, and then add
the counterexample to our linear program, and search for a candidate CC again.
While conditions (18) and (19) are more conservative, the search for a
candidate is much quicker.

We adopt a similar approach to find a CC for the synchronized product as in
Definition 4, that acts as a proof that the traces of the system are not in
the language of the NBA $\mathcal{A}=(\Sigma,Q,Q_{0},\delta,Q_{Acc})$. Here,
we encode the constraints as the following conjunctions for every state
$x_{i}\in S_{1}$, $y_{j}\in S_{2}$, and $y^{\prime}_{k}\in S_{3}$ as well as
every state $q_{\xi}\in Q$ such that
$q_{\chi}\in\delta(q_{\xi},\mathcal{L}(x_{i}))$:

$\displaystyle\underset{}{\bigwedge}\Big{(}\mathcal{T}(x_{i},\xi,x^{+},\chi)\geq
0\Big{)},$ (20)
$\displaystyle\underset{}{\bigwedge}\Big{(}\big{(}\mathcal{T}(x^{+},\chi,y_{j},\zeta)\geq
0\big{)}\implies\big{(}\mathcal{T}(x_{i},\xi,y_{j},\zeta)\geq
0\big{)}\Big{)},$ and (21)

for every state $q_{\chi}\in Q_{0}$, and $q_{\zeta},q_{\zeta^{\prime}}\in
Q_{Acc}$, we have

$\displaystyle\underset{}{\bigwedge}\Big{(}\big{(}\mathcal{T}(x_{i},\chi,y_{j},\zeta)\geq
0\big{)}\wedge\big{(}\mathcal{T}(y_{j},\zeta,y^{\prime}_{k},\zeta^{\prime})\geq
0\big{)}$
$\displaystyle\qquad\qquad\qquad\implies\big{(}\mathcal{T}(x_{i},\chi,y^{\prime}_{k},\zeta^{\prime})\leq\mathcal{T}(x_{i},\chi,y_{j},\zeta)-\delta\big{)}\Big{)}.$
(22)

In general there is no guarantee of termination when using a CEGIS approach
for uncountable state sets. However, one may strengthen the conditions as
specified in [18] to guarantee termination of the CEGIS loop. Instead of using
a CEGIS approach, one may also encode the conditions in an SMT solver over the
nonlinear theory of reals [8] such as dReal [9] or z3 [16] to search for CCs.
While all the above approaches are NP-hard [9, 5, 16], we find the CEGIS
approach to work better in practice compared to searching for a solution in
the nonlinear theory of reals. Barrier certificates face many of the same
challenges when using a CEGIS approach. Computationally, however, closure
certificates take more time in practice as these are defined over pairs of
states rather than over a single state, and so suffer more when the dimension
of the state set increases. We should add that we have not considered the
complexity for finding the NBA representing the complement of the
specification, but rather assume this NBA to be given. If we consider this as
well, then the complexity of NBA complementation is EXPTIME [29].

###  4.2 Sum-of-Squares based Approach

The technique of using semidefinite programming [22] and casting the search
for a standard barrier certificates [25] as SOS polynomials is particularly
important due to the simpler complexity of computation when compared to CEGIS
approaches. We show how one may adopt a SOS approach to find closure
certificates. To do so, we first note that a set $A\subseteq\mathbb{R}^{n}$ is
semi-algebraic if it can be defined with the help of a vector of polynomial
inequalities $h(x)$ as $A=\\{x\mid h(x)\geq 0\\}$, where the inequalities is
interpreted component-wise.

To adopt a SOS approach to find CCs as in Definition 3, we consider the sets
$\mathcal{X}$, $\mathcal{X}_{0}$, and $\mathcal{X}_{VF}$ to be semi-algebraic
sets defined with the help of vectors of polynomial inequalities $g_{A}$,
$g_{0}$, and $g_{VF}$, respectively. As these sets are semi-algebraic, the
sets $\mathcal{X}\times\mathcal{X}$ and
$\mathcal{X}_{0}\times\mathcal{X}_{VF}\times\mathcal{X}_{VF}$ are semi-
algebraic as well. Let their corresponding vectors be $g_{B}$ and $g_{C}$,
respectively. Furthermore, we assume that the user-defined basis functions
$p_{m}$ are monomials and again strengthen the implications in conditions
(10)-(11) to conditions (18)-(19). Then the search for a CC as in Definition 3
reduces to showing that the following polynomials are sum-of-squares:

$\displaystyle\mathcal{T}(x,f(x))-\lambda_{A}^{T}(x)g_{A}(x),$ (23)
$\displaystyle\mathcal{T}(x,y)-\tau_{1}\mathcal{T}(f(x),y)-\lambda_{B}^{T}(x,y)g_{B}(x,y),$
(24)
$\displaystyle\mathcal{T}(x,y^{\prime})-\delta-\tau_{2}\mathcal{T}(x,y)-\tau_{3}\mathcal{T}(y,y^{\prime})-\lambda_{C}^{T}(x,y,y^{\prime})g_{C}(x,y,y^{\prime}),$
(25)

where the multipliers $\lambda_{A}$, $\lambda_{B}$, $\lambda_{C}$, are sum-of-
squares over the state variable $x$, the state variables $x,y$, and the state
variables $x,y,y^{\prime}$ over the regions $\mathcal{X}$,
$\mathcal{X}\times\mathcal{X}$, and
$\mathcal{X}_{0}\times\mathcal{X}_{VF}\times\mathcal{X}_{VF}$ respectively,
and $\delta$, $\tau_{1}$, $\tau_{2}$, and $\tau_{3}\in\mathbb{R}_{>0}$ are
positive values.

###### Lemma 1

Assume the sets $\mathcal{X}$, $\mathcal{X}_{0}$, and $\mathcal{X}_{VF}$ are
semi-algebraic, and there exists a sum-of-squares polynomial
$\mathcal{T}(x,y)$ satisfying conditions (23)-(25). Then the function
$\mathcal{T}(x,y)$ is a CC satisfying conditions (9)-(11).

Since there are finitely many letters $\sigma\in\Sigma$, without loss of
generality, one can partition the set $\mathcal{X}$ into finitely many
partitions $\mathcal{X}_{\sigma_{1}},\ldots,\mathcal{X}_{\sigma_{p}}$, where
for all $x\in\mathcal{X}_{\sigma_{i}}$, we have $\mathcal{L}(x)=\sigma_{i}$.
Given an element $\sigma_{i}\in\Sigma$, we can uniquely characterize the
relation $\delta_{\sigma_{m}}$ as $(q_{\xi},q_{\chi})\in\delta_{\sigma_{i}}$
if and only if $q_{\chi}\in\delta(q_{\xi},\sigma_{i})$. Assume that the sets
$\mathcal{X}$, $\mathcal{X}_{0}$, and $\mathcal{X}_{\sigma_{i}}$, for all
$\sigma_{i}$, are semi-algebraic and characterized by polynomial vectors of
inequalities $g(x)$, $g_{0}(x)$, and $g_{\sigma_{i},A}(x,\chi)$, respectively.
Furthermore, we consider polynomial vectors of inequalities
$g_{\sigma_{i},B}(x,\chi,y,\zeta)$ over the product space
$\mathcal{X}\times\mathbb{N}\times\mathcal{X}\times\mathbb{N}$ and
$g_{\sigma_{i},C}(x,\chi,y,\zeta,y^{\prime},\zeta^{\prime})$ over
$\mathcal{X}_{0}\times\mathbb{N}\times\mathcal{X}\times\mathbb{N}\times\mathcal{X}\times\mathbb{N}$,
respectively. Let the state transition function $f:\mathcal{X}\to\mathcal{X}$
be a polynomial. Now, one can reduce the search for a CC to showing that the
following polynomials are SOS for all states $x,y\in\mathcal{X}$, and states
$q_{\xi},q_{\zeta}\in Q$, letters $\sigma_{i}\in\Sigma$, such that
$x^{+}=f(x)$, and $q_{\chi}\in\delta_{\sigma_{m}}(q_{\xi})$:

$\displaystyle\mathcal{T}(x,\xi,x^{+},\chi)-\lambda^{T}_{\sigma_{i},A}(x,\xi)g_{\sigma_{i},A}(x,\xi)$
(26)
$\displaystyle\mathcal{T}(x,\xi,y,\zeta)-\tau_{1}\mathcal{T}(x^{+},\chi,y,\zeta)-\lambda^{T}_{\sigma_{i},B}(x,\xi,y,\zeta)g_{\sigma_{i},C}(x,\xi,y,\zeta),$
(27)

and for every state $x\in\mathcal{X}_{0}$, $y,y^{\prime}\in\mathcal{X}$, and
states $q_{\xi}\in Q_{0}$, and $q_{\zeta},q_{\zeta^{\prime}}\in Q_{Acc}$

$\displaystyle\mathcal{T}(x,\xi,y^{\prime},\zeta^{\prime})-\delta-\tau_{2}\mathcal{T}(x,\xi,y,\zeta)-\tau_{3}\mathcal{T}(y,\zeta,y^{\prime},\zeta^{\prime})$
$\displaystyle-\lambda^{T}_{\sigma_{i},C}(x,\xi,y,\zeta,y^{\prime},\zeta^{\prime})g_{\sigma_{i},C}(x,\xi,y,\zeta,y^{\prime},\zeta^{\prime}),$
(28)

are sum-of-squares, where $\lambda^{T}_{\sigma_{i},A}$,
$\lambda^{T}_{\sigma_{i},B}$, and $\lambda^{T}_{\sigma_{i},C}$ are sum-of-
squares polynomials over their respective regions and
$\tau_{1},\tau_{2},\tau_{3},\delta\in\mathbb{R}_{>0}$ are positive values.

###### Lemma 2

Assume the sets $\mathcal{X}$, $\mathcal{X}_{0}$, $\mathcal{X}_{VF}$, and
$\mathcal{X}_{\sigma_{i}}$ for all $\sigma_{i}$ are semi-algebraic, and there
exists a sum-of-squares polynomial $\mathcal{T}(x,\xi,y,\zeta)$ satisfying
conditions (26)-(28). Then the function $\mathcal{T}(x,\xi,y,\zeta)$ is a CC
for the product satisfying conditions (12)-(14).

To determine whether the above equations are SOS, one can make use of solvers
such as [26]. The complexity of determining whether the above equations are
SOS is polynomial in $O\big{(}\binom{2n+d}{d}\times\binom{2n+d}{d}\big{)}$,
when searching for CCs for safety or ensuring finite visits, where $n$ is the
dimension of the state set, and $2d$ is the degree of the polynomial. The
complexity of verifying $\omega$-regular properties is 111Determining whether
a polynomial in $n$ variables and degree $d$ are SOS can be reduced to a
semidefinite program in $O\big{(}\binom{n+d}{d}\times\binom{n+d}{d}\big{)}$
variables [22]. polynomial in
$O\big{(}\binom{2n+2d+2}{d}\times\binom{2n+2d+2}{d}\big{)}$. This is because
the closure certificate is a function of pairs of the state set of the system
and the state of the automaton. On the other hand, the complexity of
determining whether the equations for barrier certificates are SOS is
$O\big{(}\binom{n+d}{d}\times\binom{n+d}{d}\big{)}$ [25]. If the dimension of
the system is fixed, then the complexity is polynomial in the degree $2d$. The
key issue when using an SOS approach, however, is that there may be
polynomials that satisfy the above constraints but are not SOS. Furthermore,
one cannot directly encode the implication in SOS, and, hence, suffers from
the conservatism of having to satisfy a stronger condition.

##  5 Subsuming Existing Approaches

We show that our approach generalizes the existing class of techniques using
state triplet introduced in [33] for the verification of continuous-space
systems against $\omega$-regular properties. The state triplet technique has
been used for the verification and synthesis for stochastic systems [14, 15],
for networks of systems [2, 1], and in motion-planning for nonlinear systems
[12]. Here, the transition map is a function, and the state set is a subset of
$\mathbb{R}^{n}$. First, we present the details of the state triplet approach
briefly, in Section 5.1. Then in Section 5.2, we show how one can use closure
certificates to guarantee satisfaction of $\omega$-regular properties when the
state triplet approach provides a guarantee as well.

###  5.1 The State Triplet Approach

Consider a system $\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$, where
$\mathcal{X}\subseteq\mathbb{R}^{n}$, and $f$ is a state transition function.
Consider an NBA $\mathcal{A}=(\Sigma,Q,Q_{0},\delta,Q_{Acc})$, and a labeling
function $\mathcal{L}:\mathcal{X}\to\Sigma$. The key idea of the state triplet
approach is to find barrier certificates between edges of the automaton to
disallow the system from visiting the accepting state. This ensures that
$TR(\mathfrak{S},\mathcal{L})\cap L(\mathcal{A})=\emptyset$.

The steps of the approach are as follows:

  1. 1.

Consider all the simple paths in the NBA that start from an initial state and
reach an accepting state.

  2. 2.

Break these paths into a sequence of state triplets
$(q_{i},q^{\prime}_{i},q^{\prime\prime}_{i})$ (or edge pairs
$(e_{i},e^{\prime}_{i})$).

  3. 3.

Search for a barrier certificate to “cut” at least one triplet from each path.

  4. 4.

If we can cut at least one triplet along each path, we can conclude that
$TR(\mathfrak{S},\mathcal{L})\cap L(\mathcal{A})=\emptyset$, and if not this
approach is inconclusive.

To help illustrate this approach consider a system
$\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$, and a finite alphabet
$\Sigma=\\{a,b\\}$; the labeling map $\mathcal{L}$ naturally partition the set
$\mathcal{X}$ into two sets $\mathcal{X}_{a}$ and $\mathcal{X}_{b}$. Let the
NBA $\mathcal{A}=(\Sigma,Q,Q_{0},\delta,Q_{Acc})$ in Figure 1 represent the
complement of the $\omega$-regular specification, where $\Sigma=\\{a,b\\}$,
$Q=\\{q_{0},q_{1},q_{2},q_{3}\\}$, $Q_{0}=\\{q_{0}\\}$, $Q_{Acc}=\\{q_{3}\\}$,
and $\delta$ is specified by the edges in the graph. This NBA accepts those
words which start with a $b$ and have at least two $a$’s in them. There is one
simple path starting from the initial state $q_{0}$ that reaches the accepting
state $q_{3}$. This path corresponds to the sequence of states
$(q_{0},q_{1},q_{2},q_{3})$ and can be broken into two triplets
$(q_{0},q_{1},q_{2})$ and $(q_{1},q_{2},q_{3})$. The first state triplet
corresponds to the edge pair $((q_{0},q_{1}),(q_{1},q_{2}))$ which are labeled
by the pair of letters $(b,a)$, and the second to the edge pair
$((q_{1},q_{2}),(q_{2},q_{3}))$ which are labeled by the pair of letters
$(a,a)$.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$b$$b$$a$$a$$b$$a,b$ Figure 1: Example NBA
$\mathcal{A}$ which represents the complement of a safety specification to
illustrate the state triplet approach.

To cut the transitions along the first state triplet $(q_{0},q_{1},q_{2})$, we
try to find a barrier certificate, where the initial set of states are all the
states with the label $b$ (corresponding to the edge $(q_{0},q_{1})$), i.e.
all the states of the system in $\mathcal{X}_{b}$. The unsafe states are all
the states with a label of $a$ (corresponding to the edge $(q_{1},q_{2})$),
i.e. all the states in the set $\mathcal{X}_{a}$. The existence of a barrier
certificate, proves that no trace of the system can visit a state with label
$a$, after visiting a state with label $b$, and so cannot correspond to the
run $(q_{0},q_{1},q_{2})$ in the automaton. This cuts the path from the
initial state $q_{0}$ to the accepting state $q_{3}$ of the automaton and
shows that no trace of the system can take this corresponding path in the NBA.
As there are no other simple paths to the accepting state, we conclude that no
trace of the system is in the language of the NBA. If we fail to find a
barrier certificate for the first triplet, we then search for a barrier
certificate in the next triplet $(q_{1},q_{2},q_{3})$. As the edges of the
states in the triplet have the same label $a$, we cannot find a barrier
certificate where the initial set and unsafe set are both $\mathcal{X}_{a}$.
If we fail to find a barrier certificate for both triplets, then our approach
is inconclusive.

As the state triplet approach proves that no trace of the system can reach the
accepting state, one expects that it can be leveraged in a similar fashion to
bounded model checking. Ideally unrolling the automaton for $k$-steps would
allow one to verify that no trace of the system visits the accepting state
more than $k$ times. Unfortunately, this is not true, and the state triplet
approach does not benefit when one unrolls more than once.

###### Lemma 3

Consider an NBA $\mathcal{A}=(\Sigma,Q,Q_{0},\delta,Q_{Acc})$, whose simple
paths from the initial states $Q_{0}$ to the accepting states $Q_{Acc}$ have
been divided into $m$ state triplets
$(q_{i},q^{\prime}_{i},q^{\prime\prime}_{i})$ for all $1\leq i\leq m$, such
that $q^{\prime}_{i}\in\delta(q,a_{i})$ and
$q^{\prime\prime}_{i}\in\delta(q,b_{i})$, for some $a_{i},b_{i}\in\Sigma$.
Unrolling the automaton more than once does not lead to finding a new triplet
with labels that have not been considered before.

We present the proof of Lemma 3 in Appendix 0.A.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$a$$b$$c$$b$$b,d$$a$ (a)

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$q^{\prime}_{2}$$q^{\prime}_{3}$$a$$b$$c$$b$$b,d$$a$$a$$b$$c$
(b)

Figure 2: Example NBA $\mathcal{A}$ (Figure 2(a)) and its unrolling (Figure
2(b)) from Section 5.1.

Now, with an example, we demonstrate why unrolling the automaton once might
help in finding state triplets. Consider the NBA
$\mathcal{A}=(\Sigma,Q,Q_{0},\delta,Q_{Acc})$ in Figure 2(a), with
$\Sigma=\\{a,b,c,d\\}$, $Q=\\{q_{0},q_{1},q_{2},q_{3}\\}$,
$Q_{Acc}=\\{q_{2}\\}$, and the transition relation specified by the edges in
the graph. We unroll this automaton to get the automaton
$\mathcal{A}^{\prime}$ in Figure 2(b). Unrolling the automaton once allows us
to consider the triplet $(q_{2},q^{\prime}_{3},q^{\prime}_{2})$ whose edge
labels correspond to the pair of letters $(c,b)$. Observe that no state
triplet in the original NBA corresponds to this pair of letters. Thus even if
one was not able to find a barrier certificate for a state triplet in NBA
$\mathcal{A}$ (for the state triplet $(q_{0},q_{1},q_{2})$), one may still
find a barrier certificate for a state triplet in NBA $\mathcal{A}^{\prime}$
(the state triplet $(q_{2},q^{\prime}_{3},q^{\prime}_{2})$). Hence, no trace
of the system can visit the accepting state more than once.

We observe that unrolling once does have an impact since we can now consider
those state triplets along the simple cycles of the NBA. Unfortunately,
unrolling twice does not help. Thus, one is unable to verify those traces of a
system which reach and cycle on accepting states more than twice, even if they
visit accepting states finitely often.

The state triplet approach is conservative in the following direction:
_independently of the state runs in the automaton and of the initial states of
the system $\mathfrak{S}$, one is required to break the edge pairs of every
simple path regardless of what states of the automaton may be encountered
before or after_.

###  5.2 Closure certificates subsume state triplet approaches

We now show that our approach generalizes the earlier state triplet one.
Consider an NBA $\mathcal{A}=(\Sigma,Q,Q_{0},\delta,Q_{Acc})$, and let us
assume that there exist $m$ barrier certificates
$\mathcal{B}_{1},\mathcal{B}_{2}\ldots,\mathcal{B}_{m}$ associated with state
triplets $(q_{i},q^{\prime}_{i},q^{\prime\prime}_{i})$, (or edge pairs
$(e_{i},e^{\prime}_{i})$) for each $1\leq i\leq m$, that act as a proof that
no trace of the system is in $L(\mathcal{A})$. Furthermore, let
$(a_{i},b_{i})$ be the pairs of letters associated with these triplets. We
divide the states of the NBA $\mathcal{A}$ into two sets $Q_{l}$, and $Q_{r}$.
A state $q\in Q$ is in the set $Q_{l}$ if it is not the middle element of a
state triplet and there is a path from $q$ to the middle element of _some_
state triplet. A state $q\in Q$ is in the set $Q_{r}$ if there is a path from
the middle element of every state triplet to $q$. The only states that are in
neither of the sets are middle elements of the triplets. As the state triplet
approach “cuts” the transitions of the NBA, we observe that no trace of the
system starting from a state in $Q_{l}$ can reach a state in $Q_{r}$.
Furthermore, we note that every state $q_{0}\in Q_{0}$ is in the set $Q_{l}$,
and every state $q_{acc}\in Q_{Acc}$ is in the set $Q_{r}$. We now show how
one may use closure certificates to guarantee $\omega$-regular properties when
the state triplet approach can guarantee the satisfaction of the property.

######  Theorem 5.1 (Subsuming the state triplet approach)

Consider a System $\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$, labeling map
$\mathcal{L}:\mathcal{X}\to\Sigma$, and NBA
$\mathcal{A}^{\prime}=(\Sigma,Q^{\prime},Q_{0},\delta^{\prime},Q^{\prime}_{Acc})$.
Suppose that there exists barrier certificates
$\mathcal{B}_{1},\ldots,\mathcal{B}_{m}$ that show
$TR(\mathfrak{S},\mathcal{L})\cap L(\mathcal{A}^{\prime})=\emptyset$ via the
state triplet approach. Then there exists a closure certificate $\mathcal{T}$
that also acts as a proof that $TR(\mathfrak{S},\mathcal{L})\cap
L(\mathcal{A}^{\prime})=\emptyset$.

######  Proof (sketch)

We construct a closure certificate
$\mathcal{T}:\mathcal{X}\times\mathbb{N}\times\mathcal{X}\times\mathbb{N}\to\mathbb{R}$
such that, for $x,y\in\mathcal{X}$, and $q_{i},q_{j}\in Q$, we have that
$\mathcal{T}(x,i,y,j)\geq 0$, if:

  * •

$q_{i}\in Q_{r}$;

  * •

$q_{i}\in Q_{l}$ and $q_{j}\in Q_{l}$;

  * •

$q_{i}$ is the middle element of triplet $m$, and $\mathcal{B}_{m}(x)\leq 0$,
$q_{j}\in Q_{l}$ and $\mathcal{B}_{m}(y)\leq 0$;

  * •

$q_{i}$ is the middle element of triplet $m$, and $\mathcal{B}_{m}(x)>0$; or

  * •

$q_{i}\in Q_{l}$, $q_{j}$ is the middle element of some triplet $m$, and
$\mathcal{B}_{m}(y)\leq 0$.

Moreover, $\mathcal{T}(x,i,y,j)<0$, otherwise. This certificate clearly
guarantees that no trace of the system can reach the accepting states. A
detailed proof is given in Appendix 0.B. ∎

##  6 Case Studies

###  6.1 Kuramoto Oscillator

Kuramoto model [10] has been used widely to describe chemical and biological
oscillators, with applications in neuroscience and modern power system
analysis. As a first case study, we consider a system
$\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$ to model a Kuramoto oscillator
whose dynamics are taken from [2], where $\mathcal{X}=[0,2\pi]$ indicates the
state set, $\mathcal{X}_{0}=[\frac{4\pi}{9},\frac{5\pi}{9}]$ the initial set
of states, and $\mathcal{X}_{u}=[\frac{7\pi}{9},\frac{8\pi}{9}]$ denotes the
unsafe set of states. The transition function $f$ is defined as:

$f(x)=x+\tau\Omega+t_{s}K\sin(-x)-0.532x^{2}+1.69,$

where $x\in\mathcal{X}$ indicates the phase of the oscillator, $t_{s}=0.1$ is
the sampling time, $\Omega=0.01$ is the natural frequency, and $K=0.0006$ is
the coupling strength.

We then search for a linear closure certificate as in Definition 2 to ensure
the safety of the system. To do so, we strengthen the implication in condition
(7) to condition (18), with $\tau_{1}=1$, and sample $50$ points from the
initial, unsafe, and entire state set. We then solve a linear program to find
a candidate closure certificate. As z3 [21] cannot handle the function
$\sin(-x)$, we instead use the solver dReal [9] to find counterexamples. We
add these counterexamples to the set of samples and repeat the procedure until
we find no counterexamples. We find the closure certificate
$\mathcal{T}(x,y)=10-4.094y$ that acts as a proof of safety. The time taken
for our CEGIS loop to terminate is around $20$ minutes. We should note that
the linear program encoding the barrier certificate conditions is infeasible
when we consider a linear barrier certificate rather than a CC.

###  6.2 Two Room Temperature Model

As a second case study, we consider our system
$\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$ to be an interconnected two-
room temperature model adapted from [1], where
$\mathcal{X}=[9,17]\times[9,17]\in\mathbb{R}^{2}$ indicate the temperature of
the two rooms, $\mathcal{X}_{0}=[9,10]\times[9,10]$ indicate the initial set
of states, and the transition function is defined as:

$f(T_{1},T_{2})=A\begin{bmatrix}T_{1}\\\ T_{2}\end{bmatrix}+\mu
T_{h}\begin{bmatrix}u(T_{1})\\\
u(T_{2})\end{bmatrix}+\theta\begin{bmatrix}T_{e}\\\ T_{e}\end{bmatrix},$

where $T_{i}$ represents the temperature of room $i$, for all $i\in\\{1,2\\}$,
the matrix $A$ is

$A:=\begin{bmatrix}1-2\alpha-\theta-\mu(T_{1})&\alpha\\\
\alpha&1-2\alpha-\theta-\mu(T_{1})\\\ \end{bmatrix},$

where constants $\alpha=0.01$, $\theta=0.06$, and $\mu=0.145$ represent the
conduction factors, and $u(T_{i})$ denotes the temperature controller, and is
defined as $u(T_{i})=0.59-0.011x$. The value $T_{h}=40$C denotes the heater
temperature, and $T_{e}=-5$C represents the ambient temperature. We consider
the alphabet $\Sigma=\\{p_{0},p_{1}\\}$, and the labeling function
$\mathcal{L}$ as $\mathcal{L}(x)=p_{0}$ if $x\in[9,10]\times[9,10]$ indicating
uncomfortable temperatures for both rooms, and $p_{1}$ otherwise.

Let the NBA in Figure 3 to denote the negation of the $\omega$-regular
property we wish to verify. The language $L(\mathcal{A})$ of the NBA is
$(p_{0}p_{0}(p_{1})^{*}p_{0})^{\omega}$.

First observe that one cannot make use of the state triplet approach as all
the edges along the path $(q_{0},q_{3},q_{2},q_{4})$ as well as the simple
cycle $(q_{4},q_{3},q_{2},q_{4})$ have the label $p_{0}$. We search for a
closure certificate
$\mathcal{T}:(\mathcal{X}\times\mathbb{N})\times(\mathcal{X}\times\mathbb{N})\to\mathbb{R}$
as in Definition 4 to ensure that no trace of the system is in the language of
the NBA. To do so, we assume the closure certificate $\mathcal{T}(x,i,y,j)$ to
be a polynomial of degree $4$ in the states of the system $x,y\in\mathcal{X}$
and $i,j\in Q$, respectively.

We make use of a counterexample-guided approach by first sampling $140$ points
from the state set of the system, $70$ from the set of states with label
$p_{0}$, and $70$ from the set of states with label $p_{1}$. We then encode
the conditions as a linear program and then search for counterexamples via z3
[21], after which we add these counterexamples to the set of samples and
iterate again until we find no counterexamples. The time taken for this CEGIS
loop (Section 4.1) to terminate is around $3$ hours. The resulting closure
certificate has 30 terms and is presented in a table form in Appendix 0.C.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$q_{4}$$p_{1}$$p_{0}$$p_{0}$$p_{0}$$p_{0}$$p_{0},p_{1}$$p_{1}$$p_{1}$$p_{1}$
Figure 3: A (nondeterministic) Büchi automaton $\mathcal{A}$ for the two-room
temperature case study from Section 6.

##  7 Conclusion

We proposed a notion of so-called closure certificates that act as a function
analog of transition invariants. Our notion of closure certificates provide an
abstraction-free approach to verify dynamical systems against $\omega$-regular
properties. Our approach of using closure certificates to verify
$\omega$-regular properties subsume existing approaches that use barrier
certificate to verify $\omega$-regular properties. As future work, we plan to
investigate how one may use approaches such as $k$-induction to allow for a
larger class of functions to act as closure certificates. We also plan on
investigating data driven approaches to find these closure certificates as
well as investigate their use in synthesizing controllers.

## References

  * [1] Anand, M., Lavaei, A., Zamani, M.: Compositional synthesis of control barrier certificates for networks of stochastic systems against $omega$-regular specifications. arXiv preprint arXiv:2103.02226 (2021)
  * [2] Anand, M., Lavaei, A., Zamani, M.: From small-gain theory to compositional construction of barrier certificates for large-scale stochastic systems. IEEE Transactions on Automatic Control 67(10) (2022)
  * [3] Baier, C., Katoen, J.P.: Principles of model checking. MIT press (2008)
  * [4] Barrett, C., Tinelli, C.: Satisfiability modulo theories. Springer (2018)
  * [5] Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Automata Theory and Formal Languages: 2nd GI Conference Kaiserslautern, May 20–23, 1975. pp. 134–183. Springer (1975)
  * [6] Cook, B.: Priciples of program termination. Engineering Methods and Tools for Software Safety and Security 22(161), 125 (2009)
  * [7] Dutertre, B., Moura, L.d.: A fast linear-arithmetic solver for dpll (t). In: International Conference on Computer Aided Verification. pp. 81–94 (2006)
  * [8] Gao, S., Avigad, J., Clarke, E.M.: $\delta$-complete decision procedures for satisfiability over the reals. In: Automated Reasoning. pp. 286–300. Lecture Notes in Computer Science, Springer (2012)
  * [9] Gao, S., Kong, S., Clarke, E.M.: dReal: An SMT solver for nonlinear theories over the reals. In: Automated Deduction – CADE-24. pp. 208–214. Lecture Notes in Computer Science (2013)
  * [10] Guo, Y., Zhang, D., Li, Z., Wang, Q., Yu, D.: Overviews on the applications of the kuramoto model in modern power system analysis. International Journal of Electrical Power & Energy Systems 129 (2021)
  * [11] Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2021), https://www.gurobi.com
  * [12] He, B., Lee, J., Topcu, U., Sentis, L.: Bp-rrt: Barrier pair synthesis for temporal logic motion planning. In: 2020 59th IEEE Conference on Decision and Control (CDC). pp. 1404–1409. IEEE (2020)
  * [13] Henzinger, T.A., Ho, P.H., Wong-Toi, H.: Hytech: A model checker for hybrid systems. International Journal on STTT (1997)
  * [14] Jagtap, P., Soudjani, S., Zamani, M.: Temporal logic verification of stochastic systems using barrier certificates. In: ATVA. pp. 177–193 (2018)
  * [15] Jagtap, P., Soudjani, S., Zamani, M.: Formal synthesis of stochastic systems via control barrier certificates. IEEE Transactions on Automatic Control 66(7), 3097–3110 (2020)
  * [16] Jovanović, D., De Moura, L.: Solving non-linear arithmetic. ACM Communications in Computer Algebra 46(3/4), 104–105 (2013)
  * [17] Khaled, M., Zamani, M.: Omegathreads: symbolic controller design for $\omega$-regular objectives. In: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control. pp. 1–7 (2021)
  * [18] Kong, S., Solar-Lezama, A., Gao, S.: Delta-decision procedures for exists-forall problems over the reals. In: Computer Aided Verification: 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II 30. pp. 219–235. Springer (2018)
  * [19] Kozen, D.C.: Theory of computation, vol. 121. Springer (2006)
  * [20] Lahijanian, M., Andersson, S.B., Belta, C.: Temporal logic motion planning and control with probabilistic satisfaction guarantees. IEEE Transactions on Robotics 28(2), 396–409 (2011)
  * [21] Moura, L.d., Bjørner, N.: Z3: An efficient smt solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–340 (2008)
  * [22] Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Mathematical Programming 96, 293–320 (2003)
  * [23] Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004. pp. 32–41. IEEE (2004)
  * [24] Podelski, A., Wagner, S.: Model checking of hybrid systems: From reachability towards stability. In: International Workshop on Hybrid Systems: Computation and Control. pp. 507–521. Springer (2006)
  * [25] Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: International Workshop on Hybrid Systems: Computation and Control. pp. 477–492 (2004)
  * [26] Prajna, S., Papachristodoulou, A., Parrilo, P.A.: Introducing sostools: A general purpose sum of squares programming solver. In: Proceedings of the 41st IEEE Conference on Decision and Control, 2002. pp. 741–746 (2002)
  * [27] Prajna, S., Rantzer, A.: Convex programs for temporal verification of nonlinear dynamical systems. SIAM Journal on Control and Optimization pp. 999–1021 (2007)
  * [28] Rungger, M., Zamani, M.: Scots: A tool for the synthesis of symbolic controllers. In: Proceedings of the 19th international conference on hybrid systems: Computation and control. pp. 99–104 (2016)
  * [29] Safra, S.: On the complexity of $\omega$-automata. In: Proc. 29th IEEE Symp. Found. of Comp. Sci. pp. 319–327 (1988)
  * [30] Sankaranarayanan, S., Tiwari, A.: Relational abstractions for continuous and hybrid systems. In: International Conference on Computer Aided Verification. pp. 686–702. Springer (2011)
  * [31] Solar-Lezama, A.: Program Synthesis by Sketching. PhD thesis, University of California, Berkeley (2008)
  * [32] Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer Science & Business Media (2009)
  * [33] Wongpiromsarn, T., Topcu, U., Lamperski, A.: Automata theory meets barrier certificates: Temporal logic verification of nonlinear systems. IEEE Transactions on Automatic Control (2015)

##  Appendix 0.A Proof of Lemma 3

###### Proof

First let us unroll the simple cycles of the automaton $\mathcal{A}$ that
start from an accepting state to construct an automaton
$\mathcal{A}^{\prime}=(\Sigma,Q^{\prime},Q_{0},\delta^{\prime},Q^{\prime}_{Acc})$
such that $L(\mathcal{A}^{\prime})=L(\mathcal{A})$. The states $Q^{\prime}$ of
$\mathcal{A}^{\prime}$ contain all the states $Q$ of $\mathcal{A}$ as well as
one new state $q^{\prime}_{i}$ for every state $q_{i}\in Q$ that can be
reached from an accepting state. Determining which states are reachable from
an accepting state can be done in polynomial time [19] in the number of states
of the automaton. Intuitively, these new states are meant to determine the
state runs of the system which have reached an accepting state and continue
onward. The set of initial states is the same as $\mathcal{A}$, while the set
of accepting states consist of the states $q^{\prime}_{Acc}$, i.e., those
accepting states that can be reached from an accepting state. The transitions
$\delta^{\prime}$ are the same as the transitions for $\mathcal{A}$, except
for the transitions that leave an accepting state $q_{Acc}\in Q_{Acc}$ and
additional transitions added. The transitions added are due to two reasons :

  1. 1.

For every pair of states $q_{i},q_{j}\in Q$ that are reachable from an
accepting state, and for any $\sigma\in\Sigma$ such that
$q_{j}\in\delta(q_{i},\sigma)$, we add a transition
$q^{\prime}_{j}\in\delta(q^{\prime}_{i},\sigma)$. This preserves all the
transitions for the newly added states so they behave the same as before.

  2. 2.

For every state $q_{i}\in Q$, and every accepting state $q_{Acc}\in Q_{Acc}$,
and any letter $\sigma\in\Sigma$ such that $q_{j}\in\delta(q_{Acc},\sigma)$,
we add a transition $q^{\prime}_{j}\in\delta(q_{Acc},\sigma)$. For every edge
that leaves the accepting state, we add an edge to move to the states of the
form $q^{\prime}\in Q^{\prime}\setminus Q$. Observe that there are no
transition from the states in $Q^{\prime}\setminus Q$ to the ones in $Q$.

Unrolling the automaton once, allows us to now consider the state triplets of
the form $(q,q^{\prime},q^{\prime\prime})$, where either $q^{\prime}$ and
$q^{\prime\prime}$ are in $Q^{\prime}\setminus Q$ or $q^{\prime},q^{\prime}\in
Q$ and $q^{\prime\prime}\in Q^{\prime}\setminus Q$.

Unfortunately performing the same construction again does not add any new pair
of letters to consider. Let us repeat the above construction on NBA
$\mathcal{A}^{\prime}$ to construct the NBA
$\mathcal{A}^{\prime\prime}=(\Sigma,Q^{\prime\prime},Q_{0},\delta,Q^{\prime\prime}_{f})$,
and consider a state triplet $(q,q^{\prime},q^{\prime\prime})$ in
$\mathcal{A}^{\prime\prime}$. First, if all the states $q,q^{\prime}$, and
$q^{\prime\prime}$ are in the set $Q^{\prime}$, then they were already a state
triplet in the original NBA. We now consider the different cases where a new
state triplet $(q,q^{\prime},q^{\prime\prime})$ may be considered.

  1. 1.

If all the states in the triplet are in $Q^{\prime\prime}$ or in $Q^{\prime}$,
then there are no new edge pairs to consider (as there exist triplets
$(q_{1},q^{\prime}_{1},q^{\prime\prime}_{1})$ in $\mathcal{A}^{\prime}$ that
have the same labels and have already been considered).

  2. 2.

The state $q^{\prime\prime}\in Q^{\prime\prime}\setminus Q$ is newly added
while the states $q$ and $q^{\prime}$ are in $Q^{\prime}$. In this case there
must be analogous state triplet $(q_{1},q^{\prime}_{1},q^{\prime\prime}_{1})$
such that $q^{\prime\prime}_{1}\in Q^{\prime}\setminus Q$, and the states
$q_{1}$ and $q^{\prime}_{1}$ were initially present in $Q$ which correspond to
the same pair of letters. Thus, again there are no pairs to be considered.

  3. 3.

The states $q^{\prime}$ and $q^{\prime\prime}$ are in the set
$Q^{\prime\prime}\setminus Q^{\prime}$ (they are newly added states) but $q$
is not. In this case there exists an analogous state triplet
$(q_{1},q^{\prime}_{1},q^{\prime\prime}_{1})$, such that the state $q_{1}\in
Q$ and the states $q^{\prime}_{1}$ and $q^{\prime\prime}_{1}$ are in the set
$Q^{\prime}\setminus Q$ with the same label. Hence, this again does not add a
new edge pair to be considered.

No other cases need to be considered, as no state in
$Q^{\prime\prime}\setminus Q^{\prime}$ can reach a state in $Q^{\prime}$ by
construction. As no new pairs of letters are considered when unrolling more
than once, we observe that we cannot find barrier certificates with a
different initial or unsafe condition. ∎

##  Appendix 0.B Proof of subsumption

######  Theorem 0.B.1 (Subsuming the state triplet approach)

Consider a System $\mathfrak{S}=(\mathcal{X},\mathcal{X}_{0},f)$, a labeling
map $\mathcal{L}:\mathcal{X}\to\Sigma$, and an NBA
$\mathcal{A}^{\prime}=(\Sigma,Q^{\prime},Q_{0},\delta^{\prime},Q^{\prime}_{Acc})$
representing the complement of an $\omega$-regular specification, and let
barrier certificates $\mathcal{B}_{1},\ldots,\mathcal{B}_{m}$ be used to show
that $TR(\mathfrak{S},\mathcal{L})\cap L(\mathcal{A}^{\prime})=\emptyset$ via
the state triplet approach. Then there exists a closure certificate
$\mathcal{T}$ that also acts as a proof that $TR(\mathfrak{S},\mathcal{L})\cap
L(\mathcal{A}^{\prime})=\emptyset$.

###### Proof

Fix $\delta\in\mathbb{R}_{>0}$ as a small positive value, then we define a
closure certificate
$\mathcal{T}:\mathcal{X}\times\mathbb{N}\times\mathcal{X}\times\mathbb{N}\to\mathbb{R}$
based on the following cases:

  1. 1.

The automaton states are either in $Q_{l}$ or $Q_{r}$.

  2. 2.

The first automaton state is a middle element of some triplet.

  3. 3.

The second automaton state is the middle element of some triplet.

We define $\mathcal{T}(x,i,y,j)$ for each of the above cases as follows:

  1. 1.

We define $\mathcal{T}(x,i,y,j)=0$, if $q_{i}$ and $q_{j}$ are in the same
set, i.e. both $q_{i}$ and $q_{j}$ are either in $Q_{l}$ or $Q_{r}$; or if the
state $q_{i}\in Q_{r}$, and state $q_{j}\in Q_{l}$ and for every pair of
states $x,y\in\mathcal{X}$. We define $\mathcal{T}(x,i,y,j)=-\delta$ if
$q_{i}\in Q_{l}$, and $q_{j}\in Q_{r}$. Intuitively, this assumes that all
states in $Q_{l}$ are reachable from any state in either $Q_{r}$ or $Q_{l}$,
however no state in $Q_{r}$ is reachable from some state in $Q_{l}$.

  2. 2.

Let $q_{j}=q^{\prime\prime}_{i}$ be a middle element of some triplet, then we
define $\mathcal{T}(x,j,y,k)$ depending on the value of $\mathcal{B}_{i}(x)$
and $\mathcal{B}_{i}(y)$. For all states $x\in\mathcal{X}$, such that
$\mathcal{B}_{i}(x)\leq 0$, we define $\mathcal{T}(x,j,y,k)=0$ for all states
$y\in\mathcal{X}$ such that $\mathcal{B}_{i}(y)\leq 0$ and $q_{k}\in
Q_{l}\cup\\{q_{j}\\}$; and $\mathcal{T}(x,j,y,k)=-\delta$ for all states
$q_{k}\in Q_{r}$ and $y\in\mathcal{X}$. Otherwise, we define
$\mathcal{T}(x,j,y,k)=0$ for all states $y\in\mathcal{X}$, and $q_{k}\in Q$.
Intuitively, this separates those states that can be reached from $Q_{l}$, and
those states that are in $Q_{r}$, while allowing the states in $Q_{r}$ to
reach the states in $Q_{l}$.

  3. 3.

Finally, let $q_{j}=q^{\prime}_{i}$ be a middle element of some triplet, then
we define $\mathcal{T}(x,l,y,j)=0$ for all states $x\in\mathcal{X}$, $q_{l}\in
Q_{l}$, and every state $y\in\mathcal{X}$ such that $\mathcal{B}_{i}(y)\leq 0$
and $\mathcal{T}(x,l,y,j)=-\delta$ otherwise. Similarly, we define
$\mathcal{T}(x,r,y,j)=0$ for all states $x\in\mathcal{X}$, $q_{r}\in Q_{r}$,
and every state $q_{j}\in Q$, $y\in\mathcal{X}$. Intuitively, this enforces
that starting from a state in $Q_{l}$, one does not reach a state where the
barrier value is greater than $0$, and the automaton state is the middle
element of a triplet.

The closure certificate assumes that the middle element of the triplet, and
all states with a nonpositive barrier value can be reached by all states, and
all states with a positive barrier value and automaton state in $Q_{r}$ or the
middle element of some triplet are reachable from $Q_{r}$ and not reachable
from $Q_{l}$ or those states with a nonpositive barrier value.

We now show that $\mathcal{T}$ is a Closure certificate. First, we observe
that condition (14) trivially holds as all states $q_{0}\in Q_{0}$ are in the
set $Q_{l}$ and all states $q_{r}\in Q_{Acc}$ are in the set $Q_{r}$,
therefore by definition we must have $\mathcal{T}(x,0,y,r)=-\delta$ for all
states $x\in\mathcal{X}_{0}$, and $y\in\mathcal{X}$. Second, let us assume
that condition (12) fails to hold, i.e. there exists a states $q_{i}\in Q$,
and $x\in\mathcal{X}$, $x^{+}=f(x)$ and
$q_{j}\in\delta(q_{i},\mathcal{L}(x))$, such that
$\mathcal{T}(x,i,x^{+},j)<0$. For this to be true
$\mathcal{T}(x,i,x^{+},j)=-\delta$. Clearly, $q_{i}\in Q_{l}$ and $q_{j}\in
Q_{r}$ cannot hold as the barrier certificates disallow reaching the states in
$Q_{r}$ from $Q_{l}$. Thus either $q_{i}$ or $q_{j}$ must be the middle
element of some triplet. If $q_{i}$ is the middle element of some triplet,
then we must have $q_{j}\in Q_{r}$, and $\mathcal{B}_{i}(x)\leq 0$. As
$\mathcal{B}_{i}(x)\leq 0$, we must have $\mathcal{B}_{i}(x^{+})\leq 0$ as
well and so $q_{j}$ cannot be the last element of the triplet. If $q_{j}$ is
another state in $Q_{r}$ that is to the right of every triplet, then it could
not be reached from any state in $Q_{l}$ and hence cannot be reached from any
state that is reachable from $q_{j}$ and therefore $q_{i}$ cannot be a middle
element of some triplet. Lastly, if $q_{j}$ is the middle element of some
triplet, then it must be the case that $\mathcal{B}_{i}(y)>0$, and following
the last condition of the barrier no state in $Q_{l}$ should be able to reach
$q_{j}$. Thus condition (13) must hold. Finally, assume that condition (14)
fails to hold, then there exists some state $x\in\mathcal{X}$,
$y\in\mathcal{X}$, and states $q_{\xi}$, $q_{\zeta}\in Q$, such that for
$x^{+}=f(x)$, and $q_{\chi}\in\delta(q_{\xi},\mathcal{L}(x))$, and we have
$\mathcal{T}(x^{+},\chi,y,\zeta)\geq 0$ and
$\mathcal{T}(x,\xi,y,\zeta)=-\delta$. For this to be true, one of the
following must hold:

  1. 1.

the state $q_{\xi}$ is in $Q_{l}$, and the state $q_{\zeta}$ is in $Q_{r}$. As
$\mathcal{T}(x^{+},\chi,y,\zeta)\geq 0$, we can reach state $q_{\zeta}$ from
$q_{\chi}$, as $q_{\xi}\in\delta(q_{\zeta},\mathcal{L}(x))$, by definition, we
must have $\mathcal{T}(x,\xi,x^{+},\chi)\geq 0$, and as $q_{\xi}$ is in
$Q_{l}$, it must follow that state $q_{\chi}$ is also either in $q_{l}$ or the
middle element of some triplet such that $\mathcal{B}_{i}(x^{+})\leq 0$ for
some $0\leq i\leq m$. From the previous conditions, it follows, that
$\mathcal{T}(x^{+},\xi,y,\zeta)=-\delta$.

  2. 2.

The state $q_{\xi}$ is the middle element of some triplet, such that
$\mathcal{B}_{i}(x)\leq 0$ and either $q_{\zeta}$ is in $Q_{r}$ or
$\mathcal{B}_{i}(y)>0$. If $q_{\zeta}$ is in $Q_{r}$, we observe that
$\mathcal{T}(x^{+},\chi,y,\zeta)\geq 0$, and so we must have
$\mathcal{B}_{i}(x^{+})>0$ which cannot hold or $q_{\chi}$ is in $Q_{r}$.
However, $q_{\chi}\in\delta(q_{\xi},\mathcal{L}(x))$, and so similar to the
previous case, this cannot be true.

  3. 3.

Finally, the state $q_{\zeta}$ is the middle element of some triplet. If so,
we must have $q_{\xi}\in Q_{l}$, and $\mathcal{B}_{i}(y)>0$. We observe that
the we must have $\mathcal{T}(x,\xi,x^{+},\chi)\geq 0$ as the first condition
holds, and so $q_{\chi}\in Q_{l}$. If $\mathcal{T}(x^{+},\chi,y,\zeta)\geq 0$,
then it must be the case that $\mathcal{B}_{i}(y)\leq 0$ by construction as
$q_{\chi}\in Q_{l}$. This is a contradiction.

∎

##  Appendix 0.C Closure Certificate for the two room example and NBA in
Figure 3

We define the closure certificate $\mathcal{T}(x_{0},x_{1},i,,y_{0},y_{1},j)$
as

|  | $\mathcal{T}(x,_{0},x_{1},i,y_{0},y_{1},j)=$ |  |  |
---|---|---|---|---|---
$-10$ | $-10(j-i)$ | $-1.3251i^{2}j$ | $+1.3251j^{2}i$ | $-0.7099i^{2}$ | $+5.2962j^{2}$
$-7.5718i$ | $+20j$ | $+10x_{0}$ | $-7.6132x_{1}$ | $+10y_{0}$ | $-10y_{1}$
$-2.4802y_{0}j$ | $-0.0270x_{0}i$ | $+0.2000x_{1}i$ | $-2.5238y_{1}j$ | $+0.1791x_{0}^{2}$ | $-0.2006x_{0}x_{1}$
$-0.0060y_{0}^{2}$ | $-0.0003y_{0}y_{1}$ | $-2.5277(x_{0}-x_{1})$ | $-10(y_{0}-y_{1})$ | $-10(x_{0}-y_{0})$ | $-10(x1-y1)$
$+0.5607x_{1}^{2}$ | $0.007856y_{1}^{2}$ | $-0.0002y_{1}^{3}$ | $+0.0001y_{0}^{3}$ | $+0.1893i^{3}j$ | $-0.1893j^{3}i$

where $(x_{0},x_{1})\in\mathcal{X}$ and $(y_{0},y_{1})\in\mathcal{X}$ are
states that denote the two room temperatures, and $i,j\in\\{0,1,\ldots,4\\}$
are the automaton states.