Probabilistic Communication Structured Acyclic Nets

Abstract

As the real world is full of uncertainty, we often estimate, or even guess to quantify uncertainty. Probabilistic models are the key to cope with uncertainty. One of the most prominent concurrent probabilistic models are probabilistic Petri nets. Petri nets are one of the mathematical modeling languages for the representation of distributed systems. They have been characterised as one of the expressive models to capture the notion of concurrency. Developing probabilistic concurrent system has been proved to be a difficult and ongoing problem. This is because in a concurrent systems different executions of a concurrent computation should have the same probability. However, this is not always guaranteed as concurrent systems may exhibit confusion. Confusion is an overlapping between conflict and concurrency – two fundamental concepts used in the area of concurrent systems modelling – which interferes with probability analysis. In this thesis, we set out to develop a probabilistic framework and outline approaches leading to a model where distributed choices are resolved in a way which allows one to carry out probabilistic estimation. In particular, the concept of cluster-acyclic net is introduced to transform a net with confusion into another net whose structure is free-choice which facilitates probabilistic estimation. Moreover, we formally extend calculating probabilities and the definition of conflict and confusion to Communication Structured Acyclic Nets (CSA-nets). Intuitively, in CSA-nets, acyclic nets are integrated into one structure that allows them to interact by the means of asynchronous and synchronous communications. CSA-nets are sets of interacting acyclic nets derived from Structured Occurrence Nets (SO-nets), which are a Petri net based formalism for representing the behaviour of complex evolving systems. We show that a CSA-net with confusion can be translated into another, confusion-free net, whose behaviour is closely linked to the behaviour of the original CSA-net. Also, a boolean satisfiability model is introduced to formally verify behavioural properties of CSA-nets.