Semantics of Probabilistic Processes

An Operational Approach

verfasst von: Yuxin Deng

Verlag: Springer Berlin Heidelberg

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book discusses the semantic foundations of concurrent systems with nondeterministic and probabilistic behaviour. Particular attention is given to clarifying the relationship between testing and simulation semantics and characterising bisimulations from metric, logical, and algorithmic perspectives. Besides presenting recent research outcomes in probabilistic concurrency theory, the book exemplifies the use of many mathematical techniques to solve problems in computer science, which is intended to be accessible to postgraduate students in Computer Science and Mathematics. It can also be used by researchers and practitioners either for advanced study or for technical reference.

Inhaltsverzeichnis

Frontmatter

1. Introduction

Abstract

This introduction briefly reviews the history of probabilistic concurrency theory and three approaches to the semantics of concurrent systems: denotational, axiomatic and operational. This book focuses on the last one and more specifically on (bi)simulation semantics and testing semantics. The second section surveys the contents and main results for other chapters of the book.

Yuxin Deng

2. Mathematical Preliminaries

Abstract

We briefly introduce some mathematical concepts and associated important theorems that will be used in the subsequent chapters to study the semantics of probabilistic processes. The main topics covered in this chapter include the Knaster–Tarski fixed-point theorem, continuous functions over complete lattices, induction and coinduction proof principles, compact sets in topological spaces, the separation theorem, the Banach fixed-point theorem, the π-λ theorem and the duality theorem in linear programming. Most of the theorems are stated without proofs because they can be found in many textbooks.

Yuxin Deng

3. Probabilistic Bisimulation

Abstract

We introduce the operational model of probabilistic labelled transition systems, where a state evolves into a distribution after performing some action. To define relations between distributions, we need to lift a relation on states to be a relation on distributions of states. There is a natural lifting operation that nicely corresponds to the Kantorovich metric, a fundamental concept used in mathematics to lift a metric on states to a metric on distributions of states, which is also related to the maximum flow problem in optimisation theory.

The lifting operation yields a neat notion of probabilistic bisimulation, for which we provide logical, metric and algorithmic characterisations. Specifically, we extend the Hennessy–Milner logic and the modal mu-calculus with a new modality, resulting in an adequate and an expressive logic for probabilistic bisimilarity. The correspondence of the lifting operation and the Kantorovich metric lead to a characterisation of bisimulations as pseudometrics that are postfixed points of a monotone function. Probabilistic bisimilarity also admits both partition refinement and “on-the-fly” decision algorithms; the latter exploits the close relationship between the lifting operation and the maximum flow problem.

Yuxin Deng

4. Probabilistic Testing Semantics

Abstract

In this chapter we extend the traditional testing theory of De Nicola and Hennessy to the probabilistic setting. We first set up a general testing framework, and then introduce a vector-based testing approach that employs multiple success actions. It turns out that for finitary systems, i.e. finite-state and finitely branching systems, vector-based testing is equivalent to scalar testing that uses only one success action. Other variants, such as reward testing and extremal reward testing, are also discussed. They all coincide with vector-based testing as far as finitary systems are concerned.

Yuxin Deng

5. Testing Finite Probabilistic Processes

Abstract

In this chapter we focus on finite processes and understand testing semantics from three different aspects. First, we coinductively define simulation relations. Unlike the nonprobabilistic setting, where there is a clear gap between testing and simulation semantics, here testing semantics is as strong as simulation semantics. Second, a probabilistic logic is presented to completely determine testing preorders. Therefore, both positive and negative results can be established. For example, if two finite processes P and Q are related by may preorder then we can construct a simulation relation to witness this, otherwise a modal formula can be constructed that is satisfiable by P but not by Q. Moreover, the distinguishing formula can be turned into a test that P can pass but Q cannot. Finally, for finite processes, both may and must testing preorders can be completely axiomatised.

Yuxin Deng

6. Testing Finitary Probabilistic Processes

Abstract

In this chapter we extend the results of Chap. 5 from finite to finitary processes, that is, finite-state and finitely branching processes. Testing preorders can still be characterised as simulation preorders and admit modal characterisations. However, to prove these results demands more advanced techniques. A new notion of weak derivation is introduced; some of its fundamental properties are established. Of particular importance is the finite generability property of the set of derivatives from any distribution, which enables us to approximate coinductive simulation relations by stratified inductive relations. This opens the way to characterise the behaviour of finitary process by a finite modal logic. Therefore, if two processes are related it suffices to construct a simulation relation, otherwise a finite test can be constructed to tell them apart.

We also introduce a notion of real-reward testing that allows for negative rewards. Interestingly, for finitary convergent processes, real-reward testing preorder coincides with nonnegative-reward testing preorder.

Yuxin Deng

7. Weak Probabilistic Bisimulation

Abstract

By taking the symmetric form of simulation preorder, we obtain a notion of weak probabilistic bisimulation. It provides a sound and complete proof methodology for an extensional behavioural equivalence, a probabilistic variant of the traditional reduction barbed congruence.

Yuxin Deng

Backmatter

Titel: Semantics of Probabilistic Processes
verfasst von: Yuxin Deng
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-662-45198-4
Print ISBN: 978-3-662-45197-7
DOI: https://doi.org/10.1007/978-3-662-45198-4