Given a logical formula and a system described as the composition of arbitrarily many copies of some process template, the parameterized model checking problem wants to establish whether the system satis es 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 in nite state system, and thus undecidable problem in general. Several authors identi ed 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 nding an upper bound to the size of the system, known as cuto , ensuring that adding more participants does not change the set of satis able formulae. A distinction exists between dynamic cuto s, depending both on the process templates and the formula, and static cuto s, that only consider the templates. We start by introducing disjunctive timed networks. We show they do not admit static cuto s, in general. Then we identify a subfamily that admits static cuto , implying that the parameterized model checking problem is decidable.
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 veri cation problem is the problem of checking whether a speci cation 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 parameterized model checking problem is decidable.
In this work we focus on a speci c subset of systems, viz. real-time systems
where processes are nite 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
networks by Abdulla et al. [
We also focus on a restriction of the parameterized veri cation 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 satis es exactly the same logical formulae that are satis ed by systems
up to c instances. If this is the case, c is called a cuto . If the cuto depends
on both the structure of the processes and the formula, we call it dynamic,
following Kaiser et al. terminology [
Contribution. In this work we rst show that the family of disjunctive timed networks does not admit static cuto s, in the most general case. Next, we show a subset of such family that instead admits such cuto . 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
We de ne iMTL, an indexed extension of real-time (linear) temporal logic MTL
[
De nition 1 (Syntax of iMTL). Let fS1; : : : ; Skg be a nite set of sorts and V a nite set of variables. Let p be an atomic proposition in AP. iMTL is the multi-sorted logic whose set of formulae is inductively de ned as follows: ::= 8i : Sl: j ::= > j p hii j p hSl; ai j ^ j : j
U c where
2 f<; ; ; >; =g, l 2 [1; k], a 2 N>0, i 2 V , p 2 AP and c 2 T.
Let us call the pair hSl; ai in the above grammar a concrete instance identier (or just instance identi er ), while i 2 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 identi er hSl; ai. Missing boolean operators (_; !; : : : ) and temporal operators (G; F; W; : : : ) can be de ned in the usual ways. 1
Examples. Given a sort P representing a process, and a set of propositions AP = fcs; : : :g, the familiar mutual exclusion property can be expressed with the formula 8i : P: 8j : P: G 0:(cs hii ^ cs hji). The alternative formula 8i : P: 8j : 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 8i : 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 in nite sequence I = I0I1 : : : 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 2 T s.t. a < b < c; { (progress) for every t 2 T, there exists j 0 such that t 2 Ij . Given the set of propositions AP and sorts S1; : : : ; Sk, let us call state any subset of the following set: fp hSl; ai s:t: p 2 AP; l 2 [1; k]; a 2 N>0g. For instance, given a sort P representing a process and a set of propositions AP = fa; b; cg, the set fa hP; 1i ; b hP; 1i ; c hP; 2ig 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 in nite 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 = I0I1 : : :, then 0 = i if t 2 Ii, for some i 2 N 0. Let us now introduce the satis ability relation of iMTL.
Assume t 2 T and let be a timed state sequence. The satis ability relation of an iMTL formula is de ned inductively on the structure of the formula itself: ; t j= 8i : Sl: i ; t j= > ; t j= p hSl; ai i ; t j= 1 ^ 2 i ; t j= : 1 i ; t j= 1 U c 2 i ; t j= [i
a] for any a 2 N>0 p hSl; ai 2 (t) ; t j= 1 and ; t j= 2 ; t 6j= 1 9t0 > t : t0 c and ; t0 j= 8t00 2 [t; t0): ; t00 j= 2 and 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 speci cation language to sorted variables. It can be de ned as the following subset of iMTL: ::= 8i : Sl: j ::= > j p hii j p hSl; ai j ^ j : j
G cp hii j F cp hii j G c(p hii ! F cp hii) j
G cp hSl; ai j F cp hSl; ai j G c(p hSl; ai ! F cp hSl; ai) where
2 f<; ; ; >; =g, l 2 [1; k], a 2 N>0, i 2 V , p 2 AP, and c 2 T. 2
2 Let us underline that usually the Uppaal speci cation logic is presented as a fragment
of the real-time (branching time) temporal logic TCTL [
Assume a set of clock variables C. We call temporal constraints T C(C) the terms of the grammar: TC(C) ::= > j : T C(C) j T C(C) _ T C(C) j C C j C T, where 2 f<; ; >; ; =g is a comparison operator and T is the same dense time domain introduced in Sec. 2.
Ul is a tuple hQl; q^l; Cl; l; l; Ili where Ql is a nite set of locations, q^l 2 Ql is a distinguished initial location, Cl is a nite set of clock variables, l is a nite set of synchronization labels, l Ql T C(Cl) 2Cl l Ql is a nite set of transitions, Il : Ql ! T C(Cl) maps locations to temporal constraints. In the following we write jUlj to denote the number of locations jQlj 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 nite combination of templates, and we will call timed network the family of networks of arbitrary size.
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 2 [1; k] and i 2 [1; nl]. De nition 5 (Timed networks). Given any set of timed automaton templates U1; : : : ; Uk, it induces a timed network (TN for short) de ned as the following family of networks of timed automata:
f(U1; : : : ; Uk)(n1;:::;nk) : n1; : : : ; nk 2 N>0g 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.
junctive template i the following holds: { l is a set of boolean guards of the form:
Wh2[1;k] 9i : h 6= l _ i 6= self: qh1(i) _ for every h 2 [1; k] and some r 2 N 0; { Il(q^l) = >. _ qhr(i) where fqh1; : : : ; qhrg
We call disjunctive timed network (or DTN) a TN made of only disjunctive
templates. The formal de nition 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 [
Let us de ne the parameterized model checking problem of DTN on top of the usual de nitions of model checking NTAs.
: : : ; Uk)(n1;:::;nk) and a iMTL formula . The model checking problem (MCP for short) is de ned 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 6j= , 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 [
Let us now extend the model checking problem to timed networks.
sume a DTN (U1; : : : ; Uk) and a iMTL formula . Its parameterized model checking problem (PMCP) is de ned 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 6j= , { yes otherwise.
We introduce blueprints to delineate the property of a tuple being a cuto .
N>0, Pk is a family of systems with k templates, and F a family of temporal logic formulae. A blueprint is a pair: (P; F ) = f(P; k; F ) : k 2 N>0g.
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 the set of disjunctive timed networks with k templates and de ne DTN = Sk2N>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) i ai a0i for all i 2 [1; k].
In order to say that a tuple of positive natural numbers is a cuto 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 cuto . De nition 10. (Dynamic cuto ) Let (P; k; F ) be a k-blueprint, U 2 Pk a system template, and 2 F a formula. A dynamic cuto is any tuple c 2 Nk>0: (8m c: U m j= ) , (8n 2 Nk>0: U n j= )
Any R(Pk;F) Nk>0 Pk F is a dynamic cuto relation i c is a dynamic cuto w.r.t. system template U and formula , for any (c; U ; ) 2 R(Pk;F).
We call this type of cuto dynamic since it may return di erent values depending on both the system template and the formula to be veri ed. De nition 12. (Static cuto ) Let (P; k; F ) be a k-blueprint and U 2 Pk a system template. A static cuto is any tuple c 2 Nk>0: 8 2 F : (8m c: U m j= ) , (8n 2 Nk>0: U n j= )
RPk Nk>0 Pk is a static cuto template U , for any (c; U ) 2 R k.
P relation) Let (P; k; F ) be a k-blueprint. Any
relation i c is a static cuto w.r.t. system
We call this second type of cuto static since it only depends on the system template structure, thus relating the same cuto tuple for any logical formula.
Fixing a system template and a speci cation, it is immediate to understand that, whenever a tuple is a cuto for them, than any bigger tuple is also a cuto . In other words, any system template and speci cation either admit in nitely many cuto s or none. The same holds for static cuto relations on k-blueprints.
Let us observe that by xing both a system template and a formula, there always exists a tuple that is a cuto for them: the idea is that either the speci cation does hold for any size of the system, thus the cuto is (1; : : : ; 1), or it does not hold and thus the cuto is the smallest system size that falsi es it.
Then there exists some dynamic cuto relation R k (P;F): 8U 2 Pk: 8
2 F : 9c 2 Nk>0: (c; U ; ) 2 R(Pk;F):
The proof of the property above reduces the problem of nding a cuto to the PMCP. If the PMCP is decidable, we also obtain an algorithm for computing it. Nevertheless, the cuto obtained in this way is of little practical use for veri cation purposes, since usually one desires to know the cuto to the aim of deciding the PMCP.
blueprint and RPk 2 Nk>0 Pk a static cuto relation. Then, there exists a dynamic cuto relation R k
(P;F).
The proof is immediate, since we can de ne R k (P;F) = f(c; U ; ) : (c; U ) 2 cRuPtko; , i2t isFigm, pfoliredanthyatgiRve(nPk;Fst)aitsica cduytnoamrieclactuioton RfoPkr.thBeybdlueepnriitniot.n of static
Let us underline that a cuto relation does not require to include all tuples that are cuto s for the given system template and formula. Notice also that any total and computable function f : Pk F ! Nk>0 (resp. f : Pk ! N>0) returning a tuple which is a dynamic (resp. static) cuto for the input, induces a dynamic (resp. static) cuto relation. Indeed, for every input, it is enough to take all the tuples that are greater than the returned one to have a cuto relation. We call any such f a dynamic cuto algorithm (resp. static cuto algorithm).
namic cuto i for every k-blueprint (P; k; F ) there exists a dynamic cuto relation R k
(P;F). We say it admits a static cuto relation i for every k-blueprint (P; k; F ) there exists a static cuto relation R k.
P
In the next section, we will see that the blueprint formed by disjunctive timed networks and iMTL does not admit a static cuto .
Such negative result does not imply that all the system templates in the blueprint cannot have a static cuto for iMTL formulae. Indeed, the existence of the static cuto 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 subfamily of disjunctive timed networks for which a static cuto can be computed. 5
Let us introduce a witness disjunctive timed network and a family of formulae that can count the number of running processes in the system.
sink t 1 pre t := 0 start s1 9i: prei t 1 Theorem 1. There exists a TA template U such that for every number c 2 N>0 there exists a formula c 2 iMTL with the following property:
Lemma 1. Let k; h 2 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 cuto algorithm for the k-blueprint.
This lemma is proven by contradiction, exploiting Thm. 1. Let us now introduce DTN as the subfamily of DTN such that every TA template U = hQ; q^; C; ; ; Ii satis es the following property: for every location q 2 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 cuto s.
Let us x a family of static cuto algorithm for DTN's, inspired by the
algorithm used by Emerson and Kahlon to prove the cuto theorems for disjunctive
processes [
Such total mappings return cuto s 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 instances does not cause to loose counterexamples, while the latter shows that for any counterexample found in systems bigger than the cuto it is possible to nd a similar counterexample in the system with as many instances as the cuto . Together they imply that a property holds in the system whose size equals the cuto if and only if it holds in any bigger instance.
For any k; h 2 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) 6j=
) (U1; : : : ; Uk)(m1;:::;mk) 6j=
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.
For any k; h 2 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) = dckh((U1; : : : ; Uk)) and (c1; : : : ; ck) (n1; : : : ; nk). Then the following holds: (U1; : : : ; Uk)(n1;:::;nk) 6j=
) (U1; : : : ; Uk)(c1;:::;ck) 6j=
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 cuto . Given the falsi ed 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 jUij additional processes for each template i 2 [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.
For any k; h 2 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) = dckh((U1; : : : ; Uk)) and (c1; : : : ; ck) (n1; : : : ; nk). Then the following holds: (U1; : : : ; Uk)(n1;:::;nk) j=
, (U1; : : : ; Uk)(c1;:::;ck) j=
(DTN ; iMTL) admits a static cuto relation. 6
The undecidability of the MCP for timed automata against MTL speci cations (see Property 1) yields the following.
Corollary 2. For any k; h 2 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 cuto algorithm f : Pk ! Nk>0. Call O(TIMEMCP(n)) the upper bound on time computational complexity 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 = maxfjU1j; : : : ; jUkjg, (c1; : : : ; ck) = f (U1; : : : ; Uk), and cU = maxfc1; : : : ; ckg.
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
In this work we studied di erent types of cuto s to the aim of verifying properties on timed networks of arbitrary size. We discovered an interesting boundary between systems that only admit dynamic cuto s w.r.t. those that can admit static cuto s. 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 cuto relation exist that does not assume the decidability of the corresponding parameterized model checking problem? RQ2 Does a static cuto relation exist? RQ3 Does a cuto algorithm return the smallest possible cuto , for the blueprint and speci cation in input? RQ4 Is the PMCP of a blueprint with unknown cuto decidable?
It is remarkable that, to the best of our knowledge, almost all cuto results
in literature consists of nding static cuto s, i.e. answering RQ2. For instance,
Emerson et al. [11{13] present examples of static cuto s 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. [
PMCP undecidable
rendez-vous processes (PR for short) and iLTLh formulae do not admit a static
cuto (even for h = 1). In contrast, in a previous work [
A notable exception is Kaiser et al. [
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) [
We underline that even blueprints admitting static cuto s are worth investigating for existence of dynamic cuto s considering the veri ed speci cation. It may lead to obtaining smaller cuto s, 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 cuto s
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 cuto s for them have been proven by Emerson and
Kahlon [