Symbolic Analysis of Linear Hybrid Automata – 25 Years Later

Abstract

We present a collection of advances in the algorithmic verification of hybrid automata with piecewise linear derivatives, so-called Linear Hybrid Automata. New ways to represent and compute with polyhedra, in combination with heuristic algorithmic improvements, have led to considerable speed-ups in checking safety properties through set propagation. We also showcase a CEGAR-style approach that iteratively constructs a polyhedral abstraction. We illustrate the efficiency and scalability of both approaches with two sets of benchmarks.

1 Introduction

Hybrid automata are a modeling paradigm that combines finite state machines with differential equations in order to capture processes in which discrete, event-based, behavior interacts with continuous, time-based behavior. They came to rise in the beginning of the 1990s, throughout a collaboration of scientists from various disciplines, notably computer scientists and control theorists. By that time, formal methods such as abstract interpretation [19] and model checking [18, 44] had demonstrated their potential to increase the trustworthiness of safety critical software and digital hardware designs. The goal was to develop similar techniques for discrete systems that interact with processes that can be described by differential equations, like some mechanical or biological processes, so-called hybrid systems. In The Theory of Hybrid Automata, whose first version was published 25 years ago in 1996, Tom Henzinger pointed out a class of hybrid automata that hit a particular sweet spot for the purposes of symbolic (set-based) analysis: linear hybrid automata (LHA). LHA are characterized by linear predicates over the continuous variables and the evolution of the continuous variables is governed by differential inclusions that depend only on the discrete state, not the continuous variables themselves. LHA readily lend themselves as sound abstractions of complex natural and technical processes and as asymptotically complete approximations of a large class of hybrid automata [35]. While properties like safety are not decidable for LHA, the states reachable over a given finite path can be computed exactly and symbolically, in the form of continuous sets associated to discrete states. In a sense, the continuous time domain can be abstracted away for LHA, so that the symbolic analysis resembles that of linear programs. Consequently, techniques from linear program analysis, such as the polyhedral computations in [30], could be applied. This led to symbolic analysis tools such as the pioneering model checker HyTech [33]. Since then, much research effort has been invested in making symbolic analysis more efficient, in order to scale up to systems of practical interest.

In this paper, we present a selection of techniques that, applied to the symbolic analysis of LHA, have led to performance improvements of several orders of magnitude since the days of HyTech. We focus entirely on safety properties encoded as reachability problems, i.e., whether a state is reachable from any state in a given set of initial states. We start with a simple fixed-point algorithm for computing reachable sets of states, using convex polyhedra as set representations. We then present various advances in polyhedral computations as well as efficient abstractions that serve as heuristics to speed up the fixed-point algorithm, and illustrate the performance gains with experiments. As an alternative approach, we also present a technique based on the CEGAR (Counter-Example Guided Abstraction Refinement) paradigm. Starting from an initial, coarse abstraction, the finite-path encoding of LHA is used to iteratively refine the abstraction until either a counterexample has been found or the system is proved safe. Our overview is far from exhaustive and limited to work by the authors. We point the reader to the references in [1, 3, 40, 51] for related work. Other CEGAR approaches are implemented, e.g., in the tools HARE [46] and HyCOMP/IC3 [13]. To take an instance of an entirely different approach, we point to the work in [43], where LHA are encoded as linear programs, which are then analyzed by the software model checker ARMC. Bounded model checking for LHA has been implemented in the tool BACH [14].

The remainder of the paper is structured as follows. In Sect. 2, we define linear hybrid automata and give a brief overview on set-based reachability. In Sect. 3 we show how set-based reachability can be implemented efficiently, either exactly or by resorting to overapproximations. In Sect. 4 we present a CEGAR framework than can further enhance scalability. In Sect. 5, a series of experiments illustrates the impact of the different approaches and techniques on performance. Finally, we conclude in Sect. 6.

2 Symbolic Analysis of Linear Hybrid Automata

Hybrid automata describe the evolution of a set of real-valued variables over time. In this section, we give a formal definition of hybrid automata and their behaviors, and illustrate the concept with an example. But first, we introduce some notation for describing real-valued variables and sets of these values in the form of predicates and polyhedra.

2.1 Preliminaries

Variables: Let $X = \{x_1, \dots , x_n\}$ be a finite set of variables. A valuation over X is written as ${x} \in \mathbb {R}^X$ or ${x}: X \rightarrow \mathbb {R}$. We use the primed variables $X' = \{x_1', \dots , x_n'\}$ to denote successor values and the dotted variables $\dot{X} = \{\dot{x}_1, \dots , \dot{x}_n\}$ to denote the derivatives of the variables with respect to time. Given a set of variables $Y \subseteq X$, the projection ${y} ={x} \downarrow _{ Y}$ is a valuation over Y that maps each variable in Y to the same value that it has in x. We may simply use a vector ${x} \in \mathbb {R}^n$ if it is clear from the context which index of the vector corresponds to which variable. We denote the i-th element of a vector ${x}$ as ${x} _i$ or ${x} (i)$ if the former is ambiguous. In the following, we use $\mathbb {R}^n$ instead of $\mathbb {R}^X$ except when the correspondence between indices and variables is not obvious, e.g., when valuations over different sets of variables are involved.

Predicates: A predicate over X is an expression that, given a valuation ${x}$ over X, can be evaluated to either true or false. A linear constraint is a predicate $a_1 x_1+a_2 x_2+ \cdots +a_n x_n \bowtie b,$ where $a_1,\ldots a_n$ and b are real-valued constants, and whose sign may be strict or nonstrict (i.e., $\mathop {\bowtie } \in \{ \mathop {<}, \mathop {\le }\}$). A linear constraint is written in vector notation as ${a}^{\textsf{T}}\!{x} \bowtie b,$ with coefficient vector ${a} \in \mathbb {R}^n$ and inhomogeneous coefficient $b \in \mathbb {R}$. A halfspace $\mathcal {H} \subseteq \mathbb {R}^n$ is the set of points satisfying a linear constraint. A predicate over X defines a continuous set, which is the subset of $\mathbb {R}^X$ on which the predicate evaluates to true.

Polyhedra: A conjunction of finitely many linear constraints defines a polyhedron in constraint form, also called $\mathcal {H}$-polyhedron,

$$\mathcal {P} = \Bigl \{ {x} \Bigm | {\bigwedge }_{i=1}^{m} {a}_i^{\textsf{T}}\!{x} \bowtie _i b_i \Bigr \}, \text { with } \mathop {\bowtie _i} \in \{ \mathop {<}, \mathop {\le } \}, $$

with facet normals ${a}_i\in \mathbb {R}^n$ and inhomogeneous coefficients $b_i\in \mathbb {R}$. A bounded polyhedron is called a polytope. Note that the set of constraints defining $\mathcal {P}$ is not necessarily unique. The representation of a polyhedron has a big impact on the computational cost of different geometric operations. Other representations for polyhedra can be more efficient for model checking, and will be discussed in detail in Sect. 3.

2.2 Linear Hybrid Automata

We now give a formal definition of a linear hybrid automaton and its run semantics.

Definition 1 (Linear Hybrid Automaton)

[2, 32, 36] A linear hybrid automaton $H=(X, \textsf{Loc}, \textsf{Edg}, \textsf{Lab}, \textsf{Init}, \textsf{Inv}, \textsf{Flow}, \textsf{Jump}, \textsf{Event})$ consists of

• a finite set of variables $X = \{x_1, \dots , x_n\}$, partitioned into uncontrolled variables U and controlled variables Y;

• a finite directed multigraph $(\textsf{Loc}, \textsf{Edg})$, called the control graph, which consists of a set of locations $\textsf{Loc}= \{\ell _1, \dots , \ell _m\}$ that represent discrete modes, and a set of edges $\textsf{Edg}$ that represent discrete transitions between modes;

• a finite set of synchronization labels $\textsf{Lab}$;

• a polyhedral constraint over variables $\textsf{Inv}(\ell ) \in \mathbb {R}^{X}$ called invariant or staying condition, which restricts the values the variables can possibly take over location $\ell \in \textsf{Loc}$; a state of H consists of a location $\ell$ and a value $x \in \textsf{Inv}(\ell )$ for the variables, and is denoted by $s=(\ell ,{x})$;

• a polyhedral constraint $\textsf{Init}(\ell ) \subseteq \textsf{Inv}(\ell )$ called initial condition, which determines the set of initial values for the variables at location $\ell \in \textsf{Loc}$; every behavior of H must start in one of the initial conditions;

• a polyhedral constraint over dotted variables $\textsf{Flow}(\ell ) \subseteq \mathbb {R}^{\dot{X}}$ called flow condition, which gives for each location $\ell \in \textsf{Loc}$ the set of possible derivatives a trajectory can possibly take using a differential inclusion such as $\dot{{x}} \in \textsf{Flow}(\ell );$

• a polyhedral constraint $\textsf{Jump}(e) \subseteq \mathbb {R}^{X} \times \mathbb {R}^{X'}$ over unprimed and primed variables called jump relation, which defines the set of possible successors ${x} '$ of ${x}$ when transition $e \in \textsf{Edg}$ is taken; jump relations are typically given by a polyhedral guard constraint $\mathcal {G} _e \subseteq \mathbb {R}^X$ and an affine assignment (or reset) ${x} '=r_e({x})$ as $\textsf{Jump}(e) = \{ ({x},{x} ') \mid {x} \in \mathcal {G} _e \wedge {x} '=r_e({x}) \};$ also, under certain definitions, every location $\ell$ is associated with an uncontrolled transition ${\bar{e}} \in \textsf{Edg}$ from l to itself and jump relation defined as $\textsf{Jump}({\bar{e}}) = \{ ({x},{x} ') \mid {{x} '}\downarrow _{ Y} = {x} \downarrow _{ Y} \wedge {x} ' \in \textsf{Inv}(\ell ) \},$ which represents arbitrary assignments that the environment might perform on the uncontrolled variables $U=X\setminus Y$;

• an event function $\textsf{Event}(e) \in \textsf{Lab}\cup \{ \tau \}$ that maps every edge $e \in \textsf{Edg}$ to either a synchronization label or the internal event $\tau$; uncontrolled transitions are always mapped to $\tau$.

We define the behavior of a hybrid automaton with a run: starting from one of the initial states, the state evolves according to the differential equations whilst time passes, and according to the jump relations when taking an (instantaneous) transition.

Definition 2 (Run semantics)

A run of H is a sequence

$$\begin{aligned} (\ell _0,{x} _0) \xrightarrow {\delta _0} (\ell _0,y_0) \xrightarrow [e_1]{\alpha _1} (\ell _1,{x} _1) \xrightarrow {\delta _1} (\ell _1,y_1) \xrightarrow [e_2]{\alpha _2} \ldots \xrightarrow {\delta _k} (\ell _k,y_k), \end{aligned}$$

that satisfies for the three conditions listed below.

• 1. Initialisation: the first state satisfies an initial condition, i.e., ${x} _0 \in \textsf{Init}(\ell _0)$.

• 2. Continuous flow: for every $i = 0, \dots , k$, there exist a trajectory $\xi : [0,\delta _i] \rightarrow \mathbb {R}^X$ from $x_i$ to $y_i$ and with dwell time $\delta _i \in \mathbb {R}_{\ge 0}$ over location $l_i$, that is, $\xi$ is a continuously differentiable function such that $\xi (0) = x_i$, $\xi (\delta _i) = y_i$, and it holds true that $\dot{\xi }(t) \in \textsf{Flow}(\ell _i)$ and $\xi (t) \in \textsf{Inv}(\ell _i)$ for all $t \in [0,\delta _i]$.

• 3. Discontinuous jumps: for every $i=1,\dots ,k$ we have that $e_i \in \textsf{Edg}$ has source $\ell _{i-1}$ and destination $\ell _{i}$, $\alpha _i = \textsf{Event}(e_i)$, and $(y_{i-1},{x} _{i}) \in \textsf{Jump}(e_i)$.

A state $(\ell ,{x})$ is reachable if there exists a run with $(\ell _i,{x} _i)=(\ell ,{x})$ for some i.

The existence of a run can be reduced to satisfiability of a conjunction of linear constraints. This has been exploited to synthesise parameters [27] and in Counter Example Guided Abstraction Refinement (CEGAR) frameworks [38], which we will discuss in more detail in Sect. 4. It also follows from these semantics that with a simple model transformation,¹ a LHA can be verified by model checkers able to handle linear constraints over the rationals, see [43].

2.3 Symbolic Analysis

A standard method to compute the reachable states is to iterate the following one-step successor operators for discrete and continuous transitions. Given a set of variables valuations $S \subseteq \mathbb {R}^n$, let $\textsf{post}_C(\ell , S)$ be the set of valuations reachable by letting time elapse from any valuation in S over location $\ell \in \textsf{Loc}$,

$$\begin{aligned} \textsf{post}_C(\ell , S) = \Bigl \{ y \Bigm | \exists x \in S, \delta \in \mathbb {R}_{\ge 0} :(\ell ,{x}) \xrightarrow {\delta } \bigl (\ell ,y\bigr ) \Bigr \}. \end{aligned}$$

(1)

Let $\textsf{post}_D(e, S)$ be the set of valuations resulting from transition $e\in \textsf{Edg}$ from any valuation in S

$$\begin{aligned} \textsf{post}_D(e, S) = \Bigl \{ {x} ' \Bigm | \exists {x} \in S : (\ell ,{x}) \xrightarrow [e]{\alpha } (\ell ',{x} ') \Bigr \}, \end{aligned}$$

(2)

where $\ell$ and $\ell '$ are source and target locations of e and $\alpha = \textsf{Event}(e)$.

Starting from the initial states, $\textsf{post}_C$ and $\textsf{post}_D$ are applied in alternation along the structure of the control graph.

In model checkers such as HyTech [33], PHAVer [22] and SpaceEx [28], the symbolic analysis of a linear hybrid automaton is performed using symbolic states $s=(\ell ,\mathcal {P})$, where $\ell \in \textsf{Loc}$ and $\mathcal {P}$ is a polyhedron. Computing the timed successors $\textsf{post}_C$ of a symbolic state $s=(\ell ,\mathcal {P})$ produces a new symbolic state $s'=(\ell ,\mathcal {P} ')$. Computing the jump successors $\textsf{post}_D$ of $s=(\ell ,\mathcal {P})$ involves iterating over all outgoing transitions of $\ell$, and produces a set of symbolic states, each in one of the target locations. A waiting list contains the symbolic states whose successors still need to be explored, and a passed list contains all symbolic states computed so far. The fixed-point computation proceeds according to the steps below.

• 1. Initialization: compute the continuous successors of the initial states, put them on the waiting list, and proceed to step 2.

• 2. Containment checking: pop a symbolic state $s = (\ell , \mathcal {P})$ from the waiting list and check whether it has been encountered before, i.e., it is subsumed by some symbolic state in passed or waiting list. Repeat step 2 until either the waiting list is empty or a never encountered state is found. If the waiting list is empty, terminate and return. If a new state is found, proceed to step 3.

• 3. Post computation: compute all one-step successors $\textsf{post}_C(\ell ', \textsf{post}_D(e, \mathcal {P}))$ of s along all transition e that are outgoing from $\ell$ (and have destination $\ell '$) and push them to the waiting list. Add s to the passed list and repeat step 2.

Upon termination of the procedure (which happens empirically, and is not guaranteed in general), the passed list R represents the whole set of reachable states.

An important aspect of the fixed point algorithm outlined above is that it attempts to reduce redundant exploration. This is taken care of by step 2, resp. line 6 in Algorithm 1, which implicitly performs the following operations:

• 2.1 it discards states that are contained in any symbolic state on the passed list,

• 2.2 it discards states that are contained in any remaining symbolic state on the waiting list—this is known as waiting list filtering.

Note that filtering the waiting list is a heuristic, which may or may not lead to an efficiency improvement with respect to a containment check over the passed list only; however, in practice, it leads to savings in computational time which compensates for the overhead of comparing a large number of symbolic states.

3 Implementing Symbolic Analysis Using Polyhedra

In this section we briefly describe how to implement the symbolic analysis outlined in Sect. 2.3 when adopting a domain of convex polyhedra for the representation of symbolic states.

The Double Description Method 

Even though there exist polyhedra libraries that are exclusively based on the constraint form,² the classical approach [20] is based on the Double Description (DD) method [42], where the constraint form is paired with a generator form and conversion algorithms [16] can compute each representation from the other, removing redundancies so as to obtain minimal descriptions, as well as keeping them in synch after an incremental update. Polyhedra libraries based on the DD method include PolyLib (www.irisa.fr/polylib/), ELINA [50], NewPolka in Apron [37], PPL (Parma Polyhedra Library) [6], and PPLite [10]; the last three also support strict linear constraints.

Generator Form and $\mathcal {V}$-Polyhedra. The classical definition of generators for closed polyhedra has been extended in [6] to the case of NNC (not necessarily closed) polyhedra. Namely, an $\mathcal {H}$-polyhedron can be equivalently represented in generator form by three finite sets (P, C, R), where $P \subseteq \mathbb {R}^n$ is a set of points of $\mathcal {P}$ (including its vertices), $C \subseteq \mathbb {R}^n$ is a set of closure points, and $R \subseteq \mathbb {R}^n$ is a set of rays. The generator form defines a $\mathcal {V}$ -polyhedron as

$$ \mathcal {P} = { \left\{ \, \sum _{p_i \in P} \pi _i \cdot p_i + \sum _{c_j \in C} \gamma _j \cdot c_j + \sum _{r_k \in R} \rho _k \cdot r_k \,\left| \, \begin{array}{@{}l@{}} \pi _i \ge 0, \gamma _j \ge 0, \rho _k \ge 0, \\ \textstyle {\sum _{i} \pi _i + \sum _{j} \gamma _j = 1}, \textstyle {\sum _{i} \pi _i \ne 0}, \end{array} \right. \,\right\} } $$

which consists of the convex hull of points and closure points, extended towards infinity along the directions of the rays; the requirement that at least one point $p_i$ positively contributes to the convex combination means that the closure points, which are in the topological closure of $\mathcal {P}$, are not necessarily contained in $\mathcal {P}$.

Both NewPolka and PPL, following the approach outlined in [30, 31] and further developed in [5], use an additional slack variable (usually named $\epsilon$) to encode the strict constraints as nonstrict ones, obtaining closed $\epsilon$-representations of the NNC polyhedra. While allowing for a simple reuse of the classical conversion algorithms, this choice easily leads to a significant computation overhead. In contrast, the PPLite library is based on a direct representation for the strict constraints, leveraging on enhanced versions of the Chernikova procedures [7, 8] fully supporting the use of strict constraints and closure points.

Converting Between $\mathcal {H}$ and $\mathcal {V}$ Representations. No matter if using the direct or the slack variable representation, the core algorithmic step of the DD method $\langle \mathcal {H}, \mathcal {V} \rangle \xrightarrow {\beta } \langle \mathcal {H} ', \mathcal {V} ' \rangle$ modifies a DD pair by adding a single constraint (resp., generator) $\beta$. From this, the conversion procedure computing the generator form $\mathcal {V} = \mathcal {V} _m$ for a given constraint form $\mathcal {H} = \{ \beta _0, \dots , \beta _m \}$ is obtained by incrementally processing the constraints, starting from a DD pair $\langle \mathcal {H} _0, \mathcal {V} _0 \rangle \equiv \mathbb {R}^n$ representing the whole vector space:

$$ \langle \mathcal {H} _0, \mathcal {V} _0 \rangle \xrightarrow {\beta _0} \dots \xrightarrow {\beta _{k-1}} \langle \mathcal {H} _k, \mathcal {V} _k \rangle \xrightarrow {\beta _k} \langle \mathcal {H} _{k+1}, \mathcal {V} _{k+1} \rangle \xrightarrow {\beta _{k+1}} \dots \xrightarrow {\beta _m} \langle \mathcal {H} _m, \mathcal {V} _m \rangle . $$

The conversion from generators to constraints works similarly, starting from a DD pair representing the empty polyhedron and incrementally adding the generators. The same approach can also be used to compute the set intersection $\mathcal {P} _1 \cap \mathcal {P} _2$ (resp., the convex polyhedral hull $\mathcal {P} _1 \uplus \mathcal {P} _2$) of polyhedra $\mathcal {P} _1 \equiv \langle \mathcal {H} _1, \mathcal {V} _1 \rangle$ and $\mathcal {P} _2 \equiv \langle \mathcal {H} _2, \mathcal {V} _2 \rangle$: the constraints in $\mathcal {H} _2$ (resp., the generators in $\mathcal {V} _2$) are incrementally added to the DD pair describing $\mathcal {P} _1$.

Cartesian Factoring. Converting between $\mathcal {H}$ and $\mathcal {V}$ polyhedra has a worst case complexity that is exponential in the size of the input representation; it is therefore essential to keep representations small, e.g., by removing redundancies. Cartesian factoring [29] can greatly reduce the space needed to represent a $\mathcal {V}$-polyhedron. The space dimensions $X = \{ x_1, \dots , x_n \}$ are partitioned into a sequence of blocks $( B_1, \dots , B_k )$ so that each linear constraint in the $\mathcal {H}$-representation mentions the dimensions of a single block $B_i$; then, the $\mathcal {H}$-polyhedron $\mathcal {P}$ is factored into k polyhedra $(\mathcal {P} _1, \dots , \mathcal {P} _k)$; if needed, these $\mathcal {H}$-polyhedra are converted to a sequence of $\mathcal {V}$-polyhedra. This can be much more efficient in time and space compared to a direct conversion. The ELINA library [50] uses a very efficient implementation of Cartesian factoring; the technique is also implemented in PPLite.

Implementation of Containment Checks 

The overall efficiency of the procedure computing the set of reachable states is deeply affected by the efficiency of the polyhedra containment check. When using the DD method, the inclusion test $\mathcal {P} _1 \subseteq \mathcal {P} _2$ is implemented by checking that all the $m_1$ generators of $\mathcal {P} _1$ satisfy all the $m_2$ constraints of $\mathcal {P} _2$. In the worst case, i.e., when the inclusion holds, this amounts to the computation of $m_1 \cdot m_2$ scalar products, each one requiring $\mathcal {O}(n)$ arbitrary precision multiplications and additions, where n is the number of variables.

Fig. 1.

Incomplete decision procedures speed up the containment checks.

As shown in [9], impressive efficiency improvements can be obtained by exploiting the fact that each one-step successor state $s'_i$ is checked against all the states stored in the passed list before being added to the passed and waiting lists. It is therefore possible to compute, and cache for reuse, simpler abstractions of the polyhedra that are enough to quickly semi-decide the containment check. The boxed polyhedra proposal in [9] uses a two-level scheme, where each polyhedron $\mathcal {P} _i$ is abstracted into its bounding box $\mathcal {B} _i$, which in turn is further abstracted in the pseudo-volume information.³

Figure 1 shows a few examples, where for each polyhedron $\mathcal {P} _i$ (solid blue) we draw the corresponding bounding box $\mathcal {B} _i$ (dashed black). Intuitively, we know that $\mathcal {P} _1 \not \subseteq \mathcal {P} _2$ because $\mathop {\textrm{vol}}\nolimits (\mathcal {B} _1) > \mathop {\textrm{vol}}\nolimits (\mathcal {B} _2)$; we know that $\mathcal {P} _3 \not \subseteq \mathcal {P} _1$ because $\mathop {\mathrm {num\_rays}}\nolimits (\mathcal {B} _3) = 1 > 0 = \mathop {\mathrm {num\_rays}}\nolimits (\mathcal {B} _1)$; we know that $\mathcal {P} _2 \not \subseteq \mathcal {P} _4$ because $\mathcal {B} _2 \not \subseteq \mathcal {B} _4$ (even though $\mathop {\textrm{vol}}\nolimits (\mathcal {B} _2) = \mathop {\textrm{vol}}\nolimits (\mathcal {B} _4)$ and $\mathop {\mathrm {num\_rays}}\nolimits (\mathcal {B} _2) = \mathop {\mathrm {num\_rays}}\nolimits (\mathcal {B} _4)$); finally, when checking whether or not $\mathcal {P} _5 \subseteq \mathcal {P} _6$, since $\mathcal {B} _5 \subseteq \mathcal {B} _6$ no semi-decision procedure applies and we need to resort to the more expensive polyhedra containment check.

Implementing the Continuous Post Operator 

For a fixed location $\ell$, the flow relation of an LHA is specified by a polyhedron $\mathcal {Q}_\ell = \textsf{Flow}(\ell )$ describing the possible values of the first time derivatives of the system variables. The possible trajectories starting from the states in polyhedron $\mathcal {P}$ are obtained by the time-elapse operator:

$$\begin{aligned} \mathcal {P} \mathop {\nearrow }\nolimits \mathcal {Q}_\ell = \{\, p + t \cdot q \mid p \in \mathcal {P}, q \in \mathcal {Q}_\ell , t \in \mathbb {R}, t \ge 0 \,\}. \end{aligned}$$

(3)

Assuming that $\mathcal {Q}_\ell$ is a closed $\mathcal {V}$-polyhedron described by generators (P, C, R), where $C = \emptyset$, the set $\mathcal {P} \mathop {\nearrow }\nolimits \mathcal {Q}_\ell$ is a convex polyhedron that can be computed by (incrementally) adding to $\mathcal {P}$ the finite set of rays $R' = P \cup R$ [30].⁴

An example of applying the continuous post operator to a symbolic state $(\ell , \mathcal {P})$ is shown on the left hand side of Fig. 2. Suppose that $\mathcal {I}_\ell = \textsf{Inv}(\ell )$ and $\mathcal {Q}_\ell = \textsf{Flow}(\ell )$ are the polyhedra representing the invariant and the flow condition for location $\ell$. Then, $\textsf{post}_C(\ell , \mathcal {P}) = (\mathcal {P} \mathop {\nearrow }\nolimits \mathcal {Q}_\ell ) \cap \mathcal {I}_\ell = \mathcal {R}$,⁵ is computed by first adding rays $r_1$ and $r_2$ to $\mathcal {P}$ and then computing set intersection to restore the invariant $\mathcal {I}_\ell$.

Fig. 2.

Continuous and discrete post operators.

Implementing the Discrete Post Operator 

The discrete post operator can be implemented by combining several lower level operators on the polyhedra domain.

Uncontrolled Assignments. Consider first the case of an uncontrolled assignment to the variables in the set $U \subseteq X$. In order to avoid projection (which would imply a change of space dimension), this can be implemented by the existential quantification of the variables in U, followed by the intersection with the location invariant. When using the DD method, existential quantification is obtained by (incrementally) adding the set of rays $R_U = \{\, e_u, -e_u \mid u \in U \,\}$, where each $e_u$ is the standard basis vector for variable u.⁶

Guarded Assignments. Let $e \in \textsf{Edg}$ be a transition composed by a polyhedral guard $\mathcal {G}$ and a reset $x' = r_e(x)$ only containing affine assignments. Then, the image of relation $\textsf{Jump}(e)$ on input $\mathcal {P}$ can be computed as $\mathcal {P} ' = r_e[\mathcal {P} \cap \mathcal {G} _e]$, where $r_e[X] = \{ r_e(x) :x \in X \}$ denotes the image of set $X \subseteq \mathbb {R}^n$ though the linear transformation $r_e$. To avoid inefficiencies, particular care has to be taken when implementing the image of linear transformation $r_e[\cdot ]$. Most polyhedra libraries implement a sequential assignment operator, which can be directly used when the (parallel) reset operator $r_e$ does not contain cyclic dependencies, so that the assignments can be topologically sorted without affecting their semantics. The sequential assignment further distinguishes between invertible and non-invertible assignments. In the invertible case (e.g., $x'_1 = 2 \cdot x_1 + x_2$), both the constraint and the generator forms can be updated by simply applying $r_e^{-1}$ and $r_e$, respectively. In the non-invertible case (e.g., $x'_1 = x_2 + 3$), only the generator form is updated (using $r_e$), while the constraint form has to be recomputed from scratch using the conversion procedure. An alternative approach, better exploiting the incrementality of the DD method, implements the non-invertible assignment by temporarily adding a fresh variable. Letting $X' = X \setminus \{ x_1 \} \cup \{ x'_1 \}$, the assignment $x'_1 = \textrm{rhs}$ can be computed as⁷

$$\begin{aligned} \bigl ( (\mathcal {P} \uparrow _{\{ x'_1 \}}) \mathrel {\cap } \{ x'_1 - \textrm{rhs} \le 0, \textrm{rhs} - x'_1 \le 0 \} \bigr ) \downarrow _{X'}, \end{aligned}$$

(4)

followed by a renaming of $x'_1$ into $x_1$. This approach has been extended in [9] so as to be also applicable to parallel assignments having cyclic dependencies: the parallel assignment is compiled into an equivalent sequence of sequential assignments, taking care to introduce a minimal number of fresh variables (only when breaking a dependency cycle).

An example of application of the discrete post operator is shown in the middle of Fig. 2. Suppose that there exists a single transition e exiting from source location $\ell$ to target location $\ell '$, having the polyhedron $\mathcal {G} _e$ as guard component and a reset component modeled by affine transformation $r_e$ (which combines a rotation and a translation); let also $\mathcal {I}_{\ell '}$ be the invariant for the target location $\ell '$. Then, starting from $\mathcal {R}$, we obtain $\textsf{post}_D(e, \mathcal {R}) = r_e[\mathcal {R} \cap \mathcal {G} _e] \cap \mathcal {I}_{\ell '} = r_e[\mathcal {S}] \cap \mathcal {I}_{\ell '} = \mathcal {S}' \cap \mathcal {I}_{\ell '} = \mathcal {P} '$. On the right hand side of Fig. 2 we also show an example where, by using the boxed polyhedra proposal of [9], it is sometimes possible to efficiently detect disabled transitions. Namely, the cheaper (but incomplete) check for disjointness $\mathcal {B} _1 \cap \mathcal {B} _2 = \emptyset$ on the bounding boxes $\mathcal {B} _1$ and $\mathcal {B} _2$ for the polyhedron state $\mathcal {P} _1$ and the polyhedral guard $\mathcal {G} _2$, when successful, is enough to conclude that $\mathcal {P} _1$ and $\mathcal {G} _2$ are disjoint too.

Computing Overapproximations for Scalability 

While some verification tasks require the exact symbolic computation of the set of reachable states, there exists cases where an overapproximation may be good enough (e.g., when trying to prove a safety property of the hybrid automaton). One possibility is to choose a less precise symbolic domain, such as octagons [41] or template polyhedra [48]. A less radical alternative is to maintain the full generality of the domain of convex polyhedra and give up some precision in specific contexts or on specific operators. As a classical example, in [31] all symbolic states $(\ell _i, \mathcal {P} _i)$ for location $\ell _i$ are merged into a single state $(\ell _i, \uplus \{ \mathcal {P} _i \})$. Since the computation of the convex polyhedral hull might still be expensive, it can be further approximated by computing, for instance, their constraint hull $(\ell _i, \uplus _{\textrm{w}} \{ \mathcal {P} _i \})$ (also called weak join [47]): this resembles the join operator defined on template polyhedra, since it is restricted to only use those constraint slopes that already occur in the arguments. Figure 3 shows a simple example of the different levels of overapproximation obtained. At the implementation level, the constraint hull of a set of polyhedra can be computed either by solving many Linear Programming problems or by enumerating the generators of the arguments. The latter approach is adopted in PPLite, which is the only library based on the DD method directly supporting this operator. Some tools (e.g., PHAVer) allow for the user to choose if and how to approximate set union by using a single polyhedron per location.

Fig. 3.

Set union overapproximations: polyhedral hull vs. constraint hull.

4 Symbolic Analysis Using CEGAR

An exact reachability analysis using polyhedra provides strong soundness guarantees in the sense that, if a counterexample to a safety property is identified over the symbolic representation, then corresponding a trajectory must exist in the system. Also, if the analysis finds a fixed point without identifying any counterexample, then the system is safe. However, an exact symbolic analysis is computationally costly. Computing the image of a post operator amounts to a projection of a system of linear inequalities over the output variables of the operator. Methods for computing projections include quantifier elimination methods as, e.g., the Fourier-Motzkin algorithm [52], or double-description methods (see Sect. 3), which suffer from exponential complexity blow-ups in the worst case. Moreover, tight representations of the reachable states may in some cases prevent the reachability algorithm from identifying a fixed point and, therefore, produce an answer at all; conversely, coarser abstractions can help reaching a fixed point. A method that tackles the above shortcomings is abstraction.

Fig. 4.

The wrapping effect.

Abstractions for hybrid systems come with a wide variety of flavors, which typically depend both on the kind of systems under analysis and the safety specifications of interest. Examples are abstractions based on interval arithmetic, which enjoy a high generality as they can even account for system dynamics described using polynomial and transcendental functions (that is, more general than LHA) and also enjoy high efficiency. On the other hand, interval analysis suffers from the wrapping effect. An example for the wrapping effect is shown in Fig. 4. The system in this example rotates an ellipse counterclockwise by 45$^\circ$ in discrete time steps, that is, a two-dimensional systems whose dynamic is governed by a linear difference equation. An abstraction based on interval analysis constructs rectangles (1) whose facets are orthogonal to the axes of the state space of interest and (2) that over-approximate the initial set of states (the init set) and the result of every computation of the post operator. In this instance, at the first step (Fig. 4a) the abstraction constructs a rectangle that encloses the init but also includes states that do not belong to it, introducing a small error. At the second step (Fig. 4b) the post operator is first applied to the abstract set of states (depicted with dashed lines) and then abstracted again within a larger rectangle, which introduces a further error with respect to the original set of states (the ellipse). The process is repeated over the third (Fig. 4c) and all successive steps, and this causes an ever increasing accumulation of over-approximation error.

Abstract safety analysis based on over-approximation conserves soundness in the sense that, upon termination, if the abstract reach set is disjoint from an unsafe region then the system is safe. However, it loses the property for which counterexamples are always genuine. An example can be constructed over Fig. 4, considering a bad region that intersect an abstract set of states (a rectangle) but does not intersect the concrete set of states (the ellipse). In this case, an abstract safety analyser would produce a spurious counterexample to safety. On the other hand, it should be clear that if a bad region is disjoint from the abstract states then it is also disjoint from the concrete states.

Fig. 5.

Template polyhedra.

Abstractions are lightweight to compute, but may produce spurious counterexamples. Exact safety analysis always produces genuine counterexamples, but relies on heavy machinery. The approach that capitalises over the advantages of both worlds is counterexample-guided abstraction refinement (CEGAR) [17]. It consists of two phases, one that abstracts the system and another which refines the abstraction, which interact in a loop. The fundamental ingredient of a CEGAR loop is an abstraction that admits refinement, that is, an abstraction whose precision can be made tighter and tighter by changing some parameters. One example of parameterised abstraction is that of template polyhedra, which has been successfully applied not only to the verification of LHA [21], but also computer programs [49], hybrid automata with linear ODEs [39, 48], and more recently neural network control [4]. Formally, template polyhedra are defined in terms of supporting halfspaces, which are in turn defined in terms of support functions. Given a convex set of states $\mathcal{X} \subseteq \mathbb {R}^n$, the support function of $\mathcal X$ in a direction $\delta \in \mathbb {R}^n$ is

$$\begin{aligned} \rho _\mathcal{X}(\delta ) = \sup \{ \langle x, \delta \rangle :x \in \mathcal{X}\}, \end{aligned}$$

(5)

namely, the supremum of the inner product of $\delta$ with all elements of $\mathcal X$ [45]. This gives the offset with respect to the origin of the tightest halfspace contaning $\mathcal X$—the supporting halfspace—that is orthogonal to $\delta$. Finally, a template polyhedron of $\mathcal X$ is a finite intersections of supporting halfspaces of $\mathcal X$ that are orthogonal to a finite set of directions $\varDelta \subset \mathbb {R}^n$. We call $\varDelta$ a template and define the $\varDelta$-polyhedron of $\mathcal X$ as the following set:

$$\begin{aligned} \cap \{ \underbrace{\{ x :\langle x, \delta \rangle \le \rho _\mathcal{X}(\delta ) \}}_{\text {supporting halfspace}} :\delta \in \varDelta \}. \end{aligned}$$

(6)

Rectangular and octagonal abstractions are special cases of templates polyhedra, as Fig. 5a and b exemplify; an arbitrary template parameterizes the shape of the polyhedron as shown in Fig. 5c.

In this section, abstract safety analysis can be seen as the procedure in Algorithm 1, but where $\mathcal {P}$ and $\mathcal {P} '$ are over-approximated as template polyhedra at respectively lines 2 and 9. Similarly to Sect. 3, we interpret the post operators as operators over sets of states in $\mathbb {R}^n$ as follows:

$$\begin{aligned} \textsf{post}_C(\ell , \mathcal {P})&= ((\mathcal {P} \cap \mathcal {I}_\ell ) + {{\,\textrm{coni}\,}}\mathcal {Q}_\ell ) \cap \mathcal {I}_\ell \end{aligned}$$

(7)

$$\begin{aligned} \textsf{post}_D(e, \mathcal{R})&= A_e[\mathcal{R} \cap \mathcal {G} _e] + \{b_e\}, \end{aligned}$$

(8)

where $\mathcal {I}_\ell = \textsf{Inv}(\ell )$ are invariant and $\mathcal {Q}_\ell = \textsf{Flow}(\ell )$ and flow constraint of location $\ell$, and transition $e \in \textsf{Edg}$ is modeled as a guarded assignment with guard $\mathcal {G} _e$ and affine reset function $r_e(x) = A_ex + b_e$, with $A_e \in \mathbb {R}^{n \times n}$ and $b_e \in \mathbb {R}^n$ (a post operator for general jump conditions is described in [11]). Operator $\textsf{post}_C(\ell , \mathcal {P})$ in Eq. 7 represents time elapse over a mode $\ell$, and is equivalent to $((\mathcal {P} \cap \mathcal {I}_\ell ) \mathop {\nearrow }\nolimits \mathcal {Q}_\ell ) \cap \mathcal {I}_\ell$ as defined in Eq. 3; operator $\textsf{post}_D(e, \mathcal{R})$ in Eq. 8 is a rewriting of $r_e[\mathcal{R} \cap \mathcal {G} ]$. Here, post operators are defined as combinations of four basic operations over sets:

$$\begin{aligned} \begin{array}{lr} \mathcal{X} \cap \mathcal{Y} &{} \qquad \qquad (\text {intersection})\\ {{\,\textrm{coni}\,}}\mathcal{X} = \{ t \cdot x :x \in \mathcal{X}, t \ge 0\} &{} \qquad \qquad (\text {conical hull}) \\ \mathcal{X} + \mathcal{Y} = \{ x + y :x \in \mathcal{X}, y \in \mathcal{Y}\} &{} \qquad \qquad (\text {Minkowski sum}) \\ A[\mathcal{X}] = \{ Ax :x \in \mathcal{X}\} &{} \qquad \qquad (\text {linear map}) \end{array} \end{aligned}$$

where $\mathcal X$ and $\mathcal Y$ are sets in $\mathbb {R}^n$ and $A \in \mathbb {R}^{n \times n}$. Computing template polyhedra for our post operators consists of building the respective support function—inductively—over these operations over sets; a method to inductively construct support functions was introduced in [39], and later extended in [11] with exact intersection and conical hull operations. Abstract safety analysis computes an abstraction of the reach set by Algorithm 1 as a union of template polyhedra, until either it terminates or a counterexample is found; in the latter case, we refine the template polyhedra in a CEGAR loop.

Fig. 6.

Architecture of a CEGAR loop.

Refining a template polyhedron amounts to adding directions to the template [15, 25]. Intuitively, the more the directions are, the tighter the abstraction is. The objective of an abstraction refinement scheme for template polyhedra is identifying a template that avoids finding any spurious counterexamples [11, 26]. A CEGAR loop constructs this template incrementally. As depicted in Fig. 6, the initial phase computes an abstraction using some initial template. If the abstraction is determined safe then the system is also safe and then the loop terminates and returns safe. If the abstraction identifies a counterexample then this is passed to the refinement phase. Refinement determines whether the counterexample is genuine or proposes a new template. In the earlier case the loop terminates and returns unsafe. In the latter case, refinement computes a template, that is, adds new directions to the existing template, which excludes the latest spurious counterexample from the abstraction. This refined template is passed to the abstraction phase and the loop is repeated. As a result, the loop enumerates spurious counterexamples and adds directions to the template until either all counterexamples are eliminated or some genuine counterexample is found. While this loop may in general not terminate, the same counterexample can never be encountered twice; this ensures progress.

Fig. 7.

Halfspace interpolants.

A counterexample is a finite path $\ell _0, e_1, \ell _1, \dots , e_{k}, \ell _k$ over the control graph of the hybrid automaton for which the respective sequence of abstract template polyhedra encounters a bad state, that is,

$$\begin{aligned} \mathcal {P} _0 = \varDelta \text {-polyhedron of } \textsf{post}_0(\mathcal{X}_0), \dots , \mathcal {P} _k = \varDelta \text {-polyhedron of } \textsf{post}_k(\mathcal {P} _{k-1}), \end{aligned}$$

and $\mathcal {P} _k \cap \mathcal{B} \ne \emptyset$, where $\mathcal{X}_0 = \textsf{Init}(\ell _0)$ denotes the initial condition, $\mathcal{B} \subseteq \mathbb {R}^n$ denotes the bad region, $\textsf{post}_0(\mathcal{X}) = \textsf{post}_C(\ell _0, \mathcal{X})$, and $\textsf{post}_i(\mathcal{X}) = \textsf{post}_C(\ell _i,\textsf{post}_D(e_i, \mathcal{X}))$ for $i = 1, \dots , k$. The region that results from this path can be seen as a concatenation of post operators from initial to bad state. Refining the template so as to eliminate the counterexample amounts to identifying exactly one direction for each step along the counterexample. In turn, this amounts to identifying a sequence of halfspace interpolants along these steps such that the last halfspace separates the result from the bad region. More precisely, we want to construct a sequence of halfspaces $\mathcal{H}_0, \dots , \mathcal{H}_k \subseteq \mathbb {R}^n$ such that

$$\begin{aligned} \textsf{post}_0(\mathcal{X}_0) \subseteq \mathcal{H}_0,\textsf{post}_1(\mathcal{H}_0) \subseteq \mathcal{H}_1 \dots , \textsf{post}_k(\mathcal{H}_{k-1}) \subseteq \mathcal{H}_k, \mathcal{H}_k \cap \mathcal{B} = \emptyset . \end{aligned}$$

(9)

To compute these halfspaces we break down these post operators into combinations of basic operations over sets. As indicated above, four operations are sufficient for the symbolic analysis of LHA: intersection between sets $\mathcal X \cap Y$, Minkowski sum $\mathcal X + Y$, conical hull ${{\,\textrm{coni}\,}}\mathcal X$, and linear map $A[\mathcal{X}]$. For this reason, we can construct these halfspaces inductively over every operation. Specifically, for any halfspace $\mathcal H$ that contains the result of an operation, i.e., $\mathcal X \cap Y \subseteq H$, $\mathcal X + Y \subseteq H$, $\mathcal {{\,\textrm{coni}\,}}X \subseteq H$, or $A\mathcal{X} \subseteq \mathcal{H}$, we compute a second halfspace $\mathcal H'$ that includes one operand, i.e., $\mathcal X \subseteq H'$, and abstracts it so as to preserve inclusion of the result into H, i.e., $\mathcal H' \cap Y \subseteq H$, $\mathcal H' + Y \subseteq H$, $\mathcal {{\,\textrm{coni}\,}}H' \subseteq H$, or $A[\mathcal{H}'] \subseteq \mathcal{H}$ respectively. The intuition behind halfspace interpolants is depicted in Fig. 7. As it turns out, these sequences of halfspace interpolants always exists if and only if the counterexample is spurious and can be computed efficiently by solving a large linear program; the details of the method for LHA are described in  [11], and extended to hybrid automata with linear ODEs in [26]. The performance of this CEGAR approach is illustrated by some experiments in the next section.

5 Experiments

We provide some experiments to illustrate the above approaches for the analysis of Linear Hybrid Automata. They are based on results collected for the ARCH-COMP friendly verification competitions since 2017, in the category of hybrid system with piecewise constant dynamics of the [13], where different implementation techniques have been evaluated over the years. The following implementations are used:

• PHAVer [22] uses the fixed-point algorithm in Sect. 2.3 and calls the Parma Polyhedra Library [5] for the polyhedral computations in Sect. 3. PHAVer/SX is a subset of PHAVer, included as a plugin in the tool SpaceEx [28].

• PHAVerLite is a variant of PHAVer using the polyhedra library PPLite [8], which employs a novel representation and conversion algorithm [7] for NNC (Not Necessarily Closed) polyhedra. PHAVer-lite is an earlier version, implemented as a SpaceEx plugin.

• Lyse [24] is a tool for the reachability analysis of convex hybrid automata, whose constraints can be linear or non-linear but are required to be convex, as outlined in Sect. 4.

Table 1. The progress on computation times for the DISC benchmarks.

5.1 Distributed Controller

In Table 1 we provide some evidence of the incremental efficiency improvements that have been obtained in recent years. To this end, we consider the Distributed Controller (DISC) benchmarks [34], which model a distributed controller for a robot, reading data from multiple sensors and processing them according to multiple priorities. The instances DISCn are parametric on $n \in \{ 2, 3, 4, 5 \}$, which is the number of sensors: the product automaton has $1 + 4n$ variables and $4 \times (1+n) \times 4^n$ locations. The verification goal is to prove a safety property, so that overapproximations are allowed. The rows in Table 1 are labeled by a year corresponding to the edition of the competition; they provide the overall execution time spent by the corresponding model checking tool. In 2017 and 2018, the tools computed the exact reachable states, so that instances with $n > 3$ were timing out. The time improvement in 2018 is due to replacing the PPL library with PPLite. In 2019, PHAVerLite-0.1 overapproximated set unions using the constraint hull operator, thereby also solving the instance with $n = 4$; finally, in 2020 the adoption of Cartesian factoring solved the instance with $n = 5$.

In Table 2, we present a more detailed evaluation of the techniques from in Sect. 3, focussing on the instance DISC3. The first four columns show the tool configuration: (filter w-list) whether redundant polyhedra are removed from the waiting list; (boxing) whether polyhedra are boxed to speed up inclusion tests; (con-hull) whether set union is approximated using the constraint hull; and (factoring) whether polyhedra are represented using Cartesian factoring. For each of the considered combinations, in the next columns show: (iter) the number of iterations of the algorithm; (p-list) the final length of the passed list of polyhedra; (r-loc) the number of the reachable locations of the automaton; (time) the overall time spent by the tool.

When the exact reachable set needs to be computed, the filtering and boxing techniques are quite effective in improving efficiency. The constraint hull approximation provides another significant efficiency improvement; note that precision is degraded (78 reachable locations instead of 67 in the exact case), but the overapproximation is precise enough to prove safety. While here the Cartesian factoring technique only yields a marginal improvement, its effects become more relevant when considering bigger instances, as shown in Table 1, where for $n=4$ the time drops from 77.51 to 2.59 s.

The above-mentioned progress is not specific to the considered benchmark: In the 2017 edition the corresponding tool verified 13 out of 20 tasks in 4:40 h, the 2020 edition solved 27 out of 28 tasks in less than 3 min.

5.2 Adaptive Cruise Controller

With this next benchmark, we compare the performance of the set-propagation approach implemented in PHAVer with the CEGAR approach implemented in the tool Lyse. The adaptive cruise controller is a distributed system for assuring that safety distances in a platoon of cars are satisfied [11]. For n cars, the number of discrete states is $2^n$ and the number of continuous variables is n. Each variable $x_i$ encodes the relative position of the i-th car and the relative velocities are subject to drift. The specification is that the distance between adjacent cars should be positive.

Table 3 shows the computation times for instances of different complexity. First, we observe that the set propagation approach shows similar performance characteristics as in the DISC benchmark: the advances associated with the polyhedra library PPLite, as well as the heuristic improvements to the fixed-point algorithm led to drastic gains in speed. The CEGAR approach clearly outshines the early versions of the set propagation approach. It also has a clear advantage in unsafe instances, where a counterexample can be found by solving a SAT instance. Somewhat surprisingly, however, the latest generation of set propagation tools seems to outperform CEGAR.

Table 2. The effect of implementation techniques on DISC3.

Table 3. Computation times of the adaptive cruise controller [23, 24].

6 Conclusions

In this paper, we tried to draw the arc from straightforward to more sophisticated symbolic analysis methods for linear hybrid automata (LHA). We presented two flavors, one based on set propagation and one based on counterexample-guided abstraction refinemend (CEGAR). The performance of the set propagation approach depends on how efficiently the required operations can be realized on the chosen set representation. A natural choice for LHA are convex polyhedra in constraint representation. Despite the fact that convex polyhedra are used, e.g., in program analysis, since the seventies, we remark that several advances were made over the years that led to progressively more efficient libraries. In particular, a novel representation for polyhedra with strict as well as nonstrict inequalities has led to gains on this fundamental level. Further gains have been achieved through heuristics that use of multiple levels of abstraction: A property like containment is decided by going progressively through different levels of abstraction, so that the most precise and expensive checks are only carried out when cheaper checks have failed.

The CEGAR approach constructs an abstraction in the form of polyhedra iteratively, by checking whether the abstraction admits a path from the initial states to a given bad set of states, and then refining the abstraction to exclude this path if it turns out to be spurious. CEGAR easily outperformed earlier versions of the set propagation approach and in our experiments it outperforms for unsafe instances, quickly returning an unsafe path as a witness. Compared to more recent implementations of set propagation that leverage efficient encodings and a series of heuristics, CEGAR seems to lose some of the advantage.

This paper provided a small sample of implementations and benchmark instances in order to outline some of the improvements that can be had through clever encodings and heuristics. Further experimentation is needed to evaluate in which application domains such gains translate to successful analysis results.