# reconfigurability_in_reactive_multiagent_systems__cafaa478.pdf

Reconﬁgurability in Reactive Multiagent Systems

Xiaowei Huang1,2, Qingliang Chen1, Jie Meng3, Kaile Su1,4

1Department of Computer Science, Jinan University, China 2Department of Computer Science, University of Oxford, United Kingdom 3Department of Marketing and Management, Macquarie University, Australia 4Institute for Integrated and Intelligent Systems, Griﬃth University, Brisbane, Australia

Reactive agents are suitable for representing physical resources in manufacturing control systems. An important challenge of agent-based manufacturing control systems is to develop formal and structured approaches to support their speciﬁcation and veriﬁcation. This paper proposes a logic-based approach, by generalising that of model checking multiagent systems, for the reconﬁgurability of reactive multiagent systems. Two reconﬁgurability scenarios are studied, for the resulting system being a monolithic system or an individual module, and their computational complexity results are given.

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 beneﬁts in the form of improved quality, lower costs, and increased eﬃciency [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 speciﬁcations and relies on the code developers to take care of the implementation details. This development approach not only is ineﬃcient (in terms of the time and costs of the development) but also raises concerns about the reliability, performance, reusability, and reconﬁgurability of the resulting solution. Therefore, as pointed out in [Marik and Mc Farlane, 2005; Paulo Leit ao, 2009], an important challenge for agent-based manufacturing control systems is to develop formal and structured approaches to support their speciﬁcation and veriﬁcation.

In this paper, we introduce a logic-based approach for the speciﬁcation and veriﬁcation 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 communi-

cating 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 veriﬁcation 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., reconﬁgurable 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]. Reconﬁgurable 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 reconﬁgurable robots, called reconﬁgurability in the paper. Informally, the reconﬁgurability 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 ﬁrst is the scenario in which the resulting system is a monolithic system1. The reconﬁgurability 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

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

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-16)

other modules of the bigger system. The reconﬁgurability 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.

2 Model Checking Multiagent 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 = i2Agt Actsi be a set of joint actions. The environment runs a protocol Prote = (Le, te, Te, {Pi}i2Agt) where te 2 Le is an initial state2, 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) \ {;} deﬁnes 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 ﬁnite set of boolean variables. Formally3, a multiagent system is a tuple M = (S, t, T, { i}i2Agt, , F ) where

1. S Le i2Agt Li 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 s0 = (l0

n), we have (s, s0) 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, l0

i) 2 Ti, and for the environment, there is (le, (a1, ..., an), l0

4. i S S is an indistinguishable relation of agent i such

that for all states s = (le, l1, ..., ln) and s0 = (l0

n), we have (s, s0) 2 i i li = l0

i and Pi(le) = Pi(l0

5. : S ! P(V) assigns each global state with a set of

boolean variables in V, and

6. F S is a B uchi acceptance condition.

A path in M is a ﬁnite or inﬁnite sequence s0s1s2... such that (si, si+1) 2 T for all i 0. An inﬁnite path s0s1s2... is fair with

2For 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.

3Although simple, this formalisation is suﬃciently 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.

respect to F if there are inﬁnitely 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.

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

φ ::= v | φ | φ1 _ φ2 | EXφ | E(φ1Uφ2) | EGφ | Kiφ

where v 2 V and i 2 Agt. Other operators are deﬁned as usual, e.g., AFφ = EG φ and AGφ = E(true U φ). 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 deﬁned inductively as follows:

1. M, s |= v if v 2 (s), 2. M, s |= φ if not M, s |= φ, 3. M, s |= φ1 _ φ2 if M, s |= φ1 or M, s |= φ2, 4. M, s |= EXφ if there exists s0 2 rch(M) such that (s, s0) 2

T and M, s0 |= φ, 5. 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, 6. M, s |= EGφ if for there exists a fair path s0s1 . . . such

that s0 = s and M, sk |= φ for all k 0, 7. M, s |= Kiφ if for all s0 2 rch(M) with (s, s0) 2 i we

have M, s0 |= φ. 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.

Example 1 We consider a typical MCS in which a (distributor) robot distributes semi-ﬁnished 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 ﬂoor has limited space, so that at every time only one receiver can be allowed to access the distributor for the product.

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 deﬁne 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 deﬁned by directly referring to the states of the receivers, the distributor, or the signals.

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

i2Agt AG(ti ) AFci) expresses that once a receiver starts trying, it can eventually get the product,

i2Agt AGAF ci expresses that none of the receivers can access the distributor without exiting, and

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.

i2Agt(di ) Ki

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 speciﬁcation formulas can be satisﬁable on the described system.

3 Reconﬁgurability vs. Model Checking MAS

The example in the previous section shows an insuﬃciency 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 speciﬁed with their respective protocols. Therefore, the system in Example 1 is regarded as under-speciﬁed 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 satisﬁed; 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 speciﬁc 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-speciﬁed protocols, it is arguable that, for the

reconﬁguration of reactive multiagent systems, the information about the available actions and their e ects has been suﬃcient. These are exact information that we can expect for the component robots from their factory speciﬁcations. Based on these information, a reconﬁguration is to ﬁnd 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 reconﬁguration, 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 speciﬁcations. Each reconﬁguration can then be concretised as a set of restrictions on the legal behaviour. For the studying of complexity, we consider a decision-problem called reconﬁgurability, 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 deﬁnition of reconﬁgurability, 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 reconﬁgurability based on di erent scenarios.

4 Reconﬁgurability of A Monolithic System The ﬁrst variant assumes that agents have inputs via conﬁgsettings (to be deﬁned 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 speciﬁed in the environment protocol.

An agent s inputs are deﬁned with a set of conﬁg-settings, each of which deﬁnes whether some action may be selected to take based on its currently available local information, i.e., agent s local state and current observation4. Formally, for i 2 Agt and a 2 Actsi, a conﬁg-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, b 2 LActi((si, oi)) and xi,a((si, oi)) = 1. 2. 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 conﬁg-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 deﬁne multiagent system M[XA] by lifting functions LActi for i 2 Agt according to XA. Note that, for a

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

speciﬁc local information (si, oi), there can be more than one actions a such that xi,a(si, oi) = 1.

Given a multiagent system M, a set A S

i2Agt Actsi of local actions, and a CTLK(V, Agt) formula φ, the reconﬁgurability problem, written as M, A |= φ, is to decide whether there exist conﬁg-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 reconﬁgurability with conﬁg-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 satisﬁable. It can be veriﬁed that, this expression holds for systems with 2 agents.

The above example shows the advantage of reconﬁguration with conﬁg-settings over model checking in that, it can work directly with under-speciﬁed 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:

φ ::= xi,a | v | φ | φ1 _ φ2 | EXφ | E(φ1Uφ2) | EGφ | Kiφ

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

1. M, s |= xi,a if xi,a((li, Pi(le))) = 1 for s = (le, l1, ..., ln)

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 reconﬁguration) that are relevant to the actions. The reconﬁgurability problem is deﬁned the same as before. The following conclusion shows that the additional expressiveness from the new construct comes for free.

Theorem 2 The reconﬁgurability with conﬁg-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 speciﬁcation formulas in Example 1, we may be interested in

φ5 AG(xi,ai,c , Ki AX V

j2Agt(j , i ) c j)), 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 when-

ever 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 re-

ceiver 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 beneﬁt of writing such a construct xi,a directly in a formula is that, while there may exist many possible reconﬁgurations, 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 Reconﬁgurability of A Module

In the ﬁrst 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) = {l0

e | (le, a, l0

e) 2 Te}. For the second reconﬁgurability 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 reconﬁguration 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 reconﬁguration. The latter suggests that, to ensure that the resulting system can satisfy objectives, the reconﬁguration 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 deﬁnition 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 deﬁned by a strategy σ as follows: given any ﬁnite 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 = (l0

n), we have that (si, si+1) 2 T and there exists a joint action a = (a1, ..., an) such that l0

e 2 σ(s0...si, a) and (li, Pi(le), ai, l0

i) 2 Ti for all i 2 Agt. Now we can deﬁne 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 deﬁnition 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 . . . consis-

tent 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 s0 2 rch(M) and all strategies

σ0 2 (M) such that (s, s0) 2 i and s0 2 rch(M, σ0), we have M, σ0, s0 |= φ.

Considering conﬁg-settings under all possible environment strategies, we deﬁne the following reconﬁgurability 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 reconﬁgurability problem, written as M, A |=env φ, is to decide whether there exist conﬁg-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 deﬁnition, the environment has prior knowledge over agents conﬁg-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 reconﬁgurability with environment strategy is higher than without environment strategy.

Theorem 3 The reconﬁgurability with conﬁg-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 M0 = (S 0, t0, T 0, { 0

i}i2Agt, 0, F ) such that

1. S 0 = (Le L1 ... Ln k

j=1P(Li j Oij)) [ {t0},

2. the transition relation T 0 is deﬁned as follows.

(a) (t0, (te, t1, ..., tn, y1, ..., yk)) 2 T 0 if for all 1 j k,

there is y j 2 P(Li j Oi j). (b) ((le, l1, ..., ln, y1, ..., yk), (l0

n, y1, ..., yk)) 2 T 0 if there exist local actions a0

n such that (le, (a0

e) 2 Te and for all 1 m n, we have a0

m 2 Actsm, (lm, Pm(le), a0

m) 2 Tm, and (lm, Pm(le)) 2 yj if a0

m = aj for some 1 j k.

3. the relation 0

m is deﬁned as follows: s 0

m s0 i either of the following conditions holds: (a) s = s0 = t0; (b) s = (le, ..., ln, y1, ..., yk), s0 = (l0

k), lm = l0

m, Pm(le) = Pm(l0

e), and y j = y0

j for all 1 j k.

4. the function 0 is deﬁned as follows: 0(t0) = ; and

0((le, l1, ..., ln, y1, ..., yk)) = (le, l1, ..., ln).

5. the fairness constraint F 0 is deﬁned 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 conﬁg-settings, the new transition relation is consistent with conﬁg-settings, and conﬁg-settings do not change along the transitions.

Let M0(s) for s 2 S 0 be the same system with M0 except for the initial state s, that is, M0(s) = (S 0, s, T 0, { 0

i}i2Agt, 0). First of all, the reconﬁgurability problem M, A |=env φ is equivalent to M0(s), ; |=env φ for some state s = (te, t1, ..., tn, y1, ..., yk) such that {y1, ..., yk} is a set of conﬁg-settings of A.

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

For φ = xm,a with m 2 Agt and a 2 LActm, we have that M0(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 conﬁg-setting for yj.

For φ = Ki', we have M0(s), ; |=env φ i 8σ : M0(s), σ, s |= φ. Then by the semantics of knowledge operator, the latter is equivalent to 8σ8s08σ0 : s 0

i s0 s0 2 rch(M0(s), σ0) ) M0(s), σ0, s0 |= ', which in turn is equivalent to 8s0 : s 0

i s0 ) (8σ0 : s0 2 rch(M0(s), σ0) ) M0(s), σ0, s0 |= '). Because σ0 is any strategy with perfect recall memory, we have that 8s0 : s 0

i s0 ) M0(s0), ; |=env '. For φ being a CTL formula, we can check it by an automata theoretic approach. We use T 0(s) = {s0 | (s, s0) 2 T 0} to denote the set of successor states of s in system M0. Assume that s = (le, l1, ..., ln, y1, ..., yk). Let s0, s00 2 T 0(s) be two successor states of s such that s0 = (l0

n, y1, ..., yk) and s00 = (l00

1 , ..., l00

n , y1, ..., yk), we say that s0 and s00 are in the same partition of T 0(s) if l0

e and there exist local actions a1, ..., an such that for all i 2 Agt, there is {(li, Pi(le), ai, l0

i), (li, Pi(le), ai, l00

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 conﬁg-settings and environment strategy. That is, these are internal nondeterminism that cannot be eliminated by the interactions with the outside world.

From M0(s) = (S 0, s, T 0, { 0

i}i2Agt, 0), we deﬁne a B uchi tree automaton AM0(s) = ( , D, Q, δ, q0, Q) such that

1. = P(V) [ {?}, Q = S 0 {>, , ?}, q0 = (s, >),

s2S {1, ..., |T 0(s)|},

3. δ : Q D ! 2Q is deﬁned as follows: for s0 2 S 0

and k = |T 0(s0)| with T 0(s0) = (s1, ..., sk), we have (a) if m 2 { , ?} then δ((s0, m), ?, k) = {((s1, ?), ..., (sk, ?))}, and (b) if m 2 { , >}, then we let ((s1, y1), ..., (sk, yk)) 2 δ((s0, m), 0(s0), 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(s0), and

(a) yi = >, for all i 2 B, and (b) yj = , for all j < B and 1 j k. Note that we use F = Q to express that we only care about inﬁnite paths. Moreover, the formula φ needs to be modiﬁed 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(2k |φ|). To decide whether M0(s), ; |=env φ for a CTL formula is equivalent to checking the emptiness of the product automaton AM0(s) A φ. The checking of emptiness of B uchi tree automaton can be done in quadratic time, so the checking of M0(s), ; |=env φ can be done in exponential time.

Therefore, checking whether M0(s), ; |=env φ can be done in exponential time with respect to |S |, | S

i2Agt Actsi|, and |φ|. That is, the reconﬁgurability M, A |=env φ is in EXPTIME.

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. !

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

M, A |=env φ for φ φ1 φ2 φ3 φ4 φ5 φ6 φ7, it is actually checking reconﬁgurability 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 reconﬁguration with environment strategy over model checking in that, it can work directly with under-speciﬁed 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 conﬁg-settings are essential for the reconﬁguration of MCSs.

6 Related Work Methodological research has been conducted on the speciﬁcation 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 speciﬁcation and veriﬁcation of multiagent systems, and therefore is rigorous and automated.

The interests towards the reconﬁguration of systems are recent with prototype systems appearing, see e.g., [Bishop et al., 2005; Oung et al., 2010]. The reconﬁguration 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 speciﬁc 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 reconﬁgurability, 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, conﬁg-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 conﬁg-settings (See formulas φ5, φ6, φ7 in Example 3 for such examples). These di erences distance the concept of reconﬁgurablity 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.

Reconﬁguration 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 conﬁg-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 Future Work

In the paper, aiming at the applications in smart factories and Industrie 4.0, we formalise the reconﬁgurability for reactive multiagent systems, by generalising the approaches of model checking multiagent systems. Two reconﬁguration 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 reconﬁguration with stochastic conﬁg-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.

References [Alur et al., 2002] Rajeev Alur, Thomas A. Henzinger, and

Orna Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672 713, 2002. [Bishop et al., 2005] J. Bishop, S. Burden, E. Klavins, and

R. Kreisberg. Programmable parts: a demonstration of the grammatical approach to self-organization. In IROS 2005, pages 3684 3691, 2005. [Chen et al., 2006] I-Ming Chen, Guilin Yang, and Song Huat Yeo. Automatic modeling for modular reconﬁgurable robotic systems theory and practice. In Industrial Robotics: Theory, Modelling and Control. Pro Literatur Verlag, Germany, 2006. [Clarke et al., 1999] E. Clarke, O. Grumberg, and D. Peled.

Model Checking. The MIT Press, 1999. [Dennis et al., 2014] Louise A. Dennis, Michael Fisher, Jonathan M. Aitken, Sandor M. Veres, Yang Gao, A an Shaukat, and Guy Burroughes. Reconﬁgurable autonomy. K unstliche Intelligenz, 28(3):199 207, 2014. [Fagin et al., 1995] R. Fagin, J. Halpern, Y. Moses, and

M. Vardi. Reasoning About Knowledge. MIT Press, 1995. [Gammie and van der Meyden, 2004] P. Gammie and R. van der Meyden. MCK: Model checking the logic of knowledge. In CAV2004, pages 479 483, 2004. [Huang and Kwiatkowska, 2016] Xiaowei Huang and Marta

Kwiatkowska. Model Checking Probabilistic Knowledge: A PSPACE Case. In AAAI 2016, 2016. [Huang and Luo, 2013] Xiaowei Huang and Cheng Luo. A

Logic of Probabilistic Knowledge and Strategy. In AAMAS 2013, pages 845 852, 2013. [Huang and van der Meyden, 2014a] Xiaowei Huang and Ron van der Meyden. An Epistemic Strategy Logic. In SR 2014, pages 35 41, 2014. [Huang and van der Meyden, 2014b] Xiaowei Huang and Ron van der Meyden. Symbolic model checking epistemic strategy logic. In AAAI 2014, pages 1426 1432, 2014. [Huang and van der Meyden, 2014c] Xiaowei Huang and Ron van der Meyden. A temporal logic of strategic knowledge. In KR 2014, 2014. [Huang et al., 2012] Xiaowei Huang, Kaile Su, and Chenyi

Zhang. Probabilistic Alternating-time Temporal Logic of Incomplete information and Synchronous Perfect Recall. In AAAI-12, pages 765 771, 2012. [Huang, 2015] Xiaowei Huang. Bounded model checking of

strategy ability with perfect recall. Artiﬁcial Intelligence, 222:182 200, 2015.

[Ind, 2011] Industrie 4.0: Mit dem internet der dinge auf

dem weg zur 4. industriellen revolution, 2011. [Jamroga and Murano, 2014] Wojciech Jamroga and Aniello

Murano. On module checking and strategies. In AAMAS 2014, pages 701 708, 2014. [Jamroga and Murano, 2015] Wojciech Jamroga and Aniello

Murano. Module checking of strategic ability. In AAMAS 2015, pages 227 235, 2015. [Kasper Støy et al., 2010] Kasper Støy, David Brandt, and

David J. Christensen. Self-Reconﬁgurable Robots. MIT Press, 2010. [Koren et al., 2003] Y. Koren, U. Heisel, F. Jovane, T. Mori-

waki, G. Pritschow, G. Ulsoy, and H. Van Brussel. Reconﬁgurable manufacturing systems. In Manufacturing Technologies for Machines of the Future, pages 627 665. Springer, 2003. [Kupferman and Vardi, 1996] Orna Kupferman and Moshe Y. Vardi. Module checking. In CAV 1996, pages 75 86, 1996. [Lomuscio et al., 2009] A. Lomuscio, H. Qu, and F. Rai-

mondi. MCMAS: A model checker for the veriﬁcation of multi-agent systems. In CAV2009, pages 682 688, 2009. [Marik and Mc Farlane, 2005] V. Marik and D. Mc Farlane.

Industrial adoption of agent-based technologies. IEEE Intelligent Systems, 20(1):IEEE Intelligent Systems, 2005. [Meignan et al., 2007] David Meignan, Olivier Simonin, and

Abderraﬁaa Koukam. Simulation and evaluation of urban bus-networks using a multiagent approach. Simulation Modelling Practice and Theory, 15(6):659 671, 2007. [Nikolaus, 2014] Katrin Nikolaus. Manufacturing: Selforganizing factories, 2014. [Oung et al., 2010] R. Oung, F. Bourgault, M. Donovan, and

R. D Andrea. The distributed ﬂight array. In ICRA2010, pages 601 607, 2010. [Paulo Leit ao, 2009] Paulo Leit ao. Agent-based distributed

manufacturing control: A state-of-the-art survey. Engineering Applications of Artiﬁcial Intelligence, 22(7):979 991, 2009. [Reif, 1979] John H. Reif. Complexity of the mover s prob-

lem and generalizations. In FOCS 1979, pages 421 427, 1979. [Tang and Wong, 2005] H.P. Tang and T.N. Wong. Reactive

multi-agent system for assembly cell control. Robotics and Computer-Integrated Manufacturing, 21(2):87 98, 2005. [Vardi and Wolper, 1986] Moshe Y. Vardi and Pierre Wolper.

Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci., 32(2):183 221, 1986. [Yang et al., 2008] Sibo Yang, F. Gechter, and A. Koukam.

Application of reactive multi-agent system to vehicle collision avoidance. In ICTAI 2008, pages 197 204, 2008. [Zaske, 2015] Sara Zaske. Germany s vision for industrie 4.0: The revolution will be digitised, 2015.