| | All
sessions take place in auditorium 3.09:30- | 10:30
| André
Schiper, EPFL Lausanne, Switzerland Invited
talk: **Failure detection vs. group membership in fault-tolerant distributed
systems: hidden trade-offs** Failure
detection and group membership are two important
components of fault-tolerant distributed systems. Understanding their role
is essential when developing efficient solutions, not only in failure-free
runs, but also in runs in which processes do crash. While group membership
provides consistent information about the status of processes in the
system, failure detectors provide inconsistent information. This paper
discusses the trade-offs related to the use of these two components, and
clarifies their roles using three examples. The first example shows a case
where group membership may favourably be replaced by a failure detection
mechanism. The second example illustrates a case where group membership is
mandatory. Finally, the third example shows a case where neither group
membership nor failure detectors are needed (they may be replaced by *weak
ordering* oracles). |
11:00- | 11:40
| Marta Kwiatkowska, U Birmingham, UK Rashid
Mehmood, U Birmingham, UK
**Out-of-core
solution of large linear systems of equations arising
from stochastic modelling** Many
physical or computer systems can be modelled as Markov
chains. A range of solution techniques exist to address the state-space
explosion problem, encountered while analysing such Markov models. However,
numerical solution of these Markov chains is impeded by the need to store
the probability vector(s) explicitly in the main memory. In this paper, we
extend the earlier out-of-core methods for the numerical solution of large
Markov chains and introduce an algorithm which uses a disk to hold the
probability vector as well as the matrix. We give experimental results of
the implementation of the algorithm for a Kanban manufacturing system and a
flexible manufacturing system. Next, we describe how the algorithm can be
modified to exploit sparsity structure of a model, leading to better
performance. We discuss two models, a cyclic server polling system and a
workstation cluster system, in this context and present results for the
polling models. We also introduce a new sparse matrix storage format which
can provide 30% or more saving over conventional
schemes. |
11:40- | 12:20
| Henrik Bohnenkamp, U Twente, The
Netherlands Boudewijn
Haverkort, Aachen U of Techn., Germany
**The
mean value of the maximum** This
paper treats a practical problem that arises in the area of
stochastic process algebras. The problem is the efficient computation of
the mean value of the maximum of phase-type distributed random variables.
The maximum of phase-type distributed random variables is again phase-type
distributed, however, its representation grows exponentially in the number
of considered random variables. Although an efficient representation in
terms of Kronecker sums is straightforward, the computation of the mean
value requires still exponential time, if carried out by traditional means.
In this paper, we describe an approximation method to compute the mean
value in only polynomial time in the number of considered random variables
and the size of the respective representations. We discuss complexity,
numerical stability and convergence of the approach. |
14:00- | 14:40
| Matthias Kuntz, U Erlangen, Germany Markus
Siegle, U Erlangen, Germany
**Deriving
symbolic representations from stochastic process
algebras** A
new denotational semantics for a variant of the stochastic
process algebra TIPP is presented, which maps process terms to
Multi-terminal binary decision diagrams. It is shown that the new semantics
is Markovian bisimulation equivalent to the standard SOS semantics. The
paper also addresses the difficult question of keeping the underlying state
space minimal at every construction step. |
14:40- | 15:20
| Marta Kwiatkowska, U Birmingham,
UK Gethin
Norman, U Birmingham, UK Jeremy
Sproston, U Turin, Italy
**Probabilistic
model checking of the IEEE 802.11 wireless local area
network protocol** The
international standard IEEE 802.11
was developed recently in recognition of the increased demand for wireless
local area networks. Its medium access control mechanism is described
according to a variant of the Carrier Sense Multiple Access with Collision
Avoidance (CSMA/CA) scheme. Although collisions cannot always be prevented,
randomized exponential backoff rules are used in the retransmission scheme
to minimize the likelihood of repeated collisions. More precisely, the
backoff procedure involves a uniform probabilistic choice of an
integer-valued delay from an interval, where the size of the interval grows
exponentially with regard to the number of retransmissions of the current
data packet. We model the two-way handshake mechanism of the IEEE 802.11
standard with a fixed network topology using
probabilistic timed automata, a formal description mechanism in which both
nondeterministic choice and probabilistic choice can be represented. From
our probabilistic timed automaton model, we obtain a finite-state Markov
decision process via a property-preserving discrete-time semantics. The
Markov decision process is then verified using Prism, a
probabilistic model checking tool, against
probabilistic, timed properties such as "at most 5,000
microseconds pass before a station sends its packet correctly." |
16:00- | 16:40
| Harald Fecher, U Mannheim,
Germany Mila
Majster-Cederbaum, U Mannheim, Germany Jinzhao
Wu, U Mannheim, Germany
**Action
refinement for probabilistic processes with true concurrency
models** In
this paper, we develop techniques of action refinement for
probabilistic processes within the context of a probabilistic process
algebra. A semantic counterpart is carried out in a non-interleaving
causality based setting, probabilistic bundle event structures. We show
that our refinement notion has the following nice properties: the behaviour
of the refined system can be inferred compositionally from the behaviour of
the original system and from the behaviour of the systems substituted for
actions; the probabilistic extensions of pomset trace equivalence and
history preserving bisimulation equivalence are both congruences under the
refinement; and with respect to a cpo-based denotational semantics the
syntactic and semantic refinements coincide with each other up to the
aforementioned equivalence relations when the internal actions are
abstracted away. |
16:40- | 17:20
| Stefan Haar, IRISA Rennes, France
**Probabilistic
unfoldings and partial order fairness in Petri
nets** The
article investigates fairness and conspiracy in a
probabilistic framework, based on unfoldings of Petri nets. Here, the
unfolding semantics uses a new, cluster-based view of local choice. The
algorithmic construction of the unfolding proceeds on two levels, *choice* of steps inside conflict clusters, where the choice may
be fair or unfair, and the em policy controlling the order in which
clusters may act; this policy may or may not conspire, e.g., against a
transition. In the context of an example where conspiracy can hide in the
partial order behavior of a life and 1-safe Petri net, we show that, under
non-degenerate i.i.d. randomization on both levels, both conspiracy and
unfair behavior have probability 0. The probabilistic model, using special
Gibbs potentials, is presented here in the context of 1-safe nets, but
extends to any Petri net. |
| |