NMSPA: A Non-Markovian Model for Stochastic Processes
Natalia Lopez and Manuel Núñez
Universidad Complutense de Madrid, SPAIN
Abstract
In this paper we introduce a new Stochastic Process Algebra:
NMSPA. This new language shares the usual features in
stochastic models but distributions are not restricted to be
exponential. This fact increases the expressive power of the
language in several ways. For example, we can specify
actions that can be executed with probability 1 in a finite
amount of time, so-called passive actions fall in a natural
way inside our framework, urgency of internal actions can
be expressed, etc.
In order to define an interleaving semantics for the parallel
operator, we benefit from the ideas used in timed process
algebras. Our operational transitions include information
about the time when the action can be executed, as well as
the random variable associated with it. We provide our
language with a notion of strong bisimulation which takes
into account the urgency of internal transitions.
Finally, we specify the Alternating Bit Protocol. This is a
very simple communication protocol where the channels
are faulty.
Keywords:
Formal Methods; Stochastic Process Algebras;
Bisimulation Semantics; Specification of Communication Protocols.