On the Parameterized Verification of Abstract Models of Contact Tracing Protocols Sylvain Conchon1 , Giorgio Delzanno2 and Arnaud Sangnier3 1 LRI, UniversitΓ¨ Paris, France 2 DIBRIS, University of Genova, Italy 3 IRIF, UniversitΓ¨ Paris Denis Diderot Abstract We present an automata-based formal model of distributed systems specifically devised to formalise abstractions of Contact Tracing Protocols that combine Bluetooth and network communication. The model combines pure names, read/write operations on first-order and higher-order variables and syn- chronous communication primitives. The transition system models the interaction between devices in the same physical location and between a single device and a notification server. To automatically vali- date protocols in our formalism, we resort to an extension of the Cubicle SMT-based infinite-state model checker, in which the monotonic abstraction applied during the predecessor computation is strengthen by introducing abstract predicates obtained via Counting Abstraction. 1. Introduction Contact tracing protocols, e.g., smartphone apps, are aimed at investigating who could have been contaminated by a positively diagnosed person and alert them, see e.g. [1]. After the COVID-19 pandemic, several protocols have been proposed as an automated support for this task su as PEPP-PT, DP3T, ROBERT4 and NTK5. In general the system architecture is based on a smart app, a notification server as in Publish/Subscribe architectures, and a possibly trusted server. In order to reduce the risk of a malicious use of user data (see e.g. the attacks described in [2, 1]), the protocols are based on frequent rotations of identifiers emitted via bluetooth. In centralized versions of the protocol ephemeral identifiers are downloaded from a trusted server. In decentralized versions ephemeral identifiers are generated by user apps. The user app installed on the user device (e.g. Immuni in Italy) broadcasts the currently valid ephemeral identifier. The same user app also collects all identifiers emitted in the same bluetooth range and stores them locally. When users are diagnosed to be infected, they release a report to the server. One possible implementation consists in sending the report to a central log database. Users can then consult the database to check if they crossed their way with infected users, i.e., they share some ephemeral identifier with one of them. Based on a preliminary study present at Overlay 2020 [3], in this paper we present an automata- based formal model of distributed systems specifically devised to formalise abstractions of Contact Tracing Protocols that combine Bluetooth and network communication. The model OVERLAY 2021: 3rd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, September 22, 2021, Padova, Italy Β© 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) combines pure names, read/write operations on first-order and higher-order variables and synchronous communication primitives. The transition system models the interaction between devices in the same physical location and between a single device and a notification server. Violations of safety properties for this kind of protocols typically require universally quantified conditions on global configurations (e.g. one user detects a contact while no user is positive). To automatically validate protocols in our formalism, we resort to an extension of the Cubicle SMT-based infinite-state model checker. Cubicle is a model checker that can be applied to verify safety properties of array-based systems, a syntactically restricted class of parameterized transition systems with states represented as arrays indexed by an arbitrary number of processes [4, 5]. Cubicle integrates the SMT solver Alt-Ergo [6]. Cubicle input language is a typed version of Murπœ‘ [7]. A system is describe in Cubicle by: a set of type, variable, and array declarations; a formula for the initial states; and a set of transitions. A system execution is defined by an infinite loop that at each iteration non-deterministically chooses a transition instance whose guard is true in the current state; and updates state variables according to the action of the fired transition instance. To validate instances of our model, we will exhibit a general encoding in the Cubicle array- based language and propose to refine the overapproximation of universally quantified precondi- tions applied in the Cubicle backward procedure by introducing abstract predicates obtained via Counting Abstraction. 2. Contact Tracing Systems In this section we introduce a possible general formal model for contact tracing protocol. To specify the protocol rules and behavior (computation), we will use a transition system defined on configurations consisting of a set of states of individual users. User configurations contain a local memory needed to store the list of emitted and received identifiers. System configurations contain a global memory that can be used to gather and a set of user states that corresponds to the current number of registered indivuals. We will use the following general definitions: ℐ is a denumerable set of pure names (identifiers) containing the undefined label βŠ₯; 𝑀 is a finite set of message labels (π‘Ž, 𝑏, 𝑐, . . . ); 𝑉 is a finite set of first order variables (identifiers) that are part of the local state of users (π‘₯, 𝑦, . . . ); 𝑆 is a finite set of second order variables (set of identifiers) that are part of the local state of users (𝑠, 𝑑, . . . ). We then define Act(𝑀, 𝑉, 𝑆) the set of actions defined as follows: π‘’π‘ž(π‘₯, 𝑦) and π‘›π‘œπ‘‘π‘’π‘ž(π‘₯, 𝑦), where π‘₯, 𝑦 ∈ 𝑉 , 𝑖𝑛(π‘₯, π‘š) and π‘›π‘œπ‘‘π‘–π‘›(π‘₯, π‘š), where π‘₯ ∈ 𝑉 and π‘š ∈ 𝑀 (Conditions); π‘™π‘œπ‘π‘Žπ‘™, 𝑛𝑒𝑀(π‘₯), where π‘₯ ∈ 𝑉 , π‘π‘π‘Žπ‘ π‘‘(π‘š, π‘₯) and π‘Ÿπ‘’π‘(π‘š, π‘₯), where π‘š ∈ 𝑀, π‘₯ ∈ 𝑉 ; π‘Žπ‘‘π‘‘(π‘₯, 𝑠), where π‘₯ ∈ 𝑉, 𝑠 ∈ 𝑆, π‘Ÿπ‘’π‘ π‘’π‘‘(𝑠), where 𝑠 ∈ 𝑆, π‘Ÿπ‘’π‘”(π‘š, 𝑠), where π‘š ∈ 𝑀, 𝑠 ∈ 𝑆 (Operations). A protocol is defined as a Data Automaton 𝑃 = βŸ¨π‘„, 𝑀, 𝑉, 𝑆, 𝑅, π‘ž0 ⟩, where π‘ž0 ∈ 𝑄 and 𝑅 βŠ† 𝑄 Γ— Act(𝑀, 𝑆, 𝑉 ) Γ— 𝑄. We assume here that π‘π‘π‘Žπ‘ π‘‘ and π‘Ÿπ‘’π‘” actions are always defined on distinct labels in 𝑀 . Consider a protocol 𝑃 = βŸ¨π‘„, 𝑀, 𝑉, 𝑆, 𝑅, π‘ž0 ⟩. A process configuration of 𝑃 is a triple 𝑝𝑐 = βŸ¨π‘ž, 𝛿, π›ΎβŸ© where: π‘ž ∈ 𝑄 is the current user state; 𝛿 : 𝑉 β†’ ℐ is the current evaluation of first order variables; 𝛾 : 𝑆 β†’ 𝒫(ℐ) is the current evaluation of second order variables. We denote by π’«π’ž the set of process configurations. A global configuration of 𝑃 is then a pair (𝐾, Θ), where 𝐾 ∈ Nπ’«π’ž is a finite multiset of process configurations and Θ : 𝑀 ↦→ 𝒫(ℐ) corresponds to a centralized memory. π’’π’ž denotes the set of global configurations. For 𝜎 ∈ π’’π’ž, we will use 𝑖𝑑𝑠(𝜎) to denote the set of pure names occurring in 𝜎. The operational semantics is then defined as the minimal relation β†’βŠ† 𝒒 Γ— 𝒒 that satisfies the following property definitions in which will use ⊎ to denote multiset union: - 𝜎 = ⟨{βŸ¨π‘ž, 𝛿, π›ΎβŸ©} ⊎ 𝐾, Θ⟩ β†’ ⟨{βŸ¨π‘ž β€² , 𝛿, π›ΎβŸ©} ⊎ 𝐾, Θ⟩ if one of the following conditions is satis- fied: βŸ¨π‘ž, π‘™π‘œπ‘π‘Žπ‘™, π‘ž β€² ⟩ ∈ 𝑅, βŸ¨π‘ž, π‘’π‘ž(π‘₯, 𝑦), π‘ž β€² ⟩ ∈ 𝑅 and 𝛿(π‘₯) = 𝛿(𝑦) [for π‘›π‘œπ‘‘π‘’π‘ž(π‘₯, 𝑦),𝛿(π‘₯) ΜΈ= 𝛿(𝑦)], βŸ¨π‘ž, 𝑖𝑛(π‘₯, π‘š), π‘ž β€² ⟩ ∈ 𝑅 and 𝛿(π‘₯) ∈ Θ(π‘š) [for π‘›π‘œπ‘‘π‘–π‘›(π‘₯, 𝑦) 𝛿(π‘₯) ̸∈ Θ(π‘š)]. - 𝜎 = ⟨{βŸ¨π‘ž, 𝛿, π›ΎβŸ©} ⊎ 𝐾, Θ⟩ β†’ ⟨{βŸ¨π‘ž β€² , 𝛿 β€² , π›ΎβŸ©} ⊎ 𝐾, Θ⟩ if βŸ¨π‘ž, 𝑛𝑒𝑀(π‘₯), π‘ž β€² ⟩ ∈ 𝑅 and 𝛿 β€² (π‘₯) = 𝑖𝑑 ̸∈ 𝑖𝑑𝑠(𝜎), 𝑖𝑑 ΜΈ= βŠ₯, and 𝛿 β€² (𝑦) = 𝛿(𝑦) for π‘₯ ΜΈ= 𝑦. - 𝜎 = ⟨{βŸ¨π‘ž, 𝛿, π›ΎβŸ©} ⊎ 𝐾, Θ⟩ β†’ ⟨{βŸ¨π‘ž β€² , 𝛿, 𝛾 β€² ⟩} ⊎ 𝐾, Θ⟩ if βŸ¨π‘ž, π‘Žπ‘‘π‘‘(π‘₯, 𝑠), π‘ž β€² ⟩ ∈ 𝑅 and 𝛾 β€² (𝑠) = 𝛾(𝑠) βˆͺ {𝛿(π‘₯)} and 𝛾 β€² (𝑑) = 𝛾(𝑑) for 𝑑 ΜΈ= 𝑠. - 𝜎 = ⟨{βŸ¨π‘ž, 𝛿, π›ΎβŸ©} ⊎ 𝐾, Θ⟩ β†’ ⟨{βŸ¨π‘ž β€² , 𝛿, 𝛾 β€² ⟩} ⊎ 𝐾, Θ⟩ if βŸ¨π‘ž, π‘Ÿπ‘’π‘ π‘’π‘‘(𝑠), π‘ž β€² ⟩ ∈ 𝑅 and 𝛾 β€² (𝑠) = βˆ… and 𝛾 β€² (𝑑) = 𝛾(𝑑) for 𝑑 ΜΈ= 𝑠. - 𝜎 = ⟨{βŸ¨π‘ž, 𝛿, π›ΎβŸ©} ⊎ 𝐾, Θ⟩ β†’ ⟨{βŸ¨π‘ž β€² , 𝛿, π›ΎβŸ©} ⊎ 𝐾, Ξ˜β€² ⟩ if βŸ¨π‘ž, π‘Ÿπ‘’π‘”(π‘š, 𝑠), π‘ž β€² ⟩ ∈ 𝑅 and Ξ˜β€² (π‘š) = Θ(π‘š) βˆͺ 𝛾(𝑠) and Ξ˜β€² (𝑛) = Θ(𝑛) for 𝑛 ΜΈ= π‘š. - 𝜎 = ⟨{βŸ¨π‘ž, 𝛿, π›ΎβŸ©, βŸ¨π‘ž1 , 𝛿1 , 𝛾1 ⟩, . . . , βŸ¨π‘žπ‘˜ , π›Ώπ‘˜ , π›ΎβŸ©π‘˜ } ⊎ 𝐾, Θ⟩ β†’ ⟨𝐾 β€² , Θ⟩ where 𝐾 β€² = {βŸ¨π‘ž β€² , 𝛿, π›ΎβŸ©, βŸ¨π‘ž1β€² , 𝛿1β€² , 𝛾1 ⟩, . . . , βŸ¨π‘žπ‘˜β€² , π›Ώπ‘˜β€² , π›Ύπ‘˜ ⟩} ⊎ 𝐾 if π‘˜ β‰₯ 0 and βŸ¨π‘ž, π‘π‘π‘Žπ‘ π‘‘(π‘š, π‘₯), π‘ž β€² ⟩ ∈ 𝑅 and for all 𝑖 ∈ [1, π‘˜], we have βŸ¨π‘žπ‘– , π‘Ÿπ‘’π‘(π‘š, π‘₯𝑖 ), π‘žπ‘–β€² ⟩ ∈ 𝑅 and 𝛿𝑖′ (π‘₯𝑖 ) = 𝛿(π‘₯) and 𝛿𝑖′ (𝑦) = 𝛿𝑖 (𝑦) for 𝑦 ΜΈ= π‘₯𝑖 . For the resulting model, we are interested in safety properties for parameterized version of a protocol instance. More specifically, given a protocol definition 𝑃 and a given process state π‘žπ‘’ ∈ 𝑄 that denotes an error state, we would like to verify that global configurations that contain occurrences of π‘žπ‘’ are unreachable starting from any possibile initial configuration (i.e. independently from the number of process instances). A similar property can be formulated by adding an error flags to the server state instead of selecting a special error state in 𝑄. We are also interested in properties expressed by violations in which global configurations contain a process in state π‘žπ‘’ while all other processes are in states contained in These properties are referred to as control state reachability and constrained control state reachabiliy, respectively. Violations of this kind of properties can be defined using quantified assertions, such as there exists a process 𝑖 in control state π‘žπ‘’ and, for constrained properties, universally quantified conditions on the control states of other processes. In the rest of the paper we will illustrate how to encode our formalism in Cubicle and how to verify control state reachability problems using the corresponding symbolic exploration procedure provided by the tool. 3. Case Studies: Contact Tracing Protocols We present below a formal specifications of the protocol scheme of Contact Tracing applications abstracting away identifier creation, i.e., assuming that user app generate fresh identifiers, and reasoning within the validity epoch of identifiers, i.e., those maintained in local memory. The system is composed of a finite but arbitrary number of user apps and of a server modeled via a centralized memory. Each user apps has local variables 𝑉 = {π‘₯, 𝑦, 𝑧} and 𝑆 = {𝑖𝑛, π‘œπ‘’π‘‘}. Furthermore, 𝑀 = {𝑏, π‘š} where 𝑏 denotes beacon messages broadcasted by user apps, and π‘š denotes report messages sent to the centralized memory. The user app starts their part of protocol in state π‘ž0 and operate in three different modes. In emitter mode the app generates and emits fresh beacons: βŸ¨π‘ž0 , 𝑛𝑒𝑀(π‘₯), π‘ž1 ⟩, the user app generates a fresh identifier and stores it in the local variable π‘₯; βŸ¨π‘ž1 , π‘Žπ‘‘π‘‘(π‘₯, π‘œπ‘’π‘‘), π‘ž2 ⟩, in π‘ž1 the fresh identifier stored in π‘₯ is added to the local memory π‘œπ‘’π‘‘; βŸ¨π‘ž2 , π‘π‘π‘Žπ‘ π‘‘(𝑏, π‘₯), π‘ž2 ⟩, βŸ¨π‘ž2 , π‘™π‘œπ‘π‘Žπ‘™, π‘ž0 ⟩, in π‘ž2 the user app either emits the message (𝑏, π‘₯) or returns to the initial state in order to apply a rotation scheme for the beacon identifiers or perform other steps. In reception mode the app, while in any state 𝑙0 ∈ 𝑄 βˆ– {π‘Ÿ1 , 𝑠2 }, receives a beacon, stores it in the local memory 𝑖𝑛, and then returns to the current state: βŸ¨π‘™0 , π‘Ÿπ‘’π‘(𝑏, 𝑦), 𝑙1 ⟩ in state 𝑙0 the user is always ready to receive beacons; βŸ¨π‘™1 , π‘Žπ‘‘π‘‘(𝑦, 𝑖𝑛), 𝑙0 ⟩, in state 𝑙1 the beacon is stored in the local memory 𝑖𝑛. In report mode, enabled only in state π‘Ÿ0 = π‘ž0 , the app sends its local memory π‘œπ‘’π‘‘ to the server and moves to the halt state π‘Ÿ1 : βŸ¨π‘ž0 , 𝑠𝑒𝑛𝑑(π‘š, π‘œπ‘’π‘‘), π‘Ÿ1 ⟩. In query mode, enabled only in state 𝑠0 = π‘ž0 , the user app selects a beacon 𝑧 from the local memory 𝑖𝑛, i.e., βŸ¨π‘ 0 , 𝑠𝑒𝑙(𝑖𝑛, 𝑧), 𝑠1 ⟩, sends it to the server to check whether it has been reported by another app or not. In the former case it moves to the halting state 𝑠2 , i.e, βŸ¨π‘ 1 , 𝑖𝑛(π‘š, π‘₯), 𝑠2 ⟩. In the latter case it returns to state 𝑠0 , i.e, βŸ¨π‘ 1 , π‘›π‘œπ‘‘π‘–π‘›(π‘š, π‘₯), 𝑠0 ⟩. 4. From Data Automata to Cubicle Let us now discuss how to model a protocol definition 𝑃 = βŸ¨π‘„, 𝑀, 𝑉, 𝑆, 𝑅, π‘ž0 ⟩ in Cubicle. A global configuration is a pair (𝐾, Θ), where 𝐾 is a finite multiset of process configurations and Θ corresponds to a centralized memory. The encoding if Θ is quite immediate since we can represent the global memory as a finite set of unbounded arrays π΄π‘š1 , . . . , π΄π‘šπ‘› with cells of Boolean type one for each π‘šπ‘– ∈ 𝑀 . The array π΄π‘š is such that π΄π‘š [π‘₯] = 𝑇 π‘Ÿπ‘’π‘’ if and only if π‘₯ ∈ Θ(π‘š) for each pair π‘₯, π‘š. For the encoding of 𝐾 we can proceed in several different ways. Remember that a process configuration is a triple 𝑝𝑐 = βŸ¨π‘ž, 𝛿, π›ΎβŸ©, in which π‘ž ∈ 𝑄 but is the current user state, 𝛿 is the current evaluation of first order variables; and 𝛾 is the current evaluation of second order variables. One possible encoding is defined as follows: To represent control states, we introduce an unbounded array π‘ π‘‘π‘Žπ‘‘π‘’ that associates an enumerative type associated to 𝑄 to represent the current state of each process, i.e., π‘ π‘‘π‘Žπ‘‘π‘’[𝑖] = π‘ž if process 𝑖 is in state π‘ž. To represent the current state of a first order variable 𝑣 we can introduce an unbounded array π‘£π‘Žπ‘™π‘£ such that π‘£π‘Žπ‘™π‘£ [𝑖] = 𝑑 if 𝛿(𝑣) = 𝑑 holds in 𝑝𝑐𝑖 (in process 𝑖). To represent the current state of a second order variable 𝑠 we can introduce an unbounded bidimensional array π‘£π‘Žπ‘™π‘  such that π‘£π‘Žπ‘™π‘  [𝑖, 𝑑] = 𝑇 π‘Ÿπ‘’π‘’ if and only if 𝑑 ∈ 𝛾(𝑠) holds in 𝑝𝑐𝑖 (in process 𝑖). Transition rules can then be expressed via Cubicle transition rules. In particular, to model send operation involving second order variables, we can use global operations on arrays, in which all cells of an arrays are copied into another one (whole-place operations in Petri net languages). The Cubicle verification engine is based on symbolic backward exploration. Cubicle operates over sets of existentially quantified formulas called cubes. Formulas containing universally quantified formulas (generated during the computation of predecessors) are over-approximated by existentially quantified formulas. In other words Cubicle applies monotone abstraction [8] and over-approximates predecessors via upward-closed sets of configurations. Infinite sets of unsafe states (bad configurations) are symbolically defined by using π‘’π‘›π‘ π‘Žπ‘“ 𝑒 constraints in which all variables are implicitly existentially quantified. In our case studies we are interested in checking the consistency between local and global information. More specifically, when user π‘ˆ queries the server, she/he supposed to receive a notification only in presence of at least one positive user who emitted a beacon that has been received by π‘ˆ . The server does not maintain any association between identities and beacons collected in the log. Consistency of global and local states combined with the privacy preservation property of the protocol can be tested by adding an Error state and a special rule in which we only compare local states of different users. Namely, the rule generates an error whenever there exist a user π‘ˆ in the Contact state without any positive user in the global system. If this happens the protocol does not trace physical contacts in correct way. The property is expressed by adding a global Error flag Error: bool together with the following rule: transition bad(v) requires { Contact[v] = True && forall_other u. (Pos[u] = False) } { Error := True; } To validate the considered properties, we define the following assertion that specifies bad configurations in the sense of control state reachability, unsafe () { Error = True } i.e., configurations of any size in which Error is True. Due to the presence of universally quantified conditions both in the protocol rule and in the precondition of the error rule, there is no termination guarantee on the execution of the verification task in Cubicle. Furthermore, when terminating the tool may return spurious traces as in our case study. Indeed , Cubicle, after visiting 41 cubes, detects a spurious trace of the form: start(#3, #2) -> in(#1, #2) -> end(#1, #2) -> report(#3) -> query(#1, #2) -> bad(#1) -> unsafe. The imprecision here is due to the over-approximation introduced via monotone abstraction. Preconditions with universally quantified guards are transformed into post-conditions, and thus they are not propagated through different steps of predecessor computations. Since in the correctness property of the protocol local states are put in relation via hidden data (not explicitly mentioned in control states) stored in the server memory, it seems necessary to strengthen the symbolic reasoning procedure with some form of propagation of universally quantified conditions. One solutions comes from the combination of the existentially quantified formulas used to represent sets of states in Cubicle (cubes) with other forms of constraints on the global configuration e.g. constraints inspired to counting abstraction used in Petri nets. More in detail, we enrich our assertions by adding counters that keep track of the number of users in a given state. For our purposes, we will focus only on a counter associated to the Pos flag. We now add a global variable Count whose initial state is defined as Count=0. The counter is updated in the report rule (πΆπ‘œπ‘’π‘›π‘‘ β‰₯ 0 is added to the guard and πΆπ‘œπ‘’π‘›π‘‘ := πΆπ‘œπ‘’π‘›π‘‘ + 1 is added to the body off the transition) and used as precondition in the error rule as specified below. transition bad(v) requires { Pos[v] = False && Contact[v] = True && Count = 0 } { Error := True; } The enriched assertional language combining array formulas (for expressing precise properties of individual processes and of global variables) and Presburger constraints (for expressing global constraints via the counting abstraction) is the key point in order to enforce termination and prove correctness for the desired property. When executed on the refined model, Cubicle proves the model SAFE after visiting 10 cubes and performing 138 fixpoint tests and 41 SMT solver calls. Although not yet implemented, the above mentioned strategy could be incorporated into the Cubicle algorithm for instance by associating counters to specific control states and by generating counter manipulation operations in each transition rule via a preliminary static analysis of the Cubicle specification as done in our example via human ingenuity. References [1] S. Vaudenay, Centralized or decentralized? the contact tracing dilemma, IACR Cryptol. ePrint Arch. 2020 (2020) 531. URL: https://eprint.iacr.org/2020/531. [2] G. Avitabile, V. Botta, V. Iovino, I. Visconti, Towards defeating mass surveillance and sars- cov-2: The pronto-c2 fully decentralized automatic contact tracing system, IACR Cryptol. ePrint Arch. 2020 (2020) 493. [3] P. A. Abdulla, M. F. Atig, G. Delzanno, M. Montali, A. Sangnier, On the formalization of decentralized contact tracing protocols, in: Proceedings of the 2nd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis hosted by the Bolzano Summer of Knowledge 2020 (BOSK 2020), September 25, 2020, volume 2785 of CEUR Workshop Proceedings, CEUR-WS.org, 2020, pp. 65–70. [4] S. Conchon, A. Goel, S. Krstic, A. Mebsout, F. ZaΓ―di, Cubicle: A parallel smt-based model checker for parameterized systems - tool paper, in: Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, 2012, pp. 718–724. [5] A. Mebsout, InfΓ©rence d’invariants pour le model checking de systΓ¨mes paramΓ©trΓ©s. (Invari- ants inference for model checking of parameterized systems), Ph.D. thesis, University of Paris-Sud, Orsay, France, 2014. [6] https://alt-ergo.ocamlpro.com/, 2021. [7] D. L. Dill, The murphi verification system, in: Computer Aided Verification, 8th International Conference, CAV ’96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings, volume 1102 of Lecture Notes in Computer Science, 1996, pp. 390–393. [8] P. A. Abdulla, G. Delzanno, N. B. Henda, A. Rezine, Monotonic abstraction: on efficient verification of parameterized systems, Int. J. Found. Comput. Sci. 20 (2009) 779–801. doi:10. 1142/S0129054109006887.