PAPM-PROBMIV on Thursday

Detailed program
Thursday July 25th, 2002
See also the unified by-slot program


All sessions take place in auditorium 3.

09:10-09:30  Welcome and Opening

Session 1: Invited talk

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).

Session 2: Numerical analysis algorithms

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.

Session 3: Symbolic computation

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."

Session 4: Non-interleaving models

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.

18:30-19:30  PAPM-ProbMiV business meeting