Discrete real-time and stochastic-time process algebra for performance analysis of distributed systems

We present a process algebra with conditionally distributed discrete-time delays and generally-distributed stochastic delays. It fea- tures two types of race conditions in terms of conditional random vari- ables. Building on the new theory we analyze extensions of timed process algebra with discrete stochastic time. In the new setting, typical stan- dard notions like time additivity are hard to preserve in the presence of the race condition. We propose context-sensitive interpolation as a restricted form of time additivity to accommodate the extension with stochastic time. The approach enables compositional modeling, a non- trivial expansion law, and explicit manipulation of maximal progress. The approach is illustrated by a speci¯cation of the Concurrent Alter- nating Bit Protocol with unreliable generally-distributed channels in the language Â.We compare performance analysis using discrete timed prob- abilistic reward graphs and discrete-event simulation