{'fraction_non_alphanumeric': 0.04796956039227233, 'fraction_numerical': 0.01014653590922474, 'mean_word_length': 4.539330071509221, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 3, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Bounded Satisfiability Checking of Metric First-order Temporal Logic

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.


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 [22,38]. The properties stipulated by these laws, regulations and policies -which we refer to as legal properties (LP) hereaftertypically involve reasoning about actions, ordering and time. As an example, consider the following LP, 1, derived from a health-data regulation (s. 11, PHIPA [24]): "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 [28,37]. For instance, the requirement (req 0 ) 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 1. It is important to formalize the data and time constraints of both the system requirements and LPs, such as the ones of 1 and req 0 .
Metric first-order temporal logic (MFOTL) enables the specification of data and time constraints [4] and has an expressive formalism for capturing LPs and the related system requirements that constrain data and time [1]. Existing work on MFOTL verification has focused primarily on detecting violations at run-time through monitoring [1], 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 1 is a sequence consisting of storing a value in a variable , updating 's value to ′ , then reading again and not obtaining ′ . 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) [28,37]. 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 [23]. 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 [10]. 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.

PRELIMINARIES
In this section, we introduce the necessary background on metric first order temporal logic (MFOTL).
Syntax. We begin with the syntax of MFOTL [4]. Definition 1. Let I be a non-empty interval over N. An interval ∈ I can be expressed as [b, b') where ∈ N and ′ ∈ N ∪ ∞. A signature is a tuple ( , , ), where is a set of constant and is a finite set predicate symbols, respectively. Without loss of generality, we assume all constants are from the integer domain I where the theory of linear integer arithmetic (LIA) holds. The function : → N associates each predicate symbol ∈ with an arity ( ) ∈ N. Let be a countable infinite set of variables from domain I and a term is defined inductively as : | | + | × . We denote¯as a vector of terms and¯as the vector that contains at index . The syntax of MFOTL formulas is defined as follows: (1) ⊤ and ⊥, representing values "true" and "false"; (2) = ′ and > ′ , for term and ′ (3) ( 1 ... ) for ∈ and 1 ... are terms. (4) ∧ , ¬ for MFOTL formulas and ; (5) ∃ · ( (¯) ∧ ) for MFOTL formula , relation symbol ∈ , variable ∈ and a vector of terms¯such that =¯[ ] (6) U , S , , for MFOTL formulas and , and an interval ∈ I.
The temporal operators U , S , and require the satisfaction of the formula within the time interval given by . We write [ , ) as a shorthand for [ , ∞), if is omitted, then the interval is assumed to be [0, ∞). Other classical unary temporal operators ♢ (i.e., eventually), □ (i.e., always), and ♦ (i.e., once) are defined as follows: ♢ = ⊤ U , □ = ¬♢ ¬ , and ♦ = ⊤ S . Other common logical operator such as ∨ (disjunction) and ∀ (universal quantification) are expressed through negation of ∧ and ∃, respectively.
Example 1. Suppose a data collection centre (DCC) collects and accesses personal data information with three requirements: 0 stating that no data is allowed to be accessed before being having been collected for 15 days (360 hours); 1 : data can only be updated after having been collected or last updated for more than a week (168 hours); and 2 : data can only be accessed if has been collected or updated within a week (168 hours). The signature for DCC contains three binary relations ( ): Collect, Update, and Access, such that Collect( , ), Update( , ) and Access( , ) hold at a given time point if and only if data at id is collected, updated, and accessed with value at this time point, respectively. The MFOTL formulas for 1, 0 , 1 and 2 are shown in Fig. 1. For instance, the formula 0 specifies that if a data value stored at id is accessed, then some data must have been collected and stored at id before, and the collection must have occurred prior to 360 hours ago (♦ [360,) ]).

Semantics.
A first-order (FO) structure over the signature = ( , , ) comprises a domain | | ≠ ∅ and an interpretation for ∈ | | and ⊆ | | ( ) for each ∈ and ∈ . The semantics of MFOTL formulas is defined over a sequence of FO structures = ( 0 , 1 , . . .) and a sequence of natural numbers representing time¯= ( 0 , 1 , . . .), where (a)¯is a monotonically increasing sequence; (b) | | = | +1 | for all > 0 (all have a fixed domain); and (c) each constant symbol ∈ has the same interpretation across¯(i.e., = +1 ) Property (a) ensures that time never decreases as the sequence progresses; and (b) ensures that the domain is fixed.¯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 to interpret the symbols in the signature . Intuitively, the semantics of MFOTL is defined over a trace of timed first-order structures = (¯,¯), where every structure ∈¯contains a set of holding relations , and these relations occur at a time specified by ∈¯.
Example 2. Consider the signature in the DCC example. Let 1 = 0 and 2 = 361, and let 1 and 2 be two first order structures with 1 = Collect(0, 0) and 2 = Access(0, 0), respectively. The 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.
No data is allowed to be accessed before having been collected for at least 15 days (360 hours). [1,168] ∃ ′ · (Collect( , ′ ) ∨ Update( , ′ )))) Data can only be updated after having been collected or last updated for more than a week (168 hours).
) Data can only be accessed if has been collected or updated within a week (168 hours).
)) Data cannot be re-collected.   The operators , , U and S are augmented with an interval ∈ I which defines the satisfaction of the formula within a time range specified by relative to the current time at step , i.e., .

Definition 3 (MFOTL Satisfiability
). An MFOTL formula is satisfiable if there exists a sequence of FO structures¯and natural numbers¯, and a valuation function such that (¯,¯, , 0) |= . is unsatisfiable otherwise.   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.

BOUNDED SATISFIABILITY CHECKING
The satisfiability of MFOTL properties is generally undecidable since MFOTL is expressive enough for describing the blank tape problem [33] (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 [34] 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 4 (Satisfiability Checking of MFOTL Formulas).
Let be an MFOTL formula over a signature = ( , , ), and let be a set of MFOTL requirements over . Reqs complies (denoted as Reqs ⇒ ) iff ∈ ∧ ¬ is unsatisfiable. We call a solution to ∈ ∧ ¬ (if one exists) a counterexample to Reqs ⇒ .
Example 5. Consider our DCC system requirements and the privacy data property 1 stating that if personal health information is not accurate or not up-to-date, it should not be accessed (see Fig. 1). 1 is not respected by the set of DCC requirements 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 3 ( Fig. 1) is added to prohibit re-collection of collected data, then property 1 would be respected Definition 5 (Finite trace and bounded trace). The volume of a trace = (¯,¯, ) is the total number of relations that hold across , denoted as

The trace is bounded by volume if there exists an upper bound
∈ N such that ( ) ≤ . In the rest of paper, we refer to volume-bounded traces as bounded traces.
Example 6. The volume of trace 4 in Fig. 2, ( 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, |¯|, 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 6 (Bounded satisfiability checking of MFOTL properties). Let be an MFOTL property, Reqs be a set of MFOTL requirements, and be a natural number. The bounded satisfiability checking problem determines the existence of a counterexample to Reqs ⇒ such that ( ) ≤ .

CHECKING BOUNDED SATISFIABILITY
In this section, we present an overview of the bounded satisfiability checking (BSC) process that translates MFOTL formula into firstorder 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.

Overview of BSC for MFOTL Formulas
We aim to address the bounded satisfiability checking problem (Def. 6), looking for a satisfying run within a given volume bound that limits the number of relations in . 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 , or "bounded-UNSAT").

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. contains all constants ∈ and relational objects (denoted ). Each has variables and , and a vector of argument variables ( 1 , . . . , ( ) ) associated with it. Each represents an occurrence of a relation of . at time .
. The following relationship holds for ( , ′ ) and (¯,¯, ): Intuitively, each holding relation in the trace is mapped to a relational object where the holding time of the relation is explicitly associated with the relational object's . 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 . defines the class of relational objects in . For example, ∀ : selects every relational object where . = . 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., 1 ). Fig. 2. The first-order structure of 2 is ( , ′ ), where contains three relational objects. Two of these objects are from the class , and the third one is from the class . Let 1 be the relational object corresponding to the relation For the FO domain , let | | denote the domain size, i.e., the number of its relational objects. Therefore, for any trace bounded by , we can map to a first order structure ( , ′ ) where the domain size of | | is also bounded by . Since MFOTL formulas specify constraints on , ′ in should satisfy FOL formulas corresponding to these MFOTL constraints. , ′ ) where the time information is associated with relational objects in the domain . Therefore, the time point (and its time value ) 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 . Formally, our translation function translate, abbreviated to for succinctness, translates an MFOTL formula into a function : → , where is an FOL formula over relational objects. The FOL formula corresponding to the MFOTL formula at time step is = ( , ). The translation rules for are as follows: Proposition 1 (Quantifiers on relational objects). For a MFOTL formula , the FOL formula ( ) only contains quantifiers exclusively on relational objects. [5,10] ( )) where and are unary relations. The translated FOL formula Given an MFOTL property and a set of requirements , a volume bound , the BSC problem can be solved by searching for a satisfying solution ′ for the FOL formula ( ) ∈ ( ) in a domain with at most relational objects.

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 ( ) be an FOL formula translated from an MFOTL formula , and let be the maximum quantifier nesting in ( ). NBSC solves ( ) via quantifier elimination. By Proposition 1, only relational objects can be quantified. Given a bound , the number of relational objects in any satisfying solution of ( ) should be at most . Therefore, NBSC eliminates quantifiers in ( ) by assuming presence of relational objects and then iterates over them. For example, the formula ∀ : · ( ) is converted to ( 1 ) ∧ ( 2 ) . . . ∧ ( ). After eliminating all quantifiers in the formula ( ), NBSC calls an SMT solver on the quantifier-free formula to obtain the satisfiability result.
Complexity. The size of the quantifier-free formula is ( ), where is the maximum depth of quantifier nesting. Since the background theory used in is restricted to LIA, the complexity of solving the formula is NP-complete [32]. Since Translate is linear in the size of the formula , the complexity of our approach is dominated by solving the translated formula which is NP-complete with respect to the size of the formula, .

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 since its quantifier elimination creates a quantifier-free formula of size ( ) 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 [16], 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 , "bounded-UNSAT", or "UNSAT"). The procedure continues until an answer is obtained or until the domain exceeds the bound , in which case a "bounded-UNSAT" answer is returned. If the bound increases, with the minimal volume and the UNSAT value are preserved while bounded-UNSAT may turn into 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.

Over-and Under-Approximation
IBSC searches for a counter-example in a FO domain whose size is bounded by a given volume bound . Instead of directly searching inside , IBSC starts with an under-approximated domain ↓ ⊆ where every relational object in ↓ is in also . With ↓ , we can create an over-and an underapproximation query to the bounded satisfiability problem. Such queries are used to check satisfiability of FO formulas with domain ↓ . IBSC starts with a small domain ↓ and gradually expands it until either SAT or UNSAT is returned, or the domain size exceeds some limit (bounded-UNSAT).
Over-approximation. Let be an FOL formula with quantifiers over relational objects, and ↓ be an FO domain of relation objects. The procedure Ground ( ) encodes into a quantifier-free FOL formula s.t. the unsatisfiability of implies the unsatisfiability of . We call an over-approximation of .
The procedure (Alg. 2) recursively traverses the AST of the input FOL formula. To eliminate the existential quantifier in ∃ : · (L:2), creates a new relational object (unconstrained) of class (L: 5), and replaces with in (L:6).
To eliminate the universal quantifier in ∀ : · (L: 8), expands the quantifier into a conjunction of clauses where each clause is [ ← ] (i.e., is replaced by in ) for each relational object of class in ↓ (L:10). Intuitively, an existentiallyquantified 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 ↓ .
Example 9. Consider the following FOL formula: = ∃access : Access · (∀update : Update)· ( instantiates ∃access : Access with a new relational object, 1 , and instantiates ∀update : Update with two relational objects, 1 and 2 in ↓1 . The grounded formula is Proposition 2. For every FOL formula translated from MFOTL formula and domain ↓ , the grounded formula = ( , ↓ ) is quantifier-free and contains a finite number of variables and terms.

Lemma 1 (Over-approximation Query). For an FOL formula , and a domain
Proof. We prove Lemma 1 by contradiction. Suppose is UN-SAT but there exists a solution for in some domain ( may be different from ↓ ). We show that we can always construct a solution that satisfies , which causes a contradiction. First, we construct a solution ′ for ′ = ( , ) from the solution (for ). Then, we construct a solution for from the solution ′ for ′ .
We can construct a solution ′ for ′ in ∪ where are the new relational objects added by . The encoding of uses the standard way for expanding universally quantified expression by enumerating every relation object in (L:10). For every existentially quantified expression, there exists some relation object ∈ enabled by that satisfies the expression in , whereas ′ contains a new relational object ′ ∈ for satisfying the same expression (L:6). Let ( ) = ′ ( ′ ) for and ′ , and then ′ is a solution to ′ .
For every relational object ∈ ↓ ∩ , we let ( ) = ′ ( ), and all shared constraints in and ′ are satisfied by and ′ , respectively. Therefore, is a solution to . Contradiction. □ Under-approximation. Let be an FOL formula, and ↓ be an FO domain. The over-approximation = ( , ↓ ) contains a set of new relational objects introduced by (L:5), denoted by . Let NoNewR( , ↓ ) be constraints that enforce that every new relational object in be identical to some relational objects in ↓ . Formally, . If ⊥ has a satisfying solution, then there is a solution for . We call ⊥ an underapproximation of and denote the procedure for computing it by UnderApprox( , ↓ ).
Proof. By construction, NoNewR( , ↓ ) guarantees that if is a solution to ⊥ in the domain ↓ , there exists a solution ′ to in the domain ↓ ∪ . Since every relational object ∈ ↓ has been used to instantiate a universally-quantified expression (L:10 of Alg. 2), ′ is also a solution to .
□ Suppose for some domain ↓ , an over-approximation query for an FOL formula is satisfiable while the under-approximation query ⊥ is UNSAT. Then we cannot conclude satisfiability of for ↓ . However, the solution to provides hints on how to expand ↓ to potentially obtain a satisfying solution for .
Corollary 1 (Necessary relational objects). For a satisfying FOL formula and a domain ↓ , let and ⊥ be the over-and underapproximation queries of based on ↓ , respectively. Suppose is satisfiable, and ⊥ is UNSAT, then every solution to contains some relational object mentioned in the formula but not in ↓ .
Cor. 1 holds because and ⊥ are over-and under-approximation of , respectively. Cor. 1 shows that any domain that contains a satisfying solution to must consider some relational objects from some solution to .
If is satisfiable, then IBSC solves the under-approximation query ⊥ (L:11). If ⊥ is unsatisfiable, then the current domain ↓ is too small, and IBSC expands it (LL: [15][16][17][18][19][20][21][22]. This is because satisfiability of indicates the possibility of finding a satisfying solution after adding at least one of the new relational objects in the solution of to ↓ (Cor. 1). The expansion aims to identify a minimum solution for that requires the smallest number of relational objects (L:16). For every relational object ′ ∈ , ′ is added to ↓ if it is not already in ↓ (L: 18). To obtain , we follow MaxRes [31] methods: we analyze the UNSAT core of ⊥ and incrementally weaken ⊥ towards (i.e., the weakened query ⊥ ′ is an "over-under approximation" that satisfies the condition ⊥ ⇒ ⊥ ′ ⇒ ) until a satisfying solution is obtained for the weakened query. However, if the volume of exceeds (L: 19), then bounded-UNSAT is returned (L:20).
On the other hand, if ⊥ yields a solution , then is checked on Reqs (L:23). If satisfies every in Reqs , then is returned (L:24). If violates some requirements in Reqs , then the violating requirement is added to Reqs ↓ 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 ↓ is too small or the Reqs ↓ are too weak. IBSC then starts again with either the expanded domain ↓ or the refined set of requirements Reqs ↓ . It computes the over-and under-approximation queries ( and ⊥ ) again and repeats the steps. Due to structural similarities of and ⊥ between iterations, incremental encoding and solving are enabled to allow SMT solvers to internally reuse learned clauses from previous iterations.

Correctness, Termination, Optimality
In this section, we first prove correctness of the IBSC algorithm, then show that IBSC always terminates when ≠ ∞ and finally prove that IBSC always finds a solution with a minimum volume.
If the requirement checking fails on L: 23, a violating requirement is added to Reqs ↓ (LL: [26][27][28] which ensures that any future solution ′ satisfies . Therefore, is never added to Reqs ↓ more than once. Given that Reqs is a finite set of MFOTL formulas, at most |Reqs| lessons can be learned before the algorithm terminates. The under-approximated domain ↓ can be expanded a finite number of times because the size of the minimum solution ( ) to (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 ↓ can introduce a finite number of options for adding a new relational object through the grounded encoding of on L:10, e.g., ⇒ =0 ∃ . After exploring all options to ↓ , ( ) must increase if the algorithm has not already terminated. Therefore, if ≠ ∞, then eventually ( ) > , and the algorithm will return bounded-UNSAT instead of expanding ↓ indefinitely (LL: [15][16][17][18][19][20][21][22]. □ Theorem 3 (Solution optimality). For a property and requirements Reqs, let be the FOL formula ( ) ∈Reqs ( ). If IBSC finds a solution for , then for every ′ |= , ( ) ≤ ( ′ ).
Proof. IBSC returns a solution on L:24 only if is a solution to the under-approximation query ⊥ (computed on L:10) for some domain ↓ ≠ ∅. ↓ is last expanded in some previous iterations by adding relational objects to the minimum solution (L:16) of the over-approximation query ′ (L:18). Therefore, the returned has the same number of relational objects as ( ( ) = ( )). Since is an over-approximation of the original formula , any solution ′ to has volume that is at least ( ). Therefore, Remark. IBSC finds the optimal solution because it always looks for the minimum solution to the over-approximation query (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 to such that ( ) ≤ . For example, greedy best-first search ( ) finds a solution to that minimizes the number of relational objects that are not already in ↓ , and then uses it to expand ↓ . We configured a non-optimal version of IBSC ( IBSC) that uses heuristics, and evaluate its performance in Sec. 6.  , # , and # , respectively. Initial configurations with data constraints specific to each case study: PHIM -the number of custodians (# ), patients (# ), and data (# ); CF@H and PBC -the number of users (# ), and data (# ); BST -the number of employees (# ), customers (# ), transactions (# ), and maximum amount for a transaction (sup).

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 [15] to formulate SMT queries and Z3 [10] to check their satisfiability. LEGOS and the evaluation artifacts are included in supplementary material. 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.
Cases studies. The case studies shown in Tab. 1, are summarized below: (1) PHIM (derived from [1,13]): a computer system for keeping track of personal health information with cost management; (2) CF@H 2 : a system for monitoring a COVID patients at home and enabling doctors to monitor patient data; (3) PBC [5]: an approval policy for publishing business reports within a company; (4) BST [5]: a banking system that processes customer transactions; and (5) NASA [14,30]: an automated air-traffic control system design that aims to avoid aircraft collisions. 3 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 runtime (time) and peak memory usage (mem.) of performing bounded satisfaction checking of MFOTL properties, and the volume (the number of relational objects) of the solution ( ) with (IBSC) and without ( IBSC) the optimality guarantees (see Remark 5.3 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 [28] using the state of the art symbolic model checker nuXmv [8]. 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 ( 2 :medium) and 32 minutes ( ℎ 7 :medium:IBSC) to return a solution. In the worst case, IBSC took 32 minutes for checking ℎ 7 where the property and requirements contain complex constraints. Effectively, ℎ 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 ℎ 6−7 :small, 1−3 : , and 3 :small. As mentioned in Sec. 4, the data domain constraint ensures that satisfying solutions have realistic data values. For ℎ1 − ℎ4, 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 IBSC), imposes a substantial computational cost while rarely achieving a volume reduction. The non-optimal heuristic IBSC often outperformed the optimal approach for satisfiable instances. Out of 31 satisfiable instances, 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: ℎ 7 :large and ℎ 7 :unbounded by one (3%) and three (9%), respectively. On all other satisfying instances, IBSC and IBSC both find the optimal solutions. When there is no solution, both IBSC and 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 ℎ 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 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.

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., [7,19,22,39]. MFOTL has been used in the context of runtime policy monitoring and enforcement, e.g., for monitoring security policies [3] and data privacy rules [1]. 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 [37], by applying automata-based techniques [29], or by SAT solving [6,[25][26][27]. Satisfiability checking for metric temporal logic (MTL) [34] and its variants, e.g., mission-time LTL [28] and signal temporal logic [2], 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 [9,36] 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 [17,18] such as E-matching [11,12] and conflict-based instantiation [35]. Quantifier instantiation heuristics are nonetheless generally incomplete, whereas, in our approach, we obtain completeness by bounding the volume of the satisfying solution.

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 underapproximating 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.