This report contains detailed description of the fundamentals and specific algorithms of LOBS, a theoretical analysis of its behaviour, and results of extensive experiments we conducted using a prototype implementation of LOBS. We tested LOBS with the peer-to-peer structure \mchord{} having a various number of peers. We used a real-life dataset and query sets of various distributions. The results show that LOBS is able to cope with any query-distribution and that it improves both the utilization of resources and the system performance of query processing. The costs of balancing are reasonable compared to the level of imbalance and are very small if the system has time to adapt to a query-traffic. The behaviour of LOBS is independent of the size of the network.

Strategy Synthesis for Markov Decision Processes and Branching-Time Logics

by Tomáš Brázdil, Vojtěch Forejt, A full version of the paper presented at CONCUR 2007 July 2007, 28 pages.

FIMU-RS-2007-03. Available as Postscript, PDF.

Abstract:

We consider a class of finite $1\frac{1}{2}$-player games (Markov decision processes) where the winning objectives are specified in the branching-time temporal logic qPECTL$^*$ (an extension of the qualitative PCTL$^*$). We study decidability and complexity of existence of a winning strategy in these games. %The logic is more expressive than the qualitative fragment of PCTL$^*$. We identify a fragment of qPECTL$^*$ called detPECTL$^*$ for which the existence of a winning strategy is decidable in exponential time, and also the winning strategy can be computed in exponential time (if it exists). Consequently we show that every formula of qPECTL$^*$ can be translated to a formula of detPECTL$^*$ (in exponential time) so that the resulting formula is equivalent to the original one over finite Markov chains. From this we obtain that for the whole qPECTL$^*$, the existence of a winning finite-memory strategy is decidable in double exponential time. An immediate consequence is that the existence of a winning finite-memory strategy is decidable for the qualitative fragment of PCTL$^*$ in triple exponential time. We also obtain a single exponential upper bound on the same problem for the qualitative PCTL. Finally, we study the power of finite-memory strategies with respect to objectives described in the qualitative PCTL.

Formalisms and Tools for Design and Specification of Network Protocols

by Jindřich Babica, Vojtěch Řehák, Petr Slovák, Pavel Troubil, Martin Zavadil, May 2007, 33 pages.

FIMU-RS-2007-02. Available as Postscript, PDF.

Abstract:

Message Sequence Charts (MSC) are a useful formalism for formalization of network protocols early in their design phase. In this paper, we introduce the basics of MSC language and describe some of the possibilities for automatic location of "problematic" parts in the design. Focus is then given to different modifications of MSC design (FIFO behavior, bounded channels, etc. ) as well as formal checking of more complex design properties (MSC membership, realizability). Next, an introduction of Specification and Description Language (SDL) is presented. Possibilities of automatic synthesis of system design in MSC to an SDL model and it`s correctness verification are mentioned.

LTL model checking with I/O-Efficient Accepting Cycle Detection

by Jiří Barnat, Luboš Brim, Pavel Šimeček, January 2007, 20 pages.

FIMU-RS-2007-01. Available as Postscript, PDF.

Abstract:

We show how to adopt existing non-DFS-based algorithm OWCTY for accepting cycle detection to the I/O efficient setting and compare the I/O efficiency and practical performance of the adopted algorithm to the existing I/O efficient LTL model checking approach of Edelkamp et al. We show that while the new algorithm exhibits similar I/O complexity with respect to the size of the graph, it avoids the quadratic increase in the size of the graph of the approach of Edelkamp et al. Therefore, the absolute numbers of I/O operations are significantly smaller and the algorithm exhibits better practical performance.