zbMATH — the first resource for mathematics

Probabilistic simulations for probabilistic processes. (English) Zbl 0839.68067
Summary: Several probabilistic simulation relations for probabilistic systems are defined and evaluated according to two criteria: compositionality and preservation of “interesting” properties. Here, the interesting properties of a system are identified with those that are expressible in an untimed version of the Timed Probabilistic concurrent Computation Tree Logic (TPCTL) of Hansson. The definitions are made, and the evaluations carried out, in terms of a general labeled transition system model for concurrent probabilistic computation. The results cover weak simulations, which abstract from internal computation, as well as strong simulations, which do not.

68Q45 Formal languages and automata
03B45 Modal logic (including the logic of norms)