Several formal models combine probabilistic and nondeterministic features. To allow their probabilistic simulation and statistical model checking by means of pseudo-random number sampling, all sources of nondeterminism ...

Unbounded data structures, advanced functions and data types, and/or different forms of communication are often needed to model large and complex probabilistic real-time systems such as wireless sensor network algorithms. ...

PSMaude is a probabilistic extension of Maude that provides an expressive probabilistic strategy language to quantify the nondeterminism in probabilistic rewrite theories, allowing the user to specify different probabilistic ...