AI planning and verification for Industry 4.0

Industry 4.0 will run on close collaborations between autonomous robots and humans. These tasks will typically be governed by extended planning and coordination mechanisms that adhere to strict timings, but uncertainties in deployments, such as delays in operations, unplanned failures or human intervention can lead to deviant unsafe states. While planning, monitoring and controlling robotic agents it’s possible to a achieve a level of granularity, but the participation of humans and movable objects adds a layer of uncertainty to deployments.  

This is of particular significance in the cobot case: where robots and humans collaborate in a coordinated manner. These deviations trigger violations of safety properties in human and multi-robotic agent scenarios, mandating further verification and control during execution. Onboard sensors and hard faults are possible solutions in some cases, but they can prevent tasks from being completed and require repeated manual intervention. Tasks that are deadline driven require further analysis and verification of deployments, to prevent repeated interruptions.

Here, we propose a framework for generating flexible temporal plans that can satisfy safety properties during execution called FLATPACK (flexible temporal planning, verification and controller synthesis). Temporal plans are translated to timed-game automation models for model checking verification and analysis prior to dispatch. Using the strategy synthesis engine, it’s possible to execute controlled plans that are resilient to temporal deviations.

This ensures that despite deviations in human performance, the cobots can still complete global tasks without the need for elaborate re-planning. This is a winning strategy for the plan control dispatcher, as it ensures deadlocks are avoided with only minor adjustments to the speed of operations. These aspects are demonstrated over an Industry 4.0 warehouse use case involving multiple autonomous robots with synchronized planning and executions.

Scenario: multi-robot and cobot interaction

Consider the following multi-robot and human coordination example in Figure 1, which might typically be seen in warehouse logistics. Robot 1 (initial position A1) and Human 2 (initial position B1) must pick objects from their starting positions and drop them off midway. Robot 1 and Robot 2 then make their way to their final goal positions of E1 and E2, respectively. The dropped objects are collected by Robot 3 (initial position A5) and Robot 4 (initial position C4) to drop them off at goal locations of Object 1 (goal position E5) and Object 2 (goal position E6). The values provided in Figure 1 represent the time to complete movement tasks (this can be expanded to include distances and robot speed). No two robots or humans may be at the same grid position simultaneously. This represents a task typically observed in warehouse logistics, where human and robotic participants coordinate to complete the task.

Figure 1: warehouse cobot coordination scenario: orange areas are initial positions, green areas are final positions, grey areas are shared movable positions and red areas are forbidden positions.

If any of the robots or humans reach a grid location before/after the planned time, it results in deadlocks/livelocks. This must be avoided by carefully controlling the dispatch of actions via the plan dispatcher. Robot deviations can also pose safety hazards to humans and must be avoided. The demonstration of deadlocks due to slight temporal deviations in execution is particularly interesting. Absence of deadlocks must be verified in safety critical applications, to ensure harmful states are always avoided, irrespective of deviations in executions. This verification cannot be done at plan time, as execution deviation and uncertainties occur closer to deployment.

Note: in this example we assume the robots and humans follow individual temporal plans and do not coordinate/communicate during execution. This is needed to ensure scalability and disassociate the need for a central coordinating agent.

Deadlocks and the need for temporal plan verification

In order to plan and schedule individual actions we use the Planning Domain Definition Language (PDDL) 2.1 to generate optimal plans with help from AI. The problem is specified in PDDL with objects, states, initial conditions and goals as described in Figure 1. The objective is to complete the task while minimizing delays.

This problem may be solved via conventional AI planning solvers to extract individual human and cobot plans (example below). Note that parallel movement of all cobots and humans are allowed, with durations of individual move, pick and drop actions set at 10-time units. The plan is decomposed to generate individual temporal plans for Human 2 and Robot 3 that run concurrently.

Plan for HUMAN2:

 0.0000: (PICK HUMAN2 OBJECT2 B1) [D:10.00; C:0.10]

 110.0000: (MOVE HUMAN2 B1 B2) [D:10.00; C:0.10]

 120.0000: (MOVE HUMAN2 B2 B3) [D:10.00; C:0.10]

 130.0000: (MOVE HUMAN2 B3 B4) [D:10.00; C:0.10]

 140.0000: (DROP HUMAN2 OBJECT2 B4) [D:10.00; C:0.10]

 150.0000: (MOVE HUMAN2 B4 C4) [D:10.00; C:0.10]

 160.0000: (MOVE HUMAN2 C4 C3) [D:10.00; C:0.10]

 170.0000: (MOVE HUMAN2 C3 D3) [D:10.00; C:0.10]

 180.0000: (MOVE HUMAN2 D3 D2) [D:10.00; C:0.10]

 190.0000: (MOVE HUMAN2 D2 E2) [D:10.00; C:0.10]

Plan for ROBOT3:

 0.0000: (MOVE ROBOT3 A5 B5) [D:10.00; C:0.10]

 160.0000: (MOVE ROBOT3 B5 B4) [D:10.00; C:0.10]

 170.0000: (PICK ROBOT3 OBJECT2 B4) [D:10.00; C:0.10]

 180.0000: (MOVE ROBOT3 B4 B5) [D:10.00; C:0.10]

 190.0000: (MOVE ROBOT3 B5 C5) [D:10.00; C:0.10]

 200.0000: (MOVE ROBOT3 C5 D5) [D:10.00; C:0.10]

 210.0000: (MOVE ROBOT3 D5 D6) [D:10.00; C:0.10]

 220.0000: (MOVE ROBOT3 D6 E6) [D:10.00; C:0.10]

 230.0000: (DROP ROBOT3 OBJECT2 E6) [D:10.00; C:0.10]

 240.0000: (MOVE ROBOT3 E6 E5) [D:10.00; C:0.10]

Once the individual agents’ plans are generated, the warehouse controller typically dispatches them assuming the temporal specifications guarantee avoidance of unsafe situations. However, there are repeated instances where the executions deviate slightly from the plan timeline which will lead to unintended outputs.

An example is given in Figure 2 where a ±10 time unit deviation in each action results in multiple deadlocks in the cobot human example. This is especially probable with human participants who may get distracted or fatigued during plan execution. Let’s take the interaction between Human 2 and Robot 3 as an example.

Human 2 is scheduled to reach B4 at 140 time units but gets delayed. At timestamp 150, both Human 2 and Robot 3 attempt to get to B4, which results in a deadlock / unsafe condition. The entire plan has to be aborted in this case, which can cause significant delays and hazards. This is a problem seen in multiple instances in Figure 2.

Figure 2: deadlock and unsafe conditions due to temporal deviations

As a result, it’s crucial to formally model and verify the deployed plans to ensure that  executions happen in a safe manner despite fluctuations in the intended timelines.

The FLATPACK system explained

In order to verify and control plans before dispatch, plan transformation into formal models and runtime control rules are needed. For this, we propose using the FLATPACK framework. The overall architecture of the framework is presented in Figure 3. Prior to dispatch of the temporal plan to the robot nodes, the plan is verified to guarantee safety properties in the dispatched actions. The dispatch controller may also choose to add controlled delays between task steps to ensure the deployed actions do not violate the required safety properties.

Figure 3: FLATPACK system for flexible temporal planning, verification and controller synthesis

Fig. 3 comprises of the following main modules:

Planning module: the temporal planner (1) takes the inputs from the domain request and the problem goal request to generate an optimal timing plan. Additional goal details may be incorporated in the planning environment (such as minimizing robot battery usage). This output plan is then decomposed by the plan decomposer (2) to multi-agent plans, that may run on individual robots. Note that this entails concurrent actions with timing constraints incorporated.

Plan verification and strategy synthesis module: the generated multi-agent plans are input to the Uppaal-Tiga model translator (3), that generates timed game automata models with states, transitions and timing guards correctly mapped to the individual plans. The automata models are then appended with realistic timing deviations (jitter) in the Uppaal-Tiga model update (4). The updated model is then verified with property verification (5), with alternate strategies proposed in case the properties are not satisfied. The specific controller strategy chosen to be deployed is then synthesized (6) to a format specified for deployment. This model also contains information about the zones that may be controlled, with additional delays or constraints incorporated.   

Deployment execution module: the generated plans and control strategies are sent to the dispatch controller (7). The ROS nodes and action lib modules perform the execution (8) on the robots in the warehouse. The execution monitor (9) logs the execution output – in case the recorded temporal deviations exceed the planned strategies, a re-run of steps (4) to (8) may be required.

Verification and controller synthesis

In order to study the individual robotic plans, we use the models presented in Figure 4 that consist of timed game automata generated from the individual temporal plans. Note that we make use of controllable actions (bold transitions) and uncontrollable actions (dotted transitions) as part of the timed game automata. The controller has precedence in the controllable actions as against the environment having precedence in uncontrollable actions. The controller continuously observes the system (moves and delays). The controller can then take the following actions: (i) wait (delay actions) (ii) controllable move (iii) preventing delay with a move.

In our example in Figure 4, Robot 1 and Human 2 are chosen to have only uncontrollable transitions; Robot 3 and Robot 4 have a few controllable transitions. The objective is to still satisfy safety properties despite deviations in the uncontrollable transitions in cobots and humans.

Figure 4: timed game automata model for multi-robot coordination with temporal drifts

In order to study the effect of deviations in plan times, we introduce additional deviations in state/action transitions by up to ±10 time units. This produces automata in Figure 4 with overlapping timelines that were not intended at plan time. For instance, the transition out of the Move_A5_B5 state is enabled in the range [0, 20].  Note that these automata only have a few controllable regions in Robot 3 and Robot 4. We would like to control these transitions so that properties are maintained during execution. The robots and humans should avoid collisions and deadlocks, despite the temporal deviations. This also minimizes the number of controllable transitions that are monitored and controlled by the FLATPACK system.

The objective is to generate a strategy for the dispatcher so that the following property Strict Reachability with Avoidance (Until) is satisfied in Uppaal-Tiga (other properties such as strict reachability and weak reachability may also be verified similarly): 

The above control properties prevent three occurrences of deadlocks/collisions until the goal is reached. Uppaal-Tiga generates the following winning strategy. Given the relative states of the robots and observed clock values rules are generated to takes transitions for Robot 3 and Robot 4. These rules, when followed, will ensure ''winning'' against uncontrollable environmental conditions – maintaining the temporal ordering of robot events.

Figure 5: plan strategy with uncontrollable transitions temporal drifts of ±10 units, optimal controllable zones

In order to visualize the outputs of the original timed plan and the generated strategies, we make use of timed message sequence charts (MSC) in Figure 5. The vertical lines in the timed MSC model represent instances of entities that participate in the message passing. A message is denoted by an arrow from the sending instance to the receiving instance. The messages are labeled, with the task actions that are to be performed. The messages are ordered according to the timelines specified in the temporal plan. Time stamps are provided for individual actions, with timers t1, t2, t3, t4 initialized. Dotted time measurement vertical lines are used to measure events at different temporal levels. A slanted transition in implies the range of time during which the transition may occur.

In Figure 5, through the monitoring and control of the controllable transitions, the system can ensure that the properties are maintained despite temporal deviations. Through the judicious use of controllable zones, with just 37 rules, the interactions between robots and humans are ensured to be safe and verified.

Optimal controller zones

Another important aspect to consider is the complexity of the control strategy that is generated. As these are rules on relative states and clock values of multiple agents, increasing the number of rules would imply additional complexity to the controller (number of rules to be monitored and enforced). As the proposed system is envisioned to reduce the overhead of heavy uncertainty planning or runtime re-configurations (without the need for central control/coordination), it is important to analyze the tradeoffs between the choice of controllable robots and the number of rules generated by Uppaal-Tiga.

Figure 6: number of control rules vs. control zones

We begin by analyzing Figure 6, which demonstrates the number of control rules for varying numbers of controllable transitions in the timed automata from Figure 4. The minimum number of rules are generated using our algorithm, followed by an increase if random transitions are added. We see a 150 percent increase in the number of rules if Robots 1 and 3 are made controllable. In order to reduce the overhead on monitoring and enforcing a high number of control rules, a systematic approach must be taken to generate the controllable transitions effectively.

Figure 7: (a) optimal / worst-case strategy times for increasing control rules (b) per plan state temporal drifts against control rules

With an increase in the amount of temporal drifts per state, we notice an increase in the number of control rules in Figure 7 (b). For instance, with drifts of ±10 time units, the optimal control zones provide 37 rules; if this is increased to ±20 time units, the number of rules increases to 98. This also causes a deviation in the best case and worst-case execution times as shown in Figure 7 (a). With 100 control rules (corresponding drift of ±20), the scenario time ranges lie between 230-270. Similarly, for 510 control rules (corresponding drift of ±40), the scenario time ranges lie between 210-290. These tradeoffs must be taken into account before categorizing the drifts that can be handled via execution side strategy synthesis vs. temporal re-planning from current states.

The FLATPACK system provides increased robustness to Industry 4.0 deployments by analyzing temporal plan deviations, verified properties and optimal controller synthesis.

Conclusions

Integration of automated planning and execution into environments such as Industry 4.0 logistics requires careful analysis of temporal constraints. In particular, it is important to analyze the drifts that may creep into plan executions and the cascading effects on safety and liveness properties. At the artificial intelligence research area of Ericsson research, we have introduced the FLATPACK system, that makes use of timed game automata models to synthesize alternate strategies to combat these challenges.

Learn more

Read the SCOTT Horizon 2020 project final deliverable that further elaborates this work, available on the SCOTT website.

Read our blog post about cobots and the future of manufacturing.

Explore Industry 4.0 solutions.

Learn more about connected and smart factories.