Characterising Probabilistic Processes Logically

Characterising Probabilistic Alternating Simulation for Concurrent Games

Probabilistic game structures combine both nondeterminism and stochasticity, where players repeatedly take actions simultaneously to move to the next state of the concurrent game. Probabilistic alternating simulation is an important tool to compare the behaviour of different probabilistic game structures. In this paper, we present a sound and complete modal characterisation of this simulation relation by proposing a new logic based on probabilistic distributions. The logic enables a player to enforce a property in the next state or distribution. Its extension with fixpoints, which also charact…

Characterising Testing Preorders for Finite Probabilistic Processes

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 a…

具有概率干预反事实的逻辑的表达性景观

Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals

本文在因果多团队语义下，通过线性不等式族和闭包条件，完全刻画了表达概率语句、条件化和干预反事实的几种逻辑的表达性，并揭示了严格张量析取在捕获所有线性不等式中的必要性。