# Bounded Satisfiability Checking of
Metric First-Order Temporal Logic

Nick Feng<EMAIL_ADDRESS>University of TorontoTorontoOntarioCanada ,
Lina Marsso<EMAIL_ADDRESS>University of TorontoTorontoOntarioCanada
,  Mehrdad Sabetzadeh<EMAIL_ADDRESS>University of
OttawaOttawaOntarioCanada and  Marsha Chechik<EMAIL_ADDRESS>University of TorontoTorontoOntarioCanada

###### Abstract.

Legal properties involve reasoning about data values and time. Metric first-
order temporal logic (MFOTL) provides a rich formalism for specifying legal
properties. While MFOTL has been successfully used for verifying legal
properties over operational systems via runtime monitoring, no solution exists
for MFOTL-based verification in early-stage system development captured by
requirements. Given a legal property and system requirements both formalized
in MFOTL, the compliance of the property can be verified on the requirements
via satisfiability checking. In this paper, we propose a practical, sound, and
complete (within a given bound) satisfiability checking approach for MFOTL.
The approach, based on satisfiability modulo theories (SMT), employs a
counterexample-guided strategy to incrementally search for a satisfying
solution. We implemented our approach in a tool called LEGOS, and evaluated it
on five case studies spanning the healthcare, business administration, banking
and aviation domains. Our results indicate that our approach can efficiently
determine whether legal properties of interest are met, or generate
counterexamples that lead to compliance violations.

Requirements Engineering, Metric First-order Temporal Logic (MFOTL),
Satisfiability Modulo Theories (SMT).

††conference: Technical report; September 8th, 2022;

##  1\. Introduction

Software systems, such as medical systems or banking systems, are increasingly
required to comply with laws, regulations and policies aimed at ensuring
safety, security, data protection and privacy (Shan-et-al-19, ; Islam-et-
al-10, ). The properties stipulated by these laws, regulations and policies –
which we refer to as _legal properties_ (LP) hereafter – typically involve
reasoning about actions, ordering and time. As an example, consider the
following LP, $P1$, derived from a health-data regulation (s. 11, PHIPA
(phipa-2004, )): ”If personal health information is not accurate or not up-to-
date, it should not be accessed”. In this property, the accuracy and the
freshness of the data depend on how and when the data was collected and
updated before being accessed. More precisely, this property constrains the
data action access to have accurate and up-to-date data values, which further
constrains the order and time of access with respect to other data actions.

System compliance with LPs can be checked on the system design or on an
operational model of a system implementation. In this paper, we focus on the
early stage, where one can check whether a formalization of the system
requirements satisfies an LP. The formalization can be done using a
descriptive formalism like temporal logic, instead of using an operational
one, based on transition systems (Rozier-et-al-07, ; Li-et-al-19, ). For
instance, the requirement (req0) of a data collection system: ”no data can be
accessed prior to 15 days after the data has been collected” needs to be
formalized for verifying compliance of $P1$. It is important to formalize the
data and time constraints of both the system requirements and LPs, such as the
ones of $P1$ and req0.

_Metric first-order temporal logic (MFOTL)_ enables the specification of data
and time constraints (Basin-10, ) and has an expressive formalism for
capturing LPs and the related system requirements that constrain data and time
(Arfelt-Basin-Debois-19, ). Existing work on MFOTL verification has focused
primarily on detecting violations at run-time through monitoring (Arfelt-
Basin-Debois-19, ), with MFOTL formulas being checked on execution logs. There
is an unsatisfied need on determining the _satisfiability_ of MFOTL
specifications, i.e., looking for legal-property violations possible in MFOTL
specification, which is important for designing and debugging MFOTL
requirements to satisfy legal properties.

MFOTL satisfiability checking is generally undecidable since MFOTL is an
extension of first-order logic (FOL). Restrictions are thus necessary for
making the problem decidable. In this paper, we restrict ourselves to safety
properties. While we are not aware of non-safety LP properties, it is
conceivable that they may exist. For safety properties, LP violations are
finite sequences of data actions, captured via a finite-length counterexample.
For example, a possible violation of $P1$ is a sequence consisting of storing
a value $v$ in a variable $d$, updating $d$’s value to $v^{\prime}$, then
reading $d$ again and not obtaining $v^{\prime}$. Since we are interested in
finite counterexamples, bounded verification is a natural strategy to pursue
for achieving decidability. SAT solvers have been previously used for bounded
satisfiability checking of metric temporal logic (MTL) (Rozier-et-al-07, ; Li-
et-al-19, ). However, MTL cannot effectively capture quantified data
constraints (e.g., ”Every used data must be up-to-date.”) in LPs, hence the
solution is not applicable directly. As an extension to MTL, MFOTL can
effectively capture data constraints used in LP. Yet, to the best of our
knowledge, there has not been any prior work on bounded MFOTL satisfiability
checking.

To establish a _bound_ in bounded verification, researchers predominantly
relied on bounding the size of the universe, e.g., every data type has a
bounded domain in Alloy (Jackson-02, ). In our work, bounding _the universe_
would be too restrictive because LPs routinely refer to variables with large
ranges, e.g., timed actions spanning several years. Instead, we bound the
number of data actions _in a run_ , which bounds the number of actions in the
counterexample.

Equipped with the proposed notion of a bound, we develop an incremental
approach (IBSC) for bounded satisfiability checking of MFOTL. We first
translate the MFOTL property and requirements into FOL formulas with
quantifiers over data actions. We then incrementally ground the FOL
constraints to eliminate the quantifiers by considering an increasing number
of data actions. Subsequently, we check the satisfiability of the resulting
constraints using SMT solver Z3 (Leonardo-Nikolaj-2008, ). Specifically, we
make the following contributions: (1) we propose a translation of MFOTL
formulas to FOL; (2) we provide a novel bounded satisfiability checking
solution for the translated FOL formulas with incremental and counter-example
guided over/ under-approximation. We implemented our approach IBSC in a tool
called LEGOS, and empirically evaluate it on five case studies with a total of
24 properties showing that it can effectively and efficiently find LP
violations or prove satisfiability.

The rest of this paper is organized as follows. Sec. 2 provides background and
establishes our notation. Sec. 3 defines the bounded satisfiability checking
(BSC) problem. Sec. 4 provides an overview of our solution and the translation
of MFOTL to FOL. Sec. 5 presents our solution, the algorithm and its proof of
correctness and termination. Sec. 6 reports on the experiments we have
performed to validate our bounded satisfiability checking solution for MFOTL .
Sec. 7 discusses related work. Sec. 8 concludes the paper.

##  2\. Preliminaries

In this section, we introduce the necessary background on metric first order
temporal logic (MFOTL).

$P1=\square~{}\forall d,v,v^{\prime}(\textit{Access}(d,v)\wedge$
$v^{\prime}\neq
v)\implies\neg\textit{Update}(d,v^{\prime})~{}\mathcal{S}~{}(\textit{Update}(d,v)\vee\textit{Collect}(d,v)))$
---
If a personal health information is not accurate or not up-to-date, it should
not be accessed.
$\neg P1=\lozenge~{}\exists d,v,v^{\prime}(\textit{Access}(d,v)\implies$
$(v^{\prime}\neq
v\wedge\neg\textit{Update}(d,v)~{}\mathcal{S}~{}(\textit{Update}(d,v^{\prime})\vee\textit{Collect}(d,v^{\prime}))))$
$req_{0}=\square~{}\forall
d,v(\textit{Access}(d,v)\implies\blacklozenge_{[360,)}~{}\exists
v^{\prime}\cdot\textit{Collect(d, v')})$
No data is allowed to be accessed before having been collected for at least 15
days (360 hours).
$req_{1}=\square~{}\forall d,v(\textit{Update}(d,v)\implies\neg(\exists
v^{\prime\prime}\cdot((\textit{Update}(d,v^{\prime\prime})\wedge
v^{\prime\prime}\neq v)\vee\textit{Collect(d,
v'')})\vee\blacklozenge_{[1,168]}~{}\exists
v^{\prime}\cdot(\textit{Collect}(d,v^{\prime})\vee\textit{Update}(d,v^{\prime}))))$
Data can only be updated after having been collected or last updated for more
than a week (168 hours).
$req_{2}=\square~{}\forall
d,v(\textit{Access}(d,v)\implies\blacklozenge_{[0,168]}~{}\textit{Collect}(d,v)\vee\textit{Update}(d,v))$
Data can only be accessed if has been collected or updated within a week (168
hours).
$req_{3}=\square~{}\forall d,v(\textit{Collect}(d,v)\implies\neg(\exists
v^{\prime\prime}\cdot(\textit{Collect}(d,v^{\prime\prime})\wedge v\neq
v^{\prime\prime})\vee\blacklozenge_{[1,)}~{}\exists
v^{\prime}\cdot\textit{Collect}(d,v^{\prime})))$ Data cannot be re-collected.

Figure 1. Several requirements and the legal property $P1$ of DCC, with the
signature
$S_{data}=(\emptyset,\\{\textit{Collect},\;\textit{Update},\;\textit{Access}\\},\iota_{data})$,
where
$\iota_{data}(\textit{Collect})=\iota_{data}(\textit{Update})=\iota_{data}(\textit{Access})=2$.

data
actionstime$Collect(0,0)$$Access(0,0)$$\tau_{0}=0$$\tau_{1}=361$$\sigma_{1}$

$Collect(1,0)$$Collect(1,15)$$Access(1,0)$$\tau_{0}=0$$\tau_{1}=20$$\tau_{2}=361$$\sigma_{2}$

$Update_{1}(0,0)$$Access_{1}(0,1)$$\tau_{0}=0$$\tau_{1}=1$$\sigma_{3}$

$Collect_{2}(0,1)$,$Update_{1}(0,0)$$Access_{1}(0,1)$$\tau_{0}=0$$\tau_{1}=2$$\sigma_{4}$

$Collect_{2}(0,1)$$Collect_{1}(0,0)$$Access_{1}(0,1)$$\tau_{0}=0$$\tau_{1}=1$$\tau_{2}=2$$\sigma_{5}$

Figure 2. Several traces from the DCC example.

Syntax. We begin with the syntax of MFOTL (Basin-10, ).

###### Definition 0.

Let $\mathbb{I}$ be a non-empty interval over $\mathbb{N}$. An _interval_
$I\in\mathbb{I}$ can be expressed as [b, b’) where $b\in\mathbb{N}$ and
$b^{\prime}\in\mathbb{N}\cup\infty$. A _signature_ $S$ is a tuple
$(C,R,\iota)$, where $C$ is a set of constant and $R$ is a finite set
predicate symbols, respectively. Without loss of generality, we assume all
constants are from the integer domain $\mathbb{I}$ where the theory of linear
integer arithmetic (LIA) holds. The function $\iota:R\rightarrow\mathbb{N}$
associates each predicate symbol $r\in R$ with an arity
$\iota(r)\in\mathbb{N}$. Let $V$ be a countable infinite set of variables from
domain $\mathbb{I}$ and a term $t$ is defined inductively as
$t:\>c\>|\>v\>|\>t+t\>|\>c\times t$. We denote $\bar{t}$ as a vector of terms
and $\bar{t}^{\;k}_{x}$ as the vector that contains $x$ at index $k$. The
syntax of MFOTL formulas is defined as follows:

  1. (1)

$\top$ and $\bot$, representing values “true” and “false”;

  2. (2)

$t=t^{\prime}$ and $t>t^{\prime}$, for term $t$ and $t^{\prime}$

  3. (3)

$r(t_{1}...t_{\iota{r}})$ for $r\in R$ and $t_{1}...t_{\iota}$ are terms.

  4. (4)

$\phi\wedge\psi$, $\neg\phi$ for MFOTL formulas $\phi$ and $\psi$;

  5. (5)

$\exists x\cdot(r(\bar{t}^{\;k}_{x})\wedge\phi)$ for MFOTL formula $\phi$,
relation symbol $r\in R$, variable $x\in V$ and a vector of terms
$\bar{t}^{i}_{x}$ such that $x=\bar{t}^{i}_{x}[i]$

  6. (6)

$\phi~{}\mathcal{U}_{I}~{}\psi$, $\phi~{}\mathcal{S}_{I}~{}\psi$,
$\CIRCLE_{I}~{}\phi$, $\Circle_{I}~{}\phi$ for MFOTL formulas $\phi$ and
$\psi$, and an interval $I\in\mathbb{I}$.

We considered a restricted form of quantification (syntax rule 5) similar to
guarded quantification (Hodkinson-02, ; Halle-12, ). Every existentially
quantified variable $x$ must be guarded by some relation $r$ (i.e., for some
$\bar{t}$, $r(\bar{t})$ holds and $x$ appears in $\bar{t}$). Similarly,
universal quantification must be guarded as $\forall
x\cdot(r(\bar{t})\Rightarrow\phi)$ where $x\in\bar{t}$. Under the restricted
quantification, $\exists x\cdot\neg r(x)$ (and $\forall x\cdot r(x))$ are not
allowed.

The temporal operators $\mathcal{U}_{I}$, $\mathcal{S}_{I}$, $\CIRCLE_{I}$ and
$\Circle_{I}$ require the satisfaction of the formula within the time interval
given by $I$. We write $[b,)$ as a shorthand for $[b,\infty)$, if $I$ is
omitted, then the interval is assumed to be $[0,\infty)$. Other classical
unary temporal operators $\lozenge_{I}$ (i.e., eventually), $\square_{I}$
(i.e., always), and $\blacklozenge_{I}$ (i.e., once) are defined as follows:
$\lozenge_{I}~{}\phi=\top~{}\mathcal{U}_{I}~{}\phi$,
$\square_{I}~{}\phi=\neg\lozenge_{I}~{}\neg\phi$, and
$\blacklozenge_{I}~{}\phi=\top~{}\mathcal{S}_{I}~{}\phi$. Other common logical
operator such as $\vee$ (disjunction) and $\forall$ (universal quantification)
are expressed through negation of $\wedge$ and $\exists$, respectively.

###### Example 0.

Suppose a data collection centre (DCC) collects and accesses personal data
information with three requirements: $req_{0}$ stating that no data is allowed
to be accessed before being having been collected for 15 days (360 hours);
$req_{1}$: data can only be updated after having been collected or last
updated for more than a week (168 hours); and $req_{2}$: data can only be
accessed if has been collected or updated within a week (168 hours). The
signature $S_{data}$ for DCC contains three binary relations ($R_{data}$):
Collect, Update, and Access, such that Collect($d$, $v$), Update($d$, $v$) and
Access($d$, $v$) hold at a given time point if and only if data at id $d$ is
collected, updated, and accessed with value $v$ at this time point,
respectively. The MFOTL formulas for $P1$, $req_{0}$, $req_{1}$ and $req_{2}$
are shown in Fig. 1. For instance, the formula $req_{0}$ specifies that if a
data value stored at id $d$ is accessed, then some data must have been
collected and stored at id $d$ before, and the collection must have occurred
prior to 360 hours ago ($\blacklozenge_{[360,)}]$).

Semantics. A first-order (FO) structure $D$ over the signature $S=(C,R,\iota)$
comprises a domain $|D|\neq\emptyset$ and an interpretation for $c^{D}\in|D|$
and $r^{D}\subseteq|D|^{\iota{(r)}}$ for each $c\in C$ and $r\in R$. The
semantics of MFOTL formulas is defined over a sequence of FO structures
$\bar{D}=(D_{0},D_{1},\ldots)$ and a sequence of natural numbers representing
time $\bar{\tau}=(\tau_{0},\tau_{1},\ldots)$, where (a) $\bar{\tau}$ is a
monotonically increasing sequence; (b) $|D_{i}|=|D_{i+1}|$ for all $i>0$ (all
$D_{i}$ have a fixed domain); and (c) each constant symbol $c\in C$ has the
same interpretation across $\bar{D}$ (i.e., $c^{D_{i}}=c^{D_{i+1}})$

Property (a) ensures that time never decreases as the sequence progresses; and
(b) ensures that the domain is fixed. $\bar{D}$ is similar to timed words in
metric time logic (MTL), but instead of associating a set of propositions to
each time point, MFOTL uses a structure $D$ to interpret the symbols in the
signature $S$. Intuitively, the semantics of MFOTL is defined over a trace of
timed first-order structures $\sigma=(\bar{D},\bar{\tau})$, where every
structure $D_{i}\in\bar{D}$ contains a set of holding relations $r^{D_{i}}$,
and these relations occur at a time specified by $\tau_{i}\in\bar{\tau}$.

###### Example 0.

Consider the signature $S_{data}$ in the DCC example. Let $\tau_{1}=0$ and
$\tau_{2}=361$, and let $D_{1}$ and $D_{2}$ be two first order structures with
$r^{D_{1}}=\textit{Collect}(0,0)$ and $r^{D_{2}}=\textit{Access}(0,0)$,
respectively. The trace $\sigma_{1}=([D_{1};D_{2}],[\tau_{1};\tau_{2}])$ is a
valid trace shown in Fig. 2 and representing two timed relations: (1) data
value 0 collected and stored at id 0 at hour 0 and (2) data value 0 is read by
accessing id 0 at hour 361.

A _valuation function_ $v:V\rightarrow|\bar{D}|$ maps a set of variables $V$
to their interpretations in the domain $|\bar{D}|$. For vectors
$\bar{x}=(x_{1},\ldots,x_{n})$ and
$\bar{d}=(d_{1},...,d_{n})\in|\bar{D}|^{n}$, the _update operation_
$v[\bar{x}\rightarrow\bar{d}]$ produces a new valuation function $v^{\prime}$
s.t. $v^{\prime}(x_{i})=d_{i}$ for $1\leq i\leq n$, and
$v(x^{\prime})=v^{\prime}(x^{\prime})$ for every $x^{\prime}\notin\bar{x}$.
For any constant $c$, $v(c)=c$.

###### Definition 0.

Let $\bar{D}$ be a sequence of FO structures over signature $S=(C,R,\iota)$
and $\bar{\tau}$ be a sequence of natural numbers. Let $\phi$ be an MFOTL
formula over $S$, $v$ be a valuation function and $i\in\mathbb{N}$. The
relation $(\bar{D},\bar{\tau},v,i)\models\phi$ is defined as follows:

$(\bar{D},\bar{\tau},v,i)\models t=t^{\prime}$ | iff | $v(t)=v(t^{\prime})$
---|---|---
$(\bar{D},\bar{\tau},v,i)\models t>t^{\prime}$ | iff | $v(t)>v(t^{\prime})$
$(\bar{D},\bar{\tau},v,i)\models r(t_{1},..,t_{i(r)})$ | iff | $r(v(t_{1}),..,v(t_{i(r))})\in r^{D_{i}}$
$(\bar{D},\bar{\tau},v,i)\models\neg\phi$ | iff | $(\bar{D},\bar{\tau},v,i)\not\models\phi$
$(\bar{D},\bar{\tau},v,i)\models\phi\wedge\psi$ | iff |  $(\bar{D},\bar{\tau},v,i)\models\phi$ and $(\bar{D},\bar{\tau},v,i)\models\psi$
$(\bar{D},\bar{\tau},v,i)\models\exists x\cdot(r(\bar{t}^{i}_{x})\wedge\phi)$ | iff |  $(\bar{D},\bar{\tau},v[x\rightarrow d],i)\models(r(\bar{t}^{i}_{x}))\wedge\phi$ for some $d\in|\bar{D}|$
$(\bar{D},\bar{\tau},v,i)\models\CIRCLE_{I}~{}\phi$ | iff |  $(\bar{D},\bar{\tau},v,i+1)\models\phi$ and $\tau_{i+1}-\tau_{i}\in I$
$(\bar{D},\bar{\tau},v,i)\models\Circle_{I}~{}\phi$ | iff |  $i\geq 1$ and $(\bar{D},\bar{\tau},v,i-1)\models\phi$ and $\tau_{i}-\tau_{i-1}\in I$
$(\bar{D},\bar{\tau},v,i)\models\phi~{}\mathcal{U}_{I}~{}\psi$ | iff | exists $j\geq i$ and $(\bar{D},\bar{\tau},j,v)\models\psi$ and $\tau_{j}-\tau_{i}\in I$
|  | and for all $k\in\mathbb{N}$ $i\leq k<j\Rightarrow(\bar{D},\bar{\tau},k,v)\models\phi$
$(\bar{D},\bar{\tau},v,i)\models\phi~{}\mathcal{S}_{I}~{}\psi$ | iff | exists $j\leq i$ and $(\bar{D},\bar{\tau},j,v)\models\psi$ and $\tau_{i}-\tau_{j}\in I$
|  | and for all $k\in\mathbb{N}$ $i\geq k>j\Rightarrow(\bar{D},\bar{\tau},k,v)\models\phi$

The operators $\CIRCLE_{I}$, $\Circle_{I}$, $\mathcal{U}_{I}$ and
$\mathcal{S}_{I}$ are augmented with an interval $I\in\mathbb{I}$ which
defines the satisfaction of the formula within a time range specified by $I$
relative to the current time at step $i$, i.e., $\tau_{i}$.

###### Example 0.

Consider the DCC example, the MFOTL formula $req_{0}$, and the trace
$\sigma_{1}=((\bar{D}=[D_{1};D_{2}]),(\bar{\tau}=[\tau_{1};\tau_{2}]))$ (in
Fig. 2). For a valuation function $v=\emptyset$, we have
$(\bar{D},\bar{\tau},v,0)\models req_{0}$ because data stored at id 0 is
accessed at hour 361 ($\textit{Access}(0,0)\in r^{D_{2}}\wedge\tau_{2}=361$),
and data value 0 was collected and stored at id 0 361 hours ago
($\textit{Collect}(0,0)\in r^{D_{1}}$ and $\tau_{2}-\tau_{1}\in[360,)$).

###### Definition 0 (MFOTL Satisfiability).

An MFOTL formula $\phi$ is _satisfiable_ if there exists a sequence of FO
structures $\bar{D}$ and natural numbers $\bar{\tau}$, and a valuation
function $v$ such that $(\bar{D},\bar{\tau},v,0)\models\phi$. $\phi$ is
_unsatisfiable_ otherwise.

###### Example 0.

In the DCC example, the MFOTL formula $req_{0}$ is _satisfiable_ because
$(\bar{D},\bar{\tau},v,0)\models req_{0}$ (where
$\sigma_{1}=(\bar{D},\bar{\tau})$ in Fig. 2). Let
$req_{0}^{\prime}=\lozenge_{[0,359]}~{}\exists v\cdot(\textit{Access}(0,v))$
be another MFOTL formula. $req_{0}^{\prime}\wedge req_{0}$ is _unsatisfiable_
because if data stored at id $0$ is accessed between 0 and 359 hours, then it
is impossible to collect the data at least 360 hours prior to its access.

##  3\. Bounded Satisfiability Checking

The satisfiability of MFOTL properties is generally undecidable since MFOTL is
expressive enough for describing the blank tape problem (post-47, ) (which has
been shown to be undecidable). Despite the undecidability result, we can
derive a bounded version of the problem, bounded satisfiability checking
(BSC), for which a sound and complete decision procedure exists. When facing a
hard instance for the satisfiability checking problem, the solution to BSC
provides bounded guarantees (i.e., exists a solution or there is no solution
within the given bound). In this section, we first define satisfiability
checking and then the BSC problems of MFOTL formulas.

_Satisfiability checking_ (Pradella-et-al-13, ) is a verification technique
that extends model checking by replacing a state transition system with a set
of temporal logic formulas. In the following, we define satisfiability
checking of MFOTL formulas.

###### Definition 0 (Satisfiability Checking of MFOTL Formulas).

Let $\phi$ be an MFOTL formula over a signature $S=(C,R,\iota)$, and let
$reqs$ be a set of MFOTL requirements over $S$. Reqs complies $\phi$ (denoted
as $\textit{Reqs}\Rightarrow\phi)$ iff $\bigwedge_{\psi\in
M}\psi\wedge\neg\phi$ is _unsatisfiable_. We call a solution to
$\bigwedge_{\psi\in M}\psi\wedge\neg\phi$ (if one exists) a _counterexample_
to $\textit{Reqs}\Rightarrow\phi$.

###### Example 0.

Consider our DCC system requirements and the privacy data property $P1$
stating that if personal health information is not accurate or not up-to-date,
it should not be accessed (see Fig. 1). $P1$ is not respected by the set of
DCC requirements $\\{req_{0},req_{1},req_{2}\\}$ because $\neg P1\wedge
req_{0}\wedge req_{1}\wedge req_{2}$ is _satisfiable_. The counterexample
$\sigma_{2}$ (shown in Fig. 2) indicates that data can be re-collected, and
the re-collection does not have the same time restriction as the updates. If a
fourth policy requirement $req_{3}$ (Fig. 1) is added to prohibit re-
collection of collected data, then property $P1$ would be respected
($\\{req_{0},req_{1},req_{2},req_{3}\\}\Rightarrow P1$).

###### Definition 0 (Finite trace and bounded trace).

The _volume_ of a trace $\sigma=(\bar{D},\bar{\tau},v)$ is the total number of
relations that hold across $\bar{D}$, denoted as $vol(\sigma)=\sum_{r\in
R}\sum_{D_{i}\in\bar{D}}(|r^{D_{i}}|)$. The trace $\sigma$ is _finite_ if
$vol(\sigma)$ is finite. The trace is _bounded by volume_ if there exists an
upper bound $b_{vol}\in\mathbb{N}$ such that $vol(\sigma)\leq b_{vol}$. In the
rest of paper, we refer to volume-bounded traces as _bounded traces_.

###### Example 0.

The volume of trace $\sigma_{4}$ in Fig. 2, $vol(\sigma_{4})=3$ since there
are three relations: Collect(1, 15), Update(1, 0), and Access(1, 15). Note
that the volume and the length for this trace are different. The length,
$|\bar{D}|$, corresponds to the number of time points while the volume is the
total number of holding relations across all time points. More than one
relation can hold for a single time point.

###### Definition 0 (Bounded satisfiability checking of MFOTL properties).

Let $\phi$ be an MFOTL property, Reqs be a set of MFOTL requirements, and
$b_{vol}$ be a natural number. The _bounded satisfiability checking problem_
determines the existence of a counterexample $\sigma$ to
$\textit{Reqs}\Rightarrow\phi$ such that $vol(\sigma)\leq b_{vol}$.

##  4\. Checking Bounded Satisfiability

In this section, we present an overview of the bounded satisfiability checking
(BSC) process that translates MFOTL formula into first-order logic (FOL)
formulas, and looks for a satisfying solution for the FOL formulas. Then, we
provide the translation of MFOTL formulas to FOL and discuss the complexity of
the process.

###  4.1. Overview of BSC for MFOTL Formulas

requirements (MFOTL) property (MFOTL) data domain constraints (FOL) bound
(Nat) Translate search Ground Solve (SMT solver) counterexample
$\;|\;$bounded-UNSAT ($\;|\;$UNSAT) formulas(FOL)formulas (FOL)$+$
domainquantifier-freeformulas (FOL)queryanswer

Figure 3. Overview of the naive and our incremental (IBSC) MFOTL bounded
satisfiability checking approaches. Solid boxes and arrows are shared between
the two approaches. Blue dashed arrow is specific to the naive approach. Red
dotted arrows and the additional red output in bracket are specific to IBSC.

We aim to address the bounded satisfiability checking problem (Def. 5),
looking for a satisfying run $\sigma$ within a given volume bound $b_{vol}$
that limits the number of relations in $\sigma$. First, we translate the MFOTL
formulas to FOL formulas, where each relation in a trace is mapped to a
relational object in the FO domain. The considered constraints in the formulas
include the ones of the system requirements and the legal property, and
optional data constraints specifying the data domain of the system. Second, we
search for a satisfying solution to the FOL constraints; an SMT solver is used
here to determine the satisfiability of the FOL constraints and the data
domain constraints. The answer from the SMT solver is analyzed to return an
answer to the satisfiability checking problem (a counterexample $\sigma$, or
”bounded-UNSAT”).

###  4.2. Translation of MFOTL to First-Order Logic

The translation is a two-step procedure: (1) defining the FOL search domain
and (2) translating MFOTL formulas to FOL formulas. This translation enables
to search for a solution of the bounded satisfiability problem in the FOL
domain.

####  4.2.1. Domain of the Search Space

Any volume-bounded trace $\sigma=(\bar{D},\bar{\tau},v)$ (bounded by
$b_{vol}$) can be mapped to a single FO structure $(D_{AU},v^{\prime})$ by
associating the time information in $\tau_{i}$ to every relation in $D_{i}$
for every $(D_{i},\tau_{i})$ in the trace. More specifically, let $D_{AU}$ be
the domain defined over signature $S=(C,R,\iota)$ (the same signature as
$\bar{D}$). $D_{AU}$ contains all constants $c\in C$ and $b_{vol}$ _relational
objects_ (denoted $o$). Each $o$ has variables $name$ and $time$, and a vector
of argument variables ($arg_{1},\ldots,arg_{\iota(name)}$) associated with it.
Each $o$ represents an occurrence of a relation of $o.name$ at time $o.time$.
The following relationship holds for $(D_{AU},v^{\prime})$ and
$(\bar{D},\bar{\tau},v)$: $\forall r\in R$,
$r(t_{1},t_{2}...t_{\iota{(r)}})\in r^{D_{i}}$,

iff exists a relational object $o(arg_{1},arg_{2}....arg_{\iota{(r)}})\in
D_{AU}$ s.t.
---
$v(t_{1})=v^{\prime}(arg_{1})$, $v(t_{2})=v^{\prime}(arg_{2})$, …,
$v(t_{\iota{(r)}})=v^{\prime}(arg_{\iota{(r)}})$
$\wedge\tau_{i}=v^{\prime}(o.time)\wedge v^{\prime}(o.name)=r$.

Intuitively, each holding relation in the trace $\sigma$ is mapped to a
relational object where the holding time of the relation $\tau_{i}$ is
explicitly associated with the relational object’s $time$. Therefore, if a
relation does not hold at a given time, then there is no relational object
which the relation can be mapped to. The name of the relation $o.name$ defines
the class $Cls$ of relational objects in $D_{AU}$. For example, $\forall
o:Cls$ selects every relational object where $o.name=Cls$. In the rest of the
paper, to avoid confusion, class names and relation names are capitalized
(e.g., Collect) while individual relational object names are not (e.g.,
$collect_{1}$).

###### Example 0.

Consider the trace $\sigma_{2}=(\bar{D},\bar{\tau})$, where
$\bar{D}=[D_{1};D_{2};D_{3}]$ and $\bar{\tau}=[\tau_{1};\tau_{2};\tau_{3}]$ in
Fig. 2. The first-order structure of $\sigma_{2}$ is $(D_{AU},v^{\prime})$,
where $D_{AU}$ contains three relational objects. Two of these objects are
from the class $Collect$, and the third one is from the class $Access$. Let
$collect_{1}$ be the relational object corresponding to the relation
$Collect$(1, 0) in $D_{1}$ with $\tau_{1}=0$. We have:
$v^{\prime}(collect_{1}.arg_{1})=1$, $v^{\prime}(collect_{1}.arg_{2})=0$ and
$v^{\prime}(collect_{1}.time)=0$.

For the FO domain $D_{AU}$, let $|D_{AU}|$ denote the _domain size_ , i.e.,
the number of its relational objects. Therefore, for any trace $\sigma$
bounded by $b_{vol}$, we can map $\sigma$ to a first order structure
($D_{AU},v^{\prime}$) where the domain size of $|D_{AU}|$ is also bounded by
$b_{vol}$. Since MFOTL formulas specify constraints on $\sigma$, $v^{\prime}$
in $D_{AU}$ should satisfy FOL formulas corresponding to these MFOTL
constraints.

####  4.2.2. From MFOTL Formulas to FOL Formulas.

Recall that the semantics of MFOTL formulas is defined over a trace
$\sigma=(\bar{D},\bar{\tau},v,i)$ at a time point $i$ where
$\bar{D}=[D_{1};D_{2};...]$ is a sequence of FO structures and
$\bar{\tau}=[\tau_{1};\tau_{2};]$ is a sequence of time values. The time value
of the time point $i$ is given by $\tau_{i}$, and if $i$ is not specified,
then $i=1$. The semantics of FOL formulas is defined on a single FO structure
($D_{AU}$, $v^{\prime}$) where the time information is associated with
relational objects in the domain $D_{AU}$. Therefore, the time point $i$ (and
its time value $\tau_{i}$) needs to be considered during the translation from
MFOTL to FOL since the same MFOTL formula at different time points represents
different constraints over the trace $\sigma$. Formally, our translation
function translate, abbreviated to $T$ for succinctness, translates an MFOTL
formula $\phi$ into a function $f:\tau\rightarrow\phi_{f}$, where $\phi_{f}$
is an FOL formula over relational objects. The FOL formula $\phi_{f}$
corresponding to the MFOTL formula $\phi$ at time step $i$ is
$\phi_{f}=T(\phi,\tau_{i})$. The translation rules for $T$ are as follows:

$T(t=t^{\prime},\tau_{i})$ | $\rightarrow$ | $t=t^{\prime}$
---|---|---
$T(t>t^{\prime},\tau_{i})$ | $\rightarrow$ | $t>t^{\prime}$
$T(r(t_{1},..,t_{\iota(r)}),\tau_{i})$ | $\rightarrow$ | $\exists o(arg_{1},..,arg_{i(r)}):r\wedge\bigwedge_{j=1}^{\iota(r)}(arg_{j}=t_{j})$
|  | $\wedge(\tau_{i}=o.time)$
$T(\neg\phi,\tau_{i})$ | $\rightarrow$ | $\neg T(\phi,\tau_{i})$
$T(\phi\wedge\psi,\tau_{i})$ | $\rightarrow$ | $T(\phi,\tau_{i})\wedge T(\psi,\tau_{i})$
$T(\exists x\cdot r(\bar{t}^{i}_{x})\wedge\phi,\tau_{i})$ | $\rightarrow$ | $\exists o:r\cdot T((r(\bar{t}^{i}_{x})\wedge\phi)[x\rightarrow o.{arg_{i}}],\tau_{i})$
$T(\CIRCLE_{I}~{}\phi,\tau_{i})$ | $\rightarrow$ | $T(\phi,\tau_{i+1})\wedge(\tau_{i+1}-\tau_{i})\in I$
$T(\Circle_{I}~{}\phi,\tau_{i})$ | $\rightarrow$ | $T(\phi,\tau_{i-1})\wedge(\tau_{i}-\tau_{i-1})\in I$
$T(\phi~{}\mathcal{U}_{I}~{}\psi,\tau_{i})$ | $\rightarrow$ | $\exists time\cdot(time\geq\tau_{i}\wedge(time-\tau_{i})\in I\wedge T(\psi,time)$
|  | and $\forall time^{\prime}\cdot(\tau_{i}\leq time^{\prime}<time\Rightarrow T(\phi,time^{\prime})))$
$T(\phi~{}\mathcal{S}_{I}~{}\psi,\tau_{i})$ | $\rightarrow$ | $\exists time\cdot(time\leq\tau_{i}\wedge(\tau_{i}-time)\in I\wedge T(\psi,time)$
|  | and $\forall time^{\prime}\cdot(\tau_{i}\geq time^{\prime}>time\Rightarrow T(\phi,time^{\prime})))$
$T(\phi)$ | $\rightarrow$ | $T(\phi,\tau_{1})$

###### Proposition 0 (Quantifiers on relational objects).

For a MFOTL formula $\phi$, the FOL formula $T(\phi)$ only contains
quantifiers exclusively on relational objects.

###### Example 0.

Consider a formula  $exp=\square~{}\forall
d\cdot(A(d)\implies\lozenge_{[5,10]}~{}B(d))$

where $A$ and $B$ are unary relations. The translated FOL formula  $\forall
a:A\cdot(\exists b:B\cdot a.arg_{1}=b.arg_{1}$ $\wedge\;a.time+5\leq
b.time\leq a.time+10)$

Given an MFOTL property $\phi$ and a set of $MFOTL$ requirements $Reqs$, a
volume bound $b_{vol}$, the BSC problem can be solved by searching for a
satisfying solution $v^{\prime}$ for the FOL formula
$T(\phi)\bigwedge_{\psi\in Reqs}T(\psi)$ in a domain $D_{AU}$ with at most
$b_{vol}$ relational objects.

###  4.3. Checking MFOTL Satisfiability

Below, we define a naive procedure NBSC (shown in Fig. 3) for checking
satisfiability of MFOTL formulas translated into FOL. We then discuss the
complexity of this naive procedure. Even though we do not use this naive
procedure in this paper, its complexity corresponds to the upper-bound of our
proposed approach in Sec. 5.

Searching for a satisfying solution. Let $T(\phi)$ be an FOL formula
translated from an MFOTL formula $\phi$, and let $k$ be the maximum quantifier
nesting in $T(\phi)$. NBSC solves $T(\phi)$ via quantifier elimination. By
Proposition 2, only relational objects can be quantified. Given a bound $n$,
the number of relational objects in any satisfying solution of $T(\phi)$
should be at most $n$. Therefore, NBSC eliminates quantifiers in $T(\phi)$ by
assuming presence of $n$ relational objects and then iterates over them. For
example, the formula $\forall r:R\cdot\psi(r)$ is converted to
$\psi(r_{1})\wedge\psi(r_{2})\ldots\wedge\psi(r_{n})$. After eliminating all
quantifiers in the formula $T(\psi)$, NBSC calls an SMT solver on the
quantifier-free formula to obtain the satisfiability result.

Complexity. The size of the quantifier-free formula is $O(n^{k})$, where $k$
is the maximum depth of quantifier nesting. Since the background theory used
in $\phi$ is restricted to LIA, the complexity of solving the formula is NP-
complete (DBLP:journals/jacm/Papadimitriou81, ). Since Translate is linear in
the size of the formula $\phi$, the complexity of our approach is dominated by
solving the translated formula which is NP-complete with respect to the size
of the formula, $n^{k}$.

##  5\. Incremental Search for Bounded Counterexamples

The naive BSC approach (NBSC) defined in Sec. 4.3 is inefficient for solving
the translated FOL formulas given a larger bound $n$ since its quantifier
elimination creates a quantifier-free formula of size $O(n^{k})$ even if
satisfiability may be determined using a smaller bound. Moreover, NBSC cannot
detect unbounded unsatisfiability, and cannot provide optimality guarantees on
the volume of counterexamples which are important for establishing the proof
of unbounded correctness and localizing faults (Gastin-Moro-Zeitoune-04, ),
respectively. In this section, we propose an incremental procedure, IBSC, that
can detect unbounded unsatisfiability and provide shortest counterexamples. An
overview of IBSC is shown in Fig. 3.

IBSC maintains an under-approximation of the search domain and the FOL
constraints. It uses the search domain to ground the FOL constraints, and an
off-the-shelf SMT solver to determine satisfiability of the grounded
constraints and the data domain constraints. It analyzes the SMT result and
accordingly either expands the search domain, refines the FOL constraints, or
returns an answer to the satisfiability checking problem (a counterexample
$\sigma$, ”bounded-UNSAT”, or ”UNSAT”). The procedure continues until an
answer is obtained or until the domain exceeds the bound $b_{vol}$, in which
case a “bounded-UNSAT” answer is returned. If the bound increases, $\sigma$
with the minimal volume and the UNSAT value are preserved while bounded-UNSAT
may turn into $\sigma$ or UNSAT.

In the following, we describe IBSC in more detail. We explain the key
component of IBSC, computing over and under-approximation queries in Sec. 5.1,
the algorithm itself in Sec. 5.2, and analysis of its soundness, completeness,
and the solution optimality in Sec. 5.3.

###  5.1. Over- and Under-Approximation

IBSC searches for a counter-example in a FO domain $D_{AU}$ whose size is
bounded by a given volume bound $b_{vol}$. Instead of directly searching
inside $D_{AU}$, IBSC starts with an under-approximated domain
$D_{AU\downarrow}\subseteq D_{AU}$ where every relational object in
$D_{AU\downarrow}$ is in also $D_{AU}$. With $D_{AU\downarrow}$, we can create
an over- and an under-approximation query to the bounded satisfiability
problem. Such queries are used to check satisfiability of FO formulas with
domain $D_{AU\downarrow}$. IBSC starts with a small domain $D_{AU\downarrow}$
and gradually expands it until either SAT or UNSAT is returned, or the domain
size exceeds some limit (bounded-UNSAT).

Over-approximation. Let $\phi_{f}$ be an FOL formula with quantifiers over
relational objects, and $D_{AU\downarrow}$ be an FO domain of relation
objects. The procedure Ground ($G$) encodes $\phi_{f}$ into a quantifier-free
FOL formula $\phi_{g}$ s.t. the unsatisfiability of $\phi_{g}$ implies the
unsatisfiability of $\phi_{f}$. We call $\phi_{g}$ an _over-approximation_ of
$\phi_{f}$.

The procedure $G$ (Alg. 2) recursively traverses the AST of the input FOL
formula. To eliminate the existential quantifier in $\exists r:Cls\cdot body$
(L:2), $G$ creates a new relational object $newR$ (unconstrained) of class
$Cls$ (L: 5), and replaces $r$ with $newR$ in $body$ (L:6). To eliminate the
universal quantifier in $\forall r:Cls\cdot body$ (L: 8), $G$ expands the
quantifier into a conjunction of clauses where each clause is
$body[r\leftarrow r_{i}]$ (i.e., $r$ is replaced by $r_{i}$ in $body$) for
each relational object $r_{i}$ of class $Cls$ in $D_{AU\downarrow}$ (L:10).
Intuitively, an existentially-quantified relational object is instantiated
with a new relational object, and an universally quantified relational object
is instantiated with every existing relational object of the same class in
$D_{AU\downarrow}$.

###### Example 0.

Consider the following FOL formula:

$exp_{f}=\exists\textit{access}:\textit{Access}\cdot(\forall\textit{update}:\textit{Update})\cdot$
---

$(access.arg_{1}=update.arg_{1}\Rightarrow access.time\geq update.time+5)$
---

Let $D_{AU\downarrow 1}=\\{update_{1},update_{2}\\}$. $G$($exp_{f}$,
$D_{AU\downarrow 1}$) instantiates $\exists\textit{access}:\textit{Access}$
with a new relational object, $access_{1}$, and instantiates
$\forall\textit{update}:\textit{Update}$ with two relational objects,
$update_{1}$ and $update_{2}$ in $D_{AU\downarrow 1}$. The grounded formula is

$exp_{g}=access_{1}\wedge$
---
$(update_{1}.arg_{1}=access_{1}.arg_{1}\Rightarrow access_{1}.time\geq
update_{2}.time+5)$
$\wedge$ $(update_{2}.arg_{1}=access_{1}.arg_{1}\Rightarrow
access_{1}.time\geq update_{2}.time+5)$.

###### Proposition 0.

For every FOL formula $\phi_{f}$ translated from MFOTL formula $\phi$ and
domain $D_{AU\downarrow}$, the grounded formula
$\phi_{g}=G(\phi_{f},D_{AU\downarrow})$ is quantifier-free and contains a
finite number of variables and terms.

###### Lemma 0 (Over-approximation Query).

For an FOL formula $\phi_{f}$, and a domain $D_{AU\downarrow}$, if
$\phi_{g}=G(\phi_{f},D_{AU\downarrow})$ is UNSAT, then so is $\phi_{f}$.

Proof. We prove Lemma 3 by contradiction. Suppose $\phi_{g}$ is UNSAT but
there exists a solution $v_{f}$ for $\phi_{f}$ in some domain $D_{AU}$
($D_{AU}$ may be different from $D_{AU\downarrow}$). We show that we can
always construct a solution $v_{g}$ that satisfies $\phi_{g}$, which causes a
contradiction. First, we construct a solution $v_{g}^{\prime}$ for
$\phi_{g}^{\prime}=G(\phi_{f},D_{AU})$ from the solution $v_{f}$ (for
$\phi_{f}$). Then, we construct a solution $v_{g}$ for $\phi_{g}$ from the
solution $v_{g}^{\prime}$ for $\phi_{g}^{\prime}$.

We can construct a solution $v_{g}^{\prime}$ for $\phi_{g}^{\prime}$ in
$D_{AU}\cup NewRs$ where $NewRs$ are the new relational objects added by $G$.
The encoding of $G$ uses the standard way for expanding universally quantified
expression by enumerating every relation object in $D_{AU}$ (L:10). For every
existentially quantified expression, there exists some relation object $r\in
D_{AU}$ enabled by $v_{f}$ that satisfies the expression in $\phi_{f}$,
whereas $\phi_{g}^{\prime}$ contains a new relational object $r^{\prime}\in
NewRs$ for satisfying the same expression (L:6). Let
$v_{f}(r)=v_{g}^{\prime}(r^{\prime})$ for $r$ and $r^{\prime}$, and then
$v_{g}^{\prime}$ is a solution to $\phi_{g}^{\prime}$.

To construct the solution $v_{g}$ for $\phi_{g}=G(\phi_{f},D_{AU\downarrow})$
from the solution $v_{g}^{\prime}$ for $\phi_{g}^{\prime}=G(\phi_{f},D_{AU})$,
we consider the expansion of universally quantified expression in $\phi_{f}$
(L:8). For every relational objects in $r^{+}\in D_{AU}-D_{AU\downarrow}$, $G$
creates constraints (L:10) in $\phi_{g}^{\prime}$, but not in $\phi_{g}$. On
the other hand, for every relational objects in $r^{-}\in
D_{AU\downarrow}-D_{AU}$, we disable $r^{-}$ in the solution $v_{g}$, (i.e.,
$v_{g}(r^{-})=\bot$). Therefore, the constraints instantiated by $r^{-}$ (at
L:10) in $\phi_{g}$ are vacuously satisfied.

For every relational object $r\in D_{AU\downarrow}\cap D_{AU}$, we let
$v_{g}(r)=v_{g}^{\prime}(r)$, and all shared constraints in $\phi_{g}$ and
$\phi_{g}^{\prime}$ are satisfied by $v_{g}$ and $v_{g}^{\prime}$,
respectively. Therefore, $v_{g}$ is a solution to $\phi_{g}$. Contradiction. ∎

Under-approximation. Let $\phi_{f}$ be an FOL formula, and $D_{AU\downarrow}$
be an FO domain. The over-approximation
$\phi_{g}=G(\phi_{f},D_{AU\downarrow})$ contains a set of new relational
objects introduced by $G$ (L:5), denoted by $NewRs$. Let NoNewR($NewRs$,
$D_{AU\downarrow}$) be constraints that enforce that every new relational
object $r$ in $NewRs$ be identical to some relational objects in
$D_{AU\downarrow}$. Formally,

$\textsc{NoNewR}(NewRs,D_{AU\downarrow})=\bigwedge_{r\in
NewRs}\bigvee_{r^{\prime}\in D_{AU\downarrow}}(r=r^{\prime}).$

Let $\phi_{g}^{\bot}=\phi_{g}\wedge\textsc{NoNewR}(NewRs,D_{AU\downarrow}).$
If $\phi_{g}^{\bot}$ has a satisfying solution, then there is a solution for
$\phi_{f}$. We call $\phi_{g}^{\bot}$ an _under-approximation_ of $\phi_{f}$
and denote the procedure for computing it by
$\textsc{UnderApprox}(\phi_{f},D_{AU\downarrow})$.

###### Example 0.

Consider the FOL formula $exp_{f}$ in Ex. 1 and $D_{AU\downarrow
2}=\\{update_{1},update_{2},access_{1}\\}$.

$G$ ($exp_{f}$, $D_{AU\downarrow 2})=access_{2}\wedge$
---
$(update_{1}.arg_{1}=access_{2}.arg_{1}\Rightarrow access_{2}.time\geq
update_{2}.time+5)\wedge$
$(update_{2}.arg_{1}=access_{2}.arg_{1}\Rightarrow access_{2}.time\geq
update_{2}.time+5),$

where $access_{2}$ is the new relational object introduced in the grounded
formula. In $\phi_{g}^{\bot}$, $access_{2}$ is constrained to be some
relational objects in $D_{AU\downarrow 2}$ (see
$\textsc{NoNewR}(\\{access_{2}\\},D_{AU\downarrow 2})$). Therefore,
$\phi_{g}^{\bot}$ query is $G$ ($exp_{f}$, $D_{AU\downarrow 2})\wedge
access_{2}=access_{1}$.

###### Lemma 0 (Under-Approximation Query).

For an FOL formula $\phi_{f}$, and a domain $D_{AU\downarrow}$, let
$\phi_{g}=G(\phi_{f},D_{AU\downarrow})$ and
$\phi_{g}^{\bot}=\textsc{UnderApprox}($ $\phi_{f},D_{AU\downarrow})$. If
$\sigma$ is a solution to $\phi_{g}^{\bot}$, then there exists a solution to
$\phi_{f}$.

Proof. By construction, $\textsc{NoNewR}(NewRs,D_{AU\downarrow})$ guarantees
that if $\sigma$ is a solution to $\phi_{g}^{\bot}$ in the domain
$D_{AU\downarrow}$, there exists a solution $\sigma^{\prime}$ to $\phi_{g}$ in
the domain $D_{AU\downarrow}\cup NewRs$. Since every relational object $r\in
D_{AU\downarrow}$ has been used to instantiate a universally-quantified
expression (L:10 of Alg. 2), $\sigma^{\prime}$ is also a solution to
$\phi_{f}$.∎

Suppose for some domain $D_{AU\downarrow}$, an over-approximation query
$\phi_{g}$ for an FOL formula $\phi_{f}$ is satisfiable while the under-
approximation query $\phi_{g}^{\bot}$ is UNSAT. Then we cannot conclude
satisfiability of $\phi_{f}$ for $D_{AU\downarrow}$. However, the solution to
$\phi_{g}$ provides hints on how to expand $D_{AU\downarrow}$ to potentially
obtain a satisfying solution for $\phi_{f}$.

###### Corollary 0 (Necessary relational objects).

For a satisfying FOL formula $\phi_{f}$ and a domain $D_{AU\downarrow}$, let
$\phi_{g}$ and $\phi_{g}^{\bot}$ be the over- and under-approximation queries
of $\phi_{f}$ based on $D_{AU\downarrow}$, respectively. Suppose $\phi_{g}$ is
satisfiable, and $\phi_{g}^{\bot}$ is UNSAT, then every solution to $\phi_{f}$
contains some relational object mentioned in the formula $\phi_{g}$ but not in
$D_{AU\downarrow}$.

Cor. 6 holds because $\phi_{g}$ and $\phi_{g}^{\bot}$ are over- and under-
approximation of $\phi_{f}$, respectively. Cor. 6 shows that any domain
$D_{AU}$ that contains a satisfying solution to $\phi_{f}$ must consider some
relational objects from some solution to $\phi_{g}$.

###  5.2. Counterexample-Guided Constraint Solving Algorithm

Let an MFOTL formula $\phi$, a set of MFOTL requirements Reqs, an optional
volume bound $b_{vol}$, and optionally a set of FOL data domain constraints
$T_{data}$ be given. IBSC, shown in Alg. 1, searches for a solution $\sigma$
to $\phi\bigwedge_{\psi\in\textit{Reqs}}\psi$ (while respecting $T_{data}$),
bounded by $b_{vol}$. If no such solution is possible regardless of the bound,
IBSC returns UNSAT. If no solution can be found within the given bound, but a
solution may exist for a larger bound, then IBSC returns bounded-UNSAT. If
$b_{vol}$ is not specified, IBSC will perform the search unboundedly until a
solution or UNSAT is returned.

IBSC first translates $\phi$ and every $\psi\in\textit{Reqs}$ into FOL
formulas in $\textit{Reqs}_{f}$, denoted by $\phi_{f}$ and $\psi_{f}$,
respectively. Then IBSC searches for a satisfying solution to
$\phi_{f}\wedge\bigwedge_{\psi_{f}\in\textit{Reqs}_{f}}\psi_{f}$ (denote as
$\phi_{P\wedge\textit{Reqs}}$) in the FO domain $D_{AU}$ of volume which is at
most $b_{vol}$. Instead of searching in $D_{AU}$ directly, IBSC searches for a
solution of
$\phi_{f}\wedge\bigwedge_{\psi_{f}\in\textit{Reqs}_{\downarrow}}\psi_{f}$ in
$D_{AU\downarrow}$, where
$\textit{Reqs}_{\downarrow}\subseteq\textit{Reqs}_{f}$ and
$D_{AU\downarrow}\subseteq D_{AU}$. IBSC initializes
$\textit{Reqs}_{\downarrow}$ and $D_{AU\downarrow}$ as empty sets (LL:3-4).
Then, for the FOL formula $\phi_{P\wedge\textit{Reqs}}$, IBSC creates an over-
and under-approximation query $\phi_{g}$ (L:8) and $\phi_{g}^{\bot}$ (L:10),
respectively (described in Sec. 5.1). IBSC first solves the over-approximation
query $\phi_{g}$ by querying an SMT solver (L:14). If $\phi_{g}$ is
unsatisfiable, then $\phi_{P\wedge\textit{Reqs}}$ is unsatisfiable (Lemma 3),
and IBSC returns UNSAT (L:12).

If $\phi_{g}$ is satisfiable, then IBSC solves the under-approximation query
$\phi_{g}^{\bot}$ (L:11). If $\phi_{g}^{\bot}$ is unsatisfiable, then the
current domain $D_{AU\downarrow}$ is too small, and IBSC expands it
(LL:15-22). This is because satisfiability of $\phi_{g}$ indicates the
possibility of finding a satisfying solution after adding at least one of the
new relational objects in the solution of $\phi_{g}$ to $D_{AU\downarrow}$
(Cor. 6). The expansion aims to identify a minimum solution $\sigma_{min}$ for
$\phi_{g}$ that requires the smallest number of relational objects (L:16). For
every relational object $r^{\prime}\in\sigma_{min}$, $r^{\prime}$ is added to
$D_{AU\downarrow}$ if it is not already in $D_{AU\downarrow}$ (L:18). To
obtain $\sigma_{min}$, we follow MaxRes (Narodytska-et-al-14, ) methods: we
analyze the UNSAT core of $\phi_{g}^{\bot}$ and incrementally weaken
$\phi_{g}^{\bot}$ towards $\phi_{g}$ (i.e., the weakened query
$\phi_{g}^{\bot^{\prime}}$ is an “over-under approximation” that satisfies the
condition
$\phi_{g}^{\bot}\Rightarrow\phi_{g}^{\bot^{\prime}}\Rightarrow\phi_{g}$) until
a satisfying solution $\sigma_{min}$ is obtained for the weakened query.
However, if the volume of $\sigma_{min}$ exceeds $b_{vol}$ (L:19), then
bounded-UNSAT is returned (L:20).

On the other hand, if $\phi_{g}^{\bot}$ yields a solution $\sigma$, then
$\sigma$ is checked on $\textit{Reqs}_{f}$ (L:23). If $\sigma$ satisfies every
$\psi_{f}$ in $\textit{Reqs}_{f}$, then $\sigma$ is returned (L:24). If
$\sigma$ violates some requirements in $\textit{Reqs}_{f}$ , then the
violating requirement $lesson$ is added to $\textit{Reqs}_{\downarrow}$ to be
considered in the search for the next solutions (L:28).

If IBSC does not find a solution or does not return UNSAT, it means that no
solution is found because the $D_{AU\downarrow}$ is too small or the
$\textit{Reqs}_{\downarrow}$ are too weak. IBSC then starts again with either
the expanded domain $D_{AU\downarrow}$ or the refined set of requirements
$\textit{Reqs}_{\downarrow}$. It computes the over- and under-approximation
queries ($\phi_{g}$ and $\phi_{g}^{\bot})$ again and repeats the steps. Due to
structural similarities of $\phi_{g}$ and $\phi_{g}^{\bot}$ between
iterations, incremental encoding and solving are enabled to allow SMT solvers
to internally reuse learned clauses from previous iterations.

Algorithm 1 IBSC: search for a bounded (by $b_{vol}$) solution to
$T(\phi)\bigwedge_{\psi\in\textit{Reqs}}T(\psi)$.

Input an MFOTL formula $\phi$.
Input a set of MFOTL requirements $\textit{Reqs}=\\{\psi_{1},\psi_{2},...\\}$.
Optional Input $b_{vol}$, the volume bound of the counterexample.
Optional Input data constraints $T_{data}$, default $\top$.
Output a counterexample $\sigma$, UNSAT or bounded-UNSAT.

1:$\textit{Reqs}_{f}\leftarrow\\{\
\psi_{f}=T(\psi)\;|\;\psi\in\textit{Reqs}\\}$

2:$\phi_{f}\leftarrow T(\phi)$

3:$\textit{Reqs}_{\downarrow}\leftarrow\emptyset$ //initially do not consider
any requirement

4:$D_{AU\downarrow}\leftarrow\emptyset$ //start with empty set of relational
objects

5:while $\top$ do

6: $\phi\leftarrow\phi_{f}\wedge\textit{Reqs}_{\downarrow}$

7: //over-approximation query

8: $\phi_{g}\leftarrow G(\phi,D_{AU\downarrow})$

9: //under-approximation query

10: $\phi_{g}^{\bot}\leftarrow\textsc{UnderApprox}(\phi,D_{AU\downarrow})$

11: if Solve($\phi_{g}\wedge T_{data}$) = UNSAT then

12: return UNSAT

13: end if

14: $\sigma\leftarrow\textsc{Solve}(\phi_{g}^{\bot}\wedge T_{data})$

15: if $\sigma$ = UNSAT then //expand $D_{AU\downarrow}$

16: $\sigma_{min}\leftarrow\textsc{Minimize}(\phi_{g})$

17: //add relational object from the minimal solution

18: $D_{AU\downarrow}$ += $\\{act\;|\;act\in\sigma_{min}\\}$

19: if $vol(\sigma_{min})>b_{vol}$ then

20: return bounded-UNSAT

21: end if

22: else //checks all requirements

23: if $\sigma\models\psi$ for every $\psi\in\textit{Reqs}_{f}$ then

24: return $\sigma$

25: else

26: $lesson\leftarrow$ some $\psi\in\textit{Reqs}_{f}$ such that
$\sigma\not\models\psi$

27: //add violating requirement to $\textit{Reqs}_{\downarrow}$

28: $\textit{Reqs}_{\downarrow}$.add($lesson$)

29: end if

30: end if

31:end while

Algorithm 2 $G$: ground a quantified FOL formula.

Input an FOL formula $\phi_{f}$.
Input a domain of relational objects $D_{AU\downarrow}$.
Output a grounded quantifier-free formula $\phi_{g}$ over relational objects.

1:if is_atom($\phi_{f}$) then return $\phi_{f}$ end if

2:if $\phi_{f}.op=\exists$ then //process the existential operator

3: $Cls\leftarrow\phi_{f}.class$

4: //creates a new relational object of class $Cls$

5: $newR\leftarrow\textsc{NewAct}(Cls)$

6: return $G$ ($\phi_{f}$.body[$\phi_{f}.headAct\leftarrow newR$],
$D_{AU\downarrow}$)

7:end if

8:if $\phi_{f}.op=\forall$ then //process the universal operator

9: $Cls\leftarrow\phi_{f}.class$

10: return $\bigwedge_{[r:Cls]\in D_{AU\downarrow}}$ $r\Rightarrow$ $G$
($\phi_{f}$.body[$\phi_{f}.head\leftarrow r$], $D_{AU\downarrow}$)

11:end if

12:return $\phi_{f}.op$($G$ ($\phi_{child}$, $D_{AU\downarrow}$) for
$\phi_{child}$ in $\phi_{f}$.body)

###### Example 0.

Consider the DCC example in Sec. 2. Suppose IBSC is invoked to find a
counterexample for property $P1$ (shown in Fig. 1) subject to requirements
$\textit{Reqs}=\\{req_{1},req_{2}\\}$ with the bound $b_{vol}=4$. IBSC
translates the requirements and the property to FOL, and initializes
$\textit{Reqs}_{\downarrow}$ and $D_{AU\downarrow}$ to empty sets. For each
iteration, we use $\phi_{g}$ and $\phi_{g}^{\bot}$ to represent the over- and
under-approximation queries computed on LL:8-10, respectively.

1st iteration: $D_{AU\downarrow}=\emptyset$ and
$\textit{Reqs}_{\downarrow}=\emptyset$. $\phi_{g}$ introduces three new
relational objects (from $\neg P1$): $access_{1}$, $collect_{1}$ and
$update_{1}$ such that: (C1) $access_{1}$ occurs after $collect_{1}$ and
$update_{1}$; (C2) $access_{1}.arg1=collect_{1}.arg1=update_{1}.arg1$; (C3)
$access_{1}.arg2\neq collect_{1}.arg2\wedge access_{1}.arg2\neq
update_{1}.arg2$; and (C4) either $collect_{1}$ or $update_{1}$ must be
present in the counterexample. $\phi_{g}$ is satisfiable, but
$\phi_{g}^{\bot}$ is UNSAT since $D_{AU\downarrow}$ is an empty set. WLOG, we
assume $D_{AU\downarrow}$ is expanded by adding $access_{1}$ and $update_{1}$.

2nd iteration: $D_{AU\downarrow}=\\{access_{1},update_{1}\\}$ and
$\textit{Reqs}_{\downarrow}=\emptyset$. $\phi_{g}$ stays the same, and
$\phi_{g}^{\bot}$ is now satisfiable since $access_{1}$ and $update_{1}$ are
in $D_{AU\downarrow}$. Suppose the solution is $\sigma_{3}$ (see Fig. 2).
However, $\sigma_{3}$ violates $req_{2}$, so $req_{2}$ is added to
$\textit{Reqs}_{\downarrow}$.

3rd iteration: $D_{AU\downarrow}=\\{access_{1},update_{1}\\}$ and
$\textit{Reqs}_{\downarrow}=\\{req_{2}\\}$. $\phi_{g}$ introduces two new
relational objects (from $req_{2}$): $collect_{2}$ and $update_{2}$ such that
(C5) $collect_{2}.time\leq access_{1}.time\leq collect2.time+168$; (C6)
$update_{2}.time\leq access_{1}.time\leq update_{2}.time+168$; (C7)
$access_{1}.arg1=collect_{2}.arg1=update_{2}.arg1$; (C8)
$access_{1}.arg2=collect_{2}.arg2=update_{2}.arg2$; and (C9) $collect_{2}$ or
$update_{2}$ exists. $\phi_{g}$ is satisfiable, but $\phi_{g}^{\bot}$ is UNSAT
because $update_{2}\not\in D_{AU\downarrow}$ and $update_{1}\neq update_{2}$
(C8 conflicts with C3). Therefore, $D_{AU\downarrow}$ needs to be expanded.
Assume $collect_{2}$ is added.

4th iteration: $D_{AU\downarrow}=\\{access_{1},update_{1},collect_{2}\\}$ and
$\textit{Reqs}_{\downarrow}=\\{req_{2}\\}$. $\phi_{g}$ stays the same, and
$\phi_{g}^{\bot}$ is now satisfiable since $collect_{2}$ is in
$D_{AU\downarrow}$. Suppose the solution is $\sigma_{4}$ (see Fig. 2). Since
$\sigma_{4}$ violates $req_{1}$, $req_{1}$ is added to
$\textit{Reqs}_{\downarrow}$.

5th iteration: $D_{AU\downarrow}=\\{access_{1},update_{1},collect_{2}\\}$ and
$\textit{Reqs}_{\downarrow}=\\{req_{1},req_{2}\\}$. Since $req_{1}$ is in
$\textit{Reqs}_{\downarrow}$, $\phi_{g}$ adds the following constraints (from
$req_{1}$): (C9) $\neg(update_{2}.time-168\leq collect_{1}.time\leq
update_{2}.time)$. Since (C9) conflicts with (C8),(C7) and (C1), $update_{2}$
cannot be in the solution of $\phi_{g}$. $\phi_{g}$ is satisfiable if
$collect_{1}$ (introduced in the 1st iteration) or $update_{2}$ (3rd
iteration) are in the solution. But $\phi_{g}^{\bot}$ is UNSAT since
$D_{AU\downarrow}$ does not contain $collect_{1}$ or $update_{2}$. Thus,
$D_{AU\downarrow}$ is refined. Assume $update_{2}$ is added to
$D_{AU\downarrow}$.

6th iteration:
$D_{AU\downarrow}=\\{access_{1},update_{1},collect_{2},update_{2}\\}$ and
$\textit{Reqs}_{\downarrow}=\\{req_{1},req_{2}\\}$. $\phi_{g}$ adds the
constraints (C10) $update_{2}.time\geq update_{1}.time+168$. $\phi_{g}$ (from
$req_{1}$) and (C11) $update_{2}.time\leq$ $update_{1}.time$ (from $\neg P$).
Since (C10) conflicts with (C11), $update_{2}$ cannot exist in the solution of
$\phi_{g}$. Thus, $\phi_{g}$ is satisfiable only if $collect_{1}$ is in the
solution. $\phi_{g}^{\bot}$ is UNSAT because $collect_{1}\not\in
D_{AU\downarrow}$. Therefore, $D_{AU\downarrow}$ is expanded by adding
$collect_{1}$.

final iteration:
$D_{AU\downarrow}=\\{access_{1},update_{1},collect_{2},update_{2},$
$collect_{1}\\}$ and $\textit{Reqs}_{\downarrow}=\\{req_{1},req_{2}\\}$.
$\phi_{g}^{\bot}$ becomes satisfiable, and yields the solution $\sigma_{5}$ in
Fig. 2. $\sigma_{5}$ satisfies $req_{1}$ and $req_{2}$, and is returned.

###  5.3. Correctness, Termination, Optimality

In this section, we first prove correctness of the IBSC algorithm, then show
that IBSC always terminates when $b_{vol}\neq\infty$ and finally prove that
IBSC always finds a solution with a minimum volume.

###### Theorem 8 (Soundness).

If the algorithm IBSC terminates on input $\phi$, Reqs and $b_{vol}$, then it
returns the correct result, i.e., a counter-example $\sigma$, ”UNSAT” or
”bounded-UNSAT”, when they apply.

Proof. Let $\phi_{f}$ be the FOL formula
$T(\phi)\bigwedge_{\psi\in\textit{Reqs}}T(\psi)$. We consider correctness of
IBSC for three possible outputs: the satisfying solution $\sigma$ to
$\phi_{f}$ (L:24), the UNSAT determination of $\phi_{f}$ (L:12), and the
bounded-UNSAT determination of $\phi_{f}$ (L:20).

IBSC returns a satisfying solution $\sigma$ only if (1) $\sigma$ is a solution
$\phi_{g}^{\bot}$ (L:25) and (2) $\sigma\models T(\psi)$ for every $\psi\in
Reqs$ (L:23). By (1) and Lemma 5, $\sigma$ is a solution to
$T(\phi)\bigwedge_{\psi\in\textit{Reqs}_{\downarrow}}T(\psi)$. Together with
(2), $\sigma$ is a solution to $\phi_{f}$.

IBSC returns UNSAT iff $\phi_{g}$ is UNSAT (L:11). By Lemma 3, we show
$T(\phi)\bigwedge_{\psi\in\textit{Reqs}_{\downarrow}}T(\psi)$ is UNSAT. Since
$\textit{Reqs}_{\downarrow}\subseteq Reqs$, the original formula $\phi_{f}$ is
also UNSAT.

IBSC returns bounded-UNSAT iff the volume of the minimum solution
$\sigma_{min}$ to the over-approximated query $\phi_{g}$ is larger than
$b_{vol}$ (L:19). Since $\phi_{g}$ is an over-approximation of the original
formula $\phi_{f}$, any solution $\sigma$ to the $\phi_{f}$ has volume at
least $vol(\sigma_{min})$. Therefore, when $vol(\sigma_{min})>b_{vol}$,
$vol(\sigma)>b_{vol}$ for every solution. ∎

###### Theorem 9 (Termination).

For an input property $\phi$, requirements Reqs, and a bound
$b_{vol}\neq\infty$, IBSC eventually terminates.

Proof. To prove that IBSC always terminates when the input
$b_{vol}\neq\infty$, we need to show that IBSC does not get stuck at solving
the SMT query via solve (LL:14-11), nor refining $\textit{Reqs}_{\downarrow}$
(LL:23-29), nor expanding $D_{AU\downarrow}$ (LL:18-22).

A call to solve (LL:14-11) always terminates. By Prop. 2, $T(\phi)$ may
contain quantifiers exclusively over relational objects. By Prop. 2 both the
under- and the over-approximated queries $\phi_{g}$ and $\phi_{g}^{\bot}$ are
quantifier-free. Since the background theory for $\phi$ is LIA, then
$\phi_{g}$ and $\phi_{g}^{\bot}$ are a quantifier-free LIA formula whose
satisfiability is decidable.

If the requirement checking fails on L: 23, a violating requirement $lesson$
is added to $\textit{Reqs}_{\downarrow}$ (LL:26-28) which ensures that any
future solution $\sigma^{\prime}$ satisfies $lesson$. Therefore, $lesson$ is
never added to $\textit{Reqs}_{\downarrow}$ more than once. Given that Reqs is
a finite set of MFOTL formulas, at most $|\textit{Reqs}|$ lessons can be
learned before the algorithm terminates.

The under-approximated domain $D_{AU\downarrow}$ can be expanded a finite
number of times because the size of the minimum solution $vol(\sigma_{min})$
to $\phi_{g}$ (computed on L:16) is monotonically non-decreasing between each
iteration of the loop (LL:5-31). The size will eventually increase since each
relational object in $D_{AU\downarrow}$ can introduce a finite number of
options for adding a new relational object through the grounded encoding of
$\phi_{g}$ on L:10, e.g., $r\Rightarrow\bigvee_{i=0}^{n}\exists r_{i}$. After
exploring all options to $D_{AU\downarrow}$, $vol(\sigma_{min})$ must increase
if the algorithm has not already terminated. Therefore, if
$b_{vol}\neq\infty$, then eventually $vol(\sigma_{min})>b_{vol}$, and the
algorithm will return bounded-UNSAT instead of expanding $D_{AU\downarrow}$
indefinitely (LL:15-22). ∎

###### Theorem 10 (Solution optimality).

For a property $\phi$ and requirements Reqs, let $\phi_{f}$ be the FOL formula
$T(\phi)\bigwedge_{\psi\in\textit{Reqs}}T(\psi)$. If IBSC finds a solution
$\sigma$ for $\phi_{f}$, then for every $\sigma^{\prime}\models\phi_{f}$,
$vol(\sigma)\leq vol(\sigma^{\prime})$.

Proof. IBSC returns a solution $\sigma$ on L:24 only if $\sigma$ is a solution
to the under-approximation query $\phi_{g}^{\bot}$ (computed on L:10) for some
domain $D_{AU\downarrow}\neq\emptyset$. $D_{AU\downarrow}$ is last expanded in
some previous iterations by adding relational objects to the minimum solution
$\sigma_{min}$ (L:16) of the over-approximation query $\phi_{g}^{\prime}$
(L:18). Therefore, the returned $\sigma$ has the same number of relational
objects as $\sigma_{min}$ ($vol(\sigma_{min})=vol(\sigma)$). Since $\phi_{g}$
is an over-approximation of the original formula $\phi_{f}$, any solution
$\sigma^{\prime}$ to $\phi_{f}$ has volume that is at least
$vol(\sigma_{min})$. Therefore, $vol(\sigma)\leq vol(\sigma^{\prime})$. ∎

###### Remark 0.

IBSC finds the optimal solution because it always looks for the minimum
solution $\sigma_{min}$ to the over-approximation query $\phi_{g}$ (L:16) and
uses it for domain expansion (L:18). However, looking for the minimum solution
adds cost. If the solution optimality is not required, IBSC can be configured
to heuristically find a solution $\sigma$ to $\phi_{g}$ such that
$vol(\sigma)\leq b_{vol}$. For example, greedy best-first search ($gBFS$)
finds a solution to $\phi_{g}$ that minimizes the number of relational objects
that are not already in $D_{AU\downarrow}$, and then uses it to expand
$D_{AU\downarrow}$. We configured a non-optimal version of IBSC
($n\textsc{IBSC}$) that uses $gBFS$ heuristics, and evaluate its performance
in Sec. 6.

##  6\. Evaluation

To evaluate our approach, we developed LEGOS, a tool that implements our MFOTL
bounded satisfiability checking algorithm IBSC (Algorithm 1). It includes
Python API for specifying system requirements and MFOTL safety properties. We
use pySMT (pysmt2015, ) to formulate SMT queries and Z3 (Leonardo-
Nikolaj-2008, ) to check their satisfiability. LEGOS and the evaluation
artifacts are included in supplementary material11footnotetext: available at
https://github.com/agithubuserseva/IBSC. In this section, we evaluate the
effectiveness of our approach using five case studies, aiming to answer the
following research question (RQ): How effective is our approach at determining
the bounded satisfiability of MFOTL formulas? We measure effectiveness in
terms of the ability to determine satisfiability (i.e., the satisfying
solution and its volume, UNSAT, or bounded UNSAT), and performance, i.e., time
and memory usage.

names | case study statistics | configuration values
---|---|---
$\\#reqs$ | $\\#rels$ | $\\#args$ | $\\#props$
PHIM | 18 | 22 | $[1-4]$ | 7 |  $\textit{\\#c}=2$, $\textit{\\#p}=2$, $\textit{\\#d}=5$
CF@H | 45 | 28 | $[2-3]$ | 7 |  $\textit{\\#u}=2$, $\textit{\\#d}=10$
PBC | 14 | 7 | $[1-2]$ | 1 |  $\textit{\\#u}=5$, $\textit{\\#d}=10$
BST | 10 | 3 | $[1-3]$ | 3 |  $\textit{\\#e}=1$, $\textit{\\#cus}=2$, $\textit{\\#t}=4$, $\textit{sup}=10$

Table 1. Case study statistics. The numbers of requirements, relations,
relation arguments, and properties are denoted as $\\#reqs$, $\\#rels$,
$\\#args$, and $\\#props$, respectively. Initial configurations with data
constraints specific to each case study: PHIM – the number of custodians
($\\#c$), patients ($\\#p$), and data ($\\#d$); CF@H and PBC – the number of
users ($\\#u$), and data ($\\#d$); BST – the number of employees ($\\#e$),
customers ($\\#cus$), transactions ($\\#t$), and maximum amount for a
transaction (sup).

case studies | small |  | medium |  | big |  | unbounded
---|---|---|---|---|---|---|---
| out. | time | mem. |  | out. | time | mem. |  | out. | time | mem. |  | out. | time | mem.
| (sec) | (MB) |  | (sec) | (MB) |  | (sec) | (MB) |  | (sec) | (MB)
|  $n\textsc{IBSC}$ $|$ IBSC |  $n\textsc{IBSC}$ $|$ IBSC |  $n\textsc{IBSC}$ $|$ IBSC |  |  $n\textsc{IBSC}$ $|$ IBSC |  $n\textsc{IBSC}$ $|$ IBSC |  $n\textsc{IBSC}$ $|$ IBSC |  |  $n\textsc{IBSC}$ $|$ IBSC |  $n\textsc{IBSC}$ $|$ IBSC |  $n\textsc{IBSC}$ $|$ IBSC |  |  $n\textsc{IBSC}$ $|$ IBSC |  $n\textsc{IBSC}$ $|$ IBSC |  $n\textsc{IBSC}$ $|$ IBSC
PHIM | $ph_{1}$ | U | 0.04 $|$ 0.03 | 29 $|$ 29 |  | U | 0.03 $|$ 0.03 | 136 $|$ 136 |  | U | 0.04 $|$ 0.04 | 136 $|$ 136 |  | U | 0.06 $|$ 0.05 | 64 $|$ 64
$ph_{2}$ | U | 0.03 $|$ 0.03 | 138 $|$ 138 |  | U | 0.03 $|$ 0.03 | 136 $|$ 137 |  | U | 0.03 $|$ 0.04 | 136 $|$ 136 |  | U | 0.05 $|$ 0.06 | 64 $|$ 61
$ph_{3}$ | U | 0.03 $|$ 0.03 | 134 $|$ 137 |  | U | 0.03 $|$ 0.03 | 138 $|$ 138 |  | U | 0.05 $|$ 0.05 | 137 $|$ 138 |  | U | 0.06 $|$ 0.06 | 64 $|$ 64
$ph_{4}$ | U | 0.04 $|$ 0.04 | 136 $|$ 138 |  | U | 0.04 $|$ 0.04 | 138 $|$ 135 |  | U | 0.05 $|$ 0.05 | 138 $|$ 138 |  | U | 0.06 $|$ 0.07 | 64 $|$ 64
$ph_{5}$ | U | 0.02 $|$ 0.02 | 135 $|$ 135 |  | U | 0.02 $|$ 0.02 | 608 $|$ 608 |  | 56 $|$ 56 | 30.51 $|$ 30.51 | 390 $|$ 390 |  | 56 $|$ 56 | 21.64 $|$ 21.60 | 393 $|$ 390
$ph_{6}$ | b-U | 0.18 $|$ 0.20 | 139 $|$ 139 |  | U | 0.72 $|$ 0.82 | 144 $|$ 144 |  | U | 0.88 $|$ 0.70 | 142 $|$ 142 |  | U | 0.91 $|$ 0.91 | 70 $|$ 70
$ph_{7}$ | U | 0.11 $|$ 0.11 | 139 $|$ 139 |  | 29 $|$ 29 | 13.80 $|$ 1905.40 | 193 $|$ 599 |  | 30 $|$ 29 | 20.25 $|$ 682.22 | 193 $|$ 601 |  | 32 $|$ 29 | 20.96 $|$ 1035.87 | 123 $|$ 383
CF@H | $cf_{1}$ | b-U | 4.80 $|$ 6.90 | 114 $|$ 176 |  | U | 2.87 $|$ 3.55 | 81 $|$ 86 |  | U | 2.98 $|$ 1.71 | 85 $|$ 76 |  | U | 1.71 $|$ 0.74 | 74 $|$ 68
$cf_{2}$ | b-U | 0.87 $|$ 0.93 | 70 $|$ 70 |  | 14 $|$ 14 | 3.21 $|$ 425.41 | 79 $|$ 334 |  | 14 $|$ 14 | 2.40 $|$ 778.36 | 76 $|$ 80 |  | 14 $|$ 14 | 3.32 $|$ 16.97 | 80 $|$ 205
$cf_{3}$ | b-U | 1.38 $|$ 1.31 | 145 $|$ 145 |  | 16 $|$ 16 | 6.05 $|$ 90.78 | 168 $|$ 403 |  | 16 $|$ 16 | 3.54 $|$ 371.65 | 157 $|$ 846 |  | 16 $|$ 16 | 5.35 $|$ 24.07 | 86 $|$ 164
$cf_{4}$ | b-U | 1.52 $|$ 0.73 | 74 $|$ 68 |  | 14 $|$ 14 | 4.54 $|$ 65.59 | 90 $|$ 261 |  | 14 $|$ 14 | 5.63 $|$ 57.30 | 95 $|$ 261 |  | 14 $|$ 14 | 5.65 $|$ 1227.02 | 89 $|$ 294
$cf_{5}$ | 8 $|$ 8 | 1.20 $|$ 1.17 | 146 $|$ 147 |  | 8 $|$ 8 | 0.48 $|$ 0.54 | 141 $|$ 142 |  | 8 $|$ 8 | 0.69 $|$ 0.57 | 141 $|$ 141 |  | 8 $|$ 8 | 0.72 $|$ 0.76 | 69 $|$ 69
$cf_{6}$ | 8 $|$ 8 | 1.06 $|$ 1.16 | 146 $|$ 147 |  | 8 $|$ 8 | 0.52 $|$ 0.61 | 142 $|$ 142 |  | 8 $|$ 8 | 0.60 $|$ 0.73 | 141 $|$ 141 |  | 8 $|$ 8 | 0.72 $|$ 0.72 | 69 $|$ 69
$cf_{7}$ | U | 0.58 $|$ 0.58 | 141 $|$ 142 |  | U | 0.38 $|$ 0.36 | 140 $|$ 141 |  | U | 0.47 $|$ 0.44 | 140 $|$ 141 |  | U | 0.30 $|$ 0.34 | 66 $|$ 67
PBC | $pb_{1}$ | U | 0.04 $|$ 0.04 | 29 $|$ 140 |  | U | 0.16 $|$ 0.17 | 140 $|$ 139 |  | 9 $|$ 9 | 0.28 $|$ 0.29 | 141 $|$ 141 |  | 9 $|$ 9 | 0.27 $|$ 0.28 | 67 $|$ 67
BST | $bs_{1}$ | U | 0.04 — 0.03 | 64 — 63 |  | U | 0.29 $|$ 0.24 | 70 $|$ 68 |  | U | 0.31 $|$ 0.30 | 69 $|$ 68 |  | U | 0.25 $|$ 0.25 | 69 $|$ 69
$bs_{2}$ | 2 $|$ 2 | 0.04 $|$ 0.04 | 62 $|$ 64 |  | 2 $|$ 2 | 0.04 $|$ 0.04 | 62 $|$ 62 |  | 2 $|$ 2 | 0.04 $|$ 0.04 | 64 $|$ 64 |  | 2 $|$ 2 | 0.04 $|$ 0.04 | 64$|$ 64
$bs_{3}$ | U | 0.02 $|$ 0.02 | 62 $|$ 62 |  | 5 $|$ 5 | 0.4 $|$ 0.9 | 70 $|$ 73 |  | 5 $|$ 5 | 0.39 $|$ 0.85 | 70 $|$ 74 |  | 5 $|$ 5 | 0.40 $|$0.70 | 70 $|$ 72

Table 2. Run-time performance for four case studies and 18 properties. We
record the outcome (out.) of the algorithm with (IBSC) or without
($n\textsc{IBSC}$) the optimal solution guarantee: UNSAT (U), bounded-UNSAT
(b-U), or the volume of the counterexample $\sigma$ (a natural number,
corresponding to volσ). We consider four different configurations: small (see
Tab. 1) medium (x$10$), big (x$100$), and unbounded ($\infty$) data domain
constraints and volume bound. The different volσ between IBSC and
$n\textsc{IBSC}$ are in bold.

NASA | configuration 1 |  | configuration 2
---|---|---|---
| IBSC | nuXmv |  | IBSC | nuXmv
| out. | time | mem. | out. | time | mem. |  | out. | time | mem. | out. | time | mem.
| (sec) | (MB) | (sec) | (MB) |  | (sec) | (MB) | (sec) | (MB)
$na_{1}$ | U | 0.80 | 154 | U | 0.88 | 82 |  | U | 0.13 | 141 | U | 1.65 | 90
$na_{2}$ | U | 0.16 | 141 | U | 0.47 | 70 |  | U | 0.15 | 141 | U | 1.50 | 90
$na_{3}$ | U | 0.16 | 141 | U | 0.49 | 83 |  | U | 0.13 | 141 | U | 1.48 | 90
$na_{4}$ | U | 0.77 | 80 | U | 0.54 | 83 |  | U | 0.15 | 66 | U | 1.43 | 91
$na_{5}$ | U | 0.14 | 140 | U | 0.52 | 82 |  | U | 0.15 | 141 | U | 1.43 | 90
$na_{6}$ | U | 0.03 | 62 | U | 0.57 | 72 |  | U | 0.03 | 62 | U | 1.40 | 90

Table 3. Run-time performance of our approach (IBSC) and the state of the art
model checker (nuXmv) on the NASA case study. The configurations considered
are described in Tab. 1. The configurations considered are modifying the
number of ground-separated ($\\#GSEP$) and of self-separating aircraft
($\\#SSEP$) as follow, configuration 1: $\\#GSEP=3$ and $\\#SSEP=0$; and
configuration 2: $\\#GSEP=2$ and $\\#SSEP=2$.

Cases studies. The case studies shown in Tab. 1, are summarized below: (1)
PHIM (derived from (Feng-Marsso-Garavel-21, ; Arfelt-Basin-Debois-19, )): a
computer system for keeping track of personal health information with cost
management; (2) CF@H222https://covidfreeathome.org/: a system for monitoring a
COVID patients at home and enabling doctors to monitor patient data; (3) PBC
(Basin-15, ): an approval policy for publishing business reports within a
company; (4) BST (Basin-15, ): a banking system that processes customer
transactions; and (5) NASA (Mattarei-15, ; Gario-et-al-16, ): an automated
air-traffic control system design that aims to avoid aircraft collisions.
333The requirements and properties for the NASA case study are originally
expressed in LTL, which is subsumed by MFOTL. Case studies were selected for
(i) the purpose of comparison with existing works (i.e., NASA); (ii) checking
whether our approach scales with case studies involving data/time constraints
(PBC, BST, PHIM and CF@H); or (iii) evaluating the applicability of our
approach with real-word case studies (CF@H and NASA). In addition to prior
case studies, we include PHIM and CF@H which have complex data/time
constraints. The number of requirements for the five case studies ranges
between ten (BST) and 194 (NASA). The number of relations present in the MFOTL
requirements ranges from three (BST) to 28 (CF@H), and the number of arguments
in these relations ranges from 1 (PHM, PBC, and BST) to 79 (NASA). Examples of
properties and requirements considered in this evaluation are shown in Fig. 1.

Experimental setup. Given a set of requirements, data constraints and
properties of interest for each case study, we measured the run-time (time)
and peak memory usage (mem.) of performing bounded satisfaction checking of
MFOTL properties, and the volume $vol_{\sigma}$ (the number of relational
objects) of the solution ($\sigma$) with (IBSC) and without ($n\textsc{IBSC}$)
the optimality guarantees (see Remark Remark for finding non-optimal
solutions). We conduct two experiments: the first one evaluates the efficiency
and scalability of our approach; the second one compares our approach with
satisfiability checking. Since there is no existing work for checking MFOTL
satisfiability, we compared with LTL satisfiability checking because MFOTL
subsumes LTL. To study the scalability of our approach, our first experiment
considers four different configurations obtained by increasing the data domain
constraints of the case studies requirements. The initial configuration
(small) is described in Tab. 1. The medium and large configurations are
obtained by multiplying the initial data constraints and volume bound by ten
and hundred, respectively. The last (unbounded) configuration does not bound
either the data domain or the volume. To study performance of our approach
relative to existing work, our second experiment considers two configurations
of the NASA case study verified in (Li-et-al-19, ) using the state of the art
symbolic model checker nuXmv (DBLP:conf/cav/CavadaCDGMMMRT14, ). We compare
our approach’s result against the reproduced result of nuXmv verification. For
both experiments, we report the analysis outcomes, i.e., the satisfying
solution and its volume, UNSAT, or bounded UNSAT; and performance, i.e., time
and memory usage. The experiments were conducted using a ThinkPad X1 Carbon
with an Intel Core i7 1.80 GHz processor, 8 GB RAM, and running 64-bit Ubuntu
GNU/Linux 8.

Results of the first experiment are summarized in Tab. 2. Out of the 72
trials, our approach found 31 solutions. It also returned five bounded-UNSAT
answers, and 36 UNSAT answers. The results show that our approach is effective
in checking satisfiability of case studies with different size. More
precisely, we observe that it takes under three seconds to return UNSAT and
between .04 seconds ($bs_{2}$:medium) and 32 minutes ($ph_{7}$:medium:IBSC) to
return a solution. In the worst case, IBSC took 32 minutes for checking
$ph_{7}$ where the property and requirements contain complex constraints.
Effectively, $ph_{7}$ requires the deletion of data stored at id 10, while
PHIM requires that the cost of deletion increases over time. Therefore, the
user has to perform a number of actions to obtain a sufficient balance to
delete the data. Additionally, each action that increases the user’s balance
has its own preconditions, effects, and time cost, making the process of
choosing the sequence of actions to meet the increasing deletion cost non-
trivial.

We can see a difference in time between cf2 ‘big’ and ‘unbounded’, this is
because the domain expansion followed two different paths and one produces
significantly easier SMT queries. Since our approach is guided by counter-
examples (i.e., the path is guided by the solution from the SMT solver
(Alg.1-L:16)), our approach does not have direct control over the exact path
selection. In future work, we aim to add optimizations to avoid/backtrack from
hard paths.

We observe that the data domain constraint and volume bound used in different
configurations do not affect the performance of IBSC when the satisfiability
of the instances does not depend on them which is the case for all the
instances except for $ph_{6-7}$:small, $cf_{1-3}:small$, and $bs_{3}$:small.
As mentioned in Sec. 4, the data domain constraint ensures that satisfying
solutions have realistic data values. For $ph1-ph4$, the bound used in small,
medium and large configurations creates additional constraints in the SMT
queries for each relational object, and therefore results in a larger peak
memory than the unbounded configuration.

Finding the optimal solution (by IBSC), in contrast to finding a satisfying
solution without the optimal guarantee (by $n\textsc{IBSC}$), imposes a
substantial computational cost while rarely achieving a volume reduction. The
non-optimal heuristic $n\textsc{IBSC}$ often outperformed the optimal approach
for satisfiable instances. Out of 31 satisfiable instances, $n\textsc{IBSC}$
solved 12 instances 3 times faster, 10 instances 10 times faster and seven
instances 20 times faster than IBSC. Compared to the non-optimal solution, the
optimal solution reduced the volume for only two instances: $ph_{7}$:large and
$ph_{7}$:unbounded by one (3%) and three (9%), respectively. On all other
satisfying instances, IBSC and $n\textsc{IBSC}$ both find the optimal
solutions. When there is no solution, both IBSC and $n\textsc{IBSC}$ are
equally efficient.

Results of the second experiment are summarized in Tab. 3. Our approach and
nuXmv both correctly verified that all six properties were UNSAT in both NASA
configurations. We observe that performance of our approach is comparable to
nuXmv for the first configuration with .10 to .20 seconds of difference on
average. Yet, for the second configuration, our approach terminates in less
than 0.20 sec and nuXmv takes 1.50 seconds on average. We conclude that our
approach’s performance is comparable to that of nuXmv for LTL satisfiability
checking even though our approach is not specifically designed for LTL.

Summary. In summary, we have demonstrated that our approach is effective at
determining the bounded satisfiability of MFOTL formulas using case studies
with different sizes and from different application domains. When restricted
to LTL, our approach is at least as effective as the existing work on LTL
satisfiability checking which uses the state of the art symbolic model
checker. Importantly, IBSC can often determine satisfiability of instances
without reaching the volume bound, and its performance is insensitive to data
domain. A current limitation of IBSC is its inability to directly support
constraint over aggregated values in the input formulas. As a walk-around,
aggregated values are captured using auxiliary predicates (e.g., the balance
of a user in $ph_{7}$) and data constraints to simulate the aggregation
process (e.g., how the balance is updated with respect to relevant data
actions). However, the evaluation results shows that the walk-around costs the
efficiency of IBSC. Thus, we need to study how to extend IBSC to efficiently
handle aggregation. We also observed that IBSC’s optimal guarantee imposes a
substantial computational cost while rarely achieving a volume reduction over
non-optimal solutions obtained by $n\textsc{IBSC}$. We need to investigate the
trade-off between optimality and efficiency, as well as evaluate performance
of IBSC on a broader range of benchmarks.

##  7\. Related Work

Below, we compare with the existing approaches for verifying legal properties
as well as with the approaches that address the satisfiability checking of
temporal logic and first-order logic.

Legal compliance. Various techniques have been proposed for operationalizing
legal provisions and ensuring that systems comply with these provisions, e.g.,
(Breaux-Vail-Anton-06, ; Ghanavati-Amyot-Peyton-07, ; Islam-et-al-10, ; torre-
alferez-soltana-sabetzadeh-20, ). MFOTL has been used in the context of
runtime policy monitoring and enforcement, e.g., for monitoring security
policies (Basin-et-al-10, ) and data privacy rules (Arfelt-Basin-Debois-19, ).
While our work is based on the same logic, our intended use case and the type
of reasoning we perform are different: we use MFOTL to specify requirements
and properties and then look for legal-property violations. Crucially, while
previous work requires a system implementation, our approach enables early
validation of legal property compliance by checking the requirements.

Satisfiability checking of temporal properties. Temporal logic satisfiability
checking has been studied for the verification of system designs.
Satisfiability checking for Linear Temporal Logic (LTL) can be performed by
reducing the problem to model checking (Rozier-et-al-07, ), by applying
automata-based techniques (Li-et-al-13, ), or by SAT solving (Li-et-al-20, ;
DBLP:conf/aaai/LiRPZV19, ; DBLP:journals/logcom/LiP0VH18, ;
DBLP:journals/japll/BersaniFMPRP14, ). Satisfiability checking for metric
temporal logic (MTL) (Pradella-et-al-13, ) and its variants, e.g., mission-
time LTL (Li-et-al-19, ) and signal temporal logic
(DBLP:journals/pacmpl/BaeL19, ), has been studied for the verification of
real-time system designs. These existing techniques are inadequate for our
needs: LTL and MTL cannot effectively capture quantified data constraints
commonly used in legal properties. MFOTL does not have such a limitation as it
extends MTL and LTL with first-order quantifiers, thereby supporting the
specification of data constraints. Finite model finding for first-order logic.
Finite-model finders (claessen2003new, ; DBLP:conf/cade/ReynoldsTGKDB13, )
look for a model by checking universal quantifiers exhaustively over candidate
models with progressively larger domains; we look for finite-volume solutions
using a similar approach. On the other hand, we consider an explicit bound on
the volume of the solution, and are able to find the solution with the
smallest volume. SMT solvers support quantifiers with quantifier instantiation
heuristics (DBLP:conf/cav/GeM09, ; DBLP:conf/cade/GeBT07, ) such as E-matching
(DBLP:journals/jacm/DetlefsNS05, ; DBLP:conf/cade/MouraB07, ) and conflict-
based instantiation (DBLP:conf/fmcad/ReynoldsTM14, ). Quantifier instantiation
heuristics are nonetheless generally incomplete, whereas, in our approach, we
obtain completeness by bounding the volume of the satisfying solution.

##  8\. Conclusion

In this paper, we proposed an incremental bounded satisfiability checking
approach, called IBSC, aimed to enable verification of legal properties,
expressed in MFOTL, against system requirements. IBSC first translates MFOTL
formulas to first-order logic (FOL) and then searches for a satisfying
solution to the translated FOL formulas in a bounded search space by deriving
over- and under-approximating SMT queries. IBSC starts with a small search
space and incrementally expands it until an answer is returned or until the
bound is exceeded. We implemented IBSC on top of the SMT solver Z3.
Experiments using five case studies showed that our approach was effective for
identifying errors in requirements from different application domains.

To the best of our knowledge, we are the first to study satisfiability
checking for MFOTL. Our approach is meant for use in early-stage system
development and to support building systems that comply to legal properties
before detailed behavioural models or a system implementation become
available.

Our approach is currently limited to verifying safety properties. In the
future, we plan to extend our approach so that it can handle broader property
types, including liveness and fairness. IBSC’s performance and scalability
depend crucially on how the domain of relational objects is maintained and
expanded (currently, this is done using two heuristics). As a future work, we
would like to study the effectiveness of other heuristics to improve IBSC’s
scalability (e.g., random restart, expansion with domain-specific heuristics).
We also aim to study how to learn/infer MFOTL properties during the search to
further improve the efficiency of our approach.

## References

  * [1] Emma Arfelt, David A. Basin, and Søren Debois.  Monitoring the GDPR.  In Kazue Sako, Steve A. Schneider, and Peter Y. A. Ryan, editors, Computer Security - ESORICS 2019 - 24th European Symposium on Research in Computer Security, Luxembourg, September 23-27, 2019, Proceedings, Part I, volume 11735 of Lecture Notes in Computer Science, pages 681–699. Springer, 2019.
  * [2] Kyungmin Bae and Jia Lee.  Bounded model checking of signal temporal logic properties using syntactic separation.  Proc. ACM Program. Lang., 3(POPL):51:1–51:30, 2019.
  * [3] David A. Basin, Felix Klaedtke, and Samuel Müller.  Monitoring security policies with metric first-order temporal logic.  In James B. D. Joshi and Barbara Carminati, editors, Proceedings of the 15th Symposium on Access Control Models and Technologies (SACMAT’2010), Pittsburgh, Pennsylvania, USA, pages 23–34. ACM, 2010.
  * [4] David A. Basin, Felix Klaedtke, and Samuel Müller.  Policy monitoring in first-order temporal logic.  In Tayssir Touili, Byron Cook, and Paul B. Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, pages 1–18. Springer, 2010.
  * [5] David A. Basin, Felix Klaedtke, Samuel Müller, and Eugen Zalinescu.  Monitoring metric first-order temporal properties.  J. ACM, 62(2):15:1–15:45, 2015.
  * [6] Marcello M. Bersani, Achille Frigeri, Angelo Morzenti, Matteo Pradella, Matteo Rossi, and Pierluigi San Pietro.  Constraint LTL satisfiability checking without automata.  J. Appl. Log., 12(4):522–557, 2014.
  * [7] Travis D. Breaux, Matthew W. Vail, and Annie I. Antón.  Towards regulatory compliance: Extracting rights and obligations to align requirements with regulations.  In 14th IEEE International Conference on Requirements Engineering (RE 2006), 11-15 September 2006, Minneapolis/St.Paul, Minnesota, USA, pages 46–55. IEEE Computer Society, 2006.
  * [8] Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta.  The nuxmv symbolic model checker.  In CAV, pages 334–342, 2014.
  * [9] Koen Claessen and Niklas Sörensson.  New techniques that improve mace-style finite model finding.  In Proceedings of the CADE-19 Workshop: Model Computation-Principles, Algorithms, Applications, pages 11–27. Citeseer, 2003\.
  * [10] Leonardo De Moura and Nikolaj Bjørner.  Z3: An efficient smt solver.  In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008.
  * [11] Leonardo Mendonça de Moura and Nikolaj Bjørner.  Efficient e-matching for SMT solvers.  In Frank Pfenning, editor, Proceedings of the 21st International Conference on Automated Deduction (CADE’2007), Bremen, Germany, volume 4603 of Lecture Notes in Computer Science, pages 183–198. Springer, 2007\.
  * [12] David Detlefs, Greg Nelson, and James B. Saxe.  Simplify: a theorem prover for program checking.  J. ACM, 52(3):365–473, 2005.
  * [13] Nick Feng, Lina Marsso, and Hubert Garavel.  Health record.  Model checking context model (MCC’21), Dept. of Computer Science - University of Toronto, 2021.
  * [14] Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta, and Kristin Yvonne Rozier.  Model checking at scale: Automated air traffic control design space exploration.  In Swarat Chaudhuri and Azadeh Farzan, editors, Proceedings of the 28th International Conference on Computer Aided Verification (CAV’2016), Toronto, ON, Canada, volume 9780 of LNCS, pages 3–22. Springer, 2016.
  * [15] Marco Gario and Andrea Micheli.  Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms.  In SMT Workshop 2015, 2015.
  * [16] Paul Gastin, Pierre Moro, and Marc Zeitoun.  Minimization of counterexamples in SPIN.  In Susanne Graf and Laurent Mounier, editors, Proceedings of the 11th International Workshop on Model Checking Software (SPIN’04), Barcelona, Spain, volume 2989 of Lecture Notes in Computer Science, pages 92–108. Springer, 2004.
  * [17] Yeting Ge, Clark W. Barrett, and Cesare Tinelli.  Solving quantified verification conditions using satisfiability modulo theories.  In Frank Pfenning, editor, Proceedings of the 21st International Conference on Automated Deduction (CADE’2007), Bremen, Germany, volume 4603 of Lecture Notes in Computer Science, pages 167–182. Springer, 2007\.
  * [18] Yeting Ge and Leonardo Mendonça de Moura.  Complete instantiation for quantified formulas in satisfiabiliby modulo theories.  In Ahmed Bouajjani and Oded Maler, editors, Proceedings of the 21st International Conference on Computer Aided Verification (CAV’2009), Grenoble, France, volume 5643 of Lecture Notes in Computer Science, pages 306–320. Springer, 2009.
  * [19] Sepideh Ghanavati, Daniel Amyot, and Liam Peyton.  Towards a framework for tracking legal compliance in healthcare.  In John Krogstie, Andreas L. Opdahl, and Guttorm Sindre, editors, Advanced Information Systems Engineering, 19th International Conference, CAiSE 2007, Trondheim, Norway, June 11-15, 2007, Proceedings, volume 4495 of Lecture Notes in Computer Science, pages 218–232. Springer, 2007.
  * [20] Sylvain Hallé and Roger Villemaire.  Runtime enforcement of web service message contracts with data.  IEEE Trans. Serv. Comput., 5(2):192–206, 2012.
  * [21] Ian M. Hodkinson.  Loosely guarded fragment of first-order logic has the finite model property.  Stud Logica, 70(2):205–240, 2002.
  * [22] Shareeful Islam, Haralambos Mouratidis, and Stefan Wagner.  Towards a framework to elicit and manage security and privacy requirements from laws and regulations.  In Roel J. Wieringa and Anne Persson, editors, Proceedings of the 16th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ’2010), Essen, Germany, volume 6182 of LNCS, pages 255–261. Springer, 2010.
  * [23] Daniel Jackson.  Alloy: a lightweight object modelling notation.  ACM Trans. Softw. Eng. Methodol., 11(2):256–290, 2002.
  * [24] Legislative Assembly of Ontario.  Personal health information protection act (PHIPA), 2004.
https://www.ontario.ca/laws/statute/04p03.

  * [25] Jianwen Li, Geguang Pu, Lijun Zhang, Moshe Y. Vardi, and Jifeng He.  Accelerating LTL satisfiability checking by SAT solvers.  J. Log. Comput., 28(6):1011–1030, 2018.
  * [26] Jianwen Li, Geguang Pu, Yueling Zhang, Moshe Y. Vardi, and Kristin Y. Rozier.  Sat-based explicit ltlf satisfiability checking.  Artif. Intell., 289:103369, 2020.
  * [27] Jianwen Li, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, and Moshe Y. Vardi.  Sat-based explicit ltlf satisfiability checking.  In The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019, pages 2946–2953. AAAI Press, 2019\.
  * [28] Jianwen Li, Moshe Y. Vardi, and Kristin Y. Rozier.  Satisfiability checking for mission-time LTL.  In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II, volume 11562 of Lecture Notes in Computer Science, pages 3–22. Springer, 2019.
  * [29] Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, and Jifeng He.  LTL satisfiability checking revisited.  In Proceedings of the 20th International Symposium on Temporal Representation and Reasoning, Pensacola, FL, USA, 2013, pages 91–98. IEEE Computer Society, 2013.
  * [30] Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta, and Kristin Y. Rozier.  Comparing different functional allocations in automated air traffic control design.  In Roope Kaivola and Thomas Wahl, editors, Formal Methods in Computer-Aided Design (FMCAD’2015), Austin, Texas, USA, pages 112–119. IEEE, 2015.
  * [31] Nina Narodytska and Fahiem Bacchus.  Maximum satisfiability using core-guided maxsat resolution.  In Carla E. Brodley and Peter Stone, editors, Proceedings of the 28th International Conference on Artificial Intelligence (AAAI’14), Québec City, Canada, pages 2717–2723. AAAI Press, 2014.
  * [32] Christos H. Papadimitriou.  On the complexity of integer programming.  J. ACM, 28(4):765–768, 1981.
  * [33] Emil L. Post.  Recursive unsolvability of a problem of thue.  J. Symb. Log., 12(1):1–11, 1947.
  * [34] Matteo Pradella, Angelo Morzenti, and Pierluigi San Pietro.  Bounded satisfiability checking of metric temporal logic specifications.  ACM Trans. Softw. Eng. Methodol., 22(3):20:1–20:54, 2013.
  * [35] Andrew Reynolds, Cesare Tinelli, and Leonardo Mendonça de Moura.  Finding conflicting instances of quantified formulas in SMT.  In Formal Methods in Computer-Aided Design (FMCAD’2014), Lausanne, Switzerland, pages 195–202. IEEE, 2014.
  * [36] Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, and Clark W. Barrett.  Quantifier instantiation techniques for finite model finding in SMT.  In Maria Paola Bonacina, editor, Automated Deduction - CADE-24 \- 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of Lecture Notes in Computer Science, pages 377–391. Springer, 2013.
  * [37] Kristin Y. Rozier and Moshe Y. Vardi.  LTL satisfiability checking.  In Dragan Bosnacki and Stefan Edelkamp, editors, Proceedings of the 14th International Workshop on Model Checking Software (SPIN’07), Berlin, Germany, volume 4595 of Lecture Notes in Computer Science, pages 149–167. Springer, 2007.
  * [38] Lijun Shan, Behrooz Sangchoolie, Peter Folkesson, Jonny Vinter, Erwin Schoitsch, and Claire Loiseaux.  A survey on the application of safety, security, and privacy standards for dependable systems.  In Proceedings of the 15th European Dependable Computing Conference (EDCC’2019), Naples, Italy, pages 71–72. IEEE, 2019.
  * [39] Damiano Torre, Mauricio Alférez, Ghanem Soltana, Mehrdad Sabetzadeh, and Lionel C. Briand.  Model driven engineering for data protection and privacy: Application and experience with GDPR.  CoRR, abs/2007.12046, 2020.