A Denotational Model for Probabilistic and Nondeterministic Processes
Diego Cazorla, Fernando Cuartero, Valentín Valero and Fernando L. Pelayo
Universidad de Castilla-La Mancha, SPAIN
Abstract
In this paper we present an algebraic model for the description of
probabilistic and nondeterministic processes: PNAL
(Probabilistic and Nondeterministic Algebraic Language), an
extension of EPL, defined by Matthew Hennessy, including a
probabilistic choice operator. An operational semantics and a
testing semantics for the language are presented. A denotational
semantics for the finite subset of the language, PNALf,
is proposed. Finally, we provide two results: equivalence between
nondeterministic processes in finite EPL is preserved in
PNALf, and denotational semantics is fully abstract with
respect to the testing semantics
Keywords: Formal Methods, Process Algebra, Testing,
Probability, Nondeterminism, Process Specification.