key: cord-0059581-ot3l235y
authors: Bendík, Jaroslav; Sencan, Ahmet; Gol, Ebru Aydin; Černá, Ivana
title: Timed Automata Relaxation for Reachability
date: 2021-03-01
journal: Tools and Algorithms for the Construction and Analysis of Systems
DOI: 10.1007/978-3-030-72016-2_16
sha: a5aacf665fd04c9ff1fe31face7a1841884b0c32
doc_id: 59581
cord_uid: ot3l235y

Timed automata (TA) have shown to be a suitable formalism for modeling real-time systems. Moreover, modern model-checking tools allow a designer to check whether a TA complies with the system specification. However, the exact timing constraints of the system are often uncertain during the design phase. Consequently, the designer is able to build a TA with a correct structure, however, the timing constraints need to be tuned to make the TA comply with the specification. In this work, we assume that we are given a TA together with an existential property, such as reachability, that is not satisfied by the TA. We propose a novel concept of a minimal sufficient reduction (MSR) that allows us to identify the minimal set S of timing constraints of the TA that needs to be tuned to meet the specification. Moreover, we employ mixed-integer linear programming to actually find a tuning of S that leads to meeting the specification.

A timed automaton (TA) [4] is a finite automaton extended with a set of real-time variables, called clocks, which capture the time. The clocks enrich the semantics and the constraints on the clocks restrict the behavior of the automaton, which are particularly important in modeling time-critical systems. The examples of TA models of critical systems include scheduling of real-time systems [30, 29, 33] , medical devices [43, 38] , and rail-road crossing systems [52] .

Model-checking methods allow for verifying whether a given TA meets a given system specification. Contemporary model-checking tools, such as UPPAAL [17] or Imitator [9] , have proved to be practically applicable on various industrial case studies [17, 10, 34] . Unfortunately, during the system design phase, the system information is often incomplete. A designer is often able to build a TA with correct structure, i.e., exactly capturing locations and transitions of the modeled system, however the exact clock (timing) constraints that enable/trigger the transitions are uncertain. Thus, the produced TA often does not meet the specification (i.e., it does not pass the model-checking) and it needs to be fixed. If the specification declares universal properties, e.g., safety or unavoidability, that need to hold on each trace of the TA, a model-checker either returns "yes", or it returns "no" and generates a trace along which the property is violated. This trace can be used to repair the model in an automated way [42] . However, in the case of existential properties, such as reachability, the property has to hold on a trace of the TA. The model-checker either returns "yes" and generates a witness trace satisfying the property, or returns just "no" and does not provide any additional information that would help the designer to correct the TA. Contribution. In this paper, we study the following problem: given a timed automaton A and a reachability property that is not satisfied by A, relax clock constraints of A such that the resultant automaton A 1 satisfies the reachability property. Moreover, the goal is to minimize the number of the relaxed clock constraints and, secondary, also to minimize the overall change of the timing constants used in the clock constraints. We propose a two step solution for this problem. In the first step, we identify a minimal sufficient reduction (MSR) of A, i.e., an automaton A 2 that satisfies the reachability property and originates from A by removing only a minimal necessary set of clock constraints. In the second step, instead of completely removing the clock constraints, we employ mixed integer linear programming (MILP) to find a minimal relaxation of the constraints that leads to a satisfaction of the reachability property along a witness path.

The underlying assumption is that during the design the most suitable timing constants reflecting the system properties are defined. Thus, our goal is to generate a TA satisfying the reachability property by changing a minimum number of timing constants. Some of the constraints of the initial TA can be strict (no relaxation is possible), which can easily be integrated to the proposed solution. Thus, the proposed method can be viewed as a way to handle design uncertainties: develop a TA A in a best-effort basis and apply our algorithm to find a A 1 that is as close as possible to A and satisfies the given reachability property. Related Work. Another way to handle uncertainties about timing constants is to build a parametric timed automaton (PTA), i.e., a TA where clock constants can be represented with parameters. Subsequently, a parameter synthesis tool, such as [46, 9, 26] , can be used to find suitable values of the parameters for which the resultant TA satisfies the specification. However, most of the parameter synthesis problems are undecidable [6] . While symbolic algorithms without termination guarantees exist for some subclasses [25, 39, 12] , these algorithms are computationally very expensive compared to model checking (see [5] ). Moreover, minimizing the number of modified clock constraints is not straightforward.

A related TA repair problem has been studied in a recent work [7] , where the authors also assumed that some of the constraints are incorrect. To repair the TA, they parametrized the initial TA and generated parameters by analyzing traces of the TA. However, the authors [7] do not focus on repairing the TA w.r.t. reachability properties as we do. Instead, their goal is to make the TA compliant with an oracle that decides if a trace of the TA belongs to a system or not. Thus, their approach cannot handle reachability properties. Furthermore in [7] , the total change of the timing constraints is minimized, while we primarily minimize the number of changed constraints, then the total change. x :" 0, z :" 0 e1 x ě 9 e2 z ě 3 y :" 0 e3 z :" 0 e4 u ě 22^z ě 9

z :" 0 z ě 9^x ě 25 e5 t ď 45ê 6 x ě 9 x :" 0, y :" 0 e7 x ě 9^z ď 15

x :" 0, z :" 0 e8 x ě 9^u ě 35

x :" 0, u :" 0

ig. 1. An example of a timed automaton.

A timed automaton (TA) [3, 4, 44] is a finite-state machine extended with a finite set C of real-valued clocks. A clock x P C measures the time spent after its last reset. In a TA, clock constraints are defined for locations (states) and transitions.

A simple clock constraint is defined as x´y " c where x, y P C Yt0u, " P tă, ďu and c P ZYt8u. 3 Simple clock constraints and constraints obtained by combining these with conjunction operator (^) are called clock constraints. The sets of simple and all clock constraints are denoted by Φ S pCq and ΦpCq, respectively. For a clock constraint φ P ΦpCq, Spφq denotes the simple constraints from φ, e.g., Spx´y ă 10^y ď 20q " tx´y ă 10, y ď 20u. A clock valuation v : C Ñ Rà ssigns non-negative real values to each clock. The notation v |ù φ denotes that the clock constraint φ evaluates to true when each clock x is replaced with vpxq. For a clock valuation v and d P R`, v`d is the clock valuation obtained by delaying each clock by d, i.e., pv`dqpxq " vpxq`d for each x P C. For λ Ď C, vrλ :" 0s is the clock valuation obtained after resetting each clock from λ, i.e., vrλ :" 0spxq " 0 for each x P λ and vrλ :" 0spxq " vpxq for each x P Czλ.

A timed automaton A " pL, l 0 , C, Δ, Inv q is a tuple, where L is a finite set of locations, l 0 P L is the initial location, C is a finite set of clocks, Δ Ď Lˆ2 CˆΦ pCqˆL is a finite transition relation, and Inv : L Ñ ΦpCq is an invariant function.

For a transition e " pl s , λ, φ, l t q P Δ, l s is the source location, l t is the target location, λ is the set of clocks reset on e and φ is the guard (i.e., a clock constraint) tested for enabling e. The semantics of a TA is given by a labelled transition system (LTS). An LTS is a tuple T " pS, s 0 , Σ, Ñq, where S is a set of states, s 0 P S is an initial state, Σ is a set of symbols, and Ñ Ď SˆΣˆS is a transition relation. A transition ps, a, s 1 q P Ñ is also shown as s a Ñ s 1 .

Given a TA A " pL, l 0 , C, Δ, Inv q, the labelled transition system T pAq " pS, s 0 , Σ, Ñq is defined as follows: 1 , v 1 q if there exists pl, λ, φ, l 1 q P Δ such that v |ù φ, v 1 " vrλ :" 0s, and v 1 |ù Inv pl 1 q.

The notation sÑ d s 1 is used to denote a delay transition of duration d followed by a discrete transition from s to s 1 , i.e., s d Ñ s act Ñ s 1 . A run ρ of A is either a finite or an infinite alternating sequence of delay and discrete transitions, i.e., ρ " s 0 Ñ d0 s 1 Ñ d1 s 2 Ñ d2¨¨¨. The set of all runs of A is denoted by rrAss.

A path π of A is an interleaving sequence of locations and transitions, π " l 0 , e 1 , l 1 , e 2 , . . ., where e i`1 " pl i , λ i`1 , φ i`1 , l i`1 q P Δ for each i ě 0. A path π " l 0 , e 1 , l 1 , e 2 , . . . is said to be realizable if there exists a delay sequence d 0 , d 1 , . . . such that pl 0 , 0qÑ d0 pl 1 , v 1 qÑ d1 pl 1 , v 2 qÑ d2¨¨¨i s a run of A and for every i ě 1, the ith discrete transition is taken according to e i , i.e., e i " pl i´1 ,

Given a TA A, a subset L T Ă L of its locations is reachable on A if there exists ρ " pl 0 , 0qÑ d0 pl 1 , v 1 qÑ d1 . . . Ñ dn´1 pl n , v n q P rrAss such that l n P L T ; otherwise, L T is unreachable. The reachability problem is decidable and implemented in various verification tools, e.g., [17, 9] . The verifier either returns "No" when the location is unreachable, or it generates a run (witness) reaching the set L T . Example 1. Figure 1 illustrates a TA with 8 locations: tl 0 , . . . , l 7 u, 9 transitions: te 1 , . . . , e 9 u, an initial location l 0 , and an unreachable set of locations L T " tl 4 u.

For a timed automaton A " pL, l 0 , C, Δ, Invq, the set of pairs of transition and associated simple constraints is defined in (1) and the set of pairs of location and associated simple constraints is defined in (2) .

Ψ pΔq " tpe, ϕq | e " pl s , λ, φ, l t q P Δ, ϕ P Spφqu (1) Ψ pInvq " tpl, ϕq | l P L, ϕ P SpInvplqqu (2) Definition 3 (constraint-relaxation). Let φ P ΦpCq be a constraint over C, Θ Ď Spφq be a subset of its simple constraints and r : Θ Ñ N Y t8u be a positive valued relaxation valuation. The relaxed constraint is defined as:

Intuitively, Rpφ, Θ, rq relaxes only the thresholds of simple constraints from Θ with respect to r, e.g., Rpx´y ď 10^y ă 20, ty ă 20u, rq " x´y ď 10ŷ ă 23, where rpy ă 20q " 3. Setting a threshold to 8 implies removing the corresponding simple constraint, e.g., Rpx´y ď 10^y ă 20, ty ă 20u, rq " x´y ď 10, where rpy ă 20q " 8. Note that Rpφ, Θ, rq " φ when Θ is empty. Definition 4 ((D, I, r)-relaxation). Let A " pL, l 0 , C, Δ, Invq be a TA, D Ď Ψ pΔq and I Ď Ψ pInvq be transition and location constraint sets, and r : D Y I Ñ N Y t8u be a positive valued relaxation valuation. The (D, I, r)-relaxation of A, denoted A ăD,I,rą , is a TA A 1 " pL 1 , l 1 0 , C 1 , Δ 1 , Inv 1 q such that:

-L " L 1 , l 0 " l 1 0 , C " C 1 , and -Δ 1 originates from Δ by relaxing D via r. For e " pl s , λ, φ, l t q P Δ, let D| e " tϕ | pe, ϕq P Du, and let r| e pϕq " rpe, ϕq, then Δ 1 " tpl s , λ, Rpφ, D| e , r| e q, l t q | e " pl s , λ, φ, l t q P Δu -Inv 1 originates from Inv by relaxing I via r. For l P L, let I| l " tϕ | pl, ϕq P Iu, and r| l pϕq " rpl, ϕq, then Inv 1 plq " RpInvplq, I| l , r| l q.

Intuitively, the TA A ăD,I,rą emerges from A by relaxing the guards of the transitions from the set D and relaxing invariants of the locations from I with respect to r. In the special case of setting the threshold of each constraint from D and I to 8, i.e., when rpaq " 8 for each a P D Y I, the corresponding simple constraints are effectively removed, which is called a (D,I)-reduction and denoted by A ăD,Ią . Note that A " A ăH,Hą . Proposition 1. Let A " pL, l 0 , C, Δ, Invq be a timed automaton, D Ď Ψ pΔq and I Ď Ψ pInvq be sets of simple guard and invariant constraints, and r : D Y I Ñ N Y t8u be a relaxation valuation. Then rrAss Ď rrA ăD,I,rą ss.

Proof. Observe that for a clock constraint φ P ΦpCq, a subset of its simple constraints Θ Ď Spφq, a relaxation valuation r 1 for Θ, and the relaxed constraint Rpφ, Θ, r 1 q as in Definition 3, it holds that for any clock valuation v : v |ù φ ùñ v |ù Rpφ, Θ, r 1 q. Now, consider a run ρ " pl 0 , 0qÑ d0 pl 1 , v 1 qÑ d1 pl 2 , v 2 qÑ d2¨¨¨P rrAss. Let π " l 0 , e 1 , l 1 , e 2 , . . . with e i " pl i´1 , λ i , φ i , l i q P Δ for each i ě 1 be the path realized as ρ via delay sequence d 0 , d 1 , . . .. By Definition 4 for each pl, λ, φ, l 1 q P Δ, there is pl, λ, Rpφ, D| e , r| e q, l 1 q P Δ 1 . We define a path induced by π on A ăD,I,rą as:

Thus M pπq is realizable on A ăD,I,rą via the same delay sequence and ρ P rrA ăD,I,rą ss. As ρ P rrAss is arbitrary, we conclude that rrAss Ď rrA ăD,I,rą ss.

Problem 1. Given a TA A " pL, l 0 , C, Δ, Invq and a set of target locations L T Ă L that is unreachable on A, find a (D, I, r)-relaxation A ăD,I,rą of A such that L T is reachable on A ăD,I,rą . Moreover, the goal is to identify a (D, I, r)-relaxation that minimizes the number |D Y I| of relaxed constraints, and, secondary, we tend to minimize the overall change of the clock constraints ř cPDYI rpcq.

We propose a two step solution to this problem. In the first step, we identify a subset D Y I of the simple constraints Ψ pΔq Y Ψ pInvq such that L T is reachable on the (D, I)-reduction A ăD,Ią and |D Y I| is minimized. Consequently, we can obtain a witness path of the reachability on A ăD,Ią from the verifier. The path would be realizable on A if we remove the constraints D Y I. In the second step, instead of completely removing the constraints D Y I, we find a relaxation valuation r : D Y I Ñ N Yt8u such that the path found in the first step is realizable on A ăD,I,rą . To find r, we introduce relaxation parameters for constraints in D Y I. Subsequently, we solve an MILP problem to find a valuation of the parameters, i.e., r, that makes the path realizable on A ăD,I,rą and minimizes ř cPDYI rpcq. Note that it might be the case that the reduction A ăD,Ią contains multiple realizable paths that lead to L T , and another path might result in a smaller overall change. Also, there might exist another candidate subset D 1 Y I 1 with |D 1 Y I 1 | " |D Y I| that would lead to a smaller overall change. While our approach can be applied to a number of paths and a number of candidate subsets D Y I, processing all of them can be practically intractable.

Throughout this section, we simply write a reduction when talking about a (D,I)reduction of A. To name a reduction, we either simply use capital letters, e.g., M, N, K, or we use the notation A ăD,Ią to also specify the sets D, I of simple clock constraints. Given a reduction N " A ăD,Ią , |N | denotes the cardinality |D Y I|. Furthermore, R A denotes the set of all reductions. We define a partial order relation Ď on R A as A ăD,Ią Ď A ăD 1 ,

We say that a reduction A ăD,Ią is a sufficient reduction (w.r.t. A and L T ) iff L T is reachable on A ăD,Ią ; otherwise, A ăD,Ią is an insufficient reduction. Crucial observation for our work is that the property of being a sufficient reduction is monotone w.r.t. the partial order: Proposition 2. Let A ăD,Ią and A ăD 1 ,I 1 ą be reductions such that A ăD,Ią Ď A ăD 1 ,I 1 ą . If A ăD,Ią is sufficient then A ăD 1 ,I 1 ą is also sufficient.

Proof. Note that A ăD 1 ,I 1 ą is a (D 1 zD,I 1 zI)-reduction of A ăD,Ią . By Proposition 1, rrA ăD,Ią ss Ď rrA ăD 1 ,I 1 ą ss, i.e., the run of A ăD,Ią that witnesses the reachability of L T is also a run of A ăD 1 ,I 1 ą .

Recall that a reduction A ăD,Ią is determined by D Ď Ψ pΔq and I Ď Ψ pInvq. Consequently, |R A | " 2 |Ψ pΔqYΨ pInvq| . Moreover, there can be up to`k k{2˘M SRs where k " |Ψ pΔq Y Ψ pInvq| (see Sperner's theorem [51]). Also note, that the minimality of a reduction does not mean a minimum number of simple clock constraints that are reduced by the reduction; there can exist two MSRs, M and N , such that |M | ă |N |. Since our overall goal is to relax A as little as possible, we identify a minimum MSR, i.e., an MSR M such that there is no MSR M 1 with |M 1 | ă |M |, and then use the minimum MSR for the MILP part (Section 4) of our overall approach. There can be also up to`k k{2˘m inimum MSRs.

Example 2. Assume the TA A and L T " tl 4 u from Example 1 (Fig. 1 ). There are 24 MSRs and 4 of them are minimum. For example, A ăD,Ią with D " tpe 5 , x ě 25qu and I " tpl 3 , u ď 26qu is a minimum MSR, and A ăD 1 ,I 1 ą with D 1 " tpe 9 , y ď 15q, pe 7 , z ď 15qu and I 1 " tpl 6 , x ď 10qu is a non-minimum MSR.

Algorithm 1 shows a high-level scheme of our approach for computing a minimum MSR. The algorithm iteratively identifies an ordered set of MSRs, |M 1 | ą |M 2 | ą¨¨ą |M k |, such that the last MSR M k is a minimum MSR. Each of the MSRs, say M i , is identified in two steps. First, the algorithm finds a seed, i.e., a reduction N i such that N i is sufficient and |N i | ă |M i´1 |. Second, the algorithm shrinks N i into an MSR M i such that M i Ď N i (and thus |M i | ď |N i |). The initial seed N 1 is A ăΨ pΔq,Ψ pInvqą , i.e., the reduction that removes all simple clock constraints (which makes all locations of A trivially reachable). Once there is no sufficient

Note that the algorithm also maintains two auxiliary sets, M and I, to store all identified MSRs and insufficient reductions, respectively. The two sets are used during the process of finding and shrinking a seed which we describe below.

Our approach for shrinking a seed N into an MSR M is based on two concepts: a critical simple clock constraint and a reduction core.

Definition 6 (critical constraint). Given a sufficient reduction A ăD,Ią , a simple clock constraint c is critical for A ăD,Ią iff A ăDztcu,Iztcuą is insufficient. Proposition 3. If c P D Y I is critical for a sufficient reduction A ăD,Ią then c is critical for every sufficient reduction A ăD 1 ,I 1 ą , A ăD 1 ,I 1 ą Ď A ăD,Ią . Moreover, by Definitions 5 and 6, A ăD,Ią is an MSR iff every c P D Y I is critical for A ăD,Ią . Proof. By contradiction, assume that c is critical for A ăD,Ią but not for A ăD 1 ,I 1 ą , i.e., A ăDztcu,Iztcuą is insufficient and A ăD 1 ztcu,I 1 ztcuą is sufficient. As A ăD 1 ,I 1 ą Ď A ăD,Ią , we have A ăD 1 ztcu,I 1 ztcuą Ď A ăDztcu,Iztcuą . By Proposition 2, if the reduction A ăD 1 ztcu,I 1 ztcuą is sufficient then A ăDztcu,Iztcuą is also sufficient.

Definition 7 (reduction core). Let A ăD,Ią be a sufficient reduction, ρ a witness run of the sufficiency (i.e., reachability of L T on A ăD,Ią ), and π the path corresponding to ρ. Futhermore, let M pπq " l 0 , e 1 , . . . , e n , l n be the path corresponding to π on the original TA A defined as in (4) . The reduction core of A ăD,Ią w.r.t. ρ is the reduction A ăD 1 ,I 1 ą where D 1 " tpe, ϕq | pe, ϕq P D^e " e i for some 1 ď i ď nu and I 1 " tpl, ϕq | pl, ϕq P I^l " l i for some 0 ď l ď nu.

Intuitively, the reduction core of A ăD,Ią w.r.t. ρ reduces from A only the simple clock constraints that appear on the witness path in A.

Let A ăD,Ią be a sufficient reduction, ρ the witness of reachability of L T on A ăD,Ią , and A ăD 1 ,I 1 ą the reduction core of A ăD,Ią w.r.t. ρ. Then A ăD 1 ,I 1 ą is a sufficient reduction and A ăD 1 ,I 1 ą Ď A ăD,Ią .

Proof. By Definition 7, D 1 Ď D and I 1 Ď I, thus A ăD 1 ,I 1 ą Ď A ăD,Ią . As for the sufficiency of A ăD 1 ,I 1 ą , we only sketch the proof. Intuitively, both A ăD,Ią and A ăD 1 ,I 1 ą originate from A by only removing some simple clock constraints (DYI, and D 1 Y I 1 , respectively), i.e., the graph structure of A ăD,Ią and A ăD 1 ,I 1 ą is the same, however, some corresponding paths of A ăD,Ią and A ăD 1 ,I 1 ą differ in the constraints that appear on the paths. By Definition 7, the path π that corresponds to the witness run ρ of A ăD,Ią is also a path of A ăD 1 ,I 1 ą . Since realizability of a path depends only on the constraints along the path, if π is realizable on A ăD,Ią then π is also realizable on A ăD 1 ,I 1 ą .

Our approach for shrinking a sufficient reduction N is shown in Algorithm 2. The algorithm iteratively maintains a sufficient reduction A ăD,Ią and a set X of known critical constraints for A ăD,Ią . Initially, A ăD,Ią " N and X " H. In each iteration, the algorithm picks a simple clock constraint c P pD Y IqzX and checks the reduction A ăDztcu,Iztcuą for sufficiency. If A ăDztcu,Iztcuą is insufficient, the algorithm adds c to X. Otherwise, if A ăDztcu,Iztcuą is sufficient, the algorithm obtains a witness run ρ of the sufficiency from the verifier and reduces A ăD,Ią to the corresponding reduction core. The algorithm terminates when pD Y Iq " X. An invariant of the algorithm is that every c P X is critical for A ăD,Ią . Thus, when pD Y Iq " X, A ăD,Ią is an MSR (Proposition 3).

Note that the algorithm also uses the set I of known insufficient reductions. In particular, before calling a verifier to check a reduction for sufficiency (line 4), the algorithm first checks (in a lazy manner) whether the reduction is already known to be insufficient. Also, whenever the algorithm determines a reduction A ăDztcu,Iztcuą to be insufficient, it adds A ăDztcu,Iztcuą and every N , N Ď A ăDztcu,Iztcuą to I (by Proposition 2, every such N is also insufficient).

We now describe the procedure findSeed. The input is the latest identified MSR M , the set M of known MSRs, and the set I of known insufficient reductions. The output is a seed, i.e., a sufficient reduction N such that |N | ă |M |, or null if there is no seed. Let us denote by CAND the set of all candidates on a seed, i.e., CAND " tN P R A | |N | ă |M |u. A brute-force approach would be to check individual reductions in CAND for sufficiency until a sufficient one is found, however, this can be practically intractable since |CAND| "

We provide three observations to prune the set CAND of candidates that need to be tested for being a seed. The first observation exploits the set I of already known insufficient reductions: no N P I can be a seed. The second observation exploits the set M of already known MSRs. By the definition of an MSR, for every M 1 P M and every N such that N Ĺ M 1 , the reduction N is necessarily insufficient and hence cannot be a seed. The third observation is stated below: Observation 1. For every sufficient reduction N P CAND there exists a sufficient reduction N 1 P CAND such that N Ď N 1 and |N 1 | " |M |´1.

Proof. If |N | " |M |´1, then N " N 1 . For the other case, when |N | ă |M |´1, let N " A ăD N ,I N ą and M " A ăD M ,I M ą . We construct N 1 " A ăD N 1 ,I N 1 ą by adding arbitrary p|M |´|N |q´1 simple clock constraint from pD

By definition of CAND, N 1 P CAND. Moreover, since N Ĺ N 1 and N is sufficient, then N 1 is also sufficient (Proposition 2). Based on the above observations, we build a set C of indispensable candidates on seeds that need to be tested for sufficiency:

The procedure findSeed, shown in Algorithm 3, in each iteration picks a reduction N P C and checks it for sufficiency (via the verifier). If N is sufficient, findSeed returns N as the seed. Otherwise, when N is insufficient, the algorithm first attempts to enlarge N into an insufficient reduction E such that N Ď E. By Proposition 2, every reduction N 1 such that N 1 Ď E is also insufficient, thus all these reductions are subsequently added to I and hence removed from C (note that this includes also N ). If C becomes empty, then there is no seed.

The purpose of enlarging N into E is to quickly prune the candidate set C. We could just add all the insufficient reductions tN 1 | N 1 Ď N u to I, but note that |tN 1 | N 1 Ď Eu| is exponentially larger than |tN 1 | N 1 Ď N u| w.r.t. |E|´|N |. The enlargement, shown in Algorithm 4, works almost dually to shrinking. Let N " A ăD,Ią . The algorithm attempts to one by one add the constraints from Ψ pΔqzD and Ψ pInvqzI to D and I, respectively, checking each emerged reduction for sufficiency, and keeping only the changes that preserve A ăD,Ią to be insufficient.

The final piece of the puzzle is how to efficiently manipulate with the sets I and C. In particular, we are adding reductions to I and C, removing reductions from C, checking if a reduction belongs to I, checking if C is empty, and picking a reduction from C. The problem is that the size these sets can be expontential w.r.t. |Ψ pΔq Y Ψ pInvq| (there are exponentially many reductions), and thus, it is practically intractable to maintain the sets explicitly. Instead, we use a symbolic representation. Given a TA A with simple clock constraints Ψ pΔq " tpe 1 , ϕ 1 q, . . . , pe p , ϕ p qu and Ψ pInvq " tpl 1 , ϕ 1 q, . . . , pl q , ϕ q qu, we introduce two sets X " tx 1 , . . . , x p u and Y " ty 1 , . . . , y q u of Boolean variables. Note that every valuation of the variables X Y Y one-to-one maps to the reduction A ăD,Ią such that pe i , ϕ i q P D iff x i is assigned True and pl j , ϕ j q P I iff y j is assigned True.

The set I is gradually built during the whole computation of Algorithm 1. To represent I, we build a Boolean formula I such that a reduction N does not belong to I iff N does correspond to a model of I. Initially, I " H, thus I " True. To add an insufficient reduction A ăD,Ią and all reductions N , N Ď A ăD,Ią , to I, we add to I the clause p Ž pei,ϕiqPΨ pΔqzD x i q_p Ž plj ,ϕj qPΨ pInvqzI y j q. The set C is repeatedly built during each call of the procedure findSeed based on Eq. 5 and it is encoded via a Boolean formula C such that every model of C does correspond to a reduction N P C :

where truesp|M|´1q is a cardinality encoding forcing that exactly |M |´1 variables from X YY are set to True. To check if C " H or to pick a reduction N P C, we ask a SAT solver for a model of C. To remove an insufficient reduction from C, we update the formula I (and thus also C) as described above.

Although the concept of minimal sufficient reductions (MSRs) is novel in the context of timed automata, similar concepts appear in other areas of computer , minimal correction subsets [47] , minimal inconsistent subsets [16, 18] , or minimal inductive validity cores [32] . All these concepts can be generalized as minimal sets over monotone predicates (MSMPs) [48, 49] . The input is a reference set R and a monotone predicate P : PpRq Ñ t1, 0u, and the goal is to find minimal subsets of R that satisfy the predicate. In the case of MSRs, the reference set is the set of all simple constraints Ψ pΔqYΨ pInvq and, for every DYI Ď Ψ pΔqYΨ pInvq, the predicate is defined as PpD Y Iq " 1 iff A ăD,Ią is sufficient. Many algorithms were proposed (e.g., [45, 14, 19, 22, 20, 47, 21, 37, 32, 23] ) for finding MSMPs for particular instances of the MSMP problem. However, the algorithms are dedicated to the particular instances and extensively exploit specific properties of the instances (such as we exploit reduction cores in case of MSRs). Consequently, the algorithms either cannot be used for finding MSRs, or they would be rather inefficient.

The main objective of this study is to make the target locations L T of a given TA A " pL, l 0 , C, Δ, Invq reachable by only modifying the constants of simple constraints of A. In the previous section, we presented an efficient algorithm to find a set of simple clock constraints D Ď Ψ pΔq (1) (over transitions) and I Ď Ψ pInvq (2) (over locations) such that the target set is reachable when constraints D and I are removed from A. In other words, L T is reachable on A ăD,Ią . Consequently, a verifier generates a finite run ρ 1 L T " pl 0 , 0qÑ d0 pl 1 , v 1 qÑ d1 . . . Ñ dn´1 pl n , v n q of A ăD,Ią such that l n P L T . Let π 1 L T " l 0 , e 1 1 , l 1 , . . . , e 1 n´1 , l n be the corresponding path on A ăD,Ią , i.e., π 1 L T is realizable on A ăD,Ią due to the delay sequence d 0 , d 1 , . . . , d n´1 and the resulting run is ρ 1 L T . The corresponding path on the original TA A defined as in (4) is:

L T " M pπ L T q, and π L T " l 0 , e 1 , l 1 , . . . , e n´1 , l n ,

While π 1 L T is realizable on A ăD,Ią , π L T is not realizable on A since L T is not reachable on A. We present an MILP based method to find a relaxation valuation r : DYI Ñ NYt8u such that the path induced by π L T is realizable on A ăD,I,rą .

Given an automaton path π " l 0 , e 1 , l 1 , . . . , e n´1 , l n with e i " pl i´1 , λ i , φ i , l i q for each i " 1, . . . , n´1, we introduce real valued delay variables δ 0 , . . . , δ n´1 that represent the time spent in each location along the path. Since clocks measure the time passed since their last resets, for a fixed path, a clock on a given constraint (invariant or guard) can be mapped to a sum of delay variables:

The value of clock x equals to Γ px, π, iq on the i-th transition e i along π. In (8), k is the index of the transition where x is last reset before e i along π, and it is 0 if it is not reset. Γ p0, π, iq is defined as 0 for notational convenience.

Guards. For transition e i , each simple constraint ϕ " x´y " c P Spφ i q on the guard φ i is mapped to the new delay variables as:

Γ px, π, iq´Γ py, π, iq " c`p ei,ϕ (9) where p ei,ϕ is a new integer valued relaxation variable if pe i , ϕq P D, otherwise it is set to 0. Invariants. Each clock constraint ϕ " x´y " c P SpInvpl i qq of the invariant of location l i is mapped to arriving (10) and leaving (11) constraints over the delay variables, since the invariant should be satisfied when arriving and leaving the location (and hence, due to the invariant convexity, also in the location).

Γ px, π, iq¨Ipx R λ i q´Γ py, π, iq¨Ipy R λ i q " c`p li,ϕi if i ą 0(arriving) (10) Γ px, π, i`1q´Γ py, π, i`1q " c`p li,ϕi (leaving) (11) where I is a binary function mapping true to 1 and false to 0, p li,ϕi is a new integer valued variable if pl i , ϕ i q P I, otherwise it is set to 0. Finally, we define an MILP (12) for the path π. The constraint relaxation variables tp l,ϕ | pl, ϕq P Iu and tp e,ϕ | pe, ϕq P Du (integer valued), and the delay variables δ 0 , . . . , δ n´1 (real valued) are the decision variables of the MILP. minimize ÿ pl,ϕqPI

subject to (9) for each i " 1, . . . , n´1, and x´y " c P Spφ i q (10) for each i " 1, . . . , n, and x´y " c P SpInvpl i qq (11) for each i " 0, . . . , n´1, and x´y " c P SpInvpl i qq p l,ϕ P Z`for each pl, ϕq P I, and p e,ϕ P Z`for each pe, ϕq P D Let tp ‹ l,ϕ | pl, ϕq P Iu, tp ‹ e,ϕ | pe, ϕq P Du, and δ ‹ 0 , . . . , δ ‹ n´1 denote the solution of MILP (12) . Define a relaxation valuation r with respect to the solution as rpl, ϕq " p ‹ l,ϕ for each pl, ϕq P I, rpe, ϕq " p ‹ e,ϕ for each pe, ϕq P D.

Theorem 1. Let A " pL, l 0 , C, Δ, Invq be a timed automaton, π " l 0 , e 1 , l 1 , . . . , e n , l n be a finite path of A, and D Ă Ψ pΔq, I Ă Ψ pIq be guard and invariant constraint sets. If the MILP constructed from A, π, D and I as defined in (12) is feasible, then l n is reachable on A ăD,I,rą with r as defined in (13) .

Proof sketch Let tp ‹ l,ϕ | pl, ϕq P Iu, tp ‹ e,ϕ | pe, ϕq P Du, and δ ‹ 0 , . . . , δ ‹ n´1 be the optimal solution of MILP (12) . Define clock value sequence v 0 , v 1 , . . . , v n with respect to the path π with e i " pl i´1 , λ i , φ i , l i q and the delay sequence δ ‹ 0 , . . . , δ ‹ n´1 iteratively as v i " 0 and v i " pv i´1`δ ‹ i´1 qrλ i :" 0s for each i " 1, . . . , n. Along the path π, v i is consistent with Γ p¨, π, iq (8) such that (14) MILP (12) constraints and (14) imply that the path M pπq that end in l n is realizable on A ăD,I,rą via the delay sequence δ ‹ 0 , . . . , δ ‹ n´1 . A linear programming (LP) based approach was used in [27] to generate the optimal delay sequence for a given path of a weighted timed automata. In our case, the optimization problem is in MILP form since we find an integer valued relaxation valuation (r) in addition to the delay variables.

Recall that we construct relaxation sets D and I via Algorithm 1, and define π L T (7) that reach L T such that the corresponding path π 1 L T is realizable on A ăD,Ią . Then, we define MILP (12) with respect to π L T , D and I, and define r (13) according to the optimal solution. Note that this MILP is always feasible since π 1 L T is realizable on A ăD,Ią . Finally, by Theorem 1, we conclude that L T is reachable on A ăD,I,rą .

Example 3. For the TA shown in Fig. 1 , Algorithm 1 generates A ăD,Ią with D " tpe 5 , x ě 25qu and I " tpl 3 , u ď 26qu such that π " l 0 , e 1 , l 1 , e 2 , l 2 , e 3 , l 1 , e 4 , l 3 , e 5 , l 4 is realizable on A ăD,Ią . The MILP is constructed for π, D and I with decision variables p e5,xě25 , p l3,uď26 , δ 0 , δ 1 , δ 2 , δ 3 , δ 4 and δ 5 as in (12) . The solution is p e5,xě25 " 3, p l3,uď26 " 5, and the delay sequence is 9, 4, 0, 9, 9, 0. Consequently, l 4 is reachable on A ăD,I,rą with rpe 5 , x ě 25q " 3 and rpl 3 , u ď 26q " 5.

We implemented the proposed reduction and relaxation methods in a tool called Tamus. We use UPPAAL for sufficiency checks and witness computation, and CBC solver from Or-tools library [50] for the MILP part. All experiments were run on a laptop with Intel i5 quad core processor at 2.5 GHz and 8 GB ram. The tool and used benchmarks are available at https://github.com/jar-ben/tamus.

As discussed in Section 1, an alternative approach to solve our problem (Problem 1) is to parameterize each simple clock constraint of the TA. Then, we can run a parameter synthesis tool on the parameterized TA to identify the set of all possible valuations of the parameters for which the TA satisfies the reachability property. Subsequently, we can choose the valuations that assign non-zero values (i.e., relax) to the minimum number of parameters, and out of these, we Table 1 . Results for the scheduler TA, where |Ψ | " |Ψ pΔq Y Ψ pIq| is the total number of constraints, d " |D Y U | is the minimum MSR size, v is the number of reachability checks, t is the computation time in seconds (including the reachability checks), and c m is the optimal cost of (12) . 12q 11 2 33 0.18 6 A p5,1,12q 16 3 120 0.63 10 A p7,1,12q 19 3 can choose the one with a minimum cumulative change of timing constants. In our experimental evaluation, we evaluate a state-of-the-art parameter synthesis tool called Imitator [9] to run such analysis. Although Imitator is not tailored for our problem, it allows us to measure the relative scalability of our approach compared to a well-established synthesis technique.

We used two collections of benchmarks: one is obtained from literature, and the other are crafted timed automata modeling a machine scheduling problem. All experiments were run using a time limit of 20 minutes per benchmark.

Machine Scheduling A scheduler automaton is composed of a set of paths from location l 0 to location l 1 . Each path π " l 0 e k l k e k`1 . . . l k`M´1 e k`M l 1 represents a particular scheduling scenario where an intermediate location, e.g. l i for i " k, . . . , k`M´1, belongs to a unique path (only one incoming and one outgoing transition). Thus, a TA that has p paths with M intermediate locations in each path has M¨p`2 locations and pM`1q¨p transitions. Each intermediate location represents a machine operation, and periodic simple clock constraints are introduced to mimic the limitations on the corresponding durations. For example, assume that the total time to use machines represented by locations l k`i and l k`i`1 is upper (or lower) bounded by c for i " 0, 2, . . . , M´2. To capture such a constraint with a period of t " 2, a new clock x is introduced and it is reset and checked on every t th transition along the path, i.e., for every m P ti¨t`k | i¨t ď M´1u, let e m " pl m , λ m , φ m , l m`1 q, add x to λ m , set φ m :" φ m^x ď c (x ě c for lower bound). A periodic constraint is denoted by pt, c, "q, where t is its period, c is the timing constant, and " P tă, ď, ą, ěu. A set of such constraints are defined for each path to capture possible restrictions. In addition, a bound T on the total execution time is captured with the constraint x ď T on transition e k`M over a clock x that is not reset on any transition. A realizable path to l 1 represents a feasible scheduling scenario, thus the target set is L T " tl 1 u. We have generated 24 test cases. A test case A pc,p,M q represents a timed automaton with c P t3, 5, 7u clocks, and p P t1, 2u paths with M P t12, 18, 24, 30u intermediate locations in each path. R c,i is the set of Table 2 . Experimental results for the benchmarks, where |Ψ |, d, v t and cm are as defined in Table 1 , |Ψ u | is the number of constraints considered in the analysis and m is the number of mutated constraints. t I , t IT , t Ic and t IT c are the Imitator computation times, where c indicates that the early termination flag ("counterexample") is used, otherwise the largest set of parameters is searched, and T indicates that only the constraints from the MSR identified by Tamus are parametrized, otherwise all constraints from Ψ u are parametrized. to shows that the timeout limit is reached (20 min.). We ran the Imitator with the flag "incl". Note that when run with the flag "merge", the performance of Imitator increases on 2 benchmarks, however, it decreases on other 2 benchmarks.

Source Spec. Note that A pc,2,M q emerges from A pc,1,M q by adding a path with restrictions R c,2 . Table 1 shows results achieved by Tamus on these models. Tamus solved all models and the hardest one A p7,1,30q took only 14.12 seconds. As expected, the computation time t increases with the number |Ψ | of simple clock constraints in the model. Moreover, the computation time highly correlates with the size d of the minimum MSR. Especially, if we compare two generic models A pc,1,M q and A pc,2,M q , although A pc,2,M q has one more path and more constraints, Tamus is faster on A pc,2,M q since it quickly converges to the path with smaller MSRs.

Imitator solved A p3,1,12q , A p3,2,12q , A p3,1,18q , and A p5,1,12q within 0.08, 0.5, 61, and 67 seconds, and timeouted for the other models. In addition, we run Imitator with a flag "counterexample" that terminates the computation when a satisfying valuation is found. The use of this flag reduced the computation time for the aforementioned cases, and it allowed to solve two more models: A p3,2,18q and A p5,2,12q . However, using this flag, Imitator often did not provide a solution that minimizes the number of relaxed simple clock constraints.

Benchmarks from Literature We collected 10 example models from literature that include models with a safety specification that requires avoiding a set of locations L A , and models with a reachability specification with a set of target locations L T as considered in this paper. In both cases, the original models satisfy the given specification. For the first case, we define L A as the target set and apply our method. Here, we find the minimal number of timing constants that should be changed to reach L A , i.e., to violate the original safety specification. For the second case, inspired from mutation testing [2] , we change a number of constraints on the original model so that L T becomes unreachable. Eight of the examples are networks of TAs, and while a network of TAs can be represented as a single product TA and hence our approach can handle it, Tamus currently supports only MSR computation for networks of TA, but not MILP relaxation.

The results are shown in Table 2 . Tamus computed a minimum MSR for all the models and also provided the MILP relaxation for the non-network models. Note that the bottle-neck of our approach is the MSR computation and especially the verifier calls; the MILP part always took only few milliseconds (including models from Table 1 ), thus we believe that it would be also the case for the networks of TAs. The base variant of Imitator that computes the set of all satisfying parameter valuations solved only 4 of the 10 models. When run with the early termination flag, Imitator solved 3 more models, however, as discussed above, the provided solutions might not be optimal. We have also evaluated a combination of Tamus and Imitator. In particular, we first run Tamus to compute a minimum MSR A ăD,Ią , then parameterized the constraints D Y I in the original TA A, and run Imitator on the parameterized TA. In this case, Imitator solved 9 out of 10 models. Moreover, we have the guarantee that we found the optimal solution: the MSR ensures that we relax the minimum number of simple clock constraints, and Imitator finds all satisfying parameterizations of the constraints hence also the one with minimum cumulative change of timing constants.

In this work, we proposed the novel concept of a minimum MSR for a TA, that is a minimum set of simple constraints that need to be relaxed to satisfy a reachability specification. We developed efficient methods to find a minimum MSR, and presented an MILP based solution to tune these constraints. Our analysis on benchmarks showed that our tool Tamus can generate a minimum MSR within seconds even for large systems. In addition, we compared our results with Imitator and observed that Tamus scales much better. However, Tamus minimizes the cumulative change of the constraints from a minimum MSR by considering a single witness path. If the goal is to find a minimal relaxation globally, i.e., w.r.t. all witness paths for the MSR, we recommend to use the combined version of Tamus and Imitator, i.e., first run Tamus to find a minimum MSR, parametrize each constraint from the MSR and run Imitator to find all satisfying parameter valuations, including the global optimum.

Job-shop scheduling using timed automata

Time for mutants -model-based mutation testing with timed automata

Timed automata

A theory of timed automata

A benchmark library for parametric timed model checking

What's decidable about parametric timed automata?

Repairing timed automata clock guards through abstraction and testing

Synthèse de contraintes temporisées pour une architecture d'automatisation en réseau

Imitator 2.5: A tool for analyzing robustness in scheduling problems

Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking

Offline timed pattern matching under uncertainty

Parametric verification: An introduction

Reachability preservation based parameter synthesis for timed automata

Finding a collection of muses incrementally

Finding all minimal unsatisfiable subsets

Analysing sanity of requirements for avionics systems

Uppaal 4.0

Consistency checking in requirements analysis

Jiří: Tunable online MUS/MSS enumeration

Replication-guided enumeration of minimal unsatisfiable subsets

Rotation based MSS/MCS enumeration

Recursive online enumeration of all minimal unsatisfiable subsets

Online enumeration of all minimal inductive validity cores

Language emptiness of continuoustime parametric timed automata

LTL parameter synthesis of parametric timed automata

On clock-aware LTL parameter synthesis of timed automata

On the optimal reachability problem of weighted timed automata

Parameterized reachability analysis of the IEEE 1394 root contention protocol using trex

Model-based framework for schedulability analysis using UPPAAL 4.1. In: Model-based design for embedded systems

Scheduling a steel plant with timed automata

The wireless fire alarm system: Ensuring conformance to industrial standards through formal verification

Efficient generation of all minimal inductive validity cores

Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking

Some lessons from the hytech experience

Benchmarks for temporal logic requirements for automotive systems

Tools and Algorithms for the Construction and Analysis of Systems

On computing minimal independent support and its applications to sampling and counting

Closed-loop verification of medical devices with model abstraction and refinement

Integer parameter synthesis for real-time systems

Tools and Algorithms for the Construction and Analysis of Systems

Bounded model checking for parametric timed automata

Clock bound repair for timed systems

Synthesising robust and optimal parameters for cardiac pacemakers using symbolic and evolutionary computation techniques

Time abstracted bisimulation: Implicit specifications and decidability

Fast, flexible MUS enumeration

Romeo: A parametric modelchecker for petri nets with stopwatches

On computing minimal correction subsets

Minimal sets over monotone predicates in boolean formulae

Minimal sets on propositional formulae. problems and reductions

Ein satzüber untermengen einer endlichen menge

Formal verification of timed systems: a survey and perspective