We give a complete axiomatization of trace distribution precongruence for probabilistic nondeterministic processes based on a process algebra that includes internal behavior and recursion. The axiomatization is given for two different semantics of the process algebra that are consistent with the alternating model of Hansson and the non-alternating model of Segala, respectively. It is shown that the two semantics coincide up to trace distribution precongruence.
Axiomatization of Trace Semantics for Stochastic Nondeterministic Processes
PARMA, Augusto;SEGALA, Roberto
2004-01-01
Abstract
We give a complete axiomatization of trace distribution precongruence for probabilistic nondeterministic processes based on a process algebra that includes internal behavior and recursion. The axiomatization is given for two different semantics of the process algebra that are consistent with the alternating model of Hansson and the non-alternating model of Segala, respectively. It is shown that the two semantics coincide up to trace distribution precongruence.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
