Probabilistic System Models

We have defined state-machine models for probabilistic concurrent systems, both timed and untimed. Accompanying the models is a collection of formal proof techniques that work to prove correctness and performance properties for probabilistic concurrent systems. The models admit compositional reasoning and reasoning using levels of abstraction.

Both models appear in Segala's PhD thesis, completed in June, 1995. Pieces of this may be found in a 1994 PODC paper by Lynch, Saias and Segala, a 1994 CONCUR paper by Segala and Lynch and in a 1995 CONCUR paper by Segala.

Formal verification of probabilistic systems is explored in a 1995 PODC paper by Pogosyants and Segala. T he verification technique presented in the paper supports partial automation of proofs.

A current project undertaken by Anna Pogosyants and Roberto Segala is developing verification techniques for analysis of expected complexity.

Other work on modeling probabilistic concurrent systems appears in Isaac Saias' PhD Thesis.

The models have been applied to verify correctness of some randomized distributed algorithms and to find errors in others. See our page on probabilistic system analysis.

TOC / LCS / MIT
Last modified: Thu Nov 6 22:08:46 1997 		Comments?