Embedding Real Time in Stochastic Process Algebras

Abstract. 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. 1 Introduction Traditionally, process algebras (PAs) like ACP, CCS and CSP are used for quali-tative description and verification of processes. In this setting, process behaviou