Testing Finitary Probabilistic Processes (Extended Abstract) (2009)
Yuxin Deng, Rob Van Glabbeek, Matthew Hennessy, Carroll Morgan
Abstract. This paper provides modal- and relational characterisations of mayand must-testing preorders for recursive CSP processes with divergence, featuring probabilistic as well as nondeterministic...
Characterising testing preorders for finite probabilistic processes (2009)
Yuxin Deng, Rob Van Glabbeek, Matthew Hennessy, Carroll Morgan
Abstract. In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two...
Characterising testing preorders for finite probabilistic processes (2009)
Yuxin Deng, Rob Van Glabbeek, Matthew Hennessy, Carroll Morgan
Abstract. In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two...
Game Characterizations of Process Equivalences (2009)
Abstract. In this paper we propose a hierarchy of games that allows us to make a systematic comparison of process equivalences by characterizing process equivalences as games. The well-known...
Yuxin Deng, Rob Van Glabbeek, Matthew Hennessy, Carroll Morgan
This paper provides modal- and relational characterisations of may- and must-testing preorders for recursive CSP processes with divergence, featuring probabilistic as well as nondeterministic choice....
SecCo 2005 Preliminary Version Weak Probabilistic Anonymity 1 (2008)
Yuxin Deng, Catuscia Palamidessi, Jun Pang, Inria Futurs
Abstract Anonymity means that the identity of the user performing a certain action is maintained secret. The protocols for ensuring anonymity often use random mechanisms which can be described...
On Automatic Verification of Self-stabilizing Population Protocols (2008)
Jun Pang, Zhengqin Luo, Yuxin Deng
The population protocol model [2] has emerged as an elegant computation paradigm for describing mobile ad hoc networks, consisting of a number of mobile nodes that interact with each other to carry...
Characterising testing preorders for finite probabilistic processes (2008)
Yuxin Deng, Rob Van Glabbeek, Matthew Hennessy, Carroll Morgan
Abstract. In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two...
Characterising Testing Preorders for Finite Probabilistic Processes (2008)
Deng, Yuxin, Hennessy, Matthew, Van Glabbeek, Rob, Morgan, Carroll
In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two problems that...
Characterising testing preorders for finite probabilistic processes (2008)
In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two problems that...
Abstract SecCo 2005 Preliminary Version Weak Probabilistic Anonymity 1 (2008)
Yuxin Deng, Inria Sophia-antipolis, Université Paris, Catuscia Palamidessi, Jun Pang, Inria Futurs, ...
Anonymity means that the identity of the user performing a certain action is maintained secret. The protocols for ensuring anonymity often use random mechanisms which can be described...
Characterising testing preorders for finite probabilistic processes (2008)
In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two problems that...
Characterising testing preorders for finite probabilistic processes (2008)
In 1992 Wang & Larsen extended the may- and must preorders of De Nicola and Hennessy to processes featuring probabilistic as well as nondeterministic choice. They concluded with two problems that...
Analyzing an Electronic Cash Protocol Using Applied Pi Calculus? (2008)
Zhengqin Luo, Xiaojuan Cai, Jun Pang, Yuxin Deng
Abstract. Untraceability and unreuseability are essential security properties for electronic cash protocols. Many protocols have been proposed to meet these two properties. However, most of them have...
Abstract SecCo 2005 Preliminary Version Weak Probabilistic Anonymity 1 (2008)
Yuxin Deng, Inria Sophia-antipolis, Université Paris, Catuscia Palamidessi, Jun Pang, Inria Futurs, ...
Anonymity means that the identity of the user performing a certain action is maintained secret. The protocols for ensuring anonymity often use random mechanisms which can be described...
Analyzing an Electronic Cash Protocol Using Applied Pi Calculus ⋆ (2008)
Zhengqin Luo, Xiaojuan Cai, Jun Pang, Yuxin Deng, Carl Von Ossietzky Universität Oldenburg
Abstract. Untraceability and unreuseability are essential security properties for electronic cash protocols. Many protocols have been proposed to meet these two properties. However, most of them have...
Towards Automatic Measurement of Probabilistic Processes ∗ (2008)
Lin Song, Yuxin Deng, Xiaojuan Cai
In this paper we propose a metric for finite processes in a probabilistic extension of CSP. The kernel of the metric corresponds to trace equivalence and most of the operators in the process algebra...
yuxind@cse.unsw.edu.au 2 Carl von Ossietzky Universit"at Oldenburg (2008)
Abstract. Anonymity is the property of maintaining secret the identity of users performing a certain action. Anonymity protocols often use random mechanisms which can be described probabilistically....
Axiomatisations et types pour des processus probabilistes et mobiles (2007)
Cette th`ese se concentre sur des bases th´eoriques utiles pour l'analyse d'algorithmes et de protocoles pour des syst`emes r´epartis modernes. Deux caract´eristiques importantes des mod`eles pour...
Weak Probabilistic Anonymity (2007)
Deng, Yuxin, Palamidessi, Catuscia, Pang, Jun
Anonymity means that the identity of the user performing a certain action is maintained secret. The protocols for ensuring anonymity often use random mechanisms which can be described...
Axiomatizations for probabilistic finite-state behaviors (2007)
Deng, Yuxin, Palamidessi, Catuscia
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...
Weak Probabilistic Anonymity (2007)
Deng, Yuxin, Palamidessi, Catuscia, Pang, Jun
Anonymity means that the identity of the user performing a certain action is maintained secret. The protocols for ensuring anonymity often use random mechanisms which can be described...
Axiomatizations for probabilistic finite-state behaviors (2007)
Deng, Yuxin, Palamidessi, Catuscia
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...
Scalar outcomes suffice for finitary probabilistic testing (2007)
Yuxin Deng, Rob Van Glabbeek, Carroll Morgan, Chenyi Zhang
Abstract. The question of equivalence has long vexed research in concurrency, leading to many different denotational- and bisimulation-based approaches; a breakthrough occurred with the insight that...
Measuring anonymity with relative entropy (2007)
Abstract. Anonymity is the property of maintaining secret the identity of users performing a certain action. Anonymity protocols often use random mechanisms which can be described probabilistically....
Scalar outcomes suffice for finitary probabilistic testing (2007)
Yuxin Deng, Rob Van Glabbeek, Carroll Morgan, Chenyi Zhang
Abstract. The question of equivalence has long vexed research in concurrency, leading to many different denotational- and bisimulation-based approaches; a breakthrough occurred with the insight that...
Measuring anonymity with relative entropy (2007)
Abstract. Anonymity is the property of maintaining secret the identity of users performing a certain action. Anonymity protocols often use random mechanisms which can be described probabilistically....
Axiomatizations for probabilistic finite-state behaviors (2007)
Deng, Yuxin, Palamidessi, Catuscia
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...
Weak Probabilistic Anonymity (2007)
Deng, Yuxin, Palamidessi, Catuscia, Pang, Jun
Anonymity means that the identity of the user performing a certain action is maintained secret. The protocols for ensuring anonymity often use random mechanisms which can be described...
Axiomatizations for probabilistic finite-state behaviors (2007)
Deng, Yuxin, Palamidessi, Catuscia
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...
Weak Probabilistic Anonymity (2007)
Deng, Yuxin, Palamidessi, Catuscia, Pang, Jun
Anonymity means that the identity of the user performing a certain action is maintained secret. The protocols for ensuring anonymity often use random mechanisms which can be described...
Metrics for Action-labelled Quantitative Transition Systems (2006)
Deng, Yuxin, Chothia, Tom, Palamidessi, Catuscia, Pang, Jun
This paper defines action-labelled quantitative transition systems as a general framework for combining qualitative and quantitative analysis. We define state-metrics as a natural extension of...
Metrics for Action-labelled Quantitative Transition Systems (2006)
Deng, Yuxin, Chothia, Tom, Palamidessi, Catuscia, Pang, Jun
This paper defines action-labelled quantitative transition systems as a general framework for combining qualitative and quantitative analysis. We define state-metrics as a natural extension of...
Metrics for Action-labelled Quantitative Transition Systems (2006)
Deng, Yuxin, Chothia, Tom, Palamidessi, Catuscia, Pang, Jun
This paper defines action-labelled quantitative transition systems as a general framework for combining qualitative and quantitative analysis. We define state-metrics as a natural extension of...
Metrics for Action-labelled Quantitative Transition Systems (2006)
Deng, Yuxin, Chothia, Tom, Palamidessi, Catuscia, Pang, Jun
This paper defines action-labelled quantitative transition systems as a general framework for combining qualitative and quantitative analysis. We define state-metrics as a natural extension of...
Axiomatisations et types pour des processus probabilistes et mobiles (2005)
Cette thèse se concentre sur des bases théoriques utiles pour l'analyse d'algorithmes et de protocoles pour des systèmes répartis modernes. Deux caractéristiques importantes des modèles pour...
Axiomatisations et types pour des processus probabilistes et mobiles (2005)
Cette th`ese se concentre sur des bases th´eoriques utiles pour l'analyse d'algorithmes et de protocoles pour des syst`emes r´epartis modernes. Deux caract´eristiques importantes des mod`eles pour...
Axiomatisations et types pour des processus probabilistes et mobiles (2005)
Cette th`ese se concentre sur des bases th´eoriques utiles pour l'analyse d'algorithmes et de protocoles pour des syst`emes r´epartis modernes. Deux caract´eristiques importantes des mod`eles pour...
Compositional Reasoning for Probabilistic Finite-State Behaviors (2005)
Deng, Yuxin, Palamidessi, Catuscia, Pang, Jun
We study a process algebra which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch's simple probabilistic automata. We consider strong bisimulation and...
Axiomatizations for probabilistic finite-state behaviors (2005)
Deng, Yuxin, Palamidessi, Catuscia
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...
Compositional Reasoning for Probabilistic Finite-State Behaviors (2005)
Deng, Yuxin, Palamidessi, Catuscia, Pang, Jun
We study a process algebra which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch's simple probabilistic automata. We consider strong bisimulation and...
Axiomatizations for probabilistic finite-state behaviors (2005)
Deng, Yuxin, Palamidessi, Catuscia
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...
Axiomatisations et types pour des processus probabilistes et mobiles (2005)
Cette th`ese se concentre sur des bases th´eoriques utiles pour l'analyse d'algorithmes et de protocoles pour des syst`emes r´epartis modernes. Deux caract´eristiques importantes des mod`eles pour...
Compositional reasoning for probabilistic finite-state behaviors (2005)
Yuxin Deng, Catuscia Palamidessi, Jun Pang
Abstract. We study a process algebra which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch’s simple probabilistic automata. We consider strong...
Weak probabilistic anonymity (2005)
Yuxin Deng, Catuscia Palamidessi, Jun Pang, Inria Sophia-antipolis, Université Paris, Inria Futurs, ...
Abstract. Anonymity means that the identity of the user performing a certain action is maintained secret. The protocols for ensuring anonymity often use random mechanisms which can be described...
Collège doctoral Axiomatisations and Types (2005)
The focus of this thesis are the theoretical foundations for reasoning about algorithms and pro-tocols for modern distributed systems. Two important features of models for these systems are...
Compositional reasoning for probabilistic finite-state behaviors (2005)
Yuxin Deng, Catuscia Palamidessi, Jun Pang
Abstract. We study a process algebra which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch's simple probabilistic automata. We consider strong...
Axiomatizations for probabilistic finite-state behaviors (2005)
Yuxin Deng, Catuscia Palamidessi
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...
Axiomatizations for probabilistic finite-state behaviors (2005)
Yuxin Deng, Catuscia Palamidessi, Inria Sophia-antipolis, Inria Futurs, Ecole Polytechnique
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...
Metrics for Action-labelled Quantitative Transition Systems (2005)
Yuxin Deng, Tom Chothia, Catuscia Palamidessi, Jun Pang
This paper defines action-labelled quantitative transition systems as a general framework for combining qualitative and quantitative analysis. We define state-metrics as a natural extension of...
Metrics for Action-labelled Quantitative Transition Systems (2005)
Yuxin Deng, Tom Chothia, Catuscia Palamidessi, Jun Pang
This paper defines action-labelled quantitative transition systems as a general framework for combining qualitative and quantitative analysis. We define state-metrics as a natural extension of...
Compositional Reasoning for Probabilistic Finite-State Behaviors (2005)
Yuxin Deng, Catuscia Palamidessi, Jun Pang
We study a process algebra which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch's simple probabilistic automata. We consider strong bisimulation and...
Axiomatizations for probabilistic finite-state behaviors (2005)
Yuxin Deng, Catuscia Palamidessi, Inria Sophia-antipolis, Université Paris, Inria Futurs, École Polytechnique
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...
Compositional reasoning for probabilistic finite-state behaviors (2005)
Yuxin Deng, Catuscia Palamidessi, Jun Pang
Abstract. We study a process algebra which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch’s simple probabilistic automata. We consider strong...
Axiomatizations for probabilistic finite-state behaviors (2005)
Yuxin Deng, Catuscia Palamidessi
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...
Axiomatisations et types pour des processus probabilistes et mobiles (2005)
Cette th`ese se concentre sur des bases th´eoriques utiles pour l'analyse d'algorithmes et de protocolespour des syst`emes r´epartis modernes. Deux caract´eristiques importantes des mod`eles...
Compositional Reasoning for Probabilistic Finite-State Behaviors (2005)
Deng, Yuxin, Palamidessi, Catuscia, Pang, Jun
We study a process algebra which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch's simple probabilistic automata. We consider strong bisimulation and...
Axiomatizations for probabilistic finite-state behaviors (2005)
Deng, Yuxin, Palamidessi, Catuscia
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...
Axiomatisations et types pour des processus probabilistes et mobiles (2005)
Cette th`ese se concentre sur des bases th´eoriques utiles pour l'analyse d'algorithmes et de protocolespour des syst`emes r´epartis modernes. Deux caract´eristiques importantes des mod`eles...
Compositional Reasoning for Probabilistic Finite-State Behaviors (2005)
Deng, Yuxin, Palamidessi, Catuscia, Pang, Jun
We study a process algebra which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch's simple probabilistic automata. We consider strong bisimulation and...
Axiomatizations for probabilistic finite-state behaviors (2005)
Deng, Yuxin, Palamidessi, Catuscia
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...
Axiomatisations et types pour des processus probabilistes et mobiles (2005)
Cette th`ese se concentre sur des bases th´eoriques utiles pour l'analyse d'algorithmes et de protocolespour des syst`emes r´epartis modernes. Deux caract´eristiques importantes des mod`eles...
Ensuring termination by typability (2004)
Yuxin Deng, Davide Sangiorgi Inria
Abstract. A term terminates if all its reduction sequences are of finite length. We show four type systems that ensure termination of well-typed ss-calculus processes. The systems are obtained by...
Towards an Algebraic Theory of Typed Mobile Processes (2004)
The impact of types on the algebraic theory of the π-calculus is studied. The type system has capability types. They allow one to distinguish between the ability to read from a channel, to...
Ensuring Termination by Typability (2004)
A term terminates if all its reduction sequences are of finite length. We show four type systems that ensure termination of well-typed -calculus processes. The systems are obtained by successive...
Towards an Algebraic Theory of Typed Mobile Processes (2004)
The impact of types on the algebraic theory of the π-calculus is studied. The type system has capability types. They allow one to distinguish between the ability to read from a channel, to...
Ensuring Termination by Typability (2004)
A term terminates if all its reduction sequences are of finite length. We show four type systems that ensure termination of well-typed #-calculus processes. The systems are obtained by successive...
Ensuring termination by typability (2004)
Abstract. A term terminates if all its reduction sequences are of finite length. We show four type systems that ensure termination of well-typed π-calculus processes. The systems are obtained by...
Towards an algebraic theory of typed mobile processes (2004)
Abstract. The impact of types on the algebraic theory of the π-calculus is studied. The type system has capability types. They allow one to distinguish between the ability to read from a channel, to...
Ensuring termination by typability (2004)
Abstract A term terminates if all its reduction sequences are of finite length. We show four type systems that ensure termination of well-typed π-calculus processes. The systems are obtained by...