About Probablistic Rewrite Theories

Probabilistic rewrite theories is a general semantic framework that unifies many existing models of probabilistic systems for both discrete and continuous time [KSMAtr03]. In a standard rewrite theory, transitions in a system are described by labelled rewrite rules of the form,

t => t' if cond

Intuitively, a rule of this form specifies a pattern t such that, if some fragment of the system's state matches that pattern and satisfies the condition cond, then a local transition of that state fragment changing into the pattern t' can take place. In a probabilistic rewrite rule we add probability information to such rules. Specifically, our proposed probabilistic rules are of the form,

t(X) => t'(X,Y) if cond(X) with probability Dist(X) .

The rule will match a state fragment if there is a substitution S for the variables X that makes S(t) equal to that state fragment and satisfies S(cond). Because t' is of the form t'(X,Y), the next state is not uniquely determined: it depends on the choice of an additional substitution R for the variables Y. Thus the result of applying the rule may be nondeterministic. The choice of R is made according to the probability function S(Dist), which in general is not a fixed probability function, but a family of functions: one for each match S of the variables X.

Probabilistic Maude (PMaude)

PMaude extends Maude, a high-performance rewrite engine, by allowing us to write and simulate specifications in probabilistic rewrite theories. For example, let tick be a probabilistic rule that increments the time T of a clock by time d, where d is distributed according to an Exponential distribution with rate 1.0 :

clock(T) => clock(T+d) with probability Exponential(1.0) .

The above rule can be written in PMaude as follows:

rl [tick] : clock(T) => clock(T + sampleFromExponential(1.0) ) .

where the term sampleFromExponential(1.0) rewrites to a random term representing a sample from an Exponential distribution with rate 1.0 .
Similarly, a discrete time probabilistic rewrite rule for a fair coin toss can be written as follows:

rl [toss] : coin => if sampleFromUniform(0.0,1.0) > 0.5 then head else tail fi.

The work is supported in part by the MURI ONR Grant N00014-02-1-0715 and the Defense Advanced Research Projects Agency (the DARPA IPTO TASK Program, contract number F30602-00-2-0586 and the DARPA IXO NEST Program, contract number F33615-01-C-1907).