Expressiveness of probabilistic pi calculi

Sylvain Pradalier†

Description

Niveau: Supérieur
Expressiveness of probabilistic pi-calculi? Sylvain Pradalier† Catuscia Palamidessi‡ Abstract In this work we propose a probabilistic extension of the pi-calculus. The main novelty is a probabilistic mixed choice operator, that is, a choice construct with a probability distribution on the branches, and where input and output actions can both occur as guards. We develop the operational semantics of this calculus, and then we investigate its expressiveness. In particular, we compare it with the sublanguage with the two separate choices, where input and output guards are not allowed together in the same choice construct. Our main result is that the separate choices can encode the mixed one. Further, we show that input-guarded choice can encode output-guarded choice and viceversa. In contrast, we conjecture that neither of them can encode the pair of the two separate choices. 1 Introduction In the field of concurrent languages, expressiveness is an important and intriguing problem. Differently from the case of sequential languages, the purpose of a program is not just to compute a function, but also to control the communication and the interaction of the various parallel components of a system. There are therefore more parameters and perspectives which must be taken into account when assessing the expressive power of a new formalism. Most of the main process calculi proposed in literature have been widely investigated from the point of view of the expressive power, both in abso- lute terms, i.

• probabilistic mixed


• output


• using only


• has been proved


• main probabilistic


• input- guarded choice

Sujets

• École polytechnique
• Output

Informations

• Publié par: chaeh
• Nombre de lectures: 11
• Langue: English

Extrait

Expressivenessofprobabilisticπ-calculi ∗ SylvainPradalier † CatusciaPalamidessi ‡ Abstract Inthisworkweproposeaprobabilisticextensionoftheπ-calculus. Themainnoveltyisaprobabilisticmixedchoiceoperator,thatis,a choiceconstructwithaprobabilitydistributiononthebranches,and whereinputandoutputactionscanbothoccurasguards.Wedevelop theoperationalsemanticsofthiscalculus,andthenweinvestigateits expressiveness.Inparticular,wecompareitwiththesublanguage withthetwoseparatechoices,whereinputandoutputguardsarenot allowedtogetherinthesamechoiceconstruct.Ourmainresultisthat theseparatechoicescanencodethemixedone.Further,weshowthat input-guardedchoicecanencodeoutput-guardedchoiceandviceversa. Incontrast,weconjecturethatneitherofthemcanencodethepairof thetwoseparatechoices. 1Introduction Inthefieldofconcurrentlanguages,expressivenessisanimportantand intriguingproblem.Differentlyfromthecaseofsequentiallanguages,the purposeofaprogramisnotjusttocomputeafunction,butalsotocontrol thecommunicationandtheinteractionofthevariousparallelcomponents ofasystem.Therearethereforemoreparametersandperspectiveswhich mustbetakenintoaccountwhenassessingtheexpressivepowerofanew formalism. Mostofthemainprocesscalculiproposedinliteraturehavebeenwidely investigatedfromthepointofviewoftheexpressivepower,bothinabso- luteterms,i.e.theircapabilitytosolveproblems,andinrelativeterms, i.e.theircomparison.Inparticular,therehasbeenalotofworkaiming atestablishingtherelationbetweendifferentcalculi,thusprovidingsome structureforthehugeplethoraofformalismsthathavebeenproposedin thefieldofConcurrency.Oneofthegoalsofsuchinvestigationis,ofcourse, toindividuatelanguagesthathavethesameexpressivepowerbutcanbe ∗ ThisworkhasbeenpartiallysupportedbytheINRIAARCprojectProNoBiSandby theINRIADREIE ´ quipeAssocie´ePRINTEMPS. † Lix,EcolePolytechnique,91128PalaiseauCedex,France ‡ INRIAFutursandLix,EcolePolytechnique,91128PalaiseauCedex,France 1

implementedinamoreefficientway.Theencodingitselfcanbevaluable,as thesourcelanguage,eveniflessefficient,maystillbeusefulasaspecification language.Anothergoalistofindouttheconstraintstoimplementation.For instance,ifalanguagecansolveaproblemthatisknowntobenotsolv- ableinadistributedasynchronousmodel(likeforinstancethesymmetric leaderelection),thenweknowthatlanguagecannotbeimplementedinato- tallydistributedmanner.Theinterestedreadercanfindin[11]anextended discussionontheseissues. Surprisinglyhowever,foranimportantclassofcalculi,theprobabilistic ones,thequestionofrelativeexpressivenesshasnotbeeninvestigatedmuch (asfarasweknow),despitethefactthattherehavebeenmanyproposals alreadyandthattheareaisrathermature.Amongtheseveralapproaches, wementiontheonein[17]whichissimilartooursinspirit.Wesuggestthe interestedreadertoconsult[1]forarecentoverviewandclassificationofthe mainprobabilisticcalculiandmodelsthathavebeenproposed. Inthispaper,wemakeafirststeptowardsthestudyofrelativeexpres- sivenessintheprobabilisticsetting.Wefocusononeofthekeymechanisms inConcurrency:thechoiceoperator.Thisconstructrepresentsachoicebe- tweenalternativecomputations,andmaybecontrolledbymeansofguards. Itsimportancereliesonthefactthatitisveryusefulindistributedsystems forallowingprocessestointeractandcoordinate. Onecandefinevariouskindsofchoiceoperatordependingontheguards thatareallowedtoappearinit.Inprocesscalculi,guardsareusually communicationactions(inputandoutput),anditisthennaturaltoconsider thefollowingclassification: • input-guardedchoice:theguardscanonlybeinputactions, • output-guardedchoice:theguardscanonlybeoutputactions, • separatechoice:achoicecancontaininputoroutputguards,butnot ,htob • mixedchoice:achoicecancontainbothinputandoutputguards. Inthenon-probabilisticworldithasbeenprovedthattheasynchronous π-calculus(nochoice,andonlyasynchronousoutputs)canencodeinput- guardedchoice[10]andalsotheseparatechoices[9].Onthecontrary,it cannotencodethemixedchoice[11].Themixedchoicehadbeenalready provedtobestrictlymorepowerfulthantheotherkindsofchoicealsoin CSP[3].Inboththesecases,theproofoftheseparationresultrelieson thecapability/incapabilityofexpressingthesolutiontocertainconsensus problems. Weareinterestedinexploringwhethertheprobabilisticextensionsofthe abovechoiceconstructspresentsasimilargap.Inparticular,weconsider thisquestioninthecontextoftheπ-calculus.Weknowthatprobabilities 2