Expressiveness of probabilistic pi calculi

-

English
20 Pages
Read an excerpt
Gain access to the library to view online
Learn more

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


Subjects

Informations

Published by
Reads 11
Language English
Report a problem
Expressivenessofprobabilisticπ-calculiSylvainPradalierCatusciaPalamidessiAbstractInthisworkweproposeaprobabilisticextensionoftheπ-calculus.Themainnoveltyisaprobabilisticmixedchoiceoperator,thatis,achoiceconstructwithaprobabilitydistributiononthebranches,andwhereinputandoutputactionscanbothoccurasguards.Wedeveloptheoperationalsemanticsofthiscalculus,andthenweinvestigateitsexpressiveness.Inparticular,wecompareitwiththesublanguagewiththetwoseparatechoices,whereinputandoutputguardsarenotallowedtogetherinthesamechoiceconstruct.Ourmainresultisthattheseparatechoicescanencodethemixedone.Further,weshowthatinput-guardedchoicecanencodeoutput-guardedchoiceandviceversa.Incontrast,weconjecturethatneitherofthemcanencodethepairofthetwoseparatechoices.1IntroductionInthefieldofconcurrentlanguages,expressivenessisanimportantandintriguingproblem.Differentlyfromthecaseofsequentiallanguages,thepurposeofaprogramisnotjusttocomputeafunction,butalsotocontrolthecommunicationandtheinteractionofthevariousparallelcomponentsofasystem.Therearethereforemoreparametersandperspectiveswhichmustbetakenintoaccountwhenassessingtheexpressivepowerofanewformalism.Mostofthemainprocesscalculiproposedinliteraturehavebeenwidelyinvestigatedfromthepointofviewoftheexpressivepower,bothinabso-luteterms,i.e.theircapabilitytosolveproblems,andinrelativeterms,i.e.theircomparison.Inparticular,therehasbeenalotofworkaimingatestablishingtherelationbetweendifferentcalculi,thusprovidingsomestructureforthehugeplethoraofformalismsthathavebeenproposedinthefieldofConcurrency.Oneofthegoalsofsuchinvestigationis,ofcourse,toindividuatelanguagesthathavethesameexpressivepowerbutcanbeThisworkhasbeenpartiallysupportedbytheINRIAARCprojectProNoBiSandbytheINRIADREIE´quipeAssocie´ePRINTEMPS.Lix,EcolePolytechnique,91128PalaiseauCedex,FranceINRIAFutursandLix,EcolePolytechnique,91128PalaiseauCedex,France1
implementedinamoreefficientway.Theencodingitselfcanbevaluable,asthesourcelanguage,eveniflessefficient,maystillbeusefulasaspecificationlanguage.Anothergoalistofindouttheconstraintstoimplementation.Forinstance,ifalanguagecansolveaproblemthatisknowntobenotsolv-ableinadistributedasynchronousmodel(likeforinstancethesymmetricleaderelection),thenweknowthatlanguagecannotbeimplementedinato-tallydistributedmanner.Theinterestedreadercanfindin[11]anextendeddiscussionontheseissues.Surprisinglyhowever,foranimportantclassofcalculi,theprobabilisticones,thequestionofrelativeexpressivenesshasnotbeeninvestigatedmuch(asfarasweknow),despitethefactthattherehavebeenmanyproposalsalreadyandthattheareaisrathermature.Amongtheseveralapproaches,wementiontheonein[17]whichissimilartooursinspirit.Wesuggesttheinterestedreadertoconsult[1]forarecentoverviewandclassificationofthemainprobabilisticcalculiandmodelsthathavebeenproposed.Inthispaper,wemakeafirststeptowardsthestudyofrelativeexpres-sivenessintheprobabilisticsetting.WefocusononeofthekeymechanismsinConcurrency:thechoiceoperator.Thisconstructrepresentsachoicebe-tweenalternativecomputations,andmaybecontrolledbymeansofguards.Itsimportancereliesonthefactthatitisveryusefulindistributedsystemsforallowingprocessestointeractandcoordinate.Onecandefinevariouskindsofchoiceoperatordependingontheguardsthatareallowedtoappearinit.Inprocesscalculi,guardsareusuallycommunicationactions(inputandoutput),anditisthennaturaltoconsiderthefollowingclassification:input-guardedchoice:theguardscanonlybeinputactions,output-guardedchoice:theguardscanonlybeoutputactions,separatechoice:achoicecancontaininputoroutputguards,butnot,htobmixedchoice:achoicecancontainbothinputandoutputguards.Inthenon-probabilisticworldithasbeenprovedthattheasynchronousπ-calculus(nochoice,andonlyasynchronousoutputs)canencodeinput-guardedchoice[10]andalsotheseparatechoices[9].Onthecontrary,itcannotencodethemixedchoice[11].ThemixedchoicehadbeenalreadyprovedtobestrictlymorepowerfulthantheotherkindsofchoicealsoinCSP[3].Inboththesecases,theproofoftheseparationresultreliesonthecapability/incapabilityofexpressingthesolutiontocertainconsensusproblems.Weareinterestedinexploringwhethertheprobabilisticextensionsoftheabovechoiceconstructspresentsasimilargap.Inparticular,weconsiderthisquestioninthecontextoftheπ-calculus.Weknowthatprobabilities2