Introduction

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 $maximizer$ tries to maximize eg. the termination probability, while $minimizer$ 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.