Axiomatic and logical characterizations of probabilistic preorders and trace semantics

Randomization was first introduced in computer science in order to improve the efficiency of several problems that were classified unfeasible or particularly inefficient, by giving algorithms the ability to flip coins, that is, of making probabilistic choices at some point of the computation. In the paper Probabilistic Algorithms, Rabin proposed efficient solutions to the problems of determining the nearest neighbor and to state the primality of a given number, for which there were no efficient non-probabilistic solutions. Later, he applied probability to a problem of distributed computing, which was not feasible without the use of randomiza- tion. On the base of these important results, a large set of problems were solved with the use of probabilistic choices in the computation, and a wide range of applications and modelings were proposed in the framework of concurrency theory. However, together with probabilistic behaviors, in the modeling and verification of concurrent processes it is crucial to take into account the presence of a phenomenon called nondeterminism. In general, nondeterminism is a way to model the lack of knowledge about the relative speeds of two or more processes running in parallel, as it may not be possible to determine which of the processes is performing the next action. On the other hand, there are further circumstances in which nondeterminism arises and must be modeled in order to obtain a correct description of the possible behaviors of a process. In particular, the external choices made by the environment in order to condition the execution of a process are modeled as nondeterministic choices, since the decisions taken by a user or by a malicious entity may not be predictable a priori by the system. Furthermore, since a semantic model of a process can be seen as a specification of the process, the introduction of nondeterministic choices in the model may reflect the ability to implement the specification by choosing one of the possible alternatives given, all leading to consistent implementations. The kinds of nondeterministic behaviors described can be all referred to as pure nondeterminism, in contrast with the probabilistic nondeterminism, which models the fact that events are governed by probability distributions.