inria-00200928, version 1
Axiomatizations for probabilistic finite-state behaviors
Yuxin Deng 1Catuscia Palamidessi 2
Theoretical Computer Science 373, 1-2 (2007) 92-114
Résumé : 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.
- 1 : Department of Computer Science and Engineering (CSE)
- Shanghai Jiaotong University
- 2 : COMETE (INRIA Saclay - Ile de France)
- INRIA – Polytechnique - X – CNRS : UMR7161
- Domaine : Informatique/Logique en informatique
- inria-00200928, version 1
- http://hal.inria.fr/inria-00200928
- oai:hal.inria.fr:inria-00200928
- Contributeur : Catuscia Palamidessi
- Soumis le : Samedi 22 Décembre 2007, 08:35:01
- Dernière modification le : Vendredi 8 Janvier 2010, 00:19:16