Characterising Testing Preorders for Finite Probabilistic Processes

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 problems that have remained open throughout the years, namely to find complete axiomatisations and alternative characterisations for these preorders. This paper solves both problems for finite processes with silent moves. It characterises the may preorder in terms of simulation, and the must preorder in terms of failure simulation. It also gives a characterisation of both preorders using a modal logic. Finally it axiomatises both preorders over a probabilistic version of CSP.

33 pages

Cited by in corpus (17)

• Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes
• Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation
• Logical Characterization of Bisimulation Metrics
• Characterising Probabilistic Processes Logically
• Ensuring Liveness Properties of Distributed Systems: Open Problems
• Trace and Testing Metrics on Nondeterministic Probabilistic Processes
• Termination in Convex Sets of Distributions
• Distribution Bisimilarity via the Power of Convex Algebras
• Testing Reactive Probabilistic Processes
• The Spectrum of Strong Behavioral Equivalences for Nondeterministic and Probabilistic Processes
• Reward Testing Equivalences for Processes
• Bisimulations Respecting Duration and Causality for the Non-interleaving Applied $\pi$-Calculus
• Discovering ePassport Vulnerabilities using Bisimilarity
• Fair Must Testing for I/O Automata
• A Unifying Approach to Probabilistic Testing Equivalences
• Testing Probabilistic Processes: Can Random Choices Be Unobservable?
• Characterisations of Testing Preorders for a Finite Probabilistic pi-Calculus