Situation Calculus for Controller Synthesis in Manufacturing Systems with First-Order State Representation (Extended Abstract)

1 Introduction

In the manufacturing as a service (MaaS) paradigm, manufacturing infrastructure is shared on-demand by a potentially large number of different manufacturing processes. The cost of managing and maintaining the manufacturing infrastructure is thus distributed across all customers, enhancing resource utilization and reducing unit production costs. Different manufacturing models have been proposed in the literature to achieve the MaaS vision, with an emphasis on flexibility, scalability, adaptability and customization, and the increased use of automation and data and knowledge sharing through the supply chain. In this paper, we focus on Cloud Manufacturing [Xu, 2012; Lu et al., 2014]. Enabled by an recent developments in information technology, IoT, embedded systems and cloud computing technologies, Cloud Manufacturing is an advanced MaaS paradigm and business model in which manufacturing resources, such as Computer Numerical Control (CNC) machines and robots, are packaged as abstract descriptions of manufacturing capabilities, then advertised and made available to customers through a cloud platform. Similarly, the abstract manufacturing tasks required to manufacture a product are specified as abstract, systemindependent processes that need to be matched against the abstract capability descriptions offered by manufacturing facilities in the cloud. This allows the creation of dynamic production lines on-demand, in a pay-as-you-go business model.

∗This paper is an abridged version of [De Giacomo et al., 2022].

In mass production, the process planning phase, which transforms a process specification into a process plan specifying concrete production schedules for the resources on the shop floor, is carried out by manufacturing engineers, and is largely a manual activity. This is not feasible in MaaS, where manufacturing facilities must be able to automatically synthesize process plans for novel products 'on the fly'. This requires matching the abstract manufacturing tasks in the process recipe-the specification of how the product is to be manufactured-against the available manufacturing resources in the facility. The resulting process plan details the low-level tasks to be executed and their order, the resources to be used and how materials and parts move between them [Groover, 2007]. The process plan controller, i.e., the control software that delegates each operation in the plan to the appropriate manufacturing resources, is then synthesized.

Research in AI and Computer Science can be exploited to provide a mathematical foundation for these domain concepts, and to solve the core challenges implicit in the MaaS vision. Recent work on MaaS based on fundamental ideas from the literature on service composition in CS and behavior composition in AI [De Giacomo et al., 2013], has shown how the requirements and techniques for the automated synthesis of process plan controllers can be formalized [de Silva et al., 2016; Felli et al., 2016; Felli et al., 2017; De Giacomo et al., 2018; De Giacomo et al., 2019]. While these approaches have proven fruitful for developing 'proofof-concept' MaaS implementations, they are based on a propositional description of states, which is often too idealized. In many cases, manufacturing processes depend on the objects and data they produce and consume, and in general an unbounded number of product items or basic parts may be produced. This requires a rich, relational description of states, an information model, and computational techniques able to manipulate such representations. Although some work exists that provides a basis for an unambiguous description of the manufacturing concepts [Gr¨uninger and Menzel, 2003], the scientific literature has been lacking.

We propose a relational representation of states by drawing on research on reasoning about actions in AI. Operations in manufacturing processes are described by an action theory in logic, and manufacturing processes are formalized as high-level programs over such action theories. In this way, we leverage the first-order state representations of action formalisms and the second-order/fixpoint characterization of state-change as provided by programs. Critically, we do not rely on ad-hoc representations; instead we encode information models and how they change as the result of actions in the Situation Calculus. Process recipes and manufacturing resources, in turn, are modeled as high-level ConGolog programs [Levesque et al., 1997] (over the action theories). Moreover, we deal with multiple Situation Calculus theories simultaneously, so as to model process recipes working over both an abstract information model and a concrete, facilitylevel information model. This yields a principled, formal and declarative representation of the MaaS setting.

By exploiting this rich representation, we formally define what it means to realize a process recipe in a manufacturing facility, and present techniques to automatically synthesize controllers that implement those realizations. We show that these techniques correspond to algorithms for extracting the actual controllers when the resulting Situation Calculus action theories are state-bounded [De Giacomo et al., 2016a]. In our context, state-boundedness means that, while the facility may process an infinite number of objects overall, an unbounded number of objects is never "accumulated", i.e., in any given state the number of objects being processed does not exceed a given bound. This is the typical case in practice: the number of objects handled at a given time by a facility is naturally bounded by the size and structure of the shop-floor.

We stress that, independently of the application domain we consider, we provide here the first decidability result for controller synthesis in a setting with a relational/first-order state representation. While our approach is based on the Situation Calculus, our results and constructions can also be applied in other frameworks for reasoning about actions in AI as well as data-aware/artifact-centric frameworks in databases [Hariri et al., 2013; Deutsch et al., 2018].

While this paper illustrates the main elements of our framework and the main results, the complete details can be found in the full paper [De Giacomo et al., 2022].

2 Manufacturing as a Service in SitCalc

A basic action theory (BAT) [Reiter, 2001] is a collection of axioms D describing the initial situation, preconditions and effects (and non-effects) of actions on fluents, as well as axioms for unique name assumptions and domain closure for the countably infinite object sort ∆, for which we assume unique names and domain closure [Levesque and Lakemeyer, 2001; Sardina et al., 2004]. Employing standard names for objects, we fix a single interpretation domain for models of situation calculus formulas and blur the distinction between such names and domain objects.

Manufacturing activities are modeled as action types, each taking a tuple of objects as arguments. For example, DRILL(part, dmtr, speed, x, y, z) represents the action of drilling a hole of a certain diameter, with a certain spindle speed, in a specific position of a given part.

Since we are concerned with operations that may occur simultaneously [Reiter, 2001; Bornscheuer and Thielscher, 1996; Baral and Gelfond, 1993], we adopt the concurrent, non-temporal variant of the Situation Calculus, where a compound action a is a set of simple actions that execute simultaneously [Reiter, 2001, Chapter 7]. E.g., {ROTATE(part, speed), PAINT(part, color)} represents the joint execution of rotating a part while spraying paint on it.

Axioms are used to specify preconditions and effects of sets of actions, thus offering complete control in modeling manufacturing facilities and allowing the expression of arbitrary constraints on the available resources. For example, two robots may be allowed to lift a heavy object only at the same time, while they might be prevented (by their respective theories) from doing so individually.

A(x) denotes the compound action type A with parameters x. Action instance a has precondition axioms and successor state axioms of the form Poss(a, s) ≡ φ(a, s) and f (x, do(a, s)) ≡ φ(x, a, s), with φ(a, s) and φ(x, a, s) uniform in the current situation s. We assume complete information on the initial situation S0 , which makes our BATs categorical, i.e., admitting a single model [Reiter, 2001; Sardina et al., 2004]. Observe that, although unique, the BAT model has an infinite object domain, as well as infinite situations, which makes it nontrivial to deal with, and requires a substantially different approach to that adopted in model checking [Clarke et al., 1999; De Giacomo et al., 2016a; Calvanese et al., 2018].

2.1 ConGolog High-level Programs

Several high-level programming languages have been proposed based on the Situation Calculus, including Golog [Levesque et al., 1997], which supports both standard programming and nondeterministic-choice constructs, ConGolog [De Giacomo et al., 2000], which extends Golog with concurrency, and IndiGolog [Sardina et al., 2004], which supports interleaved planning and execution. We specify manufacturing processes as programs in a variant of ConGolog without recursive procedures [De Giacomo et al., 2000] and where the test construct yields no transition and is final when satisfied [Claßen and Lakemeyer, 2008; De Giacomo et al., 2010]. This results in a synchronous test construct in which interleaving is disallowed (every transition involves the execution of one action).

All standard ConGolog constructs are allowed: simple/compound actions a, test ϕ?, sequence δ1; δ2, nondeterministic branching δ1 | δ2, nondeterministic argument choice πx.δ, nondeterministic iteration δ∗ , conditional constructs, while loops, and interleaved concurrency δ1∥δ2. A program δ is executed over a BAT D, which must include the fluents and the constants mentioned in δ, with the latter coming from the set ACD of D's active object constants. A configuration is a pair ⟨δ, s⟩ with δ a program and s a situation. ConGolog's semantics is specified in terms of single-steps, using predicates Final(δ, s), which specifies when a configuration ⟨δ, s⟩ is final (i.e., δ may terminate in s), and Trans(δ, s, δ′ , s′ ), which specifies the one-step transition from ⟨δ, s⟩ to ⟨δ′ , s′ ⟩, where δ′ remains to be executed [De Giacomo et al., 2000].

The definitions of Trans and Final for the ConGolog constructs above are standard, but, as discussed earlier, cannot express simultaneous execution of compound actions. To address this, we extend ConGolog with the synchronized concurrency operator δ1|||δ2, which states that programs δ1 and δ2 execute concurrently and synchronously, i.e., their next actions take place in the same transition step. The semantics is as follows: Final(δ1|||δ2, s) ≡ Final(δ1, s) ∧ Final(δ2, s) and Trans(δ1|||δ2, s, δ′ , s′ ) ≡ Trans′ (δ1, s, δ′1 , s′1 ) ∧ s′1 = (a1, s) ∧ Trans′ (δ2, s, δ′2 , s′2 ) ∧ s′2 = (a2, s) ∧ Poss(a1 ∪ a2, s) ∧ δ′ = (δ′1 |||δ′2 ) ∧ s′ = (a1 ∪ a2, s). Informally, Trans′ is the same axiom as Trans, but it only requires the executability of compound actions, without requiring the executability of (subsets of) their component simple actions. Indeed, we state Poss(a1 ∪ a2, s) but not Poss(a1, s) or Poss(a2, s). As a result, a number of sub-systems (manufacturing resources) can legally perform a joint step only if this is explicitly stated to be possible by a "global" BAT for compound actions (the BAT for the entire facility, see the next section). This gives great flexibility when modeling manufacturing facilities. Note that synchronized concurrency is not reducible to interleaved concurrency: δ1∥δ2 allows either δ1 or δ2 to be executed completely before starting the other, and for them to be executed alternately.

2.2 Manufacturing as a Service

A product can be manufactured if an implementation of all the possible sequences of resource-independent operations prescribed by the recipe, together with any additional lowlevel operations (not included in the recipe) required by the implementation, can be delegated step-by-step to the facility resources. Recall that process recipes are resourceindependent, i.e., specified without knowing the actual manufacturing system that will be used for their realization, but assuming only an information model common throughout the cloud. When a product is manufacturable in a facility, a controller responsible for delegating recipe actions to facility resources can be synthesized.

The resulting MaaS framework, shown in Figure 1, includes two sorts: (i) Information models, i.e., BATs D describing the data and physical objects processes manipulate and the operations to manipulate them; and (ii) Processes, i.e., programs δ0 R describing the specific capabilities and dynamics of components.

The framework comprises the following components (for simplicity, we restrict to the case of one facility in the cloud). (i) Resources: the facility manufacturing resources. Each resource is a pair ⟨Di, δi⟩, with information model Di and resource process δi. (ii) Facility information model: the information model DF obtained by combining the BATs Di of each resource on the shop floor, see the paper for details. This includes specifying the executability of compound actions (see Sec. 2.1). (iii) Facility process: the process δ0 F := δ1||| · · · |||δn, specifying the synchronous execution of the resource processes (synchronous concurrency allows different resources to execute actions at the same time). (iv) Cloud information model: the common resource-independent information model DR assumed by all recipes, representing the data and objects recipes manipulate. (v) Mappings: a set of mappings, Maps, relating the resource-independent cloud information model DR to the resource-dependent facility information model DF. Maps relates the abstract executions described by the process recipe δ0 R (see below) to the concrete executions of the facility process δ0 F . Adopting ideas from [Banihashemi et al., 2017], two forms of mappings are used. (1) For each fluent f in DR with parameters x, the atomic formula f (x, sR) is mapped to a (uniform) formula φf (x, sF) over the fluents in DR. This formula is domainindependent: its evaluation depends only on the objects occurring in the extension of DF's fluents in the current situation. Moreover, a subset Obs of DR's recipe fluents act as observations: they have no successor-state axiom and their extension is provided by Maps. For fluents not in Obs, Maps imposes a consistency requirement between the two theories. (2) For each action type A ∈ AR with parameters x, we map A(x) to a (arbitrarily complex) program δA(x) for DF which makes use of (compound) actions of the available resources. The combination of Maps with DR and DF produces a new theory DMaps R , which is not a traditional Situation Calculus theory, as it includes two completely independent situation sorts (instead of one): SF for the facility information model DF, with initial situation S0 F ∈ SF, and SR for the cloud information system DR, with initial situation S0 R ∈ SR. For how to obtain DMaps R , see the paper. (vi) Facility: a manufacturing facility is a tuple Fac = ⟨DR,DF, δ0 F ,Maps⟩, with cloud information model DR, facility information model DF, facility program δ0 F , and mappings Maps. (vii) Recipe: a resourceindependent process δ0 R over the cloud information model DR, describing the process to execute to manufacture a product. (viii) Controller: when the product is manufacturable, the controller is responsible for orchestrating the resources. Informally, it is a function relating each execution of the recipe δ0 R to an execution of the facility process δ0 F .

Given a facility Fac and a recipe δ0 R , the manufacturability problem amounts to establishing whether there exists a controller to orchestrate the resources in the Fac to realize δ0 R . The controller synthesis task is to automatically build the controller responsible for implementing the orchestration.

3 Controller Synthesis

In order to formalize when a recipe can be realized by a facility, we introduce three properties relating recipe and facility configurations ⟨δR, sR⟩ and ⟨δF, sF⟩. (i) Mappings' preservation: the value of every non-observation fluent f ̸∈ Obs of DR in ⟨δR, sR⟩ is compatible, through the mapping f (x) ↔

φf (x) in Maps, with the value of φf (x) in ⟨δF, sF⟩. For every f ∈ Obs, the mapping is respected. (ii) Legal termination: Final(δR, sR) implies Final(δF, sF), i.e., if the recipe can legally terminate, so can the resources. (iii) Recipe actions realizability: for every abstract action A(x) in the recipe executable in ⟨δR, sR⟩, there exists a program δA(x), determined through the mapping A(x) ↔ δA(x), that is executable in its entirety from ⟨δF, sF⟩ to some ⟨δ′F , s′F ⟩, representing the complete implementation of A(x) in the facility. This captures the synchronization of the recipe and facility situations: the recipe situation do(A(x, s′F ), sR) resulting from the execution of A(x) in sR depends on the new situation s′F reached by the facility after the execution of δA(x).

Realizability of a recipe by a given facility can be formalized by co-induction, by defining the largest realizability relation ⪯ between facility and recipe configurations that satisfies the three requirements above, and such that whenever the recipe executes an action and the facility executes a corresponding program through the mappings (see third point), the new situations are still in ⪯. Details are in the paper.

Definition 1 (Realizability). A recipe δ0 R is realizable by a facility Fac = ⟨DR, DF, δ0 F ,Maps⟩ iff ⟨δ0 R , S0 R ⟩ ⪯ ⟨δ0 F , S0 F ⟩. ■

Definition 2 (Controller). Given a facility Fac = ⟨DR, DF, δ0 F ,Maps⟩ and a recipe δ0 R realizable by Fac, a controller for δ0 F that realizes δ0 R is a function ρ that, given two configurations ⟨δR, sR⟩ and ⟨δF, sF⟩ such that ⟨δR, sR⟩ ⪯ ⟨δF, sF⟩, an action A(x), and a program δ′R such that Trans(δR, sR, δ′R , (A(x, S0 F ), sR)) (here S0 F is used as a placeholder, and does not affect δ′R ), returns a sequence of facility configurations ⟨δ0 F , s0F ⟩ . . . ⟨δm F , smF ⟩, such that:

• Trans(δiF , siF , δi+1 F , si+1 F ) for i ∈ [0,m-1], and δ0 F = δF and s0F = sF, i.e., the sequence is executable in Fac;
• Do(δA(x), sF, smF ): the situation smF is the result of executing the program δA(x) corresponding to A(x) in sF;
• ⟨δ′R , (A(x, smF ), sR)⟩ ⪯ ⟨δm F , smF ⟩, that is, realizability between the resulting programs is preserved. ■

Do(δ, s, s′ ) abbreviates ∃δ′ . Trans∗ (δ, s, δ′ , s′ )∧Final(δ′ , s′ ), which states that the complete execution of δ from s results in s′ [Levesque et al., 1997; De Giacomo et al., 2000].

To check realizability, we define a two-player game between ENVIRONMENT (the antagonist) and CONTROLLER (the controller), which is played over a game arena (GA) T , i.e., a labelled transition system over the vocabulary of fluents and constants from the active domain. The states of the arena are partitioned (using two propositions turnEnv and turnCtrl) so that in each state only one player can move. The state labeling of the GA holds all the information about the (current) configurations of the recipe and facility. Technically, this requires decoupling the "data" from the control-flow, i.e., the program counter [De Giacomo et al., 2016b]. Having adopted standard names, program counters and actions can then be treated as active constants and objects.

Intuitively, the game proceeds as follows: ENVIRONMENT selects an action A(x), together with the corresponding program δA(x), from those made available by the recipe δR (initially δ0 R ) in the current configuration; ENVIRONMENT then advances the recipe configuration and the cloud situation sR of DMaps R and finally passes the turn to CONTROLLER, which chooses one among the actions that are currently legal for both δF (initially δ0 F ) and δA(x) in their current configuration. A step in δA(x) is thus executed, and CONTROLLER aligns the current cloud situation sR with the resulting factory situation s′F (since the interpretation of DR's non-observation fluents is not affected by the DF's situation argument in A). Then, CONTROLLER can (but does not have to) pass the turn to ENVIRONMENT only when δ has reached a final configuration.

The paper shows that a realizability relation between δ0 R and δ0 F exists iff T satisfies the µ-calc (in fact, µLc) formula:

where, informally, ϕOK holds in those states q of T where: (i) the interpretation of every fluent f ∈ FR \Obs in the labeling of q matches the interpretation of the corresponding formula φf over the same labeling; (ii) it is ENVIRONMENT's turn; and (iii) if the recipe may terminate, so can the facility. ΦReal is true in all those states from which CONTROLLER can force the game to visit infinitely often a state where ϕOK holds, no matter how ENVIRONMENT plays. ΦReal also requires that CONTROLLER does not pass the turn until ϕOK holds.

The set Win(ΦReal) of winning states is the set of states where ΦReal holds, so the objective of CONTROLLER is to maintain the game within such a winning region. When CONTROLLER has a (memoryless) winning strategy, i.e., a function mapping each T state into a new state (i.e., a game move, corresponding to a facility action execution) from the winning region, a controller can be computed.

Theorem 1. Given a facility Fac = ⟨DR,DF, δ0 F ,Maps⟩, a recipe δ0 R over DR is realizable by δ0 F iff q0 ∈ Win(ΦReal).

The paper shows how to extract a controller from the set Win(ΦReal) of winning states.

4 Bounded Case: Decidable Synthesis

The paper analyzes the case of practical interest where the facility and the recipe induce a GA T that is both state-bounded and generic. As explained in Section 1, the former property requires state-boundedness of both DR and DF, as well as of all DR's observation fluents. The latter, which is implied by the use of BATs, requires that, whenever two states are isomorphic, they yield the same transitions modulo the same object renaming induced by the isomorphism.

Theorem 2. Given a facility Fac = ⟨DR,DF, δ0 F , Maps ⟩ such that DR and DF are bounded, and a recipe δ0 R that is realizable by Fac, there exists a controller for δ0 F that realizes δ0 R and is effectively computable.

We prove that, given a generic, state-bounded GA T , there exists a finite-state GA ¯ T (used as faithful abstraction) such that, for every µLc formula Φ, T |= Φ iff ¯ T |= Φ. Hence we can model-check ΦReal on ¯ T rather than on T . Finally, we show a constructive way of transforming a memoryless strategy as above into a controller for δ0 R that realizes δ0 F .

5 Conclusions

In this paper we illustrated all the main ideas and results of our approach for the synthesis of controllers for manufacturing systems in the Situation Calculus. Details can be found in [De Giacomo et al., 2022].