This document describes the tool PReMo(Probabilistic Recursive Models analyzer) and illustrate it on some simple examples. PReMo(read as primo) is capable of analyzing Recursive Markov Chain s(RMCs), Recursive Simple Stochastic Game s(RSSGs) and Stochastic Context Free Grammar s(SCFGs). RMCs are a natural model for recursive imperative programs with probabilistic transitions. Probability comes either from an explicit randomization like in the Quicksort algorithm or by abstracting some aspects of a program. A very tightly related model to this one is Probabilistic Pushdown Systems (pPDSs). There exist polynomial time algorithms translating one model into the other.
The theory behind RMCs and pPDSs was investigated and published in a whole
series of papers [2,4,1]. There are many
interesting question we could ask about a given Recursive Markov Chain such as computation of
termination probability, expected time of termination or its variance. Algorithms were
given in [2,1], that
use results from the Existential Theory of Reals, allowing us to decide in
PSPACE whether those values are greater than a given rational value. On top of
that, in [2], a reduction was established
from the well known Square Root Sum problem to the problem of computing the
termination probabilities for RMCs. This means that finding an algorithm with
substantially better complexity than PSPACE, would solve a long standing open
problem. On the other hand we have efficient numerical approximation
algorithms described in [2] for computing all
these values by computing the least fixed point of a specific nonlinear system
of equations, eg. using Newton's method. Related to RMCs, but placed in the
game theoretic setting, are Recursive Simple Stochastic Game s[3] where we allow some of the nodes to be
controlled by players. The player called tries to maximize eg. the
termination probability, while
tries to minimize it.
The program has four input modes: RMC for typing as an input a source of Recursive Markov Chain, RSSG for modeling Recursive Markov Decision Processes and Recursive Simple Stochastic Game s, SCFG for Stochastic Context Free Grammar and Equations where the user can type any set of recursive equations with standard functions and the system will try to find the fixed point if one exists starting at all zero vector.