A Formal Programming Framework for Digital Avatars

A Fo mal P og amming F amewo k o Digi al A a a s? Alejand o P´e ez-Ve eda, Ca los Canal, and E nes o Pimen el Uni e si y o Malaga, Spain [email p o ec ed],[email p o ec ed],[email p o ec ed] Abs ac . In he cu en IoT e a, he numbe o sma hings o in e ac wi h is aising e e yday. Howe e , each one o hem p ecises a manual and speci ic con igu a ion. In a mo e people- iendly scena io, sma hings should adap au oma ically o he p e e ences o hei use s. In his ield, we ha e pa icipa ed in he design o People as a Se ice, a mobile compu ing e e ence a chi ec u e which endows he sma phone wi h he capabili y o in e ing and sha ing a i ual p o ile o i s owne . Cu en ly, we a e de eloping Digi al A a a s, a amewo k o p og amming in e ac- ions be ween sma phones and o he de ices. This way, he sma phone becomes a pe sonalized and seamless in e ace be ween people and hei IoT en i onmen , con igu ing he sma hings wi h in o ma ion om he i ual p o ile. In his wo k, we p esen a o maliza ion o Digi al A a a s by means o a Linda-based sys em wi h mul iple sha ed uple spaces. Keywo ds: Digi al A a a s, People as a Se ice, PeaaS, Linda, Sha ed Tuple Spaces. 1 In oduc ion The In e ne o Things (IoT) is buil o e a laye o connec ed de ices and senso s ha o e speci ic in e aces o access he in o ma ion hey collec and also o con igu e how hey wo k, e.g. he equency o pick up he da a o how o o ma hem [ 9 ]. Recen esea ch in he IoT ield has p omo ed he de elopmen o de ices and senso s which a e mo e con igu able and p o ide easie in e aces. They a e known as sma hings [ 11 ]. Howe e , sma hings s ill equi e a lo o manual con igu a ion, and his p oblem becomes mo e challenging he bigge he numbe o de ices we daily in e ac wi h. In a desi able scena io, he echnology should wo k o he people and no he o he way a ound. E e y sma hing should adap o he needs o he people seamlessly and in an au oma ic way, educing he need o in e ac ion wi h he use s o he minimum. Conside ing he pe asi e p esence o sma phones, he au ho s o his pape ha e pa icipa ed in he design o a mobile compu ing e e ence a chi ec u e ? This wo k has been unded by he Spanish Go e nmen unde g an s PGC2018- 094905-B-I00 and TIN2015-67083-R (MINECO/FEDER). called People as a Se ice (PeaaS) [ 10 ]. This a chi ec u e p omo es he use o sma phones o lea n abou hei use s, c ea ing and s o ing i ual p o iles wi h hei p e e ences and con ex in o ma ion. These p o iles a e hen o e ed as a se ice o hi d pa ies in a secu e manne . This way, sma phones become seam- less and au oma ic in e aces ha nego ia e hei owne ’s p e e ences, adap ing and con igu ing he sma hings in hei su oundings. Fo ha pu pose, he equi ed in e ac ions a e no jus simple da a ans e s, bu we need mechanisms ha allow o con igu e sma hings, and also o comple e i ual p o iles wi h con ex knowledge ob ained om hese in e ac ions. The mo e comple e i ual p o iles a e, he be e may he echnology adap o he people. Wi h his goal in mind, we a e de eloping Digi al A a a s, a dynamic p og amming amewo k which allows de ining he in e ac ions be ween sma phones and sma hings by means o on- he- ly sc ip s [ 13 ]. The sc ip s a e execu ed in he sma phone, and hey make use o he i ual p o ile s o ed in i o econ igu ing he beha io o he sma hing wi h he in o ma ion a ailable. Ou p og amming amewo k is inspi ed by he ision o a P og ammable Wo ld [ 17 ], which o esees he e olu ion om oday’s IoT based on da a ecollec- ion o uly p og ammable de ices. This way, bo h sma hings and sma phones a e able o lea n om each o he , and o e ol e h ough each in e ac ion in a anspa en and dynamic way. In his pape , we p esen a o mal amewo k o Digi al A a a s. The ame- wo k p o ides a o mal desc ip ion o i ual p o iles and he sc ip s o execu e on hem, and i es ablishes he basis o issues like p i acy o secu i y, wi h secu e connec ions con olling he access o i ual p o iles. The o maliza ion is based on a mul iple sha ed uple spaces model inspi ed by Linda, which makes possible o ensu e he soundness o he amewo k, and makes easible he analysis o some in e es ing p ope ies. The es o his pape is s uc u ed as ollows. In Sec ion 2 we p esen he mo i a ions o his pape and discuss some ela ed wo ks. Nex , Sec ion 3 de ines he concep s necessa y o eason on Digi al A a a s. In Sec ion 4, we o malize he in e ac ions ha ake place in he amewo k and demons a e in e es ing o mal p ope ies o he sys em. Then, Sec ion 5 p esen s a p oo o concep and analyze i s implemen a ion using he amewo k. Finally, Sec ion 6 d aws he conclusions o he pape and b ie ly discusses u u e wo k. 2 Backg ound The de elopmen o sma hings is ans o ming people’s li es, as we inc easingly in e ac wi h hem e e yday. Social Compu ing (SC) [ 18 ] is he a ea o compu e science ha deals wi h he in e ac ion be ween social beha io and compu e sys ems. SC encompasses all hose sys ems ha collec , p ocess and dissemina e in o ma ion ela ed o indi iduals and g oups o people. The goal is lea ning abou people and hei p e e ences and p o iding an easy adap a ion o hei IoT en i onmen , educing manual con igu a ion o de ices o a minimum. Indeed, a numbe o ecen esea ch wo ks ag ee on gi ing suppo o he IoT by means o a pa adigm ocused on people [16]. Cu en ly, e y ew companies a e able o access and p ocess his eno mous quan i y o social in o ma ion, and o exploi and make a p o i om i . In p ac ice, his educes he SC ma ke place o a small numbe o big s akeholde s. As Tim Be ne s-Lee decla ed ecen ly [ 1 ], SC sys ems should empowe people, making hem he ai owne s o hei in o ma ion, and deciding who has access o i . Mo eo e , his in o ma ion mus be s o ed in a unique and accessible place which le s hi d pa ies use i in a con olled way, ollowing he p i acy p e e ences o he use s. In his same sense, we ad oca e o de eloping collabo a i e a chi ec u es based on sma phones. Thei pe asi e p esence in people’s e e yday li es and hei inc easing senso ing and compu ing capabili ies, oge he wi h hei com- munica ion skills, make hem key elemen s o ob aining, p ocessing, and sha ing in o ma ion abou hei use s [ 15 ]. Sma phones a e also he mos app op ia e de ices o be in cha ge o nego ia ing he in e ac ions o hei use s wi h sma hings in hei en i onmen . A chi ec u es based on P2P models a e g adually acqui ing a g ea e p esence in ields such as social ne wo ks [ 19 ] o ecommenda ion sys ems [ 20 ]. The basis o hese a chi ec u es a e he i ual p o iles o he use s, plen y o con ex ual da a (e.g. ac i i ies, ela ions wi h o he use s, e c.) [ 8 ]. Ou goal is sha ing hese i ual p o iles wi h hi d pa ies and o adap he IoT en i onmen o he p e e ences and needs o each use . Wi h ha pu pose in mind, ou app oach is based on a Linda-like model. Linda [ 7 ] is a coo dina ion language whe e synch oniza ion is achie ed by means o a sha ed uple space, and h ough a se o simple bu enough exp essi e p imi i es [ 2 ]. Howe e , a single sha ed uple space would iola e he p inciples o he PeaaS model. Some o he Linda-like p oposals ha e been made by di e en au ho s, in oducing some kind o mobili y, mainly based on adding capabili ies o emo ely modi ying a gi en uple space. Thus, Lime [ 14 ] was p oposed as a Linda ex ension o suppo mobile compu ing, by he de ini ion o ansien ly sha ed dis ibu ed uple spaces o es ablish P2P communica ions. Some o i s goals a e common wi h ou s, bu ou amewo k also akes in o accoun p i acy issues, which a e c ucial o i ual p o iles. Ano he well-known p oposal is KLAIM [ 5 ], which ex ends Linda by conside ing he possibili y o emo e adding uples o an accessible uple space. Wi h a simila philosophy, SCEL [ 6 ] was designed o p o ide a pa ame ic language o cap u e a ious p og amming abs ac ions o au onomic componen s and hei in e ac ion. In bo h cases, Linda-like p imi i es we e added o allow he emo e in e ac ion wi h sha ed uple spaces. Al hough he PeaaS pa adigm could be (a i icially) coded by hese languages, a numbe o assump ions and cons ain s should be made o ensu e he main PeaaS ea u es. In ac , we conside ha accessing o a i ual p o ile has o be made only by i s owne , and emo e accessing o ansien uple spaces o sha ed eposi o ies do no model hese scena ios p ope ly. 3 Modeling Digi al A a a s In o de o de ine a o mal amewo k o easoning on Digi al A a a s, we in oduce he no ion o i ual p o ile oge he wi h a numbe o ela ed concep s, and we desc ibe how i ual p o iles can be o e ed as se ices unde he PeaaS pa adigm. 3.1 De ini ions The key issue o aking in o accoun he use in an IoT en i onmen is he i ual p o ile. I con ains in o ma ion abou use p e e ences, habi s, mo emen s, o ela ions. All his in o ma ion is only s o ed in he use ’s de ice (e.g. a sma phone), and i is o e ed as a se ice o hi d pa ies. The de ini ion below o malizes his no ion. De ini ion 1. A i ual p o ile P is a mul ise o en i ies, whe e each en i y is a 5- uple = ( n, s, p, , s )composed o (i) n∈Name ep esen ing he name o he en i y, (ii) s∈Type de ines he en i y’s ype, (iii) p∈P i acy , which p o ides he le el o p i acy, (i ) ∈Value is he alue o he en i y i sel , wi h a s uc u e which will depend on he en i y’s ype, and ( ) a imes amp s ∈T ime , which allows eco ding he ime when he uple is added o he i ual p o ile. We will deno e by T he se o uples, and by P he se o i ual p o iles. The complexi y o i ual p o iles depends on he se s Name , Type , P i acy , Value , and Time . These en i ies a e s uc u ed in nes ed sec ions o he secu e and co ec unc ioning o he p o ile. Al hough he model does no depend on how hese pa icula domains a e de ined, we conside a common minimum s uc u e o p ede ined en i ies which a e cha ac e ized as ollows: Pe sonal I consis s in pe sonal and con ac in o ma ion o he use ( pe sonal ∈ Name ); he de aul p i acy is p i a e ∈P i acy , al hough i can be o e - w i en in each a ibu e o allow accessing i o amily o iends, o in- s ance. Basically, i con ains a collec ion o en i y iden i ie s like name , phone , add ess, o email wi h he co esponding in o ma ion. Rela ions I p o ides in o ma ion on how use s a e ela ed o each o he ( ela ion ∈ Name ), such ha alues includes en i y names like amily , iends , colleagues , o acquain ances . These nes ed en i ies a e collec ions o use (pe sonal) in o ma ion wi h in o ma ion abou loca ion, social p o iles and hei ce i i- ca e hash inge p in . The de aul p i acy le el o hese en i ies is p i a e ∈ P i acy. Places I de ines in o ma ion in a p o ile conce ning loca ions ( place ∈Name ): home, place o wo k, known places o o he places. Thus, cons an s like home o wo k belong o he Name se in he alue o his en i y. Thei de aul p i acy le el is us ed. A i ual p o ile can be accessed and/o modi ied by means o p ocesses execu ing app op ia e ac ions. In o de o o malize his idea, we a e inspi ed by Linda [ 4 ], a coo dina ion language [ 7 ] consis ing o a se o in e -agen communi- ca ion p imi i es, which can be i ually added o any p og amming language. P imi i es in Linda allow p ocesses o ead, dele e, and add uples in a sha ed uple space. Tuple spaces a e a con enien app oach o ep esen i ual p o iles sha ed by concu en ly unning p ocesses. A i ual p o ile is ep esen ed by a mul ise o uples encapsula ed in a de ice. Thus, we adop a mul iple uple space model. Following o he app oaches [ 3 , 12 ], we shall conside a p ocess algeb a L includ- ing he Linda communica ion p imi i es and he usual concu ency connec i es, pa allel and non-de e minis ic choice. The p imi i es pe mi o add a uple (ou ), o emo e a uple (in), and o check he p esence (o absence) o a uple ( d, n d) in a gi en p o ile ( uple space). P ocesses in L p o ide a con enien way o model sc ip s which can be downloaded om a se e and un on a sma de ice. Thus, he syn ax o L is o mally de ined as ollows: S∈ L ::= 0 |α.S |S+S|SkS|S(˜ ) α∈Ac ::= d( )|n d( )|in( )|ou (d, ) whe e 0 deno es he emp y p ocess, d∈D a de ice iden i ie , and deno es a uple. The p ocess S ( ˜ ) deno es a p ocedu e call whe e he p ocedu e de ini ion will be gi en by a sc ip empla e S ( ˜x ) (whe e ˜x is a sequence o a iables ins an ia ed by a sequence o uples ˜ ). In o de o simpli y he de ini ion o ules modelling he L p imi i e ac ions in Subsec ion 4.2, we will assume ha eading a uple do no imply he e alua ion o usual ope a ions (e.g. a i hme ic ope a ions) no he a iable ins an ia ion as usual in Linda-based languages. This assump ion does no imply any loss o gene ali y o he p oposal. No ice ha we conside p imi i es o locally accessing, adding, and emo ing uples o a uple space (i.e. a i ual p o ile). Al hough we could ha e also conside ed accessing and dele ing uples om emo e uple spaces, o ou pu poses we only need o add uples emo ely. Fo his eason, only he ou p imi i e includes as a pa ame e he de ice on which adding he uple. Tha is, d , in and n d ac ions will be made locally, on he same de ice whe e he sc ip is being un. The same conside a ions we e made in [ 12 ]. As i will be shown la e , emo e adding o uples will only a ec o he a i ac whe e he sc ip was downloaded om, hus we will no allow a bi a y emo e adding o uples. This asymme ic ea men o ou and ead p imi i es a e p ecisely one o he ea u es de o ed by he PeaaS model: local accessing is only made by de ice owne s, and emo e changes can only be made on a i ac s p o iding he sc ip s o be un. In ou amewo k, we dis inguish wo kinds o a i ac s: sma de ices and sma hings. The di e ence be ween hem is ha sma de ices exhibi compu ing capabili ies, and he e o e hey can download and execu e sc ip s, whe eas sma hings only p o ide a (link o a) sc ip . Fo mally, we de ine an a i ac as a pai consis ing o a i ual p o ile and a p ocess co esponding o he execu ion o one o se e al sc ip s. We assume ha D is a se o a i ac iden i ie s. E e y a i ac d also has associa ed a sc ip de ini ion Sd ( ˜x ) which can be downloaded by o he a i ac s wi h compu ing capabili ies (i.e. sma de ices). De ini ion 2. An a i ac d∈D is cha ac e ized by a pai hP : Sid , including a i ual p o ile P and a p ocess S∈ L , co esponding o he unning sc ip s on he a i ac . In addi ion, an a i ac can con ain a sc ip de ini ion Sd ( ˜x ). We will deno e by Sd ( P ) he sc ip ins an ia ed by he speci ic uples in he p o ile P . And we will ep esen by D=P × L × D he se o a i ac s. A sma hing will be cha ac e ized by ha ing only a p o ile; ha is, i s p ocess is always he emp y p ocess 0. A ypical example o sma hing would be a beacon b oadcas ing a Blue oo h Low Ene gy (BLE) signal which encodes he URL o a sc ip ile o be downloaded om a se e . On he o he hand, ypical sma de ices a e sma phones, able s, o any o he de ice wi h compu ing capabili ies. Bo h kinds o a i ac s —sma hings and sma de ices— s o e in o ma ion in a i ual p o ile. 3.2 Secu i y in Digi al A a a s The ac ions execu ed o e he i ual p o ile o a sma de ice may eme ge om in e nal p ocesses o he de ice, o hey may be pa o a sc ip downloaded om ano he a i ac (e.g. a beacon b oadcas ing a link o a sc ip ile) when se e al condi ions a e ul illed: he sma de ice is close enough o he beacon, he beacon a i ac is egis e ed, i s sc ip code is us ed, e c. In o de o a oid unning un us ed sc ip s, we assume a Ce i ica ion Au ho - i y capable o ensu e he us ulness o an a i ac d , and a Boolean mapping ce i y which p o ides his in o ma ion in such a way ha ce i y ( d ) is ue when he emi e o dhas been au hen ica ed. In addi ion, he ou p imi i e conside ed in he p e ious sec ion allows adding uples o bo h local and emo e i ual p o iles. Al hough he model imposes no limi a ions on which p o iles can be emo ely modi ied, he a i ac iden i ie d used in a emo e ou (d, ) in a sc ip Sd ( ˜x ) can only be ha o he a i ac d i sel . Thus, an a i ac ’s p o ile may only be emo ely modi ied by unning a sc ip downloaded om his same a i ac . Hence, in o de o gua an ee ha he ac ions execu ed while unning a sc ip on a sma de ice a e secu e, we assume a Boolean mapping accep : Ac × P → { ue, alse} ha es ic s which p imi i es a e enabled, in such a way ha accep (α, P ) is ue when he ac ion αis accep able on he p o ile P. Howe e , using ce i ica es and es ic ing emo e addi ion o uples is no enough o ensu e a co ec in e ac ion be ween sou ce and a ge a i ac s, and we also need o conside some echnical issues. Indeed, whe eas ce i y p o ides a hi d-pa y decla a ion abou he us o an a i ac , and accep con ols wha ac ions a e pe mi ed inside an a i ac once he sc ip has been downloaded, we need a way o de ec when wo a i ac s a e ac ually able o communica e wi h each o he . Fo ins ance, conside a scena io whe e a sma phone ( ep esen ed by a i ual p o ile P ) app oaches a sma hing d which p o ides a sc ip Sd ( ˜x ). Fo downloading he sc ip om d and unning i in he sma phone, we assume a mapping links : P ×D→ 2 T , which p o ides a link o connec o he sma hing, depending on he a ailabili y o download, he closeness be ween bo h a i ac s, good signal s eng h, e c. This mapping e u ns a se o uples ep esen ing links (e.g., a URI o a blue oo h connec ion) p o iding a way o access he a i ac d . I he e a e no links, o he p o ile P does no accep downloading he sc ip o e ed by d,links(P, d) will be he emp y se . No ice ha all he no ions in oduced in his subsec ion (accep ,ce i y, and links) a e applica ion speci ic, in such a way ha hei pa icula de ini ions will depend on he applica ion domain and con ex whe e ou amewo k is applied o. 4 Fo mal amewo k Now ha we ha e de ined he main elemen s and concep s o ou amewo k, we can o malize he in e ac ions be ween a i ac s by means o a ansi ion sys em wi h in-de ice and emo e ope a ions. Then, we show how some in e es ing p ope ies like bisimila i y and cong uence a e accomplished by he model. 4.1 In-de ice ansi ion sys em The ope a ional seman ics o L is modeled by he ollowing labelled ansi ion sys em: · −→⊆ D × Λ× D de ined by he ules 1 o Table 1, whe e D = P × L × D and Λ = { , , : ∈ T}∪{τ}. Rule Ou 1 desc ibes how he ou pu ope a ion p oceeds as an in e nal mo e ( ep esen ed by label τ ) which adds he uple o he p o ile P (comma is used o ep esen he mul ise union). Rule Ou 2 shows ha a uple is eady o o e i sel o he a i ac /de ice by pe o ming an ac ion labelled . Rules In and Read desc ibe he beha io o he p e ixes in ( ) and d ( ) whose labels a e and , espec i ely. Rule NRead desc ibes he p e ix ac ion n d ( ), which p oceeds when is no in he p o ile P ; he ansi ion is labelled wi h ¬ . All hese ules need ha he cu en de ice’s p o ile accep s he co esponding ac ion. I is wo h no ing ha we do no include any kind o e alua ion no a iable ins an ia ion when eading uples, as i is usually made in Linda- ela ed ansi ion ules. This is only o simplici y easons wi hou loss o gene ali y. Rule Sum is he s anda d ule o choice composi ion. Rule Sync 1 is he s anda d ule o he synch oniza ion be ween he complemen a y ac ions and . I models he e ec i e execu ion o an d ( ) ope a ion. No ice ha he esul ing p o ile is le unchanged, since he ead ope a ion d ( ) does no modi y i . Rule Sync 2 de ines he synch oniza ion be ween wo p ocesses pe o ming ansi ions labelled wi h and , espec i ely. I models he e ec i e execu ion o in ( ) 1Fo he sake o simplici y we will conside only ini e p ocesses he e. ac ion. The usual ule Pa 1 o he pa allel ope a o can be applied o any label. The ansi ion sys em is conside ed closed w. . . commu a i e and associa i e p ope ies o sum (+) and pa allel (k) ope a o s. (Ou 1)accep (ou (d, ), P ) hP:ou (d, ).Sid τ −→ hP, :Sid (Ou 2)hP, :Sid ¯ −→ hP:Sid (Read)accep ( d( ), P ) hP: d( ).Sid −→ hP:Sid (In)accep (in( ), P ) hP:in( ).Sid −→ hP:Sid (NRead) 6∈ P∧accep (n d( ), P ) hP:n d( ).Sid ¬ −→ hP:Sid (Sum)hP:S1id α −→ hP0:S0 1id hP:S1+S2id α −→ hP0:S0 1+S2id (Sync1)hP:S1id −→ hP:S0 1idhP:S2id −→ hP0:S2id hP:S1kS2id τ −→ hP:S0 1kS2id (Sync2)hP:S1id −→ hP:S0 1idhP:S2id −→ hP0:S2id hP:S1kS2id τ −→ hP0:S0 1kS2id (Pa 1)hP:S1id α −→ hP0:S0 1id hP:S1kS2id α −→ hP0:S0 1kS2id Table 1. T ansi ion sys em o sma de ices No ice ha ac ion ou ( d, ) is only conside ed in Table 1 when i is unning in he de ice d . I s ull beha io ( emo e adding o uples) will be de ined when he in e ac ion among de ices is exp essed in Table 2. 4.2 Remo e ansi ion sys em In o de o de ine how a i ac s in e ac , we conside con igu a ions composed o a pa allel composi ion o a i ac s as ollows: hP1:S1id1| hP2:S2id2| · · · | hPn:Snidn whe e Pi ( i = 1 ..n ) a e i ual p o iles o a i ac s —ei he sma de ices and sma hings—, Si a e sc ip s unning in sma de ices, and di ep esen he de ice iden i ie s. No ice ha we deno e in a di e en way he pa allel composi ion o a i ac s ( | ) and he pa allel composi ion o p ocesses inside a sma de ice ( k ). The ansi ion sys em · −→ de ined in Table 1 is ex ended o con igu a ions by he in e ence ules gi en in Table 2. (Remo e)accep (ou (e, ), Q) hP:ou (e, ).Sid| hQ:Tie τ −→ hP:Sid| hQ, :Tie (Sync3)ce i y(e)∧b∈links(P, e) hP:Sid| hQ:Tie τ −→ hP, b :SkSe(b, Q)id| hQ:Tie (Pa 2)D1 α −→ D0 1 D1|D2 α −→ D0 1|D2 Table 2. T ansi ion sys em Rule Remo e models emo e ac ions modi ying he i ual p o ile which belongs o he sma hing om which he sc ip being un was downloaded. We conside his ansi ion as a silen s ep om an obse a ional poin o iew. Fo his eason, we use he label τ. Rule Sync 3 ep esen s he in e ac ion be ween wo a i ac s ( ypically, a sma de ice and a sma hing). In his case, he sc ip associa ed wi h a sma hing e , p e iously ce i ied, is downloaded h ough a link b es ablishing a connec ion be ween he i ual p o ile P and e . Thus, he sc ip o be execu ed in he con ex o he sma de ice d (in pa allel wi h o he possible pending p ocesses) will be Se ( b, Q ) (such as i was de ined in De ini ion 2). No ice ha , in his case, he sc ip is ins an ia ed no only by he p o ile Q bu also by he link b . This allows cus omizing he sc ip o he a i ac which p o ides access o i . In addi ion, he link uple b is added o he p o ile P , so eco ding ha he sma hing has been al eady “ isi ed”. Rule Pa 2 desc ibes he way in which he pa allel composi ion o a i ac s p oceeds. No e ha he pa allel composi ion o p ocesses inside a sma de ice is modelled by Rule Pa 1 in Table 1. Ac ually, any in e ac ion in he con ex o a sma de ice is go e ned by ules in ha able. We conside he ansi ion sys em closed w. . . usual s uc u al cong uence (commu a i e and associa i e p ope ies) o bo h pa allel connec o s. The ules in Table 1 and Table 2 a e used o de ine he se o de i a ions in an en i onmen whe e sma de ices and sma hings a e in e ac ing wi h each o he . Following [ 3 ], bo h educ ions labelled τ and educ ions labelled ¬ a e conside ed. Fo mally, his co esponds o in oducing he ollowing de i a ion 3. Nadia Busi, Robe o Go ie i, and Gianluigi Za a a o. On he Tu ing equi alence o Linda coo dina ion p imi i es. Elec . No es Theo . Compu . Sci., 7:75, 1997. 4. Nicholas Ca ie o and Da id Gele n e . Linda in con ex . Commun. ACM, 32(4):444– 458, Ap il 1989. 5. R. De Nicola, G. L. Fe a i, and R. Pugliese. Klaim: a ke nel language o agen s in e ac ion and mobili y. IEEE T ansac ions on So wa e Enginee ing, 24(5):315– 330, May 1998. 6. Rocco De Nicola, Diego La ella, Albe o Lluch La uen e, Michele Lo e i, And ea Ma ghe i, Mieke Massink, And ea Mo iche a, Rosa io Pugliese, F ancesco Tiezzi, and And ea Vandin. The SCEL Language: Design, Implemen a ion, Ve i ica ion, pages 3–71. Sp inge In e na ional Publishing, Cham, 2015. 7. Da id Gele n e and Nicholas Ca ie o. Coo dina ion languages and hei signi i- cance. Commun. ACM, 35(2):96–, Feb ua y 1992. 8. To -Mo en G ønli, Gheo ghi a Ghinea, and Muhammad Younas. Con ex -awa e and au oma ic con igu a ion o mobile de ices in cloud-enabled ubiqui ous compu - ing. Pe sonal and ubiqui ous compu ing, 18(4):883–894, 2014. 9. Jaya a dhana Gubbi, Rajkuma Buyya, Sla en Ma usic, and Ma imu hu Palaniswami. In e ne o Things (IoT): A ision, a chi ec u al elemen s, and u u e di ec ions. Fu u e gene a ion compu e sys ems, 29(7):1645–1660, 2013. 10. Joaquin Guillen, Ja ie Mi anda, Ja ie Be ocal, Jose Ga cia-Alonso, Juan Manuel Mu illo, and Ca los Canal. People as a Se ice: a mobile-cen ic model o p o iding collec i e sociological p o iles. IEEE so wa e, 31(2):48–53, 2014. 11. Dominique Guina d, Vlad T i a, F iedemann Ma e n, and E ik Wilde. F om he In e ne o Things o he Web o Things: Resou ce-o ien ed a chi ec u e and bes p ac ices. In A chi ec ing he In e ne o Things, pages 97–129. Sp inge , 2011. 12. Ronaldo Menezes, And ea Omicini, and Mi ko Vi oli. On he seman ics o coo di- na ion models o dis ibu ed sys ems: The LogOp case s udy. In Founda ions o Coo dina ion Languages and So wa e A chi ec u e (FOCLASA 2003), olume 97 o Elec onic No es in Theo e ical Compu e Science, pages 97–124. Else ie , 2004. 13. Alejand o P´e ez-Ve eda, Daniel Flo es-Ma ´ın, Ca los Canal, and Juan M Mu illo. Towa ds dynamically p og ammable de ices using beacons. In In e na ional Con- e ence on Web Enginee ing, olume 11153 o LNCS, pages 49–58. Sp inge , 2018. 14. Gian Pie o Picco, Amy L. Mu phy, and G uia-Ca alin Roman. Lime: Linda mee s mobili y. In P oceedings o he 21s In e na ional Con e ence on So wa e Enginee ing, ICSE ’99, pages 368–377. ACM, 1999. 15. Mika Raen o, An i Oulas i a, and Na han Eagle. Sma phones: An eme ging ool o social scien is s. Sociological me hods & esea ch, 37(3):426–454, 2009. 16. Jo ge Sa Sil a, Pei Zhang, T e o Pe ing, Fe nando Boa ida, Takahi o Ha a, and Nicolas C Liebau. People-cen ic In e ne o Things. IEEE Communica ions Magazine, 55(2):18–19, 2017. 17. An e o Tai alsaa i and Tommi Mikkonen. A oadmap o he p og ammable wo ld: so wa e challenges in he IoT e a. IEEE So wa e, 34(1):72–80, 2017. 18. Fei-Yue Wang, Ka hleen M Ca ley, Daniel Zeng, and Wenji Mao. Social compu ing: F om social in o ma ics o social in elligence. IEEE In elligen sys ems, 22(2), 2007. 19. Yu eng Wang, A hanasios V. Vasilakos, Qun Jin, and Jianhua Ma. Su ey on mobile social ne wo king in p oximi y (MSNP): app oaches, challenges and a chi ec u e. Wi eless ne wo ks, 20(6):1295–1311, 2014. 20. Wan-Shiou Yang and San-Yih Hwang. iT a el: A ecommende sys em in mobile pee - o-pee en i onmen . Jou nal o Sys ems and So wa e, 86(1):12–20, 2013.