Axiomatizations for probabilistic finite-state behaviors

Yuxin Deng 1 Catuscia Palamidessi 2
2 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : We study a process calculus which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch's probabilistic automata. We consider various strong and weak behavioral equivalences, and we provide complete axiomatizations for finite-state processes, restricted to guarded recursion in case of the weak equivalences. We conjecture that in the general case of unguarded recursion the ``natural'' weak equivalences are undecidable. This is the first work, to our knowledge, that provides a complete axiomatization for weak equivalences in the presence of recursion and both nondeterministic and probabilistic choice.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2007, 373 (1-2), pp.92-114. 〈10.1016/j.tcs.2006.12.008〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00200928
Contributeur : Catuscia Palamidessi <>
Soumis le : samedi 22 décembre 2007 - 08:35:01
Dernière modification le : mercredi 25 avril 2018 - 10:45:26
Document(s) archivé(s) le : mardi 13 avril 2010 - 15:12:52

Fichier

tcs.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Yuxin Deng, Catuscia Palamidessi. Axiomatizations for probabilistic finite-state behaviors. Theoretical Computer Science, Elsevier, 2007, 373 (1-2), pp.92-114. 〈10.1016/j.tcs.2006.12.008〉. 〈inria-00200928〉

Partager

Métriques

Consultations de la notice

488

Téléchargements de fichiers

137