Axiomatizations for probabilistic finite-state behaviors

Yuxin Deng; Catuscia Palamidessi

doi:10.1007/978-3-540-31982-5_7

Axiomatizations for probabilistic finite-state behaviors

Yuxin Deng, Catuscia Palamidessi

Research output: Contribution to journal › Conference article › peer-review

14 Scopus citations

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 definitions 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.

Original language	English
Pages (from-to)	110-124
Number of pages	15
Journal	Lecture Notes in Computer Science
Volume	3441
DOIs	https://doi.org/10.1007/978-3-540-31982-5_7
State	Published - 2005
Externally published	Yes
Event	8th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 - Edinburgh, United Kingdom Duration: 4 Apr 2005 → 8 Apr 2005

Access to Document

10.1007/978-3-540-31982-5_7

Cite this

@article{214d6675b7d5422aaf04e99e2e439099,

title = "Axiomatizations for probabilistic finite-state behaviors",

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 definitions 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.",

author = "Yuxin Deng and Catuscia Palamidessi",

year = "2005",

doi = "10.1007/978-3-540-31982-5\_7",

language = "英语",

volume = "3441",

pages = "110--124",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer Science and Business Media Deutschland GmbH",

note = "8th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 ; Conference date: 04-04-2005 Through 08-04-2005",

}

TY - JOUR

T1 - Axiomatizations for probabilistic finite-state behaviors

AU - Deng, Yuxin

AU - Palamidessi, Catuscia

PY - 2005

Y1 - 2005

N2 - 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 definitions 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.

AB - 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 definitions 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.

UR - https://www.scopus.com/pages/publications/24644492522

U2 - 10.1007/978-3-540-31982-5_7

DO - 10.1007/978-3-540-31982-5_7

M3 - 会议文章

AN - SCOPUS:24644492522

SN - 0302-9743

VL - 3441

SP - 110

EP - 124

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - 8th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005

Y2 - 4 April 2005 through 8 April 2005

ER -

Axiomatizations for probabilistic finite-state behaviors

Abstract

Access to Document

Other files and links

Fingerprint

Cite this