A Complete Axiomatisation of Branching Bisimulation for Probabilistic Systems with an Application in Protocol Verification
Identifieur interne : 002202 ( Main/Merge ); précédent : 002201; suivant : 002203A Complete Axiomatisation of Branching Bisimulation for Probabilistic Systems with an Application in Protocol Verification
Auteurs : Suzana Andova [Norvège] ; Jos C. M. Baeten [Pays-Bas] ; Tim A. C. Willemse [Pays-Bas]Source :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2006.
Abstract
Abstract: We consider abstraction in probabilistic process algebra. The process algebra can be employed for specifying processes that exhibit both probabilistic and non-deterministic choices in their behaviour. We give a set of axioms that completely axiomatises the branching bisimulation for the strictly alternating probabilistic graph model. In addition, several recursive verification rules are identified, allowing us to remove redundant internal activity. Using the axioms and the verification rules, we have successfully conducted a verification of the Concurrent Alternating Bit Protocol. This is a simple communication protocol, slightly more ‘sophisticated’ than the well-known Alternating Bit Protocol. As channels are lossy, sending continuous streams of data through the channels is a method to overcome this possible loss of data. This instigates a considerable level of parallelism (parallel activities) and as such requires more complex techniques for proving the protocol correct. Using our process algebra we show that after abstraction of internal activity, the protocol behaves as a buffer.
Url:
DOI: 10.1007/11817949_22
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001F90
- to stream Istex, to step Curation: 001F90
- to stream Istex, to step Checkpoint: 001761
Links to Exploration step
ISTEX:9E280D47B7F1D536EA73772DFC746CD9983D5479Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Complete Axiomatisation of Branching Bisimulation for Probabilistic Systems with an Application in Protocol Verification</title><author><name sortKey="Andova, Suzana" sort="Andova, Suzana" uniqKey="Andova S" first="Suzana" last="Andova">Suzana Andova</name></author><author><name sortKey="Baeten, Jos C M" sort="Baeten, Jos C M" uniqKey="Baeten J" first="Jos C. M." last="Baeten">Jos C. M. Baeten</name></author><author><name sortKey="Willemse, Tim A C" sort="Willemse, Tim A C" uniqKey="Willemse T" first="Tim A. C." last="Willemse">Tim A. C. Willemse</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:9E280D47B7F1D536EA73772DFC746CD9983D5479</idno><date when="2006" year="2006">2006</date><idno type="doi">10.1007/11817949_22</idno><idno type="url">https://api.istex.fr/document/9E280D47B7F1D536EA73772DFC746CD9983D5479/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">001F90</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001F90</idno><idno type="wicri:Area/Istex/Curation">001F90</idno><idno type="wicri:Area/Istex/Checkpoint">001761</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001761</idno><idno type="wicri:doubleKey">0302-9743:2006:Andova S:a:complete:axiomatisation</idno><idno type="wicri:Area/Main/Merge">002202</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A Complete Axiomatisation of Branching Bisimulation for Probabilistic Systems with an Application in Protocol Verification</title><author><name sortKey="Andova, Suzana" sort="Andova, Suzana" uniqKey="Andova S" first="Suzana" last="Andova">Suzana Andova</name><affiliation wicri:level="3"><country xml:lang="fr">Norvège</country><wicri:regionArea>Department of Telematics, Norwegian University of Science, Trondheim</wicri:regionArea><placeName><settlement type="city">Trondheim</settlement><region type="région" nuts="2">Trøndelag</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Norvège</country></affiliation></author><author><name sortKey="Baeten, Jos C M" sort="Baeten, Jos C M" uniqKey="Baeten J" first="Jos C. M." last="Baeten">Jos C. M. Baeten</name><affiliation wicri:level="1"><country xml:lang="fr">Pays-Bas</country><wicri:regionArea>Department of Mathematics and Computer Science, Eindhoven University of Technology, P.O. Box 513, 5600, MB Eindhoven</wicri:regionArea><wicri:noRegion>MB Eindhoven</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Pays-Bas</country></affiliation></author><author><name sortKey="Willemse, Tim A C" sort="Willemse, Tim A C" uniqKey="Willemse T" first="Tim A. C." last="Willemse">Tim A. C. Willemse</name><affiliation wicri:level="1"><country xml:lang="fr">Pays-Bas</country><wicri:regionArea>Faculty of Science, Mathematics and Computing Science, University of Nijmegen, P.O. Box 9010, 6500, GL Nijmegen</wicri:regionArea><wicri:noRegion>GL Nijmegen</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Pays-Bas</country></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2006</date></imprint><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">9E280D47B7F1D536EA73772DFC746CD9983D5479</idno><idno type="DOI">10.1007/11817949_22</idno><idno type="ChapterID">22</idno><idno type="ChapterID">Chap22</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We consider abstraction in probabilistic process algebra. The process algebra can be employed for specifying processes that exhibit both probabilistic and non-deterministic choices in their behaviour. We give a set of axioms that completely axiomatises the branching bisimulation for the strictly alternating probabilistic graph model. In addition, several recursive verification rules are identified, allowing us to remove redundant internal activity. Using the axioms and the verification rules, we have successfully conducted a verification of the Concurrent Alternating Bit Protocol. This is a simple communication protocol, slightly more ‘sophisticated’ than the well-known Alternating Bit Protocol. As channels are lossy, sending continuous streams of data through the channels is a method to overcome this possible loss of data. This instigates a considerable level of parallelism (parallel activities) and as such requires more complex techniques for proving the protocol correct. Using our process algebra we show that after abstraction of internal activity, the protocol behaves as a buffer.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Ticri/CIDE/explor/TelematiV1/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002202 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 002202 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Ticri/CIDE
|area= TelematiV1
|flux= Main
|étape= Merge
|type= RBID
|clé= ISTEX:9E280D47B7F1D536EA73772DFC746CD9983D5479
|texte= A Complete Axiomatisation of Branching Bisimulation for Probabilistic Systems with an Application in Protocol Verification
}}
| This area was generated with Dilib version V0.6.31. |  |