Projects per year
Abstract
Stochastic process calculi represent widely accepted formalisms within Computer
Science for modelling nondeterministic stochastic systems in a compositional
way. Similar to process calculi in general, they are suited for modelling
systems in a hierarchical manner, by explicitly specifying subsystems as well
as their interdependences and communication channels. Stochastic process calculi
incorporate both the quantified uncertainty on probabilities or durations of
events and nondeterministic choices between several possible continuations of
the system behaviour.
Modelling of a system is often performed with the purpose to verify the system.
In this dissertation it is argued that the verification techniques that have
their origin in the analysis of programming code with the purpose to deduce
the properties of the code's execution, i.e. Static Analysis techniques, are transferable
to stochastic process calculi. The description of a system in the syntax
of a particular stochastic process calculus can be analysed in a compositional
way, without expanding the state space by explicitly resolving all the interdependencies
between the subsystems which may lead to the state space explosion
problem.
In support of this claim we have developed analysis methods that belong to
a particular type of Static Analysis { Data Flow / Pathway Analysis. These
methods have previously been applied to a number of nonstochastic process
calculi. In this thesis we are lifting them to the stochastic calculus of Interactive
Markov Chains (IMC). We have devised the Pathway Analysis of IMC that
is not only correct in the sense of overapproximating all possible behaviour
scenarios, as is usual for Static Analysis methods, but is also precise. This gives
us the possibility to explicitly decide on the tradeo between precision and
complexity while postprocessing the analysis results.
Another novelty of our methods consists in the kind of properties that we can
verify using the results of the Pathway Analysis. We can check both qualitative
and quantitative properties of IMC systems. In particular, we have developed
algorithms for constructing bisimulation relations, computing (overapproximations
of) sets of reachable states and computing the expected time reachability,
the last for a linear fragment of IMC. In all the cases we have the complexities
of algorithms which are low polynomial in the size of the syntactic description
of a system. The presented methods have a clear application in the areas of embedded
systems, (randomised) protocols run between a fixed number of parties
etc.
Original language  English 

Place of Publication  Kgs. Lyngby, Denmark 

Publisher  Technical University of Denmark 
Publication status  Published  2011 
Series  IMMPHD2011252 

Fingerprint Dive into the research topics of 'Verification of Stochastic Process Calculi'. Together they form a unique fingerprint.
Projects
 1 Finished

Verification of Stochastic Process Calculi
Skrypnyuk, N., Nielson, F., Seidl, H., Probst, C. W., Hankin, C., Hermanns, H. & Nielson, H. R.
01/09/2007 → 22/06/2011
Project: PhD