We present a stochastic process algebra including immediate actions, deadlock and termination, and explicit stochastic delays, in the setting of weak choice between immediate actions and passage of time. The operational semantics is a spent time semantics, avoiding explicit clocks. We discuss the embedding of weak-choice real-time process theories and analyze the behavior of parallel composition in the weak choice framework. Keywords. Stochastic delay, weak choice, race condition, real-time and stochastic process algebra.
Jasen Markovski, Erik P. de Vink