Parallel Behavior Composition for Manufacturing

1 Introduction

Manufacturing companies are increasingly faced with demands for variable volumes of high quality customised products, produced rapidly and at low cost [Foresight, 2013]. One way of meeting such demands is through increased automation, and in particular allowing production control software greater autonomy in determining how products will be manufactured. The application of autonomous systems in manufacturing has the potential to increase productivity, flexibility and reliability, add value, and compensate for an ageing skilled workforce. However, the complexity of such "autonomous manufacturing systems" has so far prevented their widespread adoption. A key challenge in realising the potential of autonomous manufacturing is moving from humanauthoring of the production control software that specifies how a particular product should be made, to the automated synthesis of controllers that are able to manufacture any instance of a given product type on a particular production or assembly line.

The problem of synthesising complex (virtual) systems from simple existing modules has been addressed in AI, where it is referred to as the behavior composition problem [De Giacomo et al., 2013]. The composition task involves synthesizing a controller to coordinate a set of available behavior modules (e.g., automatic lights or blinds, TVs, microwaves, etc.) so as to implement a novel target behavior module (e.g., a smart house system). Standard behavior

Sebastian Sardina

RMIT University, Australia sebastian.sardina@rmit.edu.au

composition assumes a single sequential execution of the target behavior module. While adequate for domains such as web-services [Calvanese et al., 2008], these approaches are not applicable to the manufacturing domain.

In manufacturing, the target represents a process specified by a production recipe, which lists the steps necessary to manufacture items of a particular product type, and the order in which those steps should be executed. The recipe encompasses all variations of the product type, e.g., variations in size, color or material, and decisions about how a particular item should be manufactured are made at run-time, based on order information associated with the item, e.g., whether the item is to be blue or green. The steps in a recipe are enacted by production resources, e.g., welding machines, painting machines, etc. For example, in garment manufacture, a production recipe may specify how to make shirts of various colors and sizes, and the production resources may be fabric cutting, sewing and pressing machines. In general, a recipe consists of multiple steps, and (depending on available production resources) it is often possible to start work on manufacturing another item before the items currently being manufactured have been completed. The aim is to construct a target production process that allows many instances of a product type (ideally as many as possible) to be produced at the same time on the available production resources. Critically, such a process must allow all variations of the product type specified by the recipe for each instance produced, as the specification of each item (e.g., whether it will be blue or green) is only known at run-time.

In this paper, we extend behavior composition [De Giacomo et al., 2013; Stroeder and Pagnucco, 2009; Lustig and Vardi, 2009] to manufacturing settings. We formalise both production recipes and production resources, and propose a technique for synthesizing a target production process and controller capable of orchestrating the behaviors of the production resources to produce multiple instances of a product type in accordance with the recipe. To the best of our knowledge, our work is the first to consider the synthesis of controllers for multiple concurrent instances of a target process.

2 Production Recipes and Cycles

We begin by presenting the notions used to specify how items of a particular product type are manufactured. A production recipe captures the basic finite process required to manufacture any instance (e.g., a blue shirt of size XL) of a particular product type (e.g., shirts).

Definition 1. A production recipe is a tuple Ρ = (L↪ l0↪A↪ λΡ↪ F) where (i) L is finite set of states and l0 ∈ L is the initial state; (ii) A is a finite set of actions; (iii) λΡ ∶ L × A → L is an acyclic transition function with all final states being sink states; (iii) F ⊆ L is the set of final states. ￿

We assume that recipes are acyclic and "terminating": the manufacture of every product item requires a bounded number of steps. 1 For example, producing an item of the product type specified by the recipe Ρ depicted in Figure 1 requires performing operation ↵ (e.g., cut fabric) followed by either action β (e.g., dye blue) or γ (e.g., dye green), after which the item is deemed manufactured (states Y and Z are final). Hence Ρ specifies two different manufacturing alternatives or product variations. As explained above, whether β or γ will be performed for a particular item is decided at run-time, externally to the recipe.

A production recipe may be arbitrarily large and include options for which action to perform in a state that encode the different ways in which a product can be manufactured (e.g., due to variations within a product type). For example, once the fabric of a shirt has been cut, it may be dyed green, red, or blue: which color should be used for a particular product item is decided at run-time and is outside the model (e.g., by a human operator, or determined by information carried by the item itself, e.g., in the form of a radio-frequency identification (RFID) tag specifying the color). If a recipe is actiondeterministic, i.e., only one action is available in each state of Ρ, this indicates that there is only one possible way of manufacturing the product type.

While recipes specify how one item of a product type is to be manufactured to completion, a production plant aims to manufacture many instances of a product simultaneously, over and over, in principle forever. This continuous process is captured through the notion of production cycle.

Definition 2. Given a product recipe Ρ = (L↪ l0↪A↪ λΡ↪ F), the production cycle induced by Ρ is a tuple ΛΡ = (L ￿ F↪ l0↪A↪λ) such that λ(l) = λΡ(l) for all l ∈ L ￿ F, and λ(l) = l0 for each l ∈ F. ￿

Intuitively, a production cycle represents the repeated execution of a recipe. To represent the completion of one item and the beginning of the next item of the product type, we add a transition from the final states to the initial state of the recipe. When an item "returns" to the initial state (through a sequence of transitions within its production cycle), it is considered as "completed," and the cycle can be "restarted" representing a new item of the product type entering the production line. For instance, the production cycle ΛΡ in Figure 1

1 It is straightforward to add constructs specifying the bounded repetition of a subprocess, e.g., to model the re-trying of a process (clean subprocess) until success (product sensed clean), and exiting after some number of repetitions (discard product).

We will use the notion of traces in the usual way to represent legal runs of recipes and cycles. For example, a trace of a production cycle Ρ is a finite sequence ⇡ = l0a1 l1a2￿a` l` (or just ⇡ = l0 a1 ￿→l1 a2 ￿→￿ a` ￿→l` ), such that ￿lj-1 ↪aj ↪ lj ￿ ∈ λ for all 1 ≤ j ≤ `. When ⇡ is a trace as above, last(⇡) denotes its last state t` . Finally, unless stated otherwise, we assume that traces start from the initial state (in this case, l0 = l0).

is induced by the recipe Ρ. When Λ is a production cycle, we denote by Λ- the extended cycle obtained from Λ by adding extra self-loops with the special action - ￿∈ A in every state. The - ("no-op") transition is used to represent a "pause" step.

3 Production Plants

Production recipes are enacted by a production plant, consisting of production resources and their associated capabilities (e.g., cutting, sewing, knitting, and pressing machines in a clothing factory). Following [De Giacomo et al., 2013], we model those capabilities as available behaviors of the form Β = (B↪ b0↪ A↪ R) where B is finite set of states, b0 ∈ B is the initial state, A is the set of actions (we assume - ￿∈ A), and R ⊆ B × A × B is Β's transition relation. Behaviors may be nondeterministic, and so are only partially controllable, i.e., once a behavior is instructed to execute an action, its evolution cannot be controlled. For example, a painting machine can non-deterministically evolve to a state signaling out-ofpaint after painting an item.

Definition 3. Given a set of m ≥ 1 behaviors {Β1↪ ▷ ▷ ▷ ↪ Βm}, with Βi = (Bi↪ b0i↪A↪Ri) for each 1 ≤ i ≤ m, the production plant system is a tuple Σ = (S↪ s0↪ Am- ↪ ⇢) where:

A production plant is composed of m ≥ 1 available behaviors, and is formally captured as the synchronous product of those behaviors. (We assume that the production plant is fixed, as it represents the capabilities of the available production resources.) From now on, we denote by indx the set of vectors k ∈ ({1↪ ▷ ▷ ▷ ↪m})m in which the components ki are pairwise distinct. As is customary, when X is a set, n ≥ 1, Xk = X × ￿ × X denotes the k cross-product of X; and when t is a tuple of size k, we use ti to denote its i-th component, for each 1 ≤ i ≤ k. When A is a set of actions, we use Ak- = (A∪ {-})k ￿ ({-})k to denote the set of vectors of k actions extended to include the distinguished no-op - action.

• S = B1 ×￿×Bm is the set of states;

Intuitively, a transition ￿b1↪ ▷ ▷ ▷ ↪ bm￿ a k ￿￿→￿b′1 ↪ ▷ ▷ ▷ ↪ b′m￿ in Σ captures the delegation of each action aj (including possibly no-op actions) to the available behavior Βkj , which evolves

• s0 = ￿b01↪ ▷ ▷ ▷ ↪ b0m￿ is Σ's initial state; · ⇢ ⊆ S ×Am- × indx×S is Σ's transition relation such that ￿b1↪ ▷ ▷ ▷ ↪ bm￿ a k ￿￿→￿b′1 ↪ ▷ ▷ ▷ ↪ b′m￿ in ⇢ iff for each 1 ≤ i ≤ m, if ai = -, then b′i = bi; otherwise b′ki ∈ Rk(bk↪aki ). ￿

￿↵↪ -￿↪ ￿↵↪ ↵￿

￿-↪ ↵￿,￿β↪ ↵￿

￿β↪-￿, ￿-↪↵￿, ￿β↪↵￿

Figure 2: A plant Σ = ￿Β1↪ Β2￿. For compactness, ￿↵↪ γ￿ in Σ stands for both ￿↵↪ γ￿￿1↪ 2￿ and ￿γ↪ ↵￿￿2↪ 1￿.

production plant system Σ. As for production cycles, traces of production plant systems are sequences of the form s0 a1 ￿→￿ a` ￿→s` , which we refer to as histories. We use Η to denote the set of histories of Σ. 3.1 Plant Controllers

from current state b′kj to successor state b′kj . As an example, Figure 2 shows two available behaviors and the resulting

Intuitively, a production plant is operated as follows. At any point in time, the "user" or "operator" of the plant-which may be human, software, or a hybrid of the two-requests the execution of up to m domain actions, where m is the number of available behaviors in the plant. A controller then delegates each domain action to an available behavior in the plant that is capable of handling the action in the current situation. The designated behaviors then execute their assigned actions and evolve as specified by their transition relation, yielding the new state of the plant, from where a new request is issued and so on. The objective is to build a controller that always fulfills the user's requests by appropriate delegation of domain actions.

P ∶ Η×Am- → indx which delegates a set of actions a ∈ Am- to available behaviors in Σ: if P(h↪a) = k, then P delegates action ai to available behavior Βki , for i ∈ {1↪ ▷ ▷ ▷ ↪m}. ￿

Definition 4. Given a production plant system Σ with m ≥ 1 available behaviors, a plant controller (or controller) is a function

Note that our notion of controller extends that of De Giacomo et al. (2013) to multiple actions, as we assume a production plant can perform more than one operation at a time, due to the concurrent operation of production resources. However, since each resource can carry out one operation at a time, in a plant with m resources, one can execute up to m actions simultaneously.

4 Target Production Processes

With the notions of production recipe and production plant system in hand, we are now ready to present one of the main contributions of the paper, namely target production processes, as a solution concept for manufacturing composition. Since production plants aim to manufacture not one, but several items of a given product type simultaneously, the natural

￿β↪ ↵￿￿γ↪ ↵￿

Figure 3: The 2-pcycles Λ2 (solid edges only) and Λ2- (solid and dotted edges) for production cycle ΛΡ from Figure 1.

question that arises is: what is the actual "target" process that a production plant needs to support?

Unlike in AI behavior composition (e.g., [De Giacomo et al., 2013]), the desired manufacturing process to be "implemented" in the production plant is neither arbitrary nor given as part of the input. Intuitively, the desired process involves the production of multiple items of a given product type, all conforming to the production cycle induced by the production recipe specifying how to manufacture items of the product type. We shall call such a process the target production process (TPP), or just the target. However it is not clear exactly what this process ought to be, let alone how to compute it, so we first spell out the requirements. The first requirements is:

• R1. ATPP should allow the manufacture of multiple product items simultaneously. When a TPP allows the manufacture of exactly n items in the plant at a given time, we say it is an n-TPP.

For example, while a shirt is being dyed by one production resource, the fabric of another shirt-another product instance-is being cut by another resource. One way of meeting R1 would be to define the production process to be the synchronous execution of multiple copies of the product production cycle, formally captured as the synchronous execution of n production cycles Λ or Λ- (see Figure 3):

• T = Ln is the set of states of Λn . When t = ￿l1↪￿↪ ln￿ ∈ T , we use sti(t) = li to denote the i-th component of t;

Definition 5. Given a production cycle Λ = (L↪ l0↪ A↪ λ) and n ≥ 1, the n-pcycle of Λ is a tuple Λn = (T↪ t0↪ An ↪ δ) where:

• t0 = ￿l0↪￿↪ l0￿ is the initial state of Λn ; and · δ ∶ T × An → T is such that t′ = δ(t↪a) (or t a￿→t′ ) iff sti(t′ ) = λ(sti(t)↪ ai) for each i ∈ {1↪ ▷ ▷ ▷ ↪ n}. ￿

However, taking Λn (or Λn- ) as the production process is too demanding: they embed all possible ways in which n product items may be manufactured (including no-op transitions), whereas the production plant may only be able to produce n items concurrently in a particular way. To address this, one could consider extracting the maximal realizable target of Λn- [Yadav and Sardina, 2012; Yadav et al., 2013] to obtain the aspects of Λn- that can be realized in the plant. However the maximal realizable target may restrict some of the production cycles, as the resulting fragments may not account for the complete production cycle. This leads to our second requirement for TPPs:

￿↵↪ β￿

Figure 4: Τ1 and Τ2 are not 2-targets for Λ as in Figure 1, while Τ3 is. Dashed edges represent transitions in δUN.

• R2. For each product item in a TPP, the complete product recipe should be available, no matter how the other product items are processed.

That is, when manufacturing each item, it should be possible to produce any variant of the product type (e.g., color of a shirt). In general, which variant a particular item corresponds to is not known at the outset (e.g., whether action β or γ will be performed is known until we reach state X in Ρ; Figure 1). As a result, Τ1 in Figure 4 is not a 2-TPP for the recipe Ρ, as it is unable to manufacture two "β items" only (or similarly two γ items): there is no transition ￿β↪ β￿ from state XX. Note that a naive projection from Τ1 on either item instance would indeed yield the production cycle of the product-more is needed to capture this requirement.

To ensure that TPPs are both general and flexible, we stipulate the following additional requirements:

• R3. The possible evolutions of the TPP may depend on how (nondeterministic) behaviors in the plant happen to evolve, as long as R2 is met.

This means that unlike in AI behavior composition, we shall accept target production processes that are "nondeterministic."

• R4. A TPP may pause certain items and account for different ways in which all of them can be concurrently produced (the decision how exactly left to the user at run-time).

That is, a TPP may include several (though not all) alternative ways of manufacturing n items concurrently, including "pausing" certain items at some point, where this is necessary due to limitations in plant resources. However we restrict the ways that - ("pause") actions may be used:

• R5. A TPP should never allow the starvation of any item: every item must eventually be completed.

For example, Τ2 in Figure 4 is also not a 2-TPP for Ρ, because the second item instance is commenced but never completely manufactured.

With the five requirements above, we are now ready to introduce the technical machinery to capture TPPs. We start by defining a notion of fragments of an n-pcycle which is extended to incorporate memory and which differentiates between controllable and uncontrollable transitions.

Definition 6. Tuple Τ = (G↪ g0↪An- ↪ δ′ ↪ δ′UN ) is an n-product of a production cycle Λ if (recall Λn- = (T↪ t0↪ An- ↪ δ)):

• G = T ×M is the set of Τ 's states, for some arbitrary finite set M, and g0 = ￿t0↪m￿ with m ∈ M is Τ 's initial state. The set M will be used to encode additional memory;
• δ′ ⊆ G×An- ×G is an arbitrary transition relation such

An n-product can therefore account for only some transitions of the corresponding n-pcycle (which means not every interleaving of the underlying production cycles are allowed), while extending it with additional memory (the set M) and distinguishing a subset of transitions as "uncontrollable".

• that if ￿t↪ c￿ a￿→￿t′ ↪ c′ ￿ in δ′ , then t a￿→t′ in δ; and · δ′UN ⊆ δ′ is arbitrary subset of transitions deemed "uncontrollable" and with the only requirement that if ￿t↪ c￿ a￿→￿t′ ↪ c′ ￿ ∈ δ′UN , then there exists another transition ￿t↪ c￿ a￿→￿t′ ↪ c′′ ￿ ∈ δ′UN such that c′ ≠ c′′ . ￿

n-products constrained to adhere to requirements R1-R5 form then the basis of our definition of TPPs. In particular, we need to make sure that by pausing a product item we do not violate either R2 or R5. Intuitively, this amounts to checking whether, whenever an item instance i is paused at a state g of TPP Τ , all actions available for i in g will be eventually available, i.e., manufacture of the item can be fully resumed. We do so in two steps. First, for any action a and instance i, we define all possible acyclic traces of Τ in which we either (i) resume the item (after a - sequence) by performing exactly a first; or (ii) not resume the item at all. This step is captured by the definition of a closure tree. Second, we check whether we are able to enforce one of the traces for (i), irrespective of the uncontrollability represented by transitions in δUN. This step is captured by the definition of controllable subsets.

1. aji = - for all 1 ≤ j < `, and either a`i = - or a`i = a; 2. no transition is taken more than once, i.e., for each gj and gq , if gj = gq then aj+1 ≠ aq+1 for 1 ≤ j↪ q < `;

Given a n-product Τ as above and a state g ∈ G, the closure tree in Τ for a component i ∈ {1↪ ▷ ▷ ▷ ↪n} and an action a ∈ A, denoted outΤ (g↪ i↪ a), is the set of all traces ⇡ = g0a1 g1a2￿a` g` of Τ , with t0 = t, such that:

1. for each 1 ≤ j < `, if there exists a transition ￿gj ↪a↪ g′ ￿ ∈ δ for some g′ and a with ai = a, then aj+1 i = a.

Informally, the closure tree outΤ (g↪ i↪ a) contains all possible finite traces of Τ , starting from g, such that (i) either it is never possible to execute a on the i-th component or only noop actions are allowed until a is executed; (ii) they are acyclic; and (iii) whenever a is executable on the i-th item instance at some step j of ⇡, then the next action vector aj+1 has a on the i-th component.

Definition 7. Given a set of traces ⇧ of an n-product Τ , the set of controllable subsets of ⇧ is the set contr(⇧) of subsets ⇧′ ⊆ ⇧ where, for each trace ⇡ = g0a1￿a` g` in ⇧′ , if for some 1 ≤ j ≤ ` we have ￿gj-1 ↪aj ↪ gj ￿ ∈ δUN, then there is in ⇧′ also a trace ⇡′ = g0a1￿aj g′j ￿ for every g′j ≠ gj with ￿gj-1 ↪ aj ↪ g′j ￿ ∈ δUN (at least one exists by definition of δUN).￿

Informally, a set of traces ⇧′ ∈ contr(⇧) is "closed" under uncontrollability of transitions: there is no trace with an uncontrollable transition at some step, unless all possible evolutions also appear in some trace.

Putting it all together, we use controllable subsets of the closure tree to verify that items paused in an n-product Τ can always be resumed, so satisfying R2 and R5. For any i, g and a, given the (unique) set of traces outΤ (g↪ i↪ a), then an element of contr(outΤ (g↪ i↪ a)) is a subset of outΤ (g↪ i↪ a) such that, by controlling only controllable transitions, we can force the resulting path to be in the subset, irrespective of the nondeterminism of δUN.

action vector a ∈ An iff bi = ai or bi = -, for each 1 ≤ i ≤ n. We now have all the elements necessary to define a target production process, i.e., the process we would like to deploy in the production plant.

Finally, we say that a vector b ∈ An- is subsumed by an

Definition 8. An n-product Τ = (G↪ g0↪An- ↪ δ′ ↪ δ′UN ) is an n target production process (n-TPP) for a production cycle Λ (of a given product recipe Ρ) if: (here Λn = (T↪ t0↪An ↪ δ))

1. ￿t↪m￿ b￿→￿t′′ ↪m′ ￿ exists with b subsumed by a; 2. for each i ∈ {1↪ ▷ ▷ ▷ ↪n}, if bi = - then there exists ⇧ ∈ contr(outΤ (￿t′′ ↪m′ ￿↪ i↪ai)) such that, for any g0 = ￿t′′ ↪m′ ￿ as above and for any trace ⇡ = g0c1 g1c2￿c` g` in ⇧ we have c`i = ai: whenever an action ai is not replicated (- is executed instead), then it is still possible to enforce a trace in Τ in which ai can be finally executed. ￿
2. Τ is an n-product of Λ; and · Τ is complete and fair wrt Λn , that is, for any state ￿t↪m￿ ∈ G and each transition t a￿→t′ in Λn :

Hence, an n-TPP is a system whose behavior is a subset of the behaviors of Λn- , but with possibly additional (bounded) memory. Note we do not require an n-TPP to be the "largest" such system (see later), only that it satisfies R1-R5.

As an example, consider Τ3 in Figure 4. It is easy to verify that it is indeed a 2-TPP of Λ, since for each trace ⇡ ∈ Λn there exists a trace performing the same actions on both product instances, and which can be extended to account for each possible future evolution of ⇡. For instance, we can perform β (resp. γ) actions on both instances, by pausing one at a time. Of course, other 2-TPPs for Λ exist. 4.1 Compositions and Production Controllers

Clearly, not any TPP is satisfactory for a given production plant. For instance, TPPs that cannot be "realized" (i.e., implemented) in the plant or that never take advantage of parallelism implicit in the plant's production resources, are not desired. Moreover, the TPP is not a problem input.

From now on, we will restrict ourselves to m-TPPs, where m is the number of behaviors (i.e., available machines) in Σ, as TPPs with more than m concurrent items will obviously never be implementable in a plant with m machines.

Following [De Giacomo and Sardina, 2007; De Giacomo et al., 2013] we first formally define what it means for a plant controller P to realize a given trace ⇡ of an m-TPP

Τ in a production plant system Σ: P is able to delegate each action in the vector (including "-" actions), at each step, to a suitable machine in the plant. For example, consider the trace ⇡ = AA ￿↵↪↵￿ ￿￿￿→XX ￿-↪β￿ ￿￿￿→XA of the TPP Τ3 from Figure 4 and plant Σ from Figure 2. Then ⇡ is realized in Σ by any controller P such that P(00↪ ￿↵↪↵￿) = ￿1↪ 2￿ and P(00 ￿↵↪↵￿ ￿￿￿→11 ￿-↪β￿ ￿￿￿→) = ￿2↪ 1￿, corresponding to one of the two traces 00 ￿↵↪↵￿￿1↪1￿ ￿￿￿￿￿→11 ￿-↪β￿￿2↪1￿ ￿￿￿￿￿→01 and 00 ￿↵↪↵￿￿1↪1￿ ￿￿￿￿￿→ 11 ￿-↪β￿￿2↪1￿ ￿￿￿￿￿→11 in Σ. Note, however, that while these traces can be extended in Τ3 with the action vector ￿β↪↵￿, this action vector can be replicated in Σ only from 11 and not from 01, so any trace of the form ⇡ ￿β↪↵￿

exists on a plant Σ, we say that Τ is realizable in Σ. Finally, because, unlike in behavior composition, the target production process is not an input to our parallel composition problem, we define the solution concept as a pair ￿Τ ↪ P ￿, such that Τ is an m-TTP for Λ and P a composition for Τ in Σ. We refer to these pairs as production controllers for Λ in Σ.

￿￿￿→￿ is not realizable. Then, again as in classical behavior composition, we say that P is a plant composition of a TPP Τ in Σ iff P realizes all the traces of Τ in Σ. When a composition for a TPP Τ

5 Largest Target Production Process

Production controllers may be evaluated against various metrics (such as average throughput, machine utilisation, load balancing, etc.) to isolate the most efficient ones. As metrics are highly dependent on the application and production plant, in this section we focus on computing production controllers ￿Τ ↪P￿ where Τ is the largest realizable production process, that is, which embody (i.e., can "mimic") all realizable production processes. It turns out such controllers can be defined in terms of the standard notion of simulation between transition systems [Milner, 1971], and in particular its nondeterministic variant [De Giacomo et al., 2013]: a target production process Τ simulates another target production process Τ ′ , denoted Τ ￿ Τ ′ , iff Τ can "replicate" every action of Τ ′ , step by step. The largest realizable production process for a given production cycle Λ and a production plant system Σ is threfore the m-TPP Τ for Λ that (i) is realizable

Λm- with the system Σ. Given a production cycle Λ, we define the enacted system Σ ∗Λ as the synchronous product of Λm- and the production plant system Σ, so that a state of Σ ∗Λ is a pair ￿t↪ s￿, where t a state of Λm- and s is a state of Σ. If ⇢∗ is the transition relation of Σ ∗Λ, then we use ⇢∗ND to denote the set of nondeterministic transitions of ⇢: s∗ a↪k ￿￿→s∗′ is in ⇢∗ND iff s∗ a↪k ￿￿→s∗′ and s∗ a↪k ￿￿→s∗′′ are in ⇢∗ , for some s∗′ ≠ s∗′′ . We also de-

in Σ; and (ii) can simulate any other realizable m-TPP Τ ′ . To capture property (i), we shall define our own notion of simulation between the production plant Σ and the mpcycle Λm, which expresses what it means for Σ to be able to "mimic" exactly m copies of the production cycle. Moreover, in order to synthesize the largest realizable m-TTP, we will also need to compute, as required by Definition 6, the set M encoding arbitrary memory and the set of uncontrollable transitions δUN. Crucially, both of these can be extracted from the so-called enacted system, capturing the joint execution of fine the notion of closure tree outΣ ∗Λ (s∗ ↪ i↪ a) for Σ ∗Λ as for n-product (see Section 4), and contr(outΣ ∗Λ (s∗ ↪ i↪ a)) is as in Definition 7, but this time with respect to transitions in ⇢∗ND . A subset in contr(outΣ ∗Λ (s∗ ↪ i↪ a)) is thus a set of traces of the enacted system Σ ∗Λ which can be enforced irrespective of the nondeterminism of the production plant system.

1. there exists a transition s b k ￿→s′ ∈ ⇢ and b is subsumed by

Definition 9. Given an m-pcycle Λm = (T↪ t0↪Am↪ δ) for some production cycle Λ, a lazy simulation relation of Λm by Σ = (S↪ s0↪Am- ↪ ⇢) is a relation σ+ ⊆ S × T such that ￿s↪ t￿ ∈ σ+ implies that for each a, if t a￿→t′ is in Λm then b↪k exist such that:

1. given t′′ , s′ and b as above, for each index 1 ≤ i ≤ n, if bi = - then there exists a set of traces ⇧ ∈ contr(outΣ ∗Λ (s∗ ↪ i↪ai)), for s∗ = ￿t′′ ↪ s′ ￿, such that for every trace s∗ c1 k1 ￿￿→￿t1 ↪ s1 ￿￿ c` k` ￿￿→￿t` ↪ s` ￿ of Σ ∗Λ in ⇧, we have (i) c`i = ai and (ii) ￿sj ↪ tj ￿ ∈ σ+ for j ≤ ` - the action ai can always eventually be performed in at least one controllable subset of traces in the enacted system, by visiting only states preserving σ+ . ￿
2. a- each ai is either replicated in bi or replaced by - ; (2) for each such s′ we have ￿s′ ↪ t′′ ￿ ∈ σ+ with t b￿→t′′ in Λm- any possible new system state s′ is in the relation with the state t′′ , which is unique; and

We say that a state s of Σ lazily simulates a state t of Λm, denoted s ￿ t, iff there exists a lazy simulation relation σ+ of Λm by Σ with ￿s↪ t￿ ∈ σ+. We say that Σ lazily simulates Λm, denoted Σ ￿ Λm, iff s0 ￿ t0. Then Σ ￿ Λm captures the fact that Σ can always replicate all actions vectors of Λm, but not in a step-by-step fashion, as some product instances may be paused. However, it guarantees the requirements discussed in Section 4.

Definition 10. Given Σ, Λm and Λm- as before, if Σ ￿ Λm then the maximal CG for Λm and Σ is the tuple Χ = (W↪w0↪Am- ↪ γ↪!) such that

Once the lazy simulation relation ￿ is computed, if Σ ￿ Λm, we can then build a finite state program, called the maximal controller generator (CG), that returns, at each step, the set of all possible action vectors that can be delegated to behaviors.

• W = {￿t↪ s￿ ∈ T × S ￿ s ￿ t} and w0 = ￿t0↪ s0￿; · γ ⊆W ×Αm × indx×W is such that ￿t↪ s￿ a k ￿→￿t′ ↪ s′ ￿ ∈ γ

Given the current state t of Λm and the current state s of the production plant system, the maximal controller generator returns the set of possible delegations, such that each member ￿a↪k￿ represents the delegation of each action ai to the behavior specified by ki. A production controller ￿Τ ↪P￿ is generated by Χ as follows:

• iff t a￿→t′ is in Λm- , s a k ￿￿→s′ is in Σ; and · ! ∶ W → 2(Am- × indx) is the controller function, defined as !(w) = {￿a↪ k￿ ￿ w a k ￿￿→w′ is in γ for some w′}. ￿
• Τ = (W↪w0↪Am- ↪ γ ′ ↪ γ ′UN ) is anm-TTP, and its transition relation γ ′ ∶ W ×Am- ×W is such that w a￿→w′ is in γ ′ iff ￿a↪ k￿ ∈ !(w);

γ ′UN is the subset of γ ′ defined as the set of transitions w a￿→w′ in γ ′ such that w a￿→w′′ is in γ ′ for some w′ ≠ w′′ : multiple transitions deriving from the existence of different available delegations of actions to behaviors (i.e. same a, different k) constitute controllable transitions, whereas multiple transitions deriving from the production plant system's nondeterminism (i.e. same a and k) will constitute uncontrollable transitions;

Τ is obtained by projecting out delegation indexes from transitions, while the corresponding composition P is obtained by selecting, at each step, for a given action a, a vector k such that a transition from the current state exists with label a↪k. Note that this means that the second component in W ⊆ T × S plays the same role of the arbitrary set M in Definition 6: for the same state in Λm, there may be more than one possible state in the production plant system Σ, as this is nondeterministic (e.g., states ￿11↪ AX￿ and ￿01↪ AX￿ in Figure 5).

• P is such that for any system history h = s0 a1 k0 ￿￿→￿ a` k` ￿￿→s` (with s0 = s0) and action vector a, if ￿s0↪ t0￿ a1 k1 ￿￿→￿s1↪ t1￿ a2 k2 ￿￿→￿ a` k` ￿￿→￿s` ↪ t` ￿ is in Χ for some t1￿t` , then P(h↪ a) = k only if ￿a↪ k￿ ∈ !(￿s` ↪ t` ￿).

Theorem 1. Let Χ be the maximal CG for Λm and Σ. Then (i) any P is a composition for Τ in Σ iff ￿Τ ↪P￿ is generated

(i) (⇐) P is a composition for Τ , i.e. it realises any trace ⇡ = t0 a1 ￿→￿ (recall t0 = t0). First, we show that for any history h` = s0 a0 k0 ￿￿→￿ a` k` ￿￿→s` in Η⇡↪P (s0 = s0) we have sj ￿ tj , for any 1 ≤ j ≤ ￿⇡￿ (for j = 0 this follows by Definition 10). By induction on `, h`+1 ∈ Η`+1 ⇡↪P is such that s` a`+1 k`+1 ￿￿￿￿￿→s`+1 is in Σ by definition, so ￿t` ↪ s` ￿ a`+1 k`+1 ￿￿￿￿￿→￿t`+1 ↪ s`+1 ￿ is in Χ, P(h` ↪a) = k`+1 , and from s` ￿ t` it follows that s`+1 ￿ t`+1 . Then, for any ⇡ and h ∈ Η⇡↪P as above with ￿h￿ < ￿⇡￿, by the definition of ￿ for any action a with t` a`+1 ￿￿→t`+1 in Τ , we have s` a`+1 k ￿￿￿→s`+1 in Σ. Further, assume Τ is not a m-TPP for Λ. Then by Definition 8, for some trace ￿t0↪ s0￿ b1 k1 ￿￿→￿ b` k` ￿￿→￿t` ↪ s` ￿ we have t` a￿→t′ in Λm such that either (1) no ￿t` ↪ s` ￿ b`+1 ￿￿→￿t`+1 ↪ s`+1 ￿ exists s.t. b`+1 is subsumed by a, or (2) there exists i s.t. bi = - and in every set ⇧ in contr(outΤ (￿t`+1 ↪ s`+1 ￿↪ i↪ai)) there is a trace ￿t`+1 ↪ s`+1 ￿ b`+2 ￿￿→￿ b`+q ￿￿→￿t`+q ↪ s`+q ￿ and b`+q ≠ ai. Then it is easy to see how this implies the same for every set ⇧′ in contr(outΣ ∗Λ (￿t`+1 ↪ s`+1 ￿↪ i↪ai)). Thus we exclude both (1)

by Χ and (ii) Τ is the largest realizable m-TPP for Λ in Σ. Proof. (Sketch) Let Η⇡↪P be the set of histories of Σ that may be obtained by running the controller P in Σ to match all the actions in a given trace ⇡ of an m-TTP Τ (see [De Giacomo and Sardina, 2007; De Giacomo et al., 2013]).

and (2) as they contradict s` ￿ t` . (i) (⇒) We prove that for any trace t0 a1 ￿→￿ a` ￿→t` of Τ and history h = s0 a1 k1 ￿￿→￿ a` k` ￿￿→s` ∈ Η`⇡↪P , if P is a composition for Τ then ￿t0 ↪ s0 ￿ b1 k1 ￿￿→￿ b` k` ￿￿→￿t` ↪ s` ￿ a k ￿→￿t↪ s￿ is in Χ for k = P(h↪a). If not, then ￿a↪k￿ ￿∈ !(￿t` ↪ s` ￿), and, by definition, either there is no s` a k ￿￿→s`+1 in Σ, no t a` ￿→t′ in Τ , by Χ. (ii) If Τ ′ ￿ Τ exists, then there exists a trace ⇡ such that last(⇡) b￿→t is in Τ ′ for some t, but last(⇡) b￿→t′ is not in Τ for any t′ . Since Τ ′ is realizable, there exists a composition P ′ s.t. h ∈ Η⇡↪P ′ where P ′ (h↪ b) is defined, and P(h↪ b) is not. So there is no trace ￿t0 ↪ s0 ￿ b1 k1 ￿￿→￿ b` k` ￿￿→￿t` ↪ s` ￿ in Χ, with s0 b1 k1 ￿￿→￿ b` k` ￿￿→s` = h and t0 b1 ￿→￿ b` ￿→t` = ⇡, s.t. ￿t` ↪ s` ￿ b k ￿→￿t↪ s￿ for some s and k, and t as above. Then by construction either s` ￿￿ t` or s ￿￿ t. ￿

or s`+1 ￿￿ t`+1 . In the first two cases P is not a composition. If the latter holds, it must be the case that in any trace ￿s`+1 ↪ t`+1 ￿ a`+1 k`+1 ￿￿￿￿￿→￿ condition (3) of Definition 9 does not hold, hence ￿Τ ↪P￿ is not a production controller generated

Computing the lazy simulation relation ￿ between Σ and Λm can be done by following the algorithm for the standard simulation relation ￿ in [De Giacomo et al., 2013], but checking the controllable closure tree at each step (Definition 9). An algorithm can be derived accordingly. Performance can be improved by reordering actions a according to indexes k in Σ so as to substantially reduce the number of transitions.

6 Conclusions

In this paper we consider the parallel behavior composition problem in a manufacturing setting, where many instances of a product are to be manufactured on a production line. We introduced a novel solution concept, target production processes, and showed how to generate the largest realizable TPP for a given production plant.

There are subtle conceptual and technical differences between the parallel behavior problem and classical behavior composition in the AI literature. In particular, multiple concurrent actions must be delegated to the available behaviors in the plant, rather than just one. We note that this is not the same as multiple behavior composition [Sardina and De Giacomo, 2008], in which several target modules are realized in the same shared available system. Multiple behavior composition is equivalent to realizing Λm- , which we argue is overly demanding. Moreover, the target desired module is not given as an input to the problem, but is part of the solution constructed from the specified production recipe and plant.

Our work is just the first step in manufacturing composition. We have defined the problem, and provided a notion of "adequacy" for solutions in the form of TPPs that respect requirements R1-R5. Further work is needed in order to refine m-TPPs to "efficient" manufacturing processes, for example, with respect to average throughput, machine utilization, load balancing, etc. Such optimizations can be done after the TPP has been built, or possibly during synthesis by discriminating between controllers from individual lazy simulation relations σj+. Another avenue we are interested in pursuing, is linking our parallel composition problem with the composition of high-level programs [Sardina and De Giacomo, 2009], at least from a representational perspective.

Acknowledgments

We thank the anonymous reviewers for their helpful feedback. We acknowledge the support of the Australian Research Council (under DP120100332) and the RMIT Foundation (under an International Visiting Fellowship for the second author to visit RMIT University).