A top down approach for describing the acquaintance organisation of multiagent systems

Salable Computing: Pratie and Experiene Volume 8, Number 1, pp. 4962. http://www.spe.org ISSN 1895-1767 © 2007 SWPS A TOP DOWN APPROACH FOR DESCRIBING THE ACQUAINTACE ORGANISATION OF MULTIAGENT SYSTEMS ∗ JOAQUÍN PEÑA † , RAFAEL CORCHUELO † AND ANTONIO RUIZ-CORTÉS † Abstrat. When the proto ol of a omplex Multi-Agent System (MAS) needs to b e develop ed, the top-down approah emphasises to start with abstrat desriptions that should be rened inrementally until we ahieve the detail level neessary to implement it. Unfortunately, there exist a semanti gap in interation proto ol metho dologies b eause most of them rst, identify whih tasks has to b e performed, and then use low level desription suh as sequenes of messages to detail them. In this pap er, we prop ose an approah to bridge this gap proposing a set of tehniques that are integrated in a methodology alled MaCMAS (Metho dology for Analysing Complex Multiagent Systems). We model MAS proto ols using several abstrat views of the tasks to b e p erformed, and provide a systemati metho d to reah message sequenes desriptions from task desriptions. These tasks are represented by means of interations that shall b e rened systematially into lower-level interations with the tehniques prop osed in this pap er (simpler interations are easier to desrib e and implement using message passing.) Unfortunately, deadlo ks may appear due to protool design mistakes or due to the renement pro ess that we present. Thus, we also propose an algorithm to ensure that protools are deadlo k free. Key words. Top-down approah, agent proto ol desriptions, interation renements, and deadlo k detetion. 1. Intro dution. Agent-Oriented Software Engineering (AOSE) is paving the way for a new paradigm in the Software Engineering eld. This is the reason why a large amount of researh pap ers on this topi are app earing in the literature. One of the main researh lines in AOSE arena is devoted to developing metho dologies for mo delling interation protools (hereafter proto ols) between agents. 1.1. Motivation. When a large system is mo deled, its omplexity b eomes a ritial fator that has to b e managed prop erly to ahieve lear, readable, reusable, and orret speiations [8, 24, 30℄. In the literature, there exist various tehniques to palliate this problem. The most imp ortant are the top down and the bottom up approahs. The top down approah, whih is the fo us of this pap er, rst tries to desrib e software from a high level of abstration, and then go es into further details until they are enough for implementing the system [32℄. When the proto ol of a large MAS has to b e developed, it is desirable to start with an abstrat desription that an b e rened inrementally aording to the top down approah . In our opinion, there exist two drawbaks in most existing methodologies: • On the one hand, most of them provide top-down approahes for mo deling and developing these systems. These metho dologies, general or proto ol-entri, agree on using abstrat messages and sequene diagrams to desrib e proto ols [3, 19, 37, 15℄. Although these messages represent a high level view of a proto ol, whih shall b e rened later, the tasks that are p erformed are formulated as a set of messages. This representation implies that the abstration level falls dramatially sine a task that is done by more than two agents requires several messages to b e represented. This o urs even if we onsider a task b etween two agents. For instane, an information request b etween two agents must be represented with two messages at least (one to ask, and another to reply). This introdues a semanti gap b etween tasks to be p erformed identied at requirements and its internal design sine it is diult to identify the tasks represented in a sequene of messages. This representation b eomes an imp ortant problem regarding readability and manageability of large MAS. • On the other hand, abstrations of proto ols (interations) that allow designers to enapsulate piees of a proto ol that is exeuted by an arbitrary numb er of agents has b een proved adequate in this ontext [3, 4, 19, 20, 38℄. Unfortunately, interations are generally used to hide unneessary details ab out some views of the proto ol. This improves readability and promotes reusability of protool patterns, but they are not used for bridging the existing semanti gap b etween tasks and its representation. 1.2. Contributions. In our proposal, we present a dierent approah to use interations, whih is based on the ideas presented in [4, 26, 38℄. This approah is integrated on a methodology alled MaCMAS that overs top-down and b ottom-up. The top down software proess is skethed in Figure 1.1. As shown, our goal is to ∗ This work has b een partially supp orted by the Europ ean Commission (FEDER) and Spanish Government under CICYT pro jet Web-Fatories (TIN2006-00472) and TIC200302737C0201 † University of Seville, {joaquinp, orhu}lsi.us.es, aruizus.es 49 50 Joaquín Peña, Rafael Corhuelo and Antonio Ruiz-Cortés                                                                                                                                                                                                                                                                                                                                                                                       !                          !                                                               "               "         "              "       #                    #                                                     "  $       "  $                                                              Fig. 1.1 . Software proess of renements. bridge this gap using interation abstrations to mo del the tasks to b e p erformed, and Finite State Automata (FSA), represented using UML 2.0, to mo del how to sequene them. Afterwards, we rene them systematially into simpler ones iteratively. This dereases the level of abstration so that the interation we obtain are simpler. Thus, they are desrib ed internally as message sequenes easily, e.g. using AUML [3℄. We have used a proto ol abstration alled multi-role interation (mRI), whih was rst prop osed in [25℄. An mRI is an abstration that enapsulates a set of messages between an arbitrary numb er of agent roles. Furthermore, the renement pro ess we use is based on the ideas presented in [10℄ sine the interation we use is similar to suh used in this work. The renement pro ess relies on analysing the knowledge used by eah role in an mRI and using this information to transform an mRI into several simpler mRIs automatially. An mRI is simpler when both the numb er of partiipant roles and the omputation made by it dereases. The main advantages of rening mRIs are the followings: • First, its internal desription is easier sine the omputation to p erform in the obtained tasks are simpler. • Seond, it is easier to implement interations with a low numb er of partiipant roles [12, page 206℄ [2, 33, 21, 35℄. • Finally, mRIs are ritial deadlo k free regions and they are mutually exlusive. Thus, if the numb er of partiipant roles inreases, the onurreny grain dereases, what is learly not desirable [34℄. The main drawbak of suh renements is that they may lead to deadlo ks. In this pap er, we also prop ose a tehnique to detet if a renement may intro due deadlo ks (see Figure 1.1); it also haraterises them by means of regular expressions that help nding the renements that are not adequate in a given ontext. It is based on analysing the FSA that represents the proto ol of a role model and some previous work on deadlok detetion in the ontext of lient/server interations [5, 14, 36℄. It improves on other results in that it an be automated beause it do es not require any knowledge about the implied, intuitive semantis of the interations as other approahes. This pap er is organised as follows: in Setion 2 we present the related work ab out proto ol mo deling in MAS and ab out interation renements; in Setion 3, we summarise the metho dology where this work is integrated; in Setion 4 we present the example that we use to illustrate our approah; in Setion 5 we present our ideas on A Top Down Approah for Desribing the Aquaintae Organisation of Multiagent Systems 51 proto ol mo deling and we show the renement tehniques appliable; in Setion 6 we present our approah to the automati deadlo k detetion pro ess; Setion 7, we show our main onlusions. Finally, an app endix that shows an implementation of the ase study using IP. 2. Related work. In this setion we over the related work on proto ol modelling and on renements. 2.1. Proto ol Mo deling. As we showed in the previous setion, we think that most approahes model proto ols at low level of abstration sine they require the designer to mo del omplex o op erations as messagebased proto ols. This issue has b een identied in the Gaia Metho dology [38℄, and also in the work of Caire et. al. [4℄, where the proto ol desription proess starts with a high level view based on desribing tasks as omplex ommuniation primitives (hereafter interations). We think that the ideas presented in b oth pap ers are adequate for this kind of systems where interations are more imp ortant than in ob jet-oriented programming. On the one hand, in the Gaia metho dology, proto ols are mo deled using abstrat textual templates. Eah template represents an interation or task to b e p erformed b etween an arbitrary numb er of partiipants. Furthermore, interations are deorated with the knowledge they pro ess and the p ermissions eah role has, their purp ose, their inputs and outputs, and so on. On the other hand, in [4℄, the authors prop ose a metho dology in whih the rst proto ol view is a stati view of the interations in a system. Eah interation is used by a set of agent roles and they are deorated with the knowledge eah role uses/supplies. Later, the internals of these interations are desrib ed using AUML [3℄. As the metho dologies ited ab ove, we also use interations to deal with the rst stage of protool modeling. Furthermore, we also represent a stati view of interations and the knowledge that eah role onsumes and pro dues in eah of them. Unfortunately, b oth metho dologies do not provide an automati metho d for rening omplex interations into smaller interations that are loser to the implementation level. In this pap er, we elab orate on suh a metho d. Furthermore, in metho dologies that use sequene diagrams to model proto ols, it has b een also identied the need for advaned multi-role interations that enapsulate a piee of proto ol. Unfortunately, in most of them these interations are used to dene reusable patterns of interation or for hiding details in some omplex views. Several examples of suh use of interations an b e found in the literature: For instane, AUML nested proto ols [3℄ or miro-proto ols [19℄. These approahes provide the user with a set of to ols to mo del omplex o-op erations; however, most designers use messagebased desriptions. 2.2. Renements. The need for suh proto ol primitives has also b een identied in other areas suh as distributed systems [11, 7, 23℄. In this ontext suh interations have b een studied for long, and there exist advaned tehniques to rene them (synhrony lo osening renements [10℄). Unfortunately, these renements an lead to deadlo k. Although the theory of renements has reahed a rather elab orate state in other ontexts, f. [1℄, there are not many results on interation renements or the haraterisation of their anomalies. The main reason is that lassial renements are ontext-free, whereas interation renements are ontextsensitive. Thus, the main problem is the establishment of their monotoniity prop erties [10℄, whereby their appliation to subparts of a proto ol preserves the orretness of the whole proto ol with resp et the set of valid synhronisation patterns it desrib es. The stateoftheart tehnique that fous on design time properties was presented in [12℄. It is based on designing a formal pro of system ( ooperating proof ) that allows to prove a suient ondition for monotoniity that ensures that a system omp osed of interations is deadlo k free. It is based on analysing linked interations, i.e., interations that need to b e exeuted in sequene, to avoid deadloks, whih was previously suggested in [9, 18℄. Unfortunately, this tehnique is quite diult to apply in pratie b eause it requires in-depth knowledge of the implied, intuitive meaning of the interations, and no automati proof rules were designed for showing the satisfation of the suient ondition. Our proposal an detet if a renement may lead to a deadlo k situation automatially, and also haraterises the set of traes that lead to it by means of regular expressions. It is based on FSA analysis used by many researhers in the ontext of lient/server deadlo k detetion of interation mo dels [5, 14, 36℄. 3. Engineering MultiAgent Systems with MaCMAS. MaCMAs 1 is a metho dology for engineering omplex multiagent systems that is integrated with several researh elds, i.e. autonomi omputing [31℄, software pro dut lines [27, 28℄ and evolving systems [29℄. 1 see james.eii.us.es/MaCMAS/ for further details on MaCMAS 52 Joaquín Peña, Rafael Corhuelo and Antonio Ruiz-Cortés Requirements Abst. Layer 1 Abst. Layer 2 Abst. Layer 3 Abst. Layer n-1 Abst. Layer n Decomp./ Ref. … Comp./ Abst. Requirements reuse reuse traceability abstraction Macro-Level Micro - Level Focus of this paper Fig. 3.1 . Proess Overview MaCMAS overs arefully the ve priniples to deal with omplexity in software engineering where top-down and b ottom-up are of high imp ortane [16, 17, 30℄: abstration, deomp osition/renements, omp osition/abstration, automation and reuse. In Figure 3.1, we show an overview of the main onepts applied in MaCMAS from the software pro ess p oint of view. As shown, mo dels of the system are strutured into a set of abstration layers. Top mo dels are the most abstrat while bottom mo dels are the most rened mo dels. MaCMAS provides also a set of vertial and horizontal transformations. Vertial transformations are applied to split mo dels or to omp ose mo dels, and horizontal transformations are used to rene and abstrat mo dels in order to over b ottom-up and top-down software pro esses. As shown, for overing the rest of priniples, traeability b etween mo dels at dierent abstration layers and reuse of mo dels and their abstrations/renements is also provided. In MaCMAS, two kind of renements are proposed. One that is base on analyzing information on requirement do uments, onretely system goals hierarhies, to reommend the user of the CASE to ol whih mo dels an b e rened and whih is the b est deomp osition reommended. The other renement, whih is the fo us of this pap er, is based on analyzing the dep endenies b etween the elements in a mo del to reommend a renement. 3.1. Mo dels. In other to engineer MASs, MaCMAS provides a rih set of UML2.0-based models that an b e summarized in: a) Stati Aquaintane Organization View: This shows the stati interation relationships between roles in the system and the knowledge pro essed by them. It omprises the following UML mo dels: Role Mo dels: shows an aquaintane sub-organization as a set of roles ollab orating by means of several mRIs. As mRIs allow abstrat representation of interations, we an use these mo dels at whatever level of abstration we desire. We use role mo dels to represent autonomous and autonomi properties of the system at the level of abstration we need. Parameterized Role Mo dels : A parameterised role mo del p ermits us to represent reusable ollaboration patterns parameterising some of their elements. Resoures dep endeny mo del: A resoures dependeny mo del provides means for do umenting the dep endenies b etween knowledge entities and servies provided by roles in the ontext of an mRI and for do umenting the dep endenies b etween the knowledge of mRIs. Relating role mo dels mo del: As a result of using deomp osition and omp osition and of instantiating parameterised role models, we usually manage role models that are obtained from others. This mo del show the relationships b etween several role mo dels. Ontology: shows the ontology shared by roles in a role mo del. It is used to add semantis to the knowledge owned and exhanged by roles. A Top Down Approah for Desribing the Aquaintae Organisation of Multiagent Systems 53 % & ' ( ) * + , - . & ' ( / 0 1 2 3 4 5 6 1 7 2 8 9 : ; < = > ; ? @ A 7 B C = D E F G 2 C 6 1 E 5 ? @ H C 0 I C ? @ J = 7 9 C 7 K 1 2 1 6 B F 7 1 5 6 C 5 7 5 9 C ? @ L M N O P Q R Q S T U V W U X Y S T U V Z T [ V U W U X Y S V \ T ] ^ _ V \ ` V a V Y [ V _ b V \ Z T [ V U S T U V Z T [ V U c Y d T U T e f g d X d b _ h _ i ] X b Y d X Y _ V c ^ e X Y b \ X d b T Y Z T [ V U \ j ^ X _ V X k b U b d f Z T [ V U l T m a U V n b d f ` T m X b Y o ] b [ V U b Y V \ ` V _ T m a p o ] b [ V U b Y V \ l T m a p o ] b [ V U b Y V \ S V ] \ V o ] b [ V U b Y V \ ` f Y X m b _ h _ i ] X b Y d X Y _ V c ^ e X Y b \ X d b T Y Z T [ V U \ W X ^ X m V d V ^ b \ V [ S T U V Z T [ V U c a V Y g f \ d V m \ o ] b [ V U b Y V \ S V U X d b Y e S T U V Z T [ V U \ j T a q [ T r Y s t u v T d d T m q ] a o ] b [ V U b Y V \ Fig. 3.2 . Aquaintane analysis disipline b) Behavior of Aquaintane Organization View: The b ehavioral asp et of an organization shows the sequening of mRIs in a partiular role mo del. It is represented by two equivalent mo dels: Plan of a role: separately represents the plan of eah role in a role mo del showing how the mRIs of the role sequene. It is represented using UML 2.0 Proto olStateMahines [22, p. 422℄. It is used to fo us on a ertain role, while ignoring others. Plan of a role mo del: represents the order of mRIs in a role mo del with a entralized desription. It is represented using UML 2.0 StateMahines [22, p. 446℄. It is used to failitate easy understanding of the whole b ehavior of a sub-organization. ) Traeability view: This mo del shows how mo dels in dierent abstration layers relate. It shows how mRIs are abstrated, omp osed or deomp osed by means of lassiation , aggregation , generalization or redenition . Notie that we usually show only the relations between interations b eause they are the fo us of modeling, but all the elements that omp ose an mRI an also b e related. Finally, sine an mRI presents a diret orrelation with system goals, traeability mo dels learly show how a ertain requirement system goal is rened and materialized. This is main what helps us to bridge the gap b etween requirements and design. For the purp ose of this pap er, we only need to detail role mo dels, role mo del plans, whih are shown in the following setions. 4. The Example. The example we use hereafter is a debitard system. This problem an b e viewed as one of the basi oordination patterns in the agent e-ommere world, and it involves three dierent agent roles (hereafter roles): a p oint of sales role (PS) whih interats with the user, a ustomer aount manager role(CA), and a merhant aount manager role (MA). When a ustomer uses his or her debit ard, the agent playing role PS agrees with a CA agent and merhant aount agent on p erforming a sequene of tasks to transfer the money from the ustomer aount to the merhant aount, whih shall also b e harged the osts of the transation. If 54 Joaquín Peña, Rafael Corhuelo and Antonio Ruiz-Cortés Fig. 5.1 . Stati interation view of the debitard system. Fig. 5.2 . Plans of the roles in the debitard system. the ustomer aount annot aord the purhase b eause it has not enough money, the ustomer aount agent then pays on hirepurhase. 5. Mo deling the Proto ol with MaCMAS. As we showed ab ove, our approah starts when the requirements system goals to b e p erformed have b een already obtained. Then, we mo del eah task as an mRI as we show in the role mo del in Figure 5.1. These system goals in our example are mo deled as the following mRIs: approv is used by the CA role to inform the other parties if it an aord a purhase; transfer is used to transfer money from the CA to the MA by means of the PS; mRI hire _ p is used to buy on hire-purhase; nally, there is a two-party mRI alled next _ sale , whih is not further detailed, whose goal is to enapsulate the op erations needed to read the sum to b e transferred and the ustomer data from his or her debit ard. For further details on the knowledge pro essed by eah partiipants and in the mRI see the App endix. One the mRIs are identied and linked with their partiipant roles, we represent their p ossible sequenes by means of FSAs (see Figure 5.2). When an mRI is exeuted by more than one role it must app ear a transition in all the roles that perform it. Eah of these transitions represents the part of the mRIs that a role p erform. Whereby, A Top Down Approah for Desribing the Aquaintae Organisation of Multiagent Systems 55 w xy z { | } ~| y   w xy z { | } ~| y   w xy z { | } ~| y   w xy z { | } ~| y   w xy z { | } ~| y   w xy z { | } ~| y   costs balance Knowledge used by transfer  Knowledge used by transfer  price costs balance balance Knowledge used by transfer a) Before refinement b) After refinement okok price balance Fig. 5.3 . Deoupling mRI transfer . to exeute an mRI we must transit from one state to another in all the roles that partiipate on it. Furthermore, with the algorithms presented in [25℄, whih we outline in setion 6, we an automatially infer a single FSA that represents the role mo del proto ol as a whole. This alternative representation an b e used for b etter readability. Finally, eah mRI have to b e deorated with some additional information: suh as the dep endenies b etween they knowledge it pro ess, a guard for eah role, and so on. The knowledge dep endeny, as we show in the next setion, an b e analysed in order to rene mRIs. Furthermore, the guard of mRIs allows eah role to deide if it want to exeute the mRI or not, whih has been proved adequate to deal with proativity of agents [7, 19, 25℄. 5.1. Renements. The mo del we presented in previous setion takes advantage of omplex threeparty mRIs, whih provides a high level design of the proto ol. However, it should b e rened in an attempt to transform its mRIs into a set of simpler ones that are loser to message sequenes desription. That is to say, desribing them internally shall be easier. This is the next step in our approah. The renements are based on analysing the dep endenies b etween the knowledge that roles use from others in a partiular mRI. In order to automate the renement pro ess the designer has to build a dep endeny graph (see Figures 5.3, 5.4 and 5.5) whih shall b e analysed with the algorithms prop osed in [18, 10℄. To illustrate how our tehnique works we applied it to our example. The rst renement we an apply is deoupling [12℄. It an transform ertain n party mRIs into an m party mRI (m < n) followed by an mRI with n−m+ 1 partiipants. We an illustrate it by means of mRI transfer in our example. Figure 5.3 shows a diagram in whih we have depited the knowledge of its roles and their dep endenies. As shown, b oth the MA and CA need to up date their balanes aording to some information in the knowledge of the PS. The idea is thus to deouple mRI transfer into two binary mRIs so that the CA up dates its balane b efore the MA. Thus, as we an see in Figure 5.3 mRI transfer1 will exeuted by PS and CA, and transfer2 by PS and MA (see Figure 5.7 for the new sequenes of exeution). We have applied this renement to the mRI hire _ p , as well. The seond renement we an apply is partiipant elimination [12℄. It onsists of eliminating those roles from the set of partiipant roles of an mRI whose knowledge is not referred to by other roles and do not refer to the knowledge of any other role. Figure 5.4 shows a diagram in whih we have depited the knowledge of the roles partiipating in mRI approv and their relationships. Obviously, role MA an b e eliminated from this mRI. Another renement alled splitting , whih annot b e apply to our example, onsist in breaking an mRI into two mRIs if the knowledge aessed by several groups of roles are disjoint as is depited in Figure 5.5 with a titious mRI. The resulting role plans after applying all renements are presented in Figure 5.7. Apparently, they works well but we an disover that the renements have intro dued a deadlo k situation if we take a loser look. Consider a trae in whih the following mRIs are exeuted: next _ sale, approv, transfer1, and hire _ p1 . This exeution deadlo ks b eause of an unfortunate interleaving in whih, after approving a sale and harging the CA, this role is ready to interat with the PS by means of transfer2 ; however, the MA is readied then to 56 Joaquín Peña, Rafael Corhuelo and Antonio Ruiz-Cortés                                                             costs balance balance Knowledge used by aprob price costs balance balance Knowledge used by aprob a) Before refinement b) After refinement ok price ok Fig. 5.4 . Eliminating role from approv .                ¡       ¢                 ¡      ¢ £ ¤ ¥ ¦ £ ¤ ¥ § £ ¨ ¥ © £¨ ¥ ¦ £ ª ¥ ¦ £ « ¥ © £ « ¥ § £ « ¥ ¦ £ ª ¥ © Knowledge used by I ¬ Knowledge used by I  £ ¤ ¥ ¦ £ ¤ ¥ § £¨ ¥ © £¨ ¥ ¦ £ ª ¥ ¦ £ « ¥ © £ « ¥ § £ « ¥ ¦ £ ª ¥ © Knowledge used by I a) Before refinement b) After refinement Fig. 5.5 . Splitting titious mRI I . exeute b oth transfer1 and hire _ p1 . If hire _ p1 is exeuted now, it leads to a situation in whih no role an ontinue b eause PS is readying transfer2 and waits for the CA to ready it, the CA is readying approv and waits for the PS to ready it, and the MA is waiting for any of them to ready transfer1 or hire _ p1 . This situation an b e avoided if we use a guard for transferi and hire _ pi that ensures that when one of these mRI is exeuted the guard of the others shall b e evaluated as false, but unfortunately this is not p ossible in general. These renements allow us to exeute several mRIs at the same time sine the the knowledge they omputed b efore renements is now omputed separately in dierent mRIs. In addition, they simplify the numb er of partiipant roles that eah mRI uses, whih lead us to easier implementations (the proto ol to o ordinate n parties is more diult that suh for two parties) [12, page. 206℄[2, 33, 21, 35℄. Finally, another advantage is that the amount of knowledge to b e pro essed in eah mRI dereases thus easing their internal design. For instane, the mRI transfer has b een broken into two simpler mRIs: transfer1 and transfer2 . transfer1 omputes the balane of the CA and transfer2 omputes the balane of the MA. Thus, simpler omputations are performed. Furthermore, the original mRI had three partiipant roles, and the new mRIs have only two, whose o ordination/negotiation proto ol is simpler to implement. The rened role model is presented in Figure 5.6. 6. Ensuring Deadlo k Free Renements. Our approah to detet deadlo ks is based on building an FSA and analysing its paths. Next, we present some results we need, and then we show how to onstrut the FSA and how to analyse it. A Top Down Approah for Desribing the Aquaintae Organisation of Multiagent Systems 57 Fig. 5.6 . Role model of the debitard system after renements. Fig. 5.7 . Role plans after renement. As we an see in Figure 5.7, the denition of the protool of eah role is done by means of FSAs. They an b e haraterised as follows: Definition 6.1 ( Finite State Automaton ). A nite state automaton (FSA) is a tuple of the form (S, Σ, δ, s0, F ) , where S is a set of states, Σ is a set of mRIs (the voabulary in FSA theory), δ:S×Σ→S is a transition funtion that represents an mRI exeution, s0∈S is an initial state, and F⊆S is a set of nal states. Thus, let Ai= (Si,Σi, δi, s0 i, Fi) (i= 1,2,···, n) b e the set of FSAs that represents eah role in a role mo del. Starting from this information we an build a new FSA C= (S, Σ, δ, s0, F ) that represents the proto ol as a whole, where •S=S1× · · · × Sn •Σ = Sn i=1 Σi •δ(a, {s1,...,sn}) = {s′ 1,...,s′ n} i ∀i∈[1..n]·(a6∈ Σi∧si=s′ i)∨(a∈Σi∧δ(a, si) = s′ i)