On the existence of cutoffs for model checking disjunctive timed networks Luca Spalazzi and Francesco Spegni DII, Università Politecnica delle Marche Abstract. Given a logical formula and a system described as the com- position of arbitrarily many copies of some process template, the param- eterized model checking problem wants to establish whether the system satisfies the formula. The focus is on the fact that the property should not depend on the actual number of participating processes. Exactly this, makes the problem equivalent to verifying an infinite state system, and thus undecidable problem in general. Several authors identified relevant sub-classes of systems or formulae to be model checked. In this work we study the parameterized model checking problem of real-time systems against real-time temporal logics. In particular we study the possibility of finding an upper bound to the size of the system, known as cutoff, ensuring that adding more partici- pants does not change the set of satisfiable formulae. A distinction exists between dynamic cutoffs, depending both on the process templates and the formula, and static cutoffs, that only consider the templates. We start by introducing disjunctive timed networks. We show they do not admit static cutoffs, in general. Then we identify a subfamily that admits static cutoff, implying that the parameterized model checking problem is decidable. 1 Motivations Many types of system are naturally described as the combination of several agents or processes cooperating in order to reach a common task (distributed algorithms, protocols, . . . ). When the number of participants is a parameter of the system, which is expected to behave correctly despite its exact value, we say that we are handling a parameterized system. The parameterized verification problem is the problem of checking whether a specification holds in a parameterized system, for any number of participants. This is known to be an undecidable problem in general, but there exists a variety of restrictions that isolate families of systems and properties whose parameter- ized model checking problem is decidable. In this work we focus on a specific subset of systems, viz. real-time systems where processes are finite state and communicate by means of transitions with disjunctive boolean guards referring to the neighbor locations . This family of systems, that we call disjunctive timed networks, is a combination of timed net- works by Abdulla et al. [2] and Emerson and Kahlon’s disjunctively guarded processes [11]. We also focus on a restriction of the parameterized verification problem via model checking of systems up to a maximum number c of participants. Such maximum number c must have the property that any system with more than c instances satisfies exactly the same logical formulae that are satisfied by systems up to c instances. If this is the case, c is called a cutoff. If the cutoff depends on both the structure of the processes and the formula, we call it dynamic, following Kaiser et al. terminology [16]. By contrast, if the cutoff only depends on the structure of the processes we call it static. Contribution. In this work we first show that the family of disjunctive timed networks does not admit static cutoffs, in the most general case. Next, we show a subset of such family that instead admits such cutoff. Roughly speaking, such subset contains timed processes that are allowed to stay in their locations as long as they wish. Finally, we determine the complexity of the parameterized model checking problem of such subset. 2 Real-time temporal logics We define iMTL, an indexed extension of real-time (linear) temporal logic MTL [9, 10]. Let us denote with T the time domain, i.e. the set of all possible time values considered by the logics, and let us consider it a dense set, i.e. T = Q≥0 . In the following AP denotes a finite set of atomic propositions. Definition 1 (Syntax of iMTL). Let {S1 , . . . , Sk } be a finite set of sorts and V a finite set of variables. Let p be an atomic proposition in AP. iMTL is the multi-sorted logic whose set of formulae is inductively defined as follows: Φ ::= ∀i : Sl . Φ | φ φ ::= > | p hii | p hSl , ai | φ ∧ φ | ¬φ | φ U∼c φ where ∼ ∈ {<, ≤, ≥, >, =}, l ∈ [1, k], a ∈ N>0 , i ∈ V , p ∈ AP and c ∈ T. Let us call the pair hSl , ai in the above grammar a concrete instance identi- fier (or just instance identifier ), while i ∈ V denotes an instance variable. Let us assume only closed formulae, where variables are all bound to a sort. The notation φ[i ← a] represents the usual replacement operation, where all free occurrences of variable i of sort Sl in the sub-formula φ are replaced by the instance identifier hSl , ai. Missing boolean operators (∨, →, . . . ) and temporal operators (G, F, W, . . . ) can be defined in the usual ways. 1 Examples. Given a sort P representing a process, and a set of propositions AP = {cs, . . .}, the familiar mutual exclusion property can be expressed with the formula ∀i : P. ∀j : P. G≥0 ¬(cs hii ∧ cs hji). The alternative formula ∀i : P. ∀j : P. G≥3 ¬(cs hii ∧ cs hji) expresses that the mutual exclusion property is ensured after a transient time of three time units. The formula ∀i : P. G≥0 (cs hii → 1 The usual “next” operator (X) does not appear, since iMTL assumes a dense time domain, thus it does not make sense to talk about a next state in time. F≤3 ¬cs hii) is an example of bounded response property; namely it states that any instance of the process must exit the critical section within three time units. In this work, executions are represented as sequences of time values together with the propositions that hold at that time. To this aim, let us call interval sequence over T any infinite sequence I = I0 I1 . . . of non-empty intervals of T with the following properties: – (adjacency) the intervals Ii = [a, b) and Ii+1 = [b, c) are adjacent, for all i ≥ 0 and a, b, c ∈ T s.t. a < b < c; – (progress) for every t ∈ T, there exists j ≥ 0 such that t ∈ Ij . Given the set of propositions AP and sorts S1 , . . . , Sk , let us call state any subset of the following set: {p hSl , ai s.t. p ∈ AP, l ∈ [1, k], a ∈ N>0 }. For instance, given a sort P representing a process and a set of propositions AP = {a, b, c}, the set {a hP, 1i , b hP, 1i , c hP, 2i} represents the state with two copies of P : in the former a and b holds, while in the latter only c holds. Let us call state sequence any infinite sequence σ = σ0 σ1 . . . of states. Finally, let us call timed state sequence a pair ρ = (σ, I) where I is an interval sequence, and σ is a state sequence. Let us write ρ(t) to denote the state σ 0 at time t, formally: given ρ = (σ, I), where σ = σ0 σ1 . . . and I = I0 I1 . . ., then σ 0 = σi if t ∈ Ii , for some i ∈ N≥0 . Let us now introduce the satisfiability relation of iMTL. Definition 2 (Satisfiability of iMTL). Assume t ∈ T and let ρ be a timed state sequence. The satisfiability relation of an iMTL formula is defined inductively on the structure of the formula itself: ρ, t |= ∀i : Sl . Φ iff ρ, t |= Φ[i ← a] for any a ∈ N>0 ρ, t |= > ρ, t |= p hSl , ai iff p hSl , ai ∈ ρ(t) ρ, t |= φ1 ∧ φ2 iff ρ, t |= φ1 and ρ, t |= φ2 ρ, t |= ¬φ1 iff ρ, t 6|= φ1 ρ, t |= φ1 U∼c φ2 iff ∃t0 > t : t0 ∼ c and ρ, t0 |= φ2 and ∀t00 ∈ [t, t0 ). ρ, t00 |= φ1 In this work we will consider also the following fragments of iMTL viz.: – iMITL. It is the restriction of iMTL to formulae where punctual intervals are not allowed (e.g. cannot use the U=c operator). – iUpp. It is an extension of the Uppaal specification language to sorted vari- ables. It can be defined as the following subset of iMTL: Φ ::= ∀i : Sl . Φ | φ φ ::= > | p hii | p hSl , ai | φ ∧ φ | ¬φ | G∼c p hii | F∼c p hii | G∼c (p hii → F∼c p hii) | G∼c p hSl , ai | F∼c p hSl , ai | G∼c (p hSl , ai → F∼c p hSl , ai) where ∼ ∈ {<, ≤, ≥, >, =}, l ∈ [1, k], a ∈ N>0 , i ∈ V , p ∈ AP, and c ∈ T. 2 2 Let us underline that usually the Uppaal specification logic is presented as a fragment of the real-time (branching time) temporal logic TCTL [7]. Nevertheless, the syntax of formulae is so limited to be expressible also as a fragment of MTL Let us denote with iMTLh iMITLh and iUpph , for h ∈ N, the subsets of the logics iMTL iMITL and iUpp, respectively, where formulae use at most h sorted variables. We also denote with iLTL (resp. iLTLh ) the subset of iMTL (resp. iMTLh ) using only universal time intervals [0, ∞). 3 Timed automata Assume a set of clock variables C. We call temporal constraints T C(C) the terms of the grammar: TC(C) ::= > | ¬ T C(C) | T C(C) ∨ T C(C) | C ∼ C | C ∼ T, where ∼ ∈ {<, ≤, >, ≥, =} is a comparison operator and T is the same dense time domain introduced in Sec. 2. Definition 3 (Timed automaton template). A timed automaton template Ul is a tuple hQl , q̂l , Cl , Γl , τl , Il i where Ql is a finite set of locations, q̂l ∈ Ql is a distinguished initial location, Cl is a finite set of clock variables, Γl is a finite set of synchronization labels, τl ⊆ Ql × T C(Cl ) × 2Cl × Γl × Ql is a finite set of transitions, Il : Ql → T C(Cl ) maps locations to temporal constraints. In the following we write |Ul | to denote the number of locations |Ql | in the template. Let us remark that the temporal constraint Il (q) for some location q will also be referred to as the invariant of location q. We call network of timed automata any finite combination of templates, and we will call timed network the family of networks of arbitrary size. Definition 4 (Network of timed automata). Assume the TA templates U1 , . . . , Uk . Let (n1 , . . . , nk ) be a tuple of positive natural numbers. Then (U1 , . . . , Uk )(n1 ,...,nk ) is a network of timed automata (NTA for short) denoting the asynchronous parallel composition of timed automata U11 k . . . k U1n1 k . . . k Uk1 k . . . k Uknk , such that Uli is the i−th disjoint copy of Ul , for each l ∈ [1, k] and i ∈ [1, nl ]. Definition 5 (Timed networks). Given any set of timed automaton templates U1 , . . . , Uk , it induces a timed network (TN for short) defined as the following family of networks of timed automata: {(U1 , . . . , Uk )(n1 ,...,nk ) : n1 , . . . , nk ∈ N>0 } Let us denote a TN with the tuple: (U1 , . . . , Uk ). The core idea of TNs with disjunctive guards is that their Γ component is a restricted (disjunctive) boolean formula allowing to look at neighbor locations before deciding to take a step. Definition 6 (Disjunctive templates). Given any template Ul , it is a dis- junctive template iff the following holds: – W Γl is a set of boolean guards of the form:  1 r 1 r h∈[1,k] ∃i : h 6= l ∨ i 6= self. qh (i) ∨ · · · ∨ qh (i) where {qh , . . . , qh } ⊆ Qh for every h ∈ [1, k] and some r ∈ N≥0 ; – Il (q̂l ) = >. We call disjunctive timed network (or DTN) a TN made of only disjunctive templates. The formal definition of NTA operational semantics is omitted for the sake of spacee. Here we informally describe the rules, well known from the theory of (safety) timed automata [8]: delay transitions cause all clock variables to increase by the same amount δ ∈ T, provided that at any point in time no process falsifies a location invariant; discrete transition causes a single process to make a move, provided that: (i) the associated disjunctive boolean guard is satisfied by the neighbors locations, (ii) the clock constraint associated to the guard is satisfied, (iii) the moving process does not falsify the location invariant after the move, (iv) if specified, some clock variables are reset. Let us define the parameterized model checking problem of DTN on top of the usual definitions of model checking NTAs. Definition 7 (NTA model checking problem). Let assume a NTA (U1 , . . . , Uk )(n1 ,...,nk ) and a iMTL formula Φ. The model checking problem (MCP for short) is defined as follows: IN : (U1 , . . . , Uk )(n1 ,...,nk ) , Φ OU T : yes or hno, xi such that the output are: – hno, xi if x is an execution in it and x, 0 6|= Φ, and – yes otherwise. Let us consider MTL, MITL, and Upp as the non-indexed restrictions of the logics presented in Section 2. Let us report known decidability of their MCP. Property 1 (Decidability of MCP). The MCP for MTL is undecidable [4]. The MCP for MITL is decidable, it has space complexity EXPSPACE-Complete [4], and thus it has time complexity in 2-EXPTIME. The MCP for Upp can be reduced to reachability in timed networks, which is decidable, it has space complexity PSPACE-complete [3], and thus it has time complexity in EXPTIME. Let us now extend the model checking problem to timed networks. Definition 8 (DTN parameterized model checking problem). Let as- sume a DTN (U1 , . . . , Uk ) and a iMTL formula Φ. Its parameterized model checking problem (PMCP) is defined as follows: IN : (U1 , . . . , Uk ), Φ OU T : yes or hno, (n1 , . . . , nk ), xi such that the output are: – hno, (n1 , . . . , nk ), xi if (U1 , . . . , Uk )(n1 ,...,nk ) is a disjunctive NTA, x is an execution in it and x, 0 6|= Φ, – yes otherwise. 4 Cutoffs We introduce blueprints to delineate the property of a tuple being a cutoff. Definition 9. (Blueprint) Let us call k-blueprint a triple (P, k, F) where k ∈ N>0 , P k is a family of systems with k templates, and F a family of temporal logic formulae. A blueprint is a pair: (P, F) = {(P, k, F) : k ∈ N>0 }. In Section 2, we have seen three families of logic formulae, namely iMTL, iMITL and iUpp. In Section 3, we have introduced a family of system templates, viz. disjunctive TNs. We will use DTNk to denote S the set of disjunctive timed networks with k templates and define DTN = k∈N>0 DTNk . In Section 5, we will introduce a sub-family of the latter. We assume the following partial ordering on tuples of natural numbers: for any natural k and tuples (a1 , . . . , ak ) and (a01 , . . . , a0k ) in Nk , we will write (a1 , . . . , ak )  (a01 , . . . , a0k ) iff ai ≤ a0i for all i ∈ [1, k]. In order to say that a tuple of positive natural numbers is a cutoff for a blueprint, we introduce a relation between tuples of natural numbers and blueprints. One may read this property also as the blueprint admits a cutoff. Definition 10. (Dynamic cutoff ) Let (P, k, F) be a k-blueprint, U ∈ P k a system template, and Φ ∈ F a formula. A dynamic cutoff is any tuple c ∈ Nk>0 : m n (∀m  c. U |= Φ) ⇔ (∀n ∈ Nk>0 . U |= Φ) Definition 11. (Dynamic cutoff relation) Let (P, k, F) be a k-blueprint. k k k Any R(P,F ) ⊆ N>0 × P × F is a dynamic cutoff relation iff c is a dynamic k cutoff w.r.t. system template U and formula Φ, for any (c, U , Φ) ∈ R(P,F ). We call this type of cutoff dynamic since it may return different values de- pending on both the system template and the formula to be verified. Definition 12. (Static cutoff ) Let (P, k, F) be a k-blueprint and U ∈ P k a system template. A static cutoff is any tuple c ∈ Nk>0 :  m n  ∀Φ ∈ F. (∀m  c. U |= Φ) ⇔ (∀n ∈ Nk>0 . U |= Φ) Definition 13. (Static cutoff relation) Let (P, k, F) be a k-blueprint. Any RPk ⊆ Nk>0 × P k is a static cutoff relation iff c is a static cutoff w.r.t. system template U , for any (c, U ) ∈ RPk . We call this second type of cutoff static since it only depends on the system template structure, thus relating the same cutoff tuple for any logical formula. Fixing a system template and a specification, it is immediate to understand that, whenever a tuple is a cutoff for them, than any bigger tuple is also a cutoff. In other words, any system template and specification either admit infinitely many cutoffs or none. The same holds for static cutoff relations on k-blueprints. Let us observe that by fixing both a system template and a formula, there always exists a tuple that is a cutoff for them: the idea is that either the spec- ification does hold for any size of the system, thus the cutoff is (1, . . . , 1), or it does not hold and thus the cutoff is the smallest system size that falsifies it. Property 2 (Dynamic cutoffs always exist). Let (P, k, F) be a k-blueprint. k Then there exists some dynamic cutoff relation R(P,F ): ∀U ∈ P k . ∀Φ ∈ F. ∃c ∈ Nk>0 . (c, U , Φ) ∈ R(P,F k ). The proof of the property above reduces the problem of finding a cutoff to the PMCP. If the PMCP is decidable, we also obtain an algorithm for computing it. Nevertheless, the cutoff obtained in this way is of little practical use for verification purposes, since usually one desires to know the cutoff to the aim of deciding the PMCP. Property 3 (Static cutoffs imply dynamic cutoffs). Let (P, k, F) be a k- blueprint and RPk ∈ Nk>0 × P k a static cutoff relation. Then, there exists a k dynamic cutoff relation R(P,F ). k The proof is immediate, since we can define R(P,F ) = {(c̄, Ū , Φ) : (c̄, Ū ) ∈ k k RP , Φ ∈ F}, for any given static cutoff relation RP . By definition of static k cutoff, it is implied that R(P,F ) is a dynamic cutoff for the blueprint. Let us underline that a cutoff relation does not require to include all tuples that are cutoffs for the given system template and formula. Notice also that any total and computable function f : P k ×F → Nk>0 (resp. f : P k → N>0 ) returning a tuple which is a dynamic (resp. static) cutoff for the input, induces a dynamic (resp. static) cutoff relation. Indeed, for every input, it is enough to take all the tuples that are greater than the returned one to have a cutoff relation. We call any such f a dynamic cutoff algorithm (resp. static cutoff algorithm). Definition 14. (Cutoff existence) We say a blueprint (P, F) admits a dy- namic cutoff iff for every k-blueprint (P, k, F) there exists a dynamic cutoff re- k lation R(P,F ) . We say it admits a static cutoff relation iff for every k-blueprint (P, k, F) there exists a static cutoff relation RPk . In the next section, we will see that the blueprint formed by disjunctive timed networks and iMTL does not admit a static cutoff. Such negative result does not imply that all the system templates in the blueprint cannot have a static cutoff for iMTL formulae. Indeed, the existence of the static cutoff can be “recovered” for a subset of system templates. Later we are going to exploit exactly this observation and we are going to introduce a sub- family of disjunctive timed networks for which a static cutoff can be computed. 5 Cutoff theorems for timed networks Let us introduce a witness disjunctive timed network and a family of formulae that can count the number of running processes in the system. start ∃i. prei t≤1 sink pre s1 s2 t≥1 t := 0 t≥1 t := 0 Fig. 1. Witness template for Theorem 1. Location pre has the invariant: I(pre) = t ≤ 1 Theorem 1. There exists a TA template U such that for every number c ∈ N>0 there exists a formula Φc ∈ iMTL with the following property: 0 (∀c0 ∈ N>0 : c0 ≤ c. (U )(c ) |= Φc ) ∧ (U )(c+1) 6|= Φc Fig. 1 shows a template P proving the above theorem, together with the following family of formulae: ∀i : P. ¬(s1 (i) U s2 (i) U . . . U s1 (i) U s2 (i)). For | {z } c alternations every value of c, the formula Φc states that it is not possible to alternate c times between states s1 and s2 . By simulating timed networks of growing sizes built with the given template, one sees that the formula is falsified only by networks of size c or more. Thus, for every candidate cutoff c, at least one formula Φc+1 holds for networks up to size c and is falsified by bigger networks. This implies that every mapping f : DTN → Nk>0 , for any k ∈ N>0 , cannot be a static cutoff algorithm. Lemma 1. Let k, h ∈ N>0 . Let (DTN, k, iMTL) be any k-blueprint. Let f be any function such that f : DTNk → Nk>0 . Then f is not a static cutoff algorithm for the k-blueprint. This lemma is proven by contradiction, exploiting Thm. 1. Let us now in- troduce DTN− as the subfamily of DTN such that every TA template U = hQ, q̂, C, Γ, τ, Ii satisfies the following property: for every location q ∈ Q, either I(q) = > or location q cannot appear in the transition guards of any template. Later we show that blueprint (DTN− , iMTL) admits static cutoffs. Let us fix a family of static cutoff algorithm for DTN’s, inspired by the algo- rithm used by Emerson and Kahlon to prove the cutoff theorems for disjunctive k processes [11]. The algorithm is the total mapping: dchk : DTN− → Nk>0 such that dchk ((U1 , . . . , Uk )) = (c1 , . . . , ck ) and for every l ∈ [1, k], cl = |Ul | + h. Such total mappings return cutoffs which are basically given by the number of process locations augmented by a constant factor h. We introduce two properties of DTN− : the former shows that adding in- stances does not cause to loose counterexamples, while the latter shows that for any counterexample found in systems bigger than the cutoff it is possible to find a similar counterexample in the system with as many instances as the cutoff. Together they imply that a property holds in the system whose size equals the cutoff if and only if it holds in any bigger instance. Lemma 2 (DTN− monotonicity). For any k, h ∈ N>0 , let Φ be any iMTLh formula, let (U1 , . . . , Uk )(n1 ,...,nk ) and (U1 , . . . , Uk )(m1 ,...,mk ) be two NTAs in DTN− , such that (n1 , . . . , nk )  (m1 , . . . , mk ). Then the following holds: (U1 , . . . , Uk )(n1 ,...,nk ) 6|= Φ ⇒ (U1 , . . . , Uk )(m1 ,...,mk ) 6|= Φ The proof is immediate: it is enough to leave the ml − nl added instances of template l in the initial state, and replay in the “big” system the counterexample of the “small” system. Lemma 3 (DTN− bounding). For any k, h ∈ N>0 , let Φ be any iMTLh formula, let (U1 , . . . , Uk )(n1 ,...,nk ) and (U1 , . . . , Uk )(c1 ,...,ck ) be two NTAs in DTN− such that (c1 , . . . , ck ) = dchk ((U1 , . . . , Uk )) and (c1 , . . . , ck )  (n1 , . . . , nk ). Then the following holds: (U1 , . . . , Uk )(n1 ,...,nk ) 6|= Φ ⇒ (U1 , . . . , Uk )(c1 ,...,ck ) 6|= Φ Intuitively, we have to prove any counterexample in a “big” system has a core of processes whose behavior can be replicated exactly in a system whose size equals the cutoff. Given the falsified formula Φ with j sorted variables, the core of the counterexample is made of j processes that falsify the formula Φ itself. We call them core processes. In the proof we use |Ui | additional processes for each template i ∈ [1, k] to enable the moves of the core processes. We call the latter enabling processes. One key observation is that any step of the computation is enabled by checking that some process of template i is in some location q. The second key observation is that working with disjunctive guards of the family DTN− , a process is never “forced” to leave its current location. This is the key feature that is not available, in general, in DTN processes. The latter, in fact, may have invariants that force a process to leave its current state. Given these assumptions, the core processes can replay (modulo some stuttering) the steps taken in the “big” system to falsify the formula Φ. Lemmata 2 and 3 imply the following results. Lemma 4 (DTN− cutoff ). For any k, h ∈ N>0 , let Φ be any iMTLh formula, let (U1 , . . . , Uk )(n1 ,...,nk ) and (U1 , . . . , Uk )(c1 ,...,ck ) be two NTAs in DTN− such that (c1 , . . . , ck ) = dchk ((U1 , . . . , Uk )) and (c1 , . . . , ck )  (n1 , . . . , nk ). Then the following holds: (U1 , . . . , Uk )(n1 ,...,nk ) |= Φ ⇔ (U1 , . . . , Uk )(c1 ,...,ck ) |= Φ Corollary 1 (Cutoff existence for (DTN− , iMTL)). The blueprint (DTN− , iMTL) admits a static cutoff relation. 6 Complexity of PMCP for timed networks The undecidability of the MCP for timed automata against MTL specifications (see Property 1) yields the following. Corollary 2. For any k, h ∈ N>0 , the parameterized model checking problems of k-blueprints (DTN, k, iMTLh ) are undecidable. Let us now lift complexity of MCP for timed automata and sub-families of iMTL to the PMCP of DTN− . Lemma 5. Assume a k-blueprint (P, k, F) and a template cutoff algorithm f : P k → Nk>0 . Call O(TIMEMCP (n)) the upper bound on time computational com- plexity of the model checking problem with system of size n. Similarly, call O(SPACEMCP (n)) the upper bound on the space complexity of the same problem. The PMCP of (U1 , . . . , Uk ) and formula Φ has the following complexities: – O(SPACEMCP (Uk·cU )), – (cU )k · O(TIMEMCP (Uk·cU )) where U = max{|U1 |, . . . , |Uk |}, (c1 , . . . , ck ) = f (U1 , . . . , Uk ), and cU = max{c1 , . . . , ck }. Lemma 5 together with Property 1 yield the following. Theorem 2. The parameterized model checking problem of blueprint (DTN− , iMITL) has space complexity 2-EXPSPACE, and time complexity in 3-EXPTIME. Theorem 3. The parameterized model checking problem of blueprint (DTN− , iUpp) has space complexity EXPSPACE, and time complexity in 2-EXPTIME. 7 Conclusions and related work In this work we studied different types of cutoffs to the aim of verifying proper- ties on timed networks of arbitrary size. We discovered an interesting boundary between systems that only admit dynamic cutoffs w.r.t. those that can admit static cutoffs. Here we share the questions that motivated our research, as a suggestions for future works on this direction. Given a blueprint, one may ask: RQ1 Does a dynamic cutoff relation exist that does not assume the decidability of the corresponding parameterized model checking problem? RQ2 Does a static cutoff relation exist? RQ3 Does a cutoff algorithm return the smallest possible cutoff, for the blueprint and specification in input? RQ4 Is the PMCP of a blueprint with unknown cutoff decidable? It is remarkable that, to the best of our knowledge, almost all cutoff results in literature consists of finding static cutoffs, i.e. answering RQ2. For instance, Emerson et al. [11–13] present examples of static cutoffs for (untimed) processes communicating via token passing and arranged in rings, or communicating via either conjunctive or disjunctive boolean guards and arranged in cliques. Aminof et al. [5] generalize Emerson template cutoff algorithms to a wider set of pro- cess topologies. The latter also showed that the blueprint composed of pairwise Static cutoff exists (CG, iLTL) (DG, iLTL) (CTN, iMITL) (CTN, iMTL) (DTN− , iMITL) (DTN− , iMTL) (CTN, iUpp) (DTN− , iUpp) (PR, iCTL? ) does not exist Static cutoff (DG, iCTL? ) (BR, iLTL) (PR, iLTL) (PRTN, iMITL) (DTN, iMTL) (DTN, iMITL) (DTN, iUpp) PMCP decidable PMCP undecidable Fig. 2. Compare decidability of PMCP vs. existence of static cutoffs. rendez-vous processes (PR for short) and iLTLh formulae do not admit a static cutoff (even for h = 1). In contrast, in a previous work [17] we have shown that the blueprint (CTN, iMITL), i.e. conjunctive timed networks and iMITL specifi- cations, admits static cutoffs and its PMCP is decidable. A notable exception is Kaiser et al. [16], that addressed RQ1, showing that dynamic cutoffs exist for the blueprint formed by finite state programs with shared variables and reachability properties. We provided a negative answer to RQ2 for the blueprint (DTN, iMITL) and a positive answer for (DTN− , iMITL). To the best of our knowledge, it is still an open question whether there exist other blueprints that answer negatively to RQ2. It is also open RQ1 for PR and DTN. While RQ4 is answered positively for (PR, iLTL) [15], it is still open for (DTN, iMITL). We underline that even blueprints admitting static cutoffs are worth investi- gating for existence of dynamic cutoffs considering the verified specification. It may lead to obtaining smaller cutoffs, thus reducing the number of invocations of the model checker, and perhaps reducing the complexity of the PMCP. Figure 2 contains an overview of several blueprints, describing either timed or untimed systems. In it we compare whether each blueprint admits static cutoffs and whether its PMCP is decidable. The blueprints crossing the decidability line denote the fact that RQ4 has not been set. Blueprints (CG, iLTL) and (DG, iLTL) denote untimed systems with conjunctive and disjunctive guards, respectively, and the existence of static cutoffs for them have been proven by Emerson and Kahlon [11]. Non existence of static cutoffs for pairwise-rendezvous systems, i.e. (PR, iLTL), as well as undecidability of PMCP for (PR, iCTL? ) and (DG, iCTL? ) have been proved by Aminof et al. [5]. Decidability of PMCP for (PR, iLTL) have been proved by German and Sistla [15]. The system template PRTN rep- resents an alternative definition of timed networks synchronizing via pairwise rendezvous, introduced by Abdulla et al. who also proved the undecidability of their PMCP for logics capable of expressing liveness specifications [1, 2]. The system template BR represents networks of untimed processes communicating via broadcast, whose undecidability of PMCP for liveness specifications have been proven by Esparza et al. [14]. All the other results in the Figure have been proven in the current work. The PMCP of several other blueprints have been proven decidable or undecidable in literature, but are not represented in the Fig- ure for the sake of conciseness. We leave as future work to determine whether the computed cutoffs for DTN− are the minimal static cutoffs (RQ3), by appealing at existing approaches for untimed systems [5, 6]. References 1. Abdulla, P., Deneux, J., Mahata, P.: Multi-clock timed networks. In: Logic in Computer Science, 2004. Proceedings of the 19th Annual IEEE Symposium on. pp. 345–354 (July 2004) 2. Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theoretical Computer Science 290(1), 241–264 (Jan 2003) 3. Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (Apr 1994) 4. Alur, R., Feder, T., Henzinger, T.: The benefits of relaxing punctuality. Journal of the ACM (JACM) (1996) 5. Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized Model Checking of Rendezvous Systems. In: CONCUR 2014, pp. 109–124. Springer (2014) 6. Außerlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. In: VMCAI, Proceedings. pp. 476–494 (2016) 7. Behrmann, G., David, A., Larsen, K.: A tutorial on UPPAAL. In: Formal methods for the design of real-time systems, pp. 33–35. No. November, Springer (2004) 8. Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. Tech. Rep. 316 (2004) 9. Bouyer, P.: Model-checking timed temporal logics. Electronic Notes in Theoretical Computer Science 231, 323–341 (2009) 10. Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Information and Computation 208(2), 97–116 (Feb 2010) 11. Emerson, A.E., Kahlon, V.: Reducing model checking of the many to the few. Automated Deduction-CADE-17 pp. 236–254 (2000) 12. Emerson, A.E., Trefler, R.J., Wahl, T.: Reducing Model Checking of the Few to the One pp. 94–113 (2006) 13. Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527–550 (2003) 14. Esparza, J., Finkel, a., Mayr, R.: On the verification of broadcast protocols. Pro- ceedings. 14th Symposium on Logic in Comp. Sci. (July) (1999) 15. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992) 16. Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: CAV, Proceedings. pp. 645–659. Springer (2010) 17. Spalazzi, L., Spegni, F.: Parameterized Model-Checking of Timed Systems with Conjunctive Guards. In: Verified Software: Theories, Tools and Experiments, pp. 235–251. Springer (2014)