Abstract
Process algebras are formalisms for abstract modeling of systems for the
purpose of qualitative veri¯cation and quantitative evaluation. The purpose
of veri¯cation is to show that the system behaves correctly, e.g., it does not
contain a deadlock or a state with some desired property is eventually going
to be reached. The quantitative or performance evaluation part gives an
approximation how well the system will behave, e.g., the average time of
a message to get through is 10 time units or the utilization (percentage of
time that something is used) of some machine is 23.5 percent.
Originally, process algebras were only developed for qualitative model
ing, but gradually they have been extended with time, probabilities, and
Markovian (exponential) and generallydistributed stochastic time. The ex
tensions up to stochastic time typically conservatively extended previous
wellestablished theories. However, mostly due to the nature of the under
lying (non)Markovian performance models, the stochastic process algebras
were built from scratch. These extensions were carried out as orthogonal
extensions of untimed process theories with exponential delays or stochastic
clocks. The underlying performance model is obtained by abstracting from
the qualitative behavior using some weak behavioral equivalence.
The thesis investigates several issues: (1) What is the relationship be
tween discrete real and generallydistributed stochastic time in the process
theories? (2) Is it possible, and if so, how, to extend timed process theories
with stochastic time? (3) Reversely, is it possible, and if so, how, to embed
discrete real time in generally distributed process theories? Additionally,
(4) is the abstraction using the weak behavioral equivalence in Markovian
process theories (and other modeling formalisms as well) performance pre
serving, and is such an approach compositional? In the end, (5) how can we
do performance analysis using discretetime and probabilistic choices?
The contents of the thesis is as follows. First, we introduce the central
concept of a race condition that de¯nes the interaction between stochastic
timed delays. We introduce a new type of race condition, which enables
the synchronization of stochastic delays with the same sample as in timed
process theories. This gives the basis for the notion of a timed delay in a
racing context, which models the expiration of stochastic delays. In this
new setting, we de¯ne a strong bisimulation relation that deals with the
(probabilistic) race condition on a symbolic level. Next, we show how to
derive stochastic delays as guarded recursive speci¯cation involving timed
delays in a racing context and we derive a groundcomplete stochastictime
process theory. Then, we take the opposite viewpoint and we develop a
stochastic process theory from scratch, relying on the same interpretation
of the race condition. We embed real time in the stochastictime setting
by using contextsensitive interpolation, a restricted notion of time additiv
ity. Afterwards, we turn to Markovian process theories and we show com
positionality of the Markov reward chains with fast and silent transitions
with respect to lumpingbased and reductionbased aggregation methods.
These methods can be used to show preservation of performance measures
when eliminating probabilistic choices and nondeterministic silent steps in
Markovian process theories. Then, we specify the underlying model of prob
abilistic timed process theories as a discretetime probabilistic reward graph
and we show its transformation to a discretetime Markov reward chain.
The approach is illustrated by extending the environment of the modeling
language Â. The developed theories are illustrated by specifying a version
of the concurrent alternating bit protocol and analyzing it in the Â toolset.
Original language  English 

Qualification  Doctor of Philosophy 
Awarding Institution 

Supervisors/Advisors 

Award date  2 Oct 2008 
Place of Publication  Eindhoven 
Publisher  
Print ISBNs  9789038613949 
DOIs  
Publication status  Published  2008 
Fingerprint Dive into the research topics of 'Real and stochastic time in process algebras for performance evaluation'. Together they form a unique fingerprint.
Cite this
Markovski, J. (2008). Real and stochastic time in process algebras for performance evaluation. Technische Universiteit Eindhoven. https://doi.org/10.6100/IR637756