Reconfigurability in Reactive Multiagent Systems

1 Introduction

Industrie 4.0 [Ind, 2011], the German vision for the future of manufacturing, recognises modular structured smart factories as one of the key ingredients. Smart factories use information and communications technologies to digitise their processes and reap huge benefits in the form of improved quality, lower costs, and increased efficiency [Zaske, 2015]. Agent-based systems have been applied to solve complex manufacturing system problems including manufacturing planning, scheduling and control, and supply chain management [Tang and Wong, 2005]. In particular, agents can represent physical resources such as machine tools, robots, auto-guided vehicles, etc [Paulo Leit˜ao, 2009]. However, the current development of such manufacturing control systems starts from simple graphical specifications and relies on the code developers to take care of the implementation details. This development approach not only is inefficient (in terms of the time and costs of the development) but also raises concerns about the reliability, performance, reusability, and reconfigurability of the resulting solution. Therefore, as pointed out in [Marik and McFarlane, 2005; Paulo Leit˜ao, 2009], an important challenge for agent-based manufacturing control systems is to develop formal and structured approaches to support their specification and verification.

In this paper, we introduce a logic-based approach for the specification and verification of manufacturing control systems (MCS), by generalising the existing approach of model checking multiagent systems. An MCS is a multiagent system, i.e., there are a set of agents interacting and communicating in an environment. In an MCS, each agent has limited, i.e., incomplete, information about the system by e.g., sensing devices. For instance, robotic arms fetching the same raw materials from a distributor robot are not supposed to observe the status (i.e., ready to fetch or not) of each other. The other characteristics of the agents in an MCS is reactivity, i.e., they behave in the way of reacting to the stimulus from the outside world [Tang and Wong, 2005]. Therefore, no memory is needed. Both incomplete information and reactivity of agents are not new in the area of model checking multiagent systems, with theoretical results [Fagin et al., 1995; Alur et al., 2002] and prototype verification softwares [Gammie and van der Meyden, 2004; Lomuscio et al., 2009].

The paper addresses a new challenge in the development of MCSs and Industrie 4.0 [Nikolaus, 2014], i.e., reconfigurable robots, which are robots whose modules can be connected in di↵erent ways to form di↵erent robots in terms of size, shape, or function [Chen et al., 2006; Kasper Støy et al., 2010; Dennis et al., 2014]. Reconfigurable manufacturing systems can quickly adjust their production capacity and functionality in response to sudden market changes or intrinsic system change [Koren et al., 2003]. In particular, the paper focuses on the decision problem for reconfigurable robots, called reconfigurability in the paper. Informally, the reconfigurability is, given a set of reactive robots, to determine whether they can form a composite robot with designated functionalities.

Two di↵erent development scenarios are considered. The first is the scenario in which the resulting system is a monolithic system 1 . The reconfigurability is to determine the existence of agents' reactive behaviour to satisfy their local functionalities and the system's global functionalities. Following the success of model checking [Clarke et al., 1999], a logic language is employed to describe the functionalities, by extending the temporal epistemic logic CTLK [Fagin et al., 1995] with the expressiveness to refer to agents' reactive behaviour directly in the formula. We show that the complexity of the problem is NP-complete.

The second is the scenario where the resulting system is an individual module of a bigger system. The resulting system has a set of nondeterministic transitions, called environment transitions in the paper, which are to accept interactions from other modules of the bigger system. The reconfigurability is to determine the existence of agents' reactive behaviour in satisfying the required functionalities, under all possible interactions. We show that the complexity of the problem is EXPTIME-complete.

1 To di↵erentiate component robots with the resulting robot, we write agents for component robots and system for the resulting robot.

2 Model CheckingMultiagent Systems

A multiagent system consists of a set Agt = {1, ..., n} of agents running in an environment [Fagin et al., 1995]. At each time, each agent is in some local state. The environment, regarded as a special agent e, is in some environment state, which keeps track of everything relevant to the system but not recorded in agents' local states. A global state s is a tuple (se, s1, ..., sn) consisting of an environment state se and a local state si for each agent i. Let Li, for i 2 Agt, be a set of agent i's local states, and Le be a set of environment states.

Each agent i has a nonempty set Actsi of local actions. Let Acts = ⇧i2AgtActsi be a set of joint actions. The environment runs a protocol Prote = (Le, te, Te, {Pi}i2Agt) where te 2 Le is an initial state 2 , Te : Le ⇥ Acts ! P(Le) \ {;} is a labeled transition function updating environment states according to the current state and agents' joint action, and Pi : Le ! Oi provides the perception/observation of agent i on the environment states. Each agent i runs a protocol Proti = (Li, Actsi, LActi, ti, Ti), where function LActi : Li ⇥ Oi ! P(Actsi) \ {;} defines for each local state and observation a nonempty set of actions that can be taken by agent i, ti 2 Li is an initial local state, and Ti : Li ⇥ Oi ⇥ Actsi ! P(Li) \ {;} is a labeled transition function. Let V be a finite set of boolean variables. Formally 3 , a multiagent system is a tuple M = (S , t, T, {⇠i}i2Agt , ⇡, F ) where

1. S ✓ Le ⇥⇧i2AgtLi is a set of global states,
2. t = (te, t1, ..., tn) is an initial global state,
3. T ✓ S ⇥ S is a transition relation such that for all states s = (le, l1, ..., ln) and s 0 = (l 0 e , l 0 1 , ..., l 0 n ), we have (s, s 0 ) 2 T i↵ there exist local actions a1, ..., an such that for all i 2 Agt, there are ai 2 LActi((li, Pi(le))) and (li, Pi(le), ai, l 0 i ) 2 Ti, and for the environment, there is (le, (a1, ..., an), l 0 e ) 2 Te,
4. ⇡ : S ! P(V) assigns each global state with a set of boolean variables in V, and
5. ⇠i✓ S ⇥S is an indistinguishable relation of agent i such that for all states s = (le, l1, ..., ln) and s 0 = (l 0 e , l 0 1 , ..., l 0 n ), we have (s, s 0 ) 2⇠i i↵ li = l 0 i and Pi(le) = Pi(l 0 e ),
6. F ✓ S is a B¨uchi acceptance condition.

A path in M is a finite or infinite sequence s0s1s2... such that (si, si+1) 2 T for all i ≥ 0. An infinite path s0s1s2... is fair with respect to F if there are infinitely many indices j for which s j 2 F . Let rch(M) be the set of fair reachable states of M, i.e., the set of states sn (for some n) such that there exists a fair path s0s1...snsn+1... with s0 = t the initial state.

2 For both the environment and the agents, we assume a single initial state. This is to ease the technicalities that will be employed in the complexity proofs. However, the results of this paper can be generalised to the case where there are a set of initial states.

3 Although simple, this formalisation is sufficiently expressive in modelling MCSs by engaging certain levels of abstractions. For example, the sensing results of robots can be modelled by agents' observations, and the communication and interactions between robots can be modelled by agents' joint actions.

The language CTLK(V, Agt) has the syntax:

where v 2 V and i 2 Agt. Other operators are defined as usual, e.g., AFφ = ¬EG¬φ and AGφ = ¬E(trueU¬φ). The semantics of the language is given by a satisfaction relation M, s |= φ, where s 2 rch(M) is a fair reachable state. This relation is defined inductively as follows:

1. M, s |= v if v 2 ⇡(s),
2. M, s |= φ1 _ φ2 if M, s |= φ1 or M, s |= φ2,
3. M, s |= ¬φ if not M, s |= φ,
4. M, s |= EXφ if there exists s 0 2 rch(M) such that (s, s 0 ) 2 T and M, s 0 |= φ,
5. M, s |= EGφ if for there exists a fair path s0s1 . . . such that s0 = s and M, sk |= φ for all k ≥ 0,
6. M, s |= E(φ1Uφ2) if there exists a fair path s0s1 . . . sn . . . such that s0 = s, M, sk |= φ1 for 0  k  n - 1 and M, sn |= φ2,
7. M, s |= Kiφ if for all s 0 2 rch(M) with (s, s 0 ) 2⇠i we have M, s 0 |= φ.

Example 1 We consider a typical MCS in which a (distributor) robot distributes semi-finished products to a set of (receiver) robots. Robots communicate with each other by wireless signals and self-organise themselves to ensure the success of this distribution task. The factory floor has limited space, so that at every time only one receiver can be allowed to access the distributor for the product.

Given a multiagent system M and a CTLK(V, Agt) formula φ, the model checking problem, written as M |= φ, is to decide whether M, t |= φ. It is shown [Clarke et al., 1999] that, if we measure the problem with the number |S | of states and the length |φ| of formula, then it is PTIME-complete.

In the system, each receiver i may be in one of the three states {wi, ti, ci}, which represents that it is waiting (i.e., it is doing other things irrelevant to the product), trying (i.e., it has decided to access the distributor as its next job), or collecting (i.e., it is accessing the distributor), respectively. Two signals ri and di are designed for each receiver i to communicate with the distributor. The signal ri = 1 represents that the receiver i is notifying the distributor with its intention to get the product, and the signal di = 1 represents that the distributor is notifying the receiver i that it is allowed to access. The distributor, modelled by the environment, may be in one of the two states { f, e}, representing that it is full (i.e., there is a receiver allowed to access) or empty. We let Li = {wi, ti, ci} and Le = { f , e} ⇥ ⇧i2Agt{ri, di}.

We define transition relations Ti and Te by describing the e↵ects of actions. The receiver i has a set {ai,>, ai,t, ai,c, ai,w} of actions. At state wi, it can take either ai,> to stay still or ai,t to start trying. The e↵ects of ai,t include turning the state into ti and letting the signal ri = 1. At state ti, it can take either ai,> to stay still or ai,c to start accessing the materials.

The e↵ect of ai,c is turning the state into ci. At state ci, it can take either ai,> to stay still or ai,w to leave the distributor. The e↵ects of ai,w include turning the state into wi and letting the signal di = 0. For the distributor, at state e, it nondeterministically chooses one of the receivers i that has sent a request, changing its own state into f , and letting di = 1 and ri = 0. The distributor does nothing if it is at state f . Whenever a receiver takes action ai,w, the distributor will update its state from f to e.

For the observation function Pi, we assume that receiver i can observe the signals ri and di. Initially, we have wi as the state of all receivers i, e as the state of the distributor, and ri = 0 and di = 0 as the states of the signals. There is no fairness condition required for the system and the labelling function is defined by directly referring to the states of the receivers, the distributor, or the signals.

For such a system, the following specification formulas describe a set of criteria for the success of the distribution task:

• φ1 ⌘ V i2Agt AG(ti ) AFci) expresses that once a receiver starts trying, it can eventually get the product,
• φ3 ⌘ AG V i2Agt V j2Agt(i , j ) ¬ci _ ¬cj) expresses that there will not be the case in which two receivers are allowed to access the distributor at the same time.
• φ2 ⌘ V i2Agt AGAF¬ci expresses that none of the receivers can access the distributor without exiting, and
• φ4 ⌘ AG V i2Agt(di ) Ki V j2Agt( j , i ) ¬di)) expresses that once a receiver is given the access, it knows that none of the other receivers has been given the access.

However, it can be checked that none of the above specification formulas can be satisfiable on the described system.

3 Reconfigurability vs. Model CheckingMAS

The example in the previous section shows an insufficiency of the approaches of model checking multiagent systems in handling interesting examples in smart factories. The techniques of model checking multiagent systems assume a closed system in which the behaviour of the agents and the environment is completely specified with their respective protocols. Therefore, the system in Example 1 is regarded as under-specified because only the available actions of the agents and their effects are described. To have a meaningful use of the model checking techniques, more details are needed to complete the protocols, including the following two aspects:

• A1. the conditions (or guards, etc) for the agents to take local actions, that is, the agents can take the actions only if their respective conditions are satisfied; for example, in Example 1, conditions may be needed for action ai,c, and di↵erent agents may have di↵erent conditions.
• A2. the interaction of the system, as a module of a bigger system, with other modules; for example, in Example 1, a resolution of the nondeterminism of the distributor on choosing a specific receiver to satisfy its request may exist if there is an interaction with other modules.

While the above discussion suggests that we need to complete the under-specified protocols, it is arguable that, for the reconfiguration of reactive multiagent systems, the information about the available actions and their e↵ects has been sufficient. These are exact information that we can expect for the component robots from their factory specifications. Based on these information, a reconfiguration is to find a way for the robots to be connected and communicated so that the resulting system can satisfy some objectives.

An important implication from the above arguments is that, for reconfiguration, instead of regarding the protocols as describing the actual behaviour, it is more reasonable to assume that the protocols describe the allowed or legal behaviour according to the robots' factory specifications. Each reconfiguration can then be concretised as a set of restrictions on the legal behaviour. For the studying of complexity, we consider a decision-problem called reconfigurability, which can be generally described as follows: given a set of reactive robots, it is to determine the existence of restrictions on their legal behaviour with respect to the objectives.

Formal definition of reconfigurability, to be given later, is scenario dependent. Here we explain the restrictions which will be imposed on the protocols. We utilise an intuition that the restrictions can be regarded as the inputs from the outside world and there are agents and environment behind their respective protocols to conduct such inputs. At each time, an input to a protocol is a (nonempty) subset of the allowed behaviour. In the following two sections, we will discuss two variants of the reconfigurability based on di↵erent scenarios.

4 Reconfigurability of AMonolithic System

The first variant assumes that agents have inputs via configsettings (to be defined below) and the environment does not have additional input. This is to model the scenario in which we are working with a monolithic system, so that we need only take care of the organisation of agents' behaviour and assume that the interactions with other systems have been completely specified in the environment protocol.

An agent's inputs are defined with a set of config-settings, each of which defines whether some action may be selected to take based on its currently available local information, i.e., agent's local state and current observation 4 . Formally, for i 2 Agt and a 2 Actsi, a config-setting xi,a : Li ⇥ Oi ! {0, 1} is a characteristic function over Li ⇥ Oi. Given xi,a, the function LActi is lifted into LActi[xi,a] : Li ⇥Oi ! P(Actsi) such that, b 2 LActi[xi,a]((si, oi)) for some state si 2 Li and observation oi 2 Oi if one of the following conditions holds:

1. a , b and b 2 LActi((si, oi)).

Intuitively, action a remains legal on state si and observation oi if (si, oi) is permitted by xi,a. These can be easily extended to work with a set of local actions A ✓ S i2Agt Actsi and a set of config-settings XA = {xi,a | i 2 Agt, a 2 A \ Actsi}. The function LActi is lifted into LActi[XA] such that LActi[XA] = (LActi[x])[XA \ {x}] for any x 2 XA , ; and LActi[;] = LActi. Furthermore, we define multiagent system M[XA] by lifting functions LActi for i 2 Agt according to XA. Note that, for a specific local information (si, oi), there can be more than one actions a such that xi,a(si, oi) = 1.

4 This definition is in line with the capability of reactive agents, which works in the stimulus-response way.

Given a multiagent system M, a set A ✓ S i2Agt Actsi of local actions, and a CTLK(V, Agt) formula φ, the reconfigurability problem, written as M, A |= φ, is to decide whether there exist config-settings XA = {xi,a | a 2 A \ Actsi, i 2 Agt} such that M[XA] |= φ. The complexity of the problem is measured over the number |S | of states, the number | S i2Agt Actsi| of local actions, and the length |φ| of formula. We have the following conclusion.

Theorem 1 The reconfigurability with config-settings is NPcomplete for CTLK(V, Agt).

We have a nondeterministic algorithm that runs in polynomial time. For each action a 2 A such that a 2 Actsi, the algorithm guesses a set of local states for xi,a. The system M is then updated into M[XA], on which a model checking procedure is held for the formula φ. Both the updating of system and the model checking can be done in polynomial time.

We note that, the problem has PTIME reductions to other problems that can be solved by SAT solvers or ASP solvers.

Example 2 (Continue with Example 1) We let A = {ai,c | i 2 Agt} be the set of local actions, and φ ⌘ φ1 ^ φ2 ^ φ3 ^ φ4 be a CTLK(V, Agt) formula. Then with expression M, A |= φ, we can check the existence of conditions for agents to take action ai,c, such that after imposing such conditions on agents' protocols, the formula φ is satisfiable. It can be verified that, this expression holds for systems with 2 agents.

The above example shows the advantage of reconfiguration with config-settings over model checking in that, it can work directly with under-specified agents' protocols and automatically verify the formulas without specifying the details of the aspect A1 (given in Section 3) for agents' protocols.

In the following, we extend the language CTLK(V, Agt) into CTLK(V, Agt, S i2Agt Actsi), which has the syntax:

where v 2 V, i 2 Agt, and a 2 Actsi. The satisfaction relation of the new construct xi,a is defined as follows.

As will explain in Example 3, xi,a, representing a set of states as that of atomic propositions, can be regarded as an atomic proposition of the resulting system (i.e., system imposed with reconfiguration) that are relevant to the actions. The reconfigurability problem is defined the same as before. The following conclusion shows that the additional expressiveness from the new construct comes for free.

Theorem 2 The reconfigurability with config-settings is NPcomplete for CTLK(V, Agt, S i2Agt Actsi).

For the algorithm, we note that checking M[XA], s |= xi,a can be done in linear time. Now we show the usefulness of the additional expressiveness.

Example 3 (Continue with Example 2) Besides those specification formulas in Example 1, we may be interested in

• φ5 ⌘ AG(xi,ai,c , KiAX V j2Agt( j , i ) ¬cj)), which expresses that whenever receiver i is permitted to take action ai,c, it knows that there is no collision with other receivers in accessing the distributor, and vice versa.
• φ6 ⌘ AG(xi,ai,c ) AXci), which expresses that whenever receiver i is permitted to take action ai,c, it will be accessing the distributor in the next state.
• φ7 ⌘ AG(xi,ai,c ) AF¬xi,ai,c ), which expresses that receiver i cannot always be accessing the distributor.

In φ5, φ6, φ7, we use the construct xi,ai,c to directly refer to the behaviour of the receiver i in the resulting system. The benefit of writing such a construct xi,a directly in a formula is that, while there may exist many possible reconfigurations, we can identify some of them that we are interested in by requiring the resulting system to satisfy formulas with constructs xi,ai,c . Recall that, xi,ai,c is a characteristic function over Li ⇥Oi, which means that it can be seen as a representation of a set of states on which action ai,c is allowed to be taken by agent i. For example, with φ6, the resulting system should satisfy the following: on every state where it is allowed to take action ai,c, agent i will take that action. Note that, this property cannot be expressed with usual CTLK(V, Agt) formulas, in particular, it is not the same as the formula AG(ti ) AXci).

5 Reconfigurability of AModule

In the first variant, the environment's behaviour is completely determined by its protocol, that is, given an environment state le and a joint action a, the set of possible next environment states is N(le, a) = {l 0 e | (le, a, l 0 e ) 2 Te}. For the second reconfigurability variant, we consider a more intriguing problem of allowing not only the inputs from agents but also the inputs from the environment. This is essential when considering a manufacturing system as an individual module of a larger system, which is typical for the vision of smart factories and Industrie 4.0 that tends to consider the connection of di↵erent factories and supply chains.

Such scenario suggests that, 1) the reconfiguration is for the agents' behaviour in the system, and 2) agents (and the system) do not have prior knowledge about how the interactions with other systems may occur after reconfiguration. The latter suggests that, to ensure that the resulting system can satisfy objectives, the reconfiguration needs to consider all possible interactions from the environment (Recall that we imagine there is an agent behind the environment protocol to conduct the inputs). Further, the definition of "all possible interactions from the environment" can be concretised by stating that the environment has complete information over the system state and perfect recall memory over the history. It is a maximal assumption over the environment's capability, but nevertheless reasonable for the reasons given above.

Now we formalise the above intuitions. The environment behaves based on the environment protocol, i.e., given an environment state le and a joint action a, the set of possible next environment states can be any nonempty subset of the set N(le, a). Formally, the inputs of the environment can be defined by a strategy σ as follows: given any finite path ⇢ = ts1...sk with t the initial state and sk = (le, l1, ..., ln) and any joint action a = (a1, ..., an) such that ai 2 LActi((li, Pi(le))) for all i 2 Agt, we have that σ(⇢, a) ✓ N(le, a) and σ(⇢, a) , ;. Let ⌃(M) be the set of all environment strategies in a multiagent system M.

Given a strategy σ of the environment, a path s0s1s2... is consistent with σ if for all i ≥ 0 with si = (le, l1, ..., ln) and si+1 = (l 0 e , l 0 1 , ..., l 0 n ), we have that (si, si+1) 2 T and there exists a joint action a = (a1, ..., an) such that l 0 e 2 σ(s0...si, a) and (li, Pi(le), ai, l 0 i ) 2 Ti for all i 2 Agt. Now we can define the semantics of a formula φ over a multiagent system M and an environment strategy σ by a satisfaction relation M, σ, s |= φ where s 2 rch(M). The definition basically follows the same pattern as M, s |= φ, except for the following points. When interpreting temporal formulas, paths need to be consistent with σ. E.g.,

1. M, σ, s |= EGφ if there exists a fair path s0s1 . . . consistent with σ, such that s0 = s and M, σ, sk |= φ for all k ≥ 0,

Let rch(M, σ) be a set of states that are fair and reachable in the system M by paths consistent with σ. The semantics of knowledge operator assumes that agents do not have prior knowledge over the environment's strategy. That is,

1. M, σ, s |= Kiφ if for all s 0 2 rch(M) and all strategies σ 0 2 ⌃(M) such that (s, s 0 ) 2⇠i and s 0 2 rch(M, σ 0 ), we have M, σ 0 , s 0 |= φ.

Considering config-settings under all possible environment strategies, we define the following reconfigurability variant. Given a multiagent system M, a set A ✓ S i2Agt Actsi of local actions, and a CTLK(V, Agt, S i2Agt Actsi) formula φ, the reconfigurability problem, written as M, A |=env φ, is to decide whether there exist config-settings XA = {xi,a | a 2 A \ Actsi, i 2 Agt} such that for all strategies σ 2 ⌃(M[XA]), we have that M[XA], σ, t |= φ. Note that, according to this definition, the environment has prior knowledge over agents' config-settings. This is in line with the maximal assumption over environment's capability. The complexity of the problem is measured over the number |S | of states, the number | S i2Agt Actsi| of local actions, and the length |φ| of formula.

As expected, the complexity of reconfigurability with environment strategy is higher than without environment strategy.

Theorem 3 The reconfigurability with config-settings and environment strategy is EXPTIME-complete for both CTLK(V, Agt) and CTLK(V, Agt, S i2Agt Actsi).

Proof: (Sketch) Let A = {a1, ..., ak} be a set of local actions such that for 1  j  k, aj 2 Actsi j for some agent i j. Given M, we construct M 0 = (S 0 , t 0 , T 0 , {⇠ 0 i }i2Agt , ⇡ 0 , F ) such that

1. the transition relation T 0 is defined as follows.
2. (a) (t 0 , (te, t1, ..., tn, y1, ..., yk)) 2 T 0 if for all 1  j  k, there is y j 2 P(Li j ⇥ Oi j ).
3. (b) ((le, l1, ..., ln, y1, ..., yk), (l 0 e , l 0 1 , ..., l 0 n , y1, ..., yk)) 2 T 0 if there exist local actions a 0 1 , ..., a 0 n such that (le, (a 0 1 , ..., a 0 n ), l 0 e ) 2 Te and for all 1  m  n, we have a 0 m 2 Actsm, (lm, Pm(le), a 0 m , l 0 m ) 2 Tm, and (lm, Pm(le)) 2 yj if a 0 m = aj for some 1  j  k.
4. the relation ⇠ 0 m is defined as follows: s ⇠ 0 m s 0 i↵ either of the following conditions holds: (a) s = s 0 = t 0 ; (b) s = (le, ..., ln, y1, ..., yk), s 0 = (l 0 e , ..., l 0 n , y 0 1 , ..., y 0 k ), lm = l 0 m , Pm(le) = Pm(l 0 e ), and yj = y 0 j for all 1  j  k.
5. the function ⇡ 0 is defined as follows: ⇡ 0 (t 0 ) = ; and ⇡ 0 ((le, l1, ..., ln, y1, ..., yk)) = ⇡(le, l1, ..., ln).
6. the fairness constraint F 0 is defined as follows: (le, l1, ..., ln, y1, ..., yk) 2 F 0 i↵ (le, l1, ..., ln) 2 F .

Intuitively, all states are attached with a set of config-settings, the new transition relation is consistent with config-settings, and config-settings do not change along the transitions.

Let M 0 (s) for s 2 S 0 be the same systemwith M 0 except for the initial state s, that is, M 0 (s) = (S 0 , s, T 0 , {⇠ 0 i }i2Agt, ⇡ 0 ). First of all, the reconfigurability problem M, A |=env φ is equivalent to M 0 (s), ; |=env φ for some state s = (te, t1, ..., tn, y1, ..., yk) such that {y1, ..., yk} is a set of config-settings of A.

For φ = xm,a with m 2 Agt and a 2 LActm, we have that M 0 (s), ; |=env φ with s = (le, l1, ..., ln, y1, ..., yk) i↵ there exists 1  j  k such that agt(yj) = m, act(yj) = a, and (lm, Pm(le)) 2 yj, where agt(yj) and act(yj) represent the corresponding agent and action of the config-setting for y j.

Then for any state s 2 S 0 , we consider the problem M 0 (s), ; |=env φ. We proceed by induction on the formula φ. For φ = p 2 V, we have that M 0 (s), ; |=env φ i↵ φ 2 ⇡ 0 (s).

For φ = Ki', we have M 0 (s), ; |=env φ i↵ 8σ : M 0 (s), σ, s |= φ. Then by the semantics of knowledge operator, the latter is equivalent to 8σ8s 0 8σ 0 : s ⇠ 0 i s 0 ^ s 0 2 rch(M 0 (s), σ 0 ) ) M 0 (s), σ 0 , s 0 |= ', which in turn is equivalent to 8s 0 : s ⇠ 0 i s 0 ) (8σ 0 : s 0 2 rch(M 0 (s), σ 0 ) ) M 0 (s), σ 0 , s 0 |= '). Because σ 0 is any strategy with perfect recall memory, we have that 8s 0 : s ⇠ 0 i s 0 ) M 0 (s 0 ), ; |=env '.

For φ being a CTL formula, we can check it by an automata theoretic approach. We use T 0 (s) = {s 0 | (s, s 0 ) 2 T 0 } to denote the set of successor states of s in system M 0 . Assume that s = (le, l1, ..., ln, y1, ..., yk). Let s 0 , s 00 2 T 0 (s) be two successor states of s such that s 0 = (l 0 e , l 0 1 , ..., l 0 n , y1, ..., yk) and s 00 = (l 00 e , l 00 1 , ..., l 00 n , y1, ..., yk), we say that s 0 and s 00 are in the same partition of T 0 (s) if l 0 e = l 00 e and there exist local actions a1, ..., an such that for all i 2 Agt, there is {(li, Pi(le), ai, l 0 i ), (li, Pi(le), ai, l 00 i )} ✓ Ti. Intuitively, two states in the same partition of T 0 (s) if they can be nondeterministically reached from s in a step after applying config-settings and environment strategy. That is, these are internal nondeterminism that cannot be eliminated by the interactions with the outside world.

From M 0 (s) = (S 0 , s, T 0 , {⇠ 0 i }i2Agt, ⇡ 0 ), we define a B¨uchi tree automaton AM 0 (s) = (⌃, D, Q, δ, q0, Q) such that

1. ⌃ = P(V) [ {?}, Q = S 0 ⇥ {>, `, ?}, q0 = (s, >),
2. D = S s2S {1, ..., |T 0 (s)|}, 3. δ : Q ⇥ ⌃ ⇥ D ! 2 Q ⇤ is defined as follows: for s 0 2 S 0 and k = |T 0 (s 0 )| with T 0 (s 0 ) = (s1, ..., sk), we have (a) if m 2 {`,?} then δ((s 0 ,m),?, k) = {((s1,?), ..., (sk,?))}, and (b) if m 2 {`,>}, then we let ((s1, y1), ..., (sk, yk)) 2 δ((s 0 , m), ⇡ 0 (s 0 ), k) such that, there exists a nonempty set B ✓ {1, ..., k} of indices such that for all i, j 2 B, si and s j are in the same partition of T 0 (s 0 ), and

• (a) yi = >, for all i 2 B, and

Note that we use F = Q to express that we only care about infinite paths. Moreover, the formula φ needs to be modified to reject those runs where ? is labeled on the states. This can be done by following the approach in [Kupferman and Vardi, 1996]. We still call the resulting formula φ.

Given a CTL formula φ and a set D ⇢ N with a maximal element k, there exists a B¨uchi tree automaton AD,¬φ that accepts exactly all the tree models of ¬φ with branching degrees in D. By [Vardi and Wolper, 1986], the size of AD,¬φ is O(2 k·|φ| ). To decide whether M 0 (s), ; |=env φ for a CTL formula is equivalent to checking the emptiness of the product automaton AM 0 (s) ⇥ A¬φ. The checking of emptiness of B¨uchi tree automaton can be done in quadratic time, so the checking of M 0 (s), ; |=env φ can be done in exponential time.

We omit the proof for the lower bound, which is reduced from the problem of a linearly bounded alternating Turing machine accepting an empty input tape.

Therefore, checking whether M 0 (s), ; |=env φ can be done in exponential time with respect to |S |, | S i2Agt Actsi|, and |φ|. That is, the reconfigurability M, A |=env φ is in EXPTIME.

boxempty Example 4 (Continue with Example 3) The behaviour of the distributor is modelled by the environment. Therefore, when checking whether

for φ ⌘ φ1 ^φ2 ^φ3 ^φ4 ^φ5 ^φ6 ^φ7, it is actually checking reconfigurability with respect to the objective φ under all possible interactions of the distributor with the other modules of the bigger system. The interaction occurs by the inputs over the nondeterminism of the distributor on choosing agents to satisfy their requests.

The above example shows an additional advantage of reconfiguration with environment strategy over model checking in that, it can work directly with under-specified multiagent system and automatically verify the formulas without specifying the details of the aspect A2 (given in Section 3) for environment's protocol. As discussed in Section 3, both this advantage and the advantage from config-settings are essential for the reconfiguration of MCSs.

6 RelatedWork

Methodological research has been conducted on the specification of reactive multiagent systems for various applications, e.g., textile industry, vehicle collision avoidance [Yang et al., 2008], transportation network [Meignan et al., 2007], etc. The developments of these systems rely on the code developers, and the analysis of the systems is usually done by simulation techniques. Our approach is based on, and generalises, the logic-based specification and verification of multiagent systems, and therefore is rigorous and automated.

The interests towards the reconfiguration of systems are recent with prototype systems appearing, see e.g., [Bishop et al., 2005; Oung et al., 2010]. The reconfiguration actions in these system are hard-wired in their implementations, without rigorous proofs on their reliability, e.g, whether executing such an action at a specific system state is safe, or whether it is possible to executing such an action on a module of the system and at the same time ensuring the stability and predictability of the entire system. The paper complements this with the formalisation of reconfigurability, which is treated as a variant of model checking multiagent systems.

The techniques employed can be related to the module checking [Kupferman and Vardi, 1996], which considers the interactions of a monolithic system with outside world. There are major di↵erences when considering multiagent systems. In module checking, the outside world is able to interact with all nondeterministic choices of the system. This contrasts with a multiagent system, in which an environment strategy can only interact with the environment protocol and cannot directly control agents' behaviour. To enable the interaction with agents' protocols and compete with environment strategies, config-settings are considered. Moreover, to work with multiple agents and their partial observations, we consider a logic CTLK(V, Agt, S i2Agt Actsi) in which we have knowledge operator Ki and can write structure xi,a to directly refer to the config-settings (See formulas φ5, φ6, φ7 in Example 3 for such examples). These di↵erences distance the concept of reconfigurablity with that of module checking. Recently, [Jamroga and Murano, 2014] discusses the di↵erence between module checking and ATL model checking, and [Jamroga and Murano, 2015] discusses module checking based on ATL when environment is partial observation, which is different with our maximal assumption about the environment.

Reconfiguration can be regarded as a competitive game between agents and the environment. To reasoning about competitive games, various strategy logics, such as [Alur et al., 2002; Huang and van der Meyden, 2014c; 2014a], have been proposed, together with model checking algorithms [Huang and van der Meyden, 2014b; Huang, 2015]. The paper works with a particular setting: a set of reactive agents operate their config-settings against an environment which have full information about the system and agents' strategy, to achieve a goal expressed with CTLK(V, Agt, S i2Agt Actsi) formula.

7 Conclusions and FutureWork

In the paper, aiming at the applications in smart factories and Industrie 4.0, we formalise the reconfigurability for reactive multiagent systems, by generalising the approaches of model checking multiagent systems. Two reconfiguration scenarios are considered and their complexity results are given.

States and transitions of multiagent systems are high-level abstractions of the real-world manufacturing control systems. Working directly with concrete systems in which the states include geometric place information and the transitions are described by e.g., constraints in a three-dimensional space, is interesting. [Reif, 1979] considers the planning of a sequence of movements of linked polyhedra, which are suitable to precisely represent actual mechanical devices e.g., robot arms.

Moreover, we are also interested in stochastic multiagent systems, on which our e↵orts have been made towards probabilistic extensions of strategy logics [Huang et al., 2012; Huang and Kwiatkowska, 2016; Huang and Luo, 2013]. Future work includes probabilistic reconfiguration with stochastic config-settings and strategies.

Acknowledgement The authors gratefully thank the reviewers for detailed and insightful comments. The authors are supported by ERC Advanced Grant VERIWARE, EPSRC Mobile Autonomy Programme Grant EP/M019918/1, National Natural Science Foundation of China Grant 61572234 and No.61472369, Fundamental Research Funds for the Central Universities of China Grant 21615441, and ARC Grant DP150101618.