Timed Orchestration for Component-based Systems

Individual machines in flexible production lines explicitly expose capabilities at their interfaces by means of parametric skills. Given such a set of configurable machines, a line integrator is faced with the problem of finding and tuning parameters for each machine such that the overall production line implements given safety and temporal requirements in an optimized and robust fashion. We formalize this problem of configuring and orchestrating flexible production lines as a parameter synthesis problem for systems of parametric timed automata, where interactions are based on skills. Parameter synthesis problems for interaction-level LTL properties are translated to parameter synthesis problems for state-based safety properties. For safety properties, synthesis problems are solved by checking satisfiability of $\exists\forall$SMT constraints. For constraint generation, we provide a set of computationally cheap over-approximations of the set of reachable states, together with fence constructions as sufficient conditions for safety formulas. We demonstrate the feasibility of our approach by solving typical machine configuration problems as encountered in industrial automation.


Introduction
We consider the problem of automatically configuring and orchestrating a set of production machines with standardized interfaces. For example, machine interfaces in the packaging industry are expressed in the standardized PackML 3 notation, and skill sets such as fill-box or drill have recently been introduced, in the context of flexible production lines of the Industrie 4.0 programme, for describing parametric machine capabilities [18]. 4 Given such a set of configurable machines, a production line integrator is faced with the task of finding and tuning parameters for each machine such that the overall production line satisfies required safety and temporal constraints. Typical line requirements from the practice of industrial automation include, for example, line-level safety, errorhandling, and the orchestrated execution of sequences of skills intermixed with machineto-machine communication primitives. In addition, production lines are usually required to perform in an optimized and robust manner.
We tackle this problem of orchestrating and configuring parametric production systems by means of parameter synthesis problems for systems of interacting parametric timed automata (PTAs), where multi-party interactions between individual PTAs represent skills and machine-to-machine communication.
In a first step, parameter synthesis problems for interaction-level linear temporal logic (LTL) [22] properties are translated, based on constructions in bounded synthesis [23,9,13], into parameter synthesis problems for state-based safety properties. The Part of this work has been initiated at ABB Research. 3 http://www.omac.org/content/packml 4 http://www.autonomik40.de/en/OPAK.php key element here is the construction of a deterministic monitor similar to bounded LTL synthesis. Due to the use of clocks, however, there are some technical differences to this well-known construction, including a different upper bound of the maximum number of required unrolling steps. Whenever parameters are integer bounded, we demonstrate the existence of a sufficient upper bound for unrolling the negated property automata, such that one can conclude that no parameter assignment can guarantee the specified LTL property.
Then, parameter synthesis problems for safety properties are transformed to solving ∃∀SMT satisfiability problems of the form ∃x : ∀y : Reach(x, y) → (¬φ deadlock (x, y) ∧ ρ safe (x, y)), where x represents the set of parameters to be synthesized, y represents all the component states including local clocks, Reach represents the set of reachable states, ¬φ deadlock (x, y) denotes deadlock freeness, and ρ safe denotes the required safety condition. In general, the computation of the parametric image Reach is undecidable for parameters of unbounded domain [2]. For bounded (integer) parameters, however, Reach can be computed precisely by enumerating all valuations of parameters and, subsequently, constructing the region graph for each parameter valuation. Usually, zone or region diagrams [17,15] are holistic (computationally expensive) approaches used to compute precise images for parameters of bounded domain or abstraction for parameters of unbounded domains. Instead, we are proposing a set of computationally-cheap overapproximations of Reach for avoiding eager and expensive computations of Reach. Novel constructions include over-approximations based on finite depth interaction-history and fence constructions for guaranteeing safety. We also demonstrate the usefulness of these over-approximations with examples based on flexible production systems.
Due to the proposed reduction of parametric synthesis problems to general ∃∀SMT formulas, one may encode and simultaneously solve both qualitative and quantitative (e.g., min, lexicographic) requirements on synthesized solutions. Moreover, the ∃∀-centric encoding of this paper also allows for the synthesis of non-timing parameters. Our use of two SMT solvers for solving ∃∀SMT is an extension of using two SAT solvers for solving 2QBF formula [20]. The new approach here is to exploit this decoupling to also integrate quantitative aspects in solving synthesis problems.
To validate our approach, we have implemented a prototype which includes an ∃∀ constraint generator and an ∃∀ constraint solver (EFSMT). Our initial experiments are encouraging in that our prototype implementation reasonably deals with synthesis problems from our benchmark set with 20 unknown parameters and 10 clocks; that is, the proposed synthesis algorithms seems to be ready to handle the fully automatic orchestration of, at least, smaller-scale modular automation systems.
Related Work. Verification and synthesis of parametric timed automata have recently been considered, among others, by [16,5,17]. These techniques have also been implemented in the tools IMITATOR [4] and Romeo [19], which search for constraints on parameters for guaranteeing the existence of a bisimulation between any timed automata (TA) satisfying the constraints and an initial instantiation of the input PTA. One of the main differences between solving strategies centers around forward versus backwards search, as Romeo starts, using a CEGAR-like strategy, from a counterexample, whereas IMITATOR starts from a good initial valuation of the parameters. In contrast, we are finding the right parameter values which guarantee that the system is deadlock free, and satisfies state-based and interaction-level properties. Existing approaches, which are based on computing and exhaustively exploring the global state space, usually do not perform well even for relatively simple properties such as deadlock-checking, and their implementations are currently restricted to handle problems with only a relatively small number (in the order of ten) automata. contrast, we apply a constraint-based solving approach and use a number of compositional techniques for generating local timing invariants for efficiently solving ∃∀-formulae with EFSMT. Apart from scalability, the ∃∀centric approach also allows for the integration of quantitative objectives. Finally, to the best of our knowledge, current verification and synthesis tools such UPPAAL [8,7], IMITATOR, or Romeo do not support neither multi-party interactions nor qualitative interaction-level properties (LTL).
Organization of the paper. Section 2 recalls the basic definitions for PTAs, safety and transaction-level properties for interacting systems of PTAs, and the orchestration problem for these systems of PTAs. The main technical developments for solving timed orchestration synthesis are presented in Section 3. Section 5 provides some experimental results with a prototype implementation. Final conclusions are summerized in Section 6.

Parametric Component-based Systems and Properties
We briefly review some basic notions for systems of parametric timed automata, and formally state the problem of timed orchestration synthesis.
Definition 1 (Component). A component C(Q, q, X, P, Jump, Inv) is a parametric timed automaton, where: -Q is a finite set of locations, and q ∈ Q is the initial location -X is the set of clock variables -P is a finite set alphabet called ports (edge labels) -→⊆ Q × Guards × P → Q × Resets is the set of discrete jumps between locations.
Guards is the conjunction of inequalities of the form x ∼ k; Resets ⊆ X is a set of clock variables to be reset after discrete jump. We assume that every port p ∈ P is associated with only one discrete jump in Jump -Inv is the set of location conditions mapping locations to conjunctions of disequalities of form x ≤ k with x ∈ X, k ∈ N 0 ∪ V and ∼ ∈ {=, >, ≥}.
For ease of reference, we use the notation C.p to denote the port p of component C, as shown in Fig. 1.
associates each interaction σ with some ports within components. We assume that every port is associated with at least one interaction.
The concrete semantics of a system under a valuation of the unknown parameters follows the standard semantics of timed automata [3], except that discrete jumps are synchronized by interactions (see [6] for details). A time run is a maximal sequence of where q i denotes a location in the system S, σ i is an interaction and v i is a valuation of the clocks in S.
For the ease of reference, we introduce the following notations. For σ ∈ Σ, we denote en t (σ) to be the necessary condition for enabling a location combination to trigger σ Robot2 ts 1 ≤ α1 end  by only allowing finite-time evolving, where the definition of en t (σ) is taken from [24]. If from a location q one can delay the triggering of σ indefinitely, then en t (σ) for that location is by default false. Given a valuation v assigning the variables in V , S(v) denotes the resulting concrete timed system and en t (σ)(v) denotes the resulting constraint of enabling conditions. For infinite time runs ρ with infinite discrete jumps, we use ρ Σ to denote the corresponding ω-word with symbols from the interaction alphabet. Figure 1 illustrates these concepts by means of a variation of the resource contention problem in terms of timed-based control over robots, which is used as a running example. Example 1. Given n robots, robot i first accesses buffer i then buffer (i − 1)%n. Figure 1 depicts the system for n = 2, with the set of unknown parameters V = {α 1 , α 2 , β 1 , β 2 , γ 1 , γ 2 , η 1 , η 2 }. Each Robot i has four ports {occupy-l, occupy-r, release, end}. This system has the interactions Σ = {take1l, take1r, release1, take2l, take2r, release2, reset}, and ∆ is defined to the right of Figure 1. For en t (release1), the necessary condition for interaction release1 to eventually take place without discrete jumps, is The trivial condition 2 − t 1 ≤ 3 − t 1 is to guarantee that the minimum required time for t 1 to have the guard enabled does not let the location invariant of p 13 be violated. Constraint 3 − t 1 ≤ α 1 − t s1 is to ensure that the latest delay for enabling the transition, i.e., time elapse of t 1 to reach the boundary of invariant (which is larger than 2 − t 1 , the shortest delay required to enable the guard), is less than the time it takes t s1 to reach α 1 . This makes it possible to jump to location p 10 .
Definition 3 (Properties). We consider three types of properties: -Component-level properties φ C are constraints over V .
-Safety properties φ state are state properties to be satisfied in every reachable state of the system. Typically, they are location-wise and express relations between clocks. -Interaction-level properties φ int are LTL specifications over Σ. A concrete timed system S(v) satisfies φ int iff every time run ρ of S(v) involves infinitely many discrete jumps, and the corresponding ω-word ρ Σ is contained in φ int by standard LTL semantics.
Example 2. Consider the following properties to be synthesized for the robot running example as displayed in Figure 1: -Deadlock freedom [Safety property].
t 1 + t 2 should always be less than 60 [Safety property].
-Promptness / exclusiveness: φ prompt := i G(take i l → X j =i ¬take j l), i.e., disallow Robot j to perform take j l immediately after take i l from Robot i [Interaction-level property].
Definition 4 (Timed Orchestration Synthesis). Given S = (V, C, Σ, ∆) and properties φ C , φ state , φ int , the problem of timed orchestration synthesis is to find an assignment v for V such that v satisfies φ C , and S(v) satisfies both φ state and φ int ; such a satisfying assignment v is also called a solution.
For example, the assignment given in Example 1 is a solution for timed orchestration synthesis when applied to our running example.

Timed Orchestration Synthesis
This section describes our main constructions for solving timed orchestration synthesis problems. We first translate timed orchestration synthesis problems for LTL properties to corresponding synthesis problems for safety properties (Sec. 3.1). Second, ∃∀SMT constraints are generated for the latter problem, whereby existential variables quantify over the parameters to be synthesized and universal variables quantify over system states (Sec. 3.2). Third, the ∃∀SMT constraints are solved by means of two alternating quantifier-free SMT solvers (Sec. 3.3) for each polarity. In order to simplify the exposition below, we omit φ C as it ranges only over the existentially-quantified parameters in V , and concentrate on the properties φ state and φ int .

Transforming Interaction-level to Safety Properties
To effectively synthesize parameters such that interaction-level properties φ int are satisfied, we adapt bounded LTL synthesis [23] to our context. The underlying strategy is to construct a deterministic progress monitor from φ int . The monitor is meant to keep track of the final states visited in the Büchi automaton A ¬φint corresponding to ¬φ int during system execution. To achieve this, we equip the monitor with a dedicated risk state representing that a final state in A ¬φint has been visited for k times. When the risk state is never reached for all possible runs, all final states in A ¬φint are visited finitely often (i.e., less than k times). This observation is sufficient to conclude that the system satisfies φ int . This is the intuition behind Algorithm 1. Algorithm 1 uses Σ φint ⊆ Σ to be the set of interactions from φ int and # as a symbol not within Σ. On Line 2, the symbol # is used to mark labels corresponding to interactions σ not appearing in φ int . On Line 3 a deterministic progress monitor is constructed C ¬φint,k by unrolling A ¬φint via function monitor(A ¬φint , k), which is similar to the approach in bounded LTL synthesis [23]. Consequently, we omit it and instead provide a high-level description of what it does (see below example for understanding): Starting from the initial state of A ¬φint , Σ φint ∪ {#} is used to unroll all traces of A ¬φint and to create a deterministic monitor C ¬φint,k . Each location 5 in C ¬φint,k records the set of states being visited in the Büchi automaton. For each location, the number of times a final state in A ¬φint has been visited previously is counted. The algorithm maintains a queue of unprocessed locations. For each unprocessed location in the queue, every interaction σ ∈ Σ φint ∪ {#} is selected to create a successor location respectively. A state s is stored in the successor location, if state s is in the unprocessed location and if in the post-processed Büchi automaton, a transition from s to s via edge labeled σ exists. In addition, the number of visited final states is updated. Whenever a final state in A ¬φint has been visited k times, the unroll process replaces the location of C ¬φint,k by risk, a dedicated location with no outgoing edges.
Once the monitor is constructed, an augmented system S inv,k is created from S (Line 5). The interaction set in the augmented system S inv,k is the one from Line 4 where all property-unrelated interactions σ are marked with #. Finally, on Line 6 the state predicate φ deadlock expressing the deadlock condition is constructed from the new set of interactions.
Algorithm 1 Translate φ int into φ deadlock and construct a monitored system S inv,k Input: S, φint, k Output: S inv,k , φ deadlock 1: construct a Büchi automaton A ¬φ int for the negated property of φint 2: postprocess A ¬φ int by replacing every label ¬σ with We illustrate the steps of the algorithm 1 using the robot running example. As for the new interaction set in the monitored system, we show two examples with respect to whether the interaction is in φ prompt : Notice that the introduction of # symbol simplifies the unroll construction in bounded synthesis. Another difference to vanilla bounded synthesis is that, in the context of unrolling, every state has outgoing edges of size |Σ φint ∪ {#}|. In contrast, in bounded LTL synthesis, each σ is viewed as a Boolean variable, which creates, in the worst case, on the order of 2 |Σ| outgoing edges.
The following result reduces timed orchestration synthesis for interaction-level properties to a corresponding timed orchestration synthesis problem on state-based properties only.

Lemma 1.
Given v an assignment of V , S(v) satisfies φ int if all time runs of S inv,k (v) reach neither the location risk in C ¬φint,k nor a state where φ deadlock (v) holds.
Proof. (Sketch) Assume that any time run ρ in S inv,k (v) does not visit location risk or any state where φ deadlock (v) holds. We need to show that S(v) satisfies φ int .
1. Because φ deadlock (v) does not hold and because time runs are maximal, any such time run ρ is infinite. 2. From an infinite time run ρ, we show that ρ defines an ω-word ρ Σ : as φ deadlock (v) is never reached, σ∈Σ en t (σ)(v) is an invariant for all reachable states. Recall that en t (σ) is the necessary condition for enabling a location to trigger σ by only allowing finite-time evolving. Therefore, for all reachable states, one of the interaction (discrete jump) must appear after finite time. Thus, ρ contains infinitely many discrete jumps and consequently, ρ defines an ω-word ρ Σ . 3. By construction, every location in the monitor has edges labeled in σ ∈ Σ φint ∪ {#}, and # marks each property-unrelated interaction in Σ \ Σ φint (Line 4). From this observation, together with the fact that S inv,k (v) does not restrict the behavior of S(v), we have that a time run ρ in S inv,k (v) not reaching risk is bisimilar to a time run ρ in S(v), with ρ and ρ defining the same ω-word ρ Σ . 4. Recall that C ¬φint,k is an unroll of A ¬φint . From this, together with the existence of ρ Σ and the fact that while running ρ Σ in A ¬φint no final state is reached infinitely many times, we have that ρ Σ does not satisfy ¬φ int . Consequently, we can conclude that for every time run ρ in S(v), the corresponding ρ Σ satisfies φ int .
By Lemma 1, it is sufficient to only consider safety properties when performing orchestration synthesis. Notice howerver that, if for a given fixed k Lemma 1 fails for all possible assignments v then one may not conclude that no solution exists for the orchestration synthesis problem as there might be a larger k for which Lemma 1 does hold. Next we show that it is futile to go beyond a reasonable bound. More precisely, if the domains of the parameters in the input system S are bounded, then one can effectively compute a limit k * on k such that: if Lemma 1 is not applicable for k * then it is also not applicable for any strictly larger k. Given v an assignment of V , if there exists a time run of S inv,k * (v) reaching either risk in C ¬φint,k * or a state where φ deadlock (v) holds, then S(v) does not satisfy φ int .
Proof. (Sketch) Let ρ be a time run of S inv,k * (v) which reaches either risk in C ¬φint,k * or a state where φ deadlock (v) holds. We have two cases: -Case 1: risk is not reached, equally, ρ reaches a state where φ deadlock (v) holds. The deadlock of S inv,k * (v) under ρ is irrelevant to the monitor component, as the monitor component does not hinder any execution apart from risk. Therefore, S(v) contains deadlock states, and S(v) does not satisfy φ int , as reaching a deadlock state means that one can not create an ω-word from that time run. -Case 2: risk is reached in the k * -th unroll. We need to show that with a prefix of a violating time run ρ in S inv,k * (v) that visited one final state s in A ¬φint for k * times, one proves, by tailoring a fragment of ρ, the existence of a time run ρ in S(v) such that the ω-word of ρ , when applying to A ¬φint , guarantees to visit s arbitrary many times. This is done with the help of two results: (1) the number of regions in a timed automaton is finite, and (2) the pigeonhole principle. concrete values, the system is a timed automaton and the number of regions is finite. The total number of regions is bounded by δ. Recall that the executions in C ¬φint,k reflect executions in the Büchi automaton A ¬φint . Consider a discrete jump in the system. With a specific destination state s in A ¬φint , one can actually capture a discrete jump in S inv,k (v) by only viewing its change in regions and locations. To reflect such changes, we use tuples (r source , l source , s source ), σ, (r dest , l dest , s) , where r source and r dest are source and destination regions in S(v), l source and l dest are source and destination location in S(v), s source is the source state in A ¬φint with interaction σ ∈ Σ. The total number for all such (r source , l source , s source ), σ, (r dest , l dest , s) tuples is bounded by δ 2 η 2 |A ¬φint ||Σ|. Therefore, when the violating ρ visits a particular final state s in A ¬φint for k * times, in the corresponding region representation, one particular tuple (r source , l source , s source ), σ, (r dest , l dest , s) should have appeared twice (due to pigeonhole principle). The clock valuations associated to l source , resp. l dest may be different in the two tuples. However, the corresponding states are region-equivalent and consequently bisimilar. Thanks to this, S can evolve region-bisimilarly until the tuple (r source , l source , s source ), σ, (r dest , l dest , s) appears for the third time, and so on. While repeating this pattern a time run visiting s infinitely often is constructed.
Input (structure of the system) . . . Implications from locations to timings: Exploiting (simultaneous) resets: Fences -based on untimed reachability analysis risk a 1 l3l k In untimed reachability graph,l1,l2, . . . ,l k lead to risk Starting from initial location, all paths which lead to risk must passl1,l2, . . . ,l k For li ∈ {l1,l2, . . . ,l k }, it at least has one edge which can avoid leading to risk.

Generating ∃∀-Constraints for Safety Synthesis
Now, we reduce timed orchestration synthesis problem for safety properties to corresponding ∃∀SMT constraints of the form where x is the set of unknown variables to be synthesized, y is the set of clocks, locations, optional variables for encoding the history of interactions, φ S (x, y) is the summary as an over-approximation of system dynamics, ¬φ deadlock (x, y) is the translation of φ int into a safety property as described in Section 3.1, and ρ safe (x, y) is a disjunction of sufficient conditions for not reaching location risk. Constraints φ C and φ state are given system requirements as mentioned in the problem formulation in Section 2. For ease of reading, we use the notation k > 0, respectively k = 0, to distinguish the case when k-step interaction-history is encoded by means of universal variables from the case when interaction-history is not used at all in the generation of φ S (x, y). We note that any solution for Formula (1) is a solution to the problem formulated in Section 2.
Generating φ S (x, y) k=0 . Our approach to characterize the behavior of the system is compositional. This way, we avoid computing the whole product, which is, in most nontrivial cases, a costly operation. Instead, our computed invariant is the conjunction of the following three: (1) invariants for each component, (2) invariants capturing conditions when synchronization appears, and (3) untimed reachability.
(1) Component invariants CI(C i ) are properties characterizing components C i . We do not restrict their computation to a specific methodology. What matters is that such properties can be shown to be invariants. In our framework, where components are parametric timed automata, one way to obtain invariants is to compute abstractions 6 of classical zone graphs [15]. Zone graphs are symbolic representations of the reachable state space of parametric timed automata. In practice, easier solutions work as well. One example is the tactic 1 in Figure 3. As an illustration, for Robot 1 , by applying tactic 1, the resulting invariant is (p 10 → t s1 ≤ α 1 ) ∧ (p 11 → t 1 ≤ γ 1 ) ∧ (p 12 ∧ t 1 ≤ 3) ∧ (p 13 → t 1 ≤ 3). By applying tactic 2 and 3 one can derive the additional conditions for Robot 1 and Robot 2 : -(ts 1 < η 1 ) → (p 11 ) and (ts 2 < η 2 ) → (p 21 ).
(a) Consider location p 12 in Robot 1 . It has one incoming edge which resets clock t 1 .
As no other clock in the system is reset, and the incoming edge has guard t 1 ≥ η 1 , one derive that (p 12 ) → (t s1 − t 1 ≥ η 1 ), i.e., in location p 12 , all other local clock readings should at least be η 1 unit larger than t 1 .
(b) Consider interaction reset. It leads to location (p 11 , −, −, p 21 ), where initial state is located. One can derive the invariant (p 11 ∧ p 21 ) → (t s1 = t 1 = t s2 = t 2 ). By a similar argument, one can also infer that t s1 = t s2 holds, due to unique clock reset action on reset. (3) Untimed abstract reachability invariant Abs(S) is the set of reachable location combinations of S by ignoring clocks and by only considering the lockings by interactions. E.g., with untimed reachability analysis from initial locations, one can deduce that (p 11 ∧p 21 ) → (f 10 ∧f 20 ), i.e., buffers are not occupied before both robots start. Notice that Abs(S) is not sensitive to parameter change due to its ignoring of clocks.
Remark 1. Commonly, a tactic creates constraints of the form φ loc → φ clock , where φ loc is a formula over locations and φ clock is a property associated with clocks. As φ loc → φ clock ≡ ¬φ clock → ¬φ loc , the ∃∀-solver also uses such constraints to reason that under concrete timing conditions, it is impossible to be in a state in Abs(S). To illustrate this, we return to the robot example. In the untimed setup, Robot 1 and Robot 2 can execute take1l and subsequently take2l. Therefore, state (p 12 , p 22 , risk) is within Abs(S inv,k ). However, under a parameter assigment as γ 1 = η 1 := 0 and γ 2 = η 2 := 15, the constraint solver invalidates such a state by the following reasoning: -When Robot 2 is at p 22 , t s2 ≥ η 2 , i.e., t s2 ≥ 15 (by tactic 2 in Figure 3).
We define φ S (x, y) k=0 as Ci∈C CI(C i ) ∧ Π S ∧ Abs(S) and denote φ S (x, y) k=0 (v) to be the result of replacing the unknown variables V by assignment v in CI(C i ) and Π S . Using the fact that the conjunction of invariants is an invariant itself, it can be shown that indeed φ S (x, y) k=0 is an invariant of S. Lemma 3. For any assignment v for unknown parameters, φ S (x, y) k=0 (v) is an invariant of S(v).
Generating φ S (x, y) k>0 . For ∃∀-constraint solving, the precision of system invariants plays an important role. Given the set of interactions Σ, one can introduce a set of Boolean variables {prev k σ | σ ∈ Σ} to record k-previously executed interaction. As an example, consider tactic 2 in Figure 3. When one records the previously executed interactions, the condition c ≥ c + x is associated with location l 2 and the previously executed interaction σ. Assume that l 2 has another incoming interaction σ , which does not reset c. Then a memoryless approach (i.e., no history) needs to take the disjunction of conditions from all incoming edges, thereby losing the knowledge of c ≥ c + x.
The price for recording k-step interaction history, given Σ as the set of interactions, is only at the cost of introducing k|Σ| Boolean variables as universal variables. In a similar manner as for Lemma 3, it can be shown that φ S (x, y) k>0 is an invariant of the system.
Generating ρ safe (x, y) with "fence" constraints. An intuitive yet sometimes sufficient way is to assign ρ safe (x, y) to be simply ¬risk. However, one can also introduce other constraints ρ 1 , . . . , ρ n , where each of them is a sufficient condition to block the run to enter risk, and set ρ safe (x, y) := (¬risk) ∧ n i=1 ρ i , and leave the finding of solutions to the ∃∀-solver. The computation of these constraints should be light-weight. Here we present the fence-condition tactic (index 4 of Figure 3) which only involves the computation of backward untimed reachability and the static scan of components.
The underlying concept is to find a set of nodesl 1 ,l 2 , . . . ,l k in the abstract reachability graph, where every path that leads to risk must pass one nodel i ∈ {l 1 ,l 2 , . . . ,l k }. At each nodel i , there exists at least an "escape edge" which can avoid leading to risk. Finding such a set is done by solving a safety game (using standard attractor computation defined in two-player, turn-based games over finite arena; see [21] for details) with all nodes viewed as control vertices. Here we explain the attractor concept using examples. In Figure 3, the computation of attractors adds gradually {ā 1 }, {ā 2 } (as one outgoing edge leads to risk and the other leads toā 1 ), {ā 3 ,ā 4 } to the attractor of risk. Nodes such asl 3 are outside the attractor, as it can use σ 2 to escape.
With {l 1 ,l 2 , . . . ,l k } identified, whenever one can guarantee that at nodel i , interactions which leads to the attractor will never be executed, then one can guarantee that risk is never reached from the initial state for any time run. Forl i ∈ {l 1 ,l 2 , . . . ,l k }, let Σ attr,i be outgoing interactions which leads to attractor and Σ str,i be the winning strategy on l i to escape from the attractor. For interaction σ, let guard σ be the guard condition for which σ can take place. We restrict ourselves to such that guards are conjunctions of form clock ∼ k where ∼ ∈ {>, ≥}. Then we can create the following constraint: Intuitively, the constraint specifies that atl i , as long as when an interaction σ from Σ str,i can be executed in the future (i.e., en t (σ )), interaction σ in Σ attr,i should not be enabled. In Figure 3, for nodel 3 , as en t (σ 2 ) is merely the invariance condition on l q , we havel 3 → (Inv(l q ) → ¬guard σ1 ).

Finding Satisfying Instances for ∃∀ Formulas
We outline a verification procedure implemented in EFSMT for solving constraint problems of the form ∃x ∀y : φ(x, y), where φ(x, y) is a quantifier-free formula involving two variable sets x and y. This class is generic enough to fit formulas such as Formula (1) in Section 3.2. The verification procedure is based on two SMT solver instances, the so-called E-solver and F-solver. These two solvers are applied to quantifier-free formulas of different polarities in order to reflect the quantifier alternation, and they are combined by means of a counter-example guided refinement strategy.
At the k-th iteration, the E-solver either generates an instance x k for x or the procedure returns with false. An x k provided by the E-solver is passed to the F-solver for checking if ∃y : ¬φ(x k , y) holds. If not, then x k is the witness for the problem ∃x∀y : φ(x, y). In case there is a satisfying assignment y k generated at the k-th iteration, the F-solver passes the constraint φ(x, y k ) to the E-solver, for ruling out such x as potential witnesses. Future candidate x k+1 from the k + 1-th iteration should therefore not only satisfy φ(x k+1 , y 0 ), . . . , φ(x k+1 , y k−1 ) but also allow φ(x k+1 , y k ) returning true (an example is listed below, for the ease of understanding).
In many cases the domain of integer parameters is bounded, and the EFSMT solving algorithm is terminating 7 , as there are only finitely many variable assignments. Consider, for example, a constraint such as ∃x 1 ∈ [0, 100] ∩ Z, ∀y 1 ∈ [10, 20] ∩ R : x 1 − y 1 ≥ 80. Assume that the explicit enumeration and EFSMT both start with the order x 1 = 0, 1, . . . , 100. In these cases, brute-force enumeration method need to iterate 100 times, until they find x 1 = 100 (the only satisfying instance). For EFSMT, if x 1 = 0, then the counterexample provided by F-solver, for instance, y 1 = 10, falsifies it. After this step, E-solver creates a new assignment by ensuring x 1 − 10 ≥ 80 thus immediately jumping to x 1 = 90. Consequently, it omits checking assignments x 1 = 1, . . . , 89. In other words, our solver may be viewed as an acceleration of explicit enumeration of SMT via counterexamples.

Extensions
Due to the reduction of timed orchestration problems to ∃∀SMT on can readily handle richer arithmetic constraints in synthesis problems. We briefly outline how quantitative synthesis, robustness synthesis, and synthesis beyond PTA may be encoded. Quantitative Synthesis. In practice one is usually interested in obtaining parameters for optimized system behavior (e.g., min, lexicographic). For example, one might be interested in obtaining a minimum value for the parameter α 1 in our running example in in Figure 1. In solving the corresponding ∃∀SMT constraints using the proposed two solver approach, one may simply use an E-solver with optimization capabilities -e.g. a MaxSMT solver such as νZ [10]) -instead of an SMT solver. In this way, the proposed solution of the E-solver is optimal with respect to the current set of constraints. Robustness Synthesis. Using ∃∀SMT constraints, the imprecision of system may be modeled by means of universally-quantified, bounded variables. For example, one may model the imprecision for a a guard t 1 > 2 by t 1 > 2 + δ, where δ ∈ [−0.05, 0.05], and δ ∈ [−0.05, 0.05] is added as a new universally-quantified variable in the ∃∀SMT. Beyond PTA. Using the full expressivness of ∃∀-constraints, one may also encode guards, for instance, t 1 + 3 t 4 ≥ 10, which go beyond clock constraints of plain PTAs.

Evaluation
The above extensions come for free with our prototype tool 8 which we have developed for implementing the concepts in Section 3. Technically, the prototype automatically generates monitor components based upon the LTL2Buchi transformation [14] for generating Büchi automata. The symbolic reachability underlying the computation of Abs(S) and the attractor computation for fence conditions use JDD 9 , a Java package for efficiently manipulating Binary Decision Diagrams (BDDs). The construction of the ∃∀ constraint solver is based upon the combination of our E-solver and F-solver which in turn wrap SMT-solver Yices2 [12] when quantifier-free constraint solving is needed. Tables 1 and 2 show the results of our initial evaluation (under Intel i5-4300u CPU, 8GB RAM, Ubuntu 14.04 64-bit OS). The recorded execution times for other tools (e.g., IMITATOR) are based on the newest tool versions available for download. For the robot problem in Table 1, the constants in one automaton differ from those in the other automaton. This is in order to avoid symmetric effect and more importantly and additionally, to be closer to more realistic settings. As an example, using the same experiment setup  to run IMITATOR for five robots already takes about ten minutes (EFSMT is about one order of magnitude faster). In Table 1, we do not list the time needed for generating constraints, as it is neglectable compared to ∃∀-constraint solving (for abstract reachability, even for 10 robots it takes less than 5 seconds). However, the ordering of the constraints may greatly influence timings. Consequently, obtaining good results for synthesizing parameters to enforce safety properties requires both a good solver and a tailored constraint structure suitable for exploiting the locality of constraints. In our case, this is truly possible thanks to our local component invariants. From Table 1 readers may be surprised by the timing for ensuring promptness in the case of 6 robots. The increase in computation time follows from EFSMT searching for all possibilities without finding any, as the sum of all mode upper bounds is greater than 30. Another interesting behavior which occurred during our evaluation exhibits that the nondeterminism within SMT solvers (for Robot 7 it creates multiple satisfying assignments) may drastically influence performance. Table 1 also shows the result of analyzing the temperature controller problem modified from [6], where only one unknown parameter needs to be synthesized. In the experimental setup, the search starts from β = 999, then it quickly prunes the search space and identifies the result in about 2 to 5 steps. This is the reason why the computation time is surprisingly small, and clearly demonstrates the superiority of EFSMT over a brute- force enumeration method. However, as our parameterized timer invariant generation is far from precise, our generated result is not optimal. Still, for verifying our result using UPPAAL, it takes more than 10 minutes for 50 workers. This demonstrates that at least some problems may be solved by inferring synchronization properties without paying the price of doing holistic state space exploration.

Flexible Production System Case Study
In discrete manufacturing, individual workpieces are treated in multiple processing steps, typically organized sequentially with multiple machines. Under the initiatives of Industrie 4.0, it is generally perceived that machines can communicate their status, mainly on their state changes. This view fits well with our methodology. To see this, it suffices to adopt the interpretation where one can isolate the functionality of every machine as components with parameters and design each component without the use of global clocks. Along these lines, as an application of our method to discrete manufacturing, we use simplified packaging line as a case study in the food & beverage segment. The main components are displayed in Figure 4. More precisely, Figure 4 illustrates a Form-Fill-Seal (FFS) machine which fills parts produced in the upstream process into plastic bags. In turn, the plastic bags are packaged into boxes by a packaging machine. Finally, cartons are placed on a pallet for shipment. We assumed that the product to be created is breakfast cereal, while retailers can request variations on bag size and box capacity in terms of x grams per bag and y bags in one box. To handle such product variations realized by the two variables x and y, we simply need to encode them as universal variables. On the other hand, FFS machine parameters are encoded as existential variables: the execution times for filling, respectively sealing, are configured by α, respect(β sec). In the automaton for FFS, these variables are placed as the guards and location conditions to represent the lapse of time. By encoding the problem into EFSMT, we are able to synthesize α and β such that it works for all x and y specified in the range. For example, a typical encoding is ∃α, β ∀x ∈ [100, 300] ∩ R ∀y ∈ [10, 24] ∩ Z.
For this scenario we formulate a system description together with properties for excluding undesired action sequences such as "when the packaging station buffer is full, FFS should stop shipping until the buffer has space". This property is encoded in terms of the interaction-level LTL formula G(Packaging.stackfull → (¬FFS.ship U Packaging.stackavailable)).
Applicability and limitations. We apply our solver for solving the timed orchestration problem on interaction-level properties; the results of this case study are summarized in Figure 2. For those properties where EFSMT successfully synthesizes parameters, we also tried to restrict the domain and recorded required time for EFSMT to report "unable to find a solution". Our solving approach seems to scale well because of the use of compositional techniques, but at the expense of precision for relations between clocks from different components. Moreover, due to recording the history of interactions, our solver seems to perform well on LTL formulas include F or U, since these properties are translated into a template "whenever an event occurs, something good should happen within a finite number of steps" by means of unrolling. Finally, we note that constraint grouping and variable ordering plays an important role in the performance of the underlying SMT solver Yices 2. More precisely, we observe in our experiments a sever performance penalty whenever constraints are not properly grouped or whenever the evaluation order of variables does not respect the grouping. Informally, a constraint grouping may be called proper if the grouping in EFSMT follows that of the constraints in the invariants for untimed reachability. These invariants are computed by means of BDDs and FORCE ordering heuristics [1] in our implementation, which results in relatively compact representations and to also reduce the size of invariant constraints.

Conclusions
The main contributions of this paper include (1) encoding of line integration problems in terms of timed orchestration synthesis, (2) upper bound on the number of unrolling steps in bounded synthesis for PTA, (3) encoding of timed orchestration synthesis in terms of ∃∀SMT, and (4) set of computationally-cheap over-approximations for avoiding overly eager and expensive computations of the precise parametric images of the set of reachable states. Some of the key ingredients of this logical approach to solving timed orchestration problems include the translation of deterministic monitors from LTL properties, the generation of parametric invariants, the use of two SMT solvers for ∃∀ constraints, constraint grouping and variable ordering. We demonstrate the feasibility of this approach by means of solving some typical line integration problems as encountered in industrial practice; it still remains to be seen, however, if and how the proposed methodology and tools scales to solving orchestration problems for real-world production lines. In future work, we therefore plan to go beyond ω-words when considering interaction-level LTL properties, develop static analysis techniques on the system structure for obtaining cheap invariants, investigate hierarchical solving approaches, and to extend the orchestration synthesis problem to hybrid systems.