Abstract
Action hiding and probabilistic choice have independently established their roles in process algebraic modeling and verification of concurrent systems. While action hiding allows abstraction from unimportant details and model reduction, and the induced nondeterminism enables modeling uncertainty in the system behaviour, probabilistic choice allows quantification of the nondeterminism. However, as not all of the nondeterministic behaviour has a random nature, we are faced with the challenge to combine the above two aspects of concurrent systems, such that one can take maximal advantage of both. This thesis addresses two problems regarding concurrent processes that exhibit both hidden and probabilistic behaviour, or probabilistic processes for short. Namely, a proper reduction of a model, by elimination of the hidden actions, requires a semantical equivalence that preserves the process properties of interest and is a congruence for the process operators. For nonprobabilistic processes it has been shown that such an equivalence is branching bisimilarity. However, in the presence of probabilistic choice, more concretely in the alternating model of probabilistic processes, the intuitive notion of branching bisimulation is not a congruence for parallel composition. In this thesis a new branching bisimulation for this model is defined, and it is shown that this is the coarsest congruence for parallel composition that is included in the former. To achieve the congruence result, a hidden action preceding directly a nontrivial probabilistic choice cannot be eliminated. The new branching bisimulation preserves the properties expressible in the probabilistic computation tree logic, and is decidable in polynomial time. Similar to the nonprobabilistic case, a single axiom characterizes branching bisimilarity for finite probabilistic processes. The previous results imply that branching bisimilarity, although potentially useful for model reduction, may be in fact too strong to serve as an equivalence relation for probabilistic processes. Another view, taken in the may/must testing theory (as well as in the process calculus CSP), is to distinguish two processes only if they can be distinguished when interacting with their environment, i.e. with another process. However, although processes that differ only in the moment an internal (nondeterministic) choice is made are not distinguished by this theory, for probabilistic processes this is no longer valid. The problem stems from an earlier observation that the schedulers that resolve the nondeterminism in concurrent probabilistic processes are too powerful and yield unrealistic overestimations of the probabilities with which a process can pass a test. The power of the schedulers comes from the fact that they allow the same choice to be resolved in different manners in different futures. In order to restrict the schedulers and thus to obtain the right probabilities, this thesis proposes integrating the information, based on which a nondeterministic choice is resolved, in labels on the nondeterministic transitions. In this way, choices using the same information are resolved in the same way, regardless of the considered future. As a result, the new testing preorder relation can be characterized by a probabilistic readytrace preorder, a relation that is insensitive to the moment an internal choice is made, yet sensitive to deadlock and to action priorities. In other words, it combines useful features of both the bisimulationstyle and the tracestyle relations. The parallel composition is also generalized here to include both interleaving and action hiding after synchronization, and it is shown that probabilistic readytrace preorder is a precongruence with respect to it. Finally, the CSPstyle axiomatic characterization shows that all the distributivity laws for nondeterministic choice from CSP are preserved and no new laws are added.
Original language  English 

Qualification  Doctor of Philosophy 
Awarding Institution 

Supervisors/Advisors 

Award date  3 Oct 2011 
Place of Publication  Eindhoven 
Publisher  
Print ISBNs  9789038626406 
DOIs  
Publication status  Published  2011 
Fingerprint Dive into the research topics of 'Probability and hiding in concurrent processes'. Together they form a unique fingerprint.
Cite this
Georgievska, S. (2011). Probability and hiding in concurrent processes. Technische Universiteit Eindhoven. https://doi.org/10.6100/IR716397