Jan 18, 2011: Mark Timmer: Symbolic Reductions of Probabilistic Models using Linear Process Equations

January 18, 2011Symbolic Reductions of Probabilistic Models using Linear Process Equations
Room: Zi 5126Mark Timmer

In this presentation I introduce a process algebra that incorporates both probability and data; most notably, it allows parameterised, i.e., state-dependent, probabilistic choice. Clearly, the incorporation of data often results in very large state spaces. Several techniques already exist to battle the state space explosion by reducing the underlying probabilistic model directly. However, this does not solve the problem for models that are too large to generate in the first place. Therefore, the successful analysis of data-driven specifications requires symbolic optimisation techniques, operating at the language level and reducing the state space before generating it.
To enable such techniques, in earlier work we defined a probabilistic generalisation of the existing linear process equation: the LPPE. These equations are a restriction of the full process algebra, similar to the Greibach normal form. We also provided a two-phase algorithm to transform any specification in our algebra to this restricted form. The simplicity of the LPPE makes it easier to reason about many characteristics of the probabilistic specification, such as its control flow or potential commutativity of actions. So far we exploited this by defining two reductions that can be applied directly to the LPPEs: a process-algebraic variant of dead-variable reduction, and a novel probabilistic approach to confluence reduction using commuting unobservable transitions. A prototype implementation has shown that these can indeed significantly shrink the state space of actual specifications.
The process-algebraic format itself was already presented at a lunchmeeting in 2010, and the process-algebraic variant of dead-variable reduction at a lunchmeeting 2009. This time, I will briefly recall these results and mainly focus on the latest addition: confluence reduction.