This is the homepage of a tool called PReMo (read as
primo).
PReMo
is capable of analyzing:
Recursive Markov Chains (RMCs, equivalent to probabilistic Pushdown Systems and Tree-like QBDs)
Recursive Simple Stochastic Games (RSSGs, also with arbitrary positive rewards)
discrete-time Quasi-Birth-Death processes (QBDs, equivalent to probabilistic 1-counter automata)
Stochastic Context Free Grammars (SCFGs)
fixed point solutions of arbitrary equation systems (without any guarantee of termination)
RMC is 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.
If that does not work, one can always run is from the command-line like this:
java -jar PReMo-<version>-<your OS name><arch>.jar
If you encounter any problems when running PReMo first see the troubleshooting notes and then write an email to the address given at the bottom of this web page.
Examples
Equations systems generated for large Stochastic Context Free Grammars(SCFGs) used in Natural Language Processing(NLP):
grammars
(The number of production for a single non-terminal can be as huge as
few thousands and as a result the expression defining such non-terminal
is very long and very hard to manipulate. That's why I've split all
expressions in a chunks of 100 and did variable chaining, where each
such a variable is a sum of new variables corresponding to some
subexpression of the expression originally defining that variable. Names
of the main variables, in which termination probability we are really interested in, are
n_number.)
Some small examples of RMCs, RSSGs, SCFGs and equation systems:
small examples
Preliminary performance results of parallel strategy improvement and Gauss-Seidel method
for random systems of max linear equations that occur
while studying maximizing 1-RMDPs with positive rewards. The
strategy improvement employed a sparse linear solver Biconjugated Gradient
to compute the solution to the linear equation system for reward 1-RMCs.
Publications
Recursive Stochastic Games with Positive Rewards (analyzing a reward 1-exit Recursive Markov Chains and their controlled extensions that allow to compute efficiently the average/pessimal/optimal running time of a given model)
PReMo -- Probabilistic Recursive Models analyzer