Technical Reports

A list with abstracts sorted by year - 2007

Adaptive Approximate Similarity Searching through Metric Social Networks

by Jan Sedmidubský, Stanislav Bartoň, Vlastislav Dohnal, Pavel Zezula, A full version of the paper presented at ICDE 2008. November 2007, 22 pages.

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


Exploiting the concepts of social networking represents a novel approach to the approximate similarity query processing. We present an unstructured and dynamic P2P environment in which a metric social network is built. Social communities of peers giving similar results to specific queries are established and such ties are exploited for answering future queries. Based on the universal law of generalization, a new query forwarding algorithm is introduced and evaluated. The same principle is used to manage query histories of individual peers with the possibility to tune the tradeoff between the extent of the history and the level of the query-answer approximation. All proposed algorithms are tested on real data and medium-sized P2P networks consisting of tens of computers.

Key Distribution and Secrecy Amplification in Wireless Sensor Networks

by Petr Švenda, Václav Matyáš, November 2007, 63 pages.

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


This report targets the area of wireless sensor networks, and in particular their security. Probabilistic key pre-distribution schemes were developed to deal with limited memory of a single node and high number of potential neighbours. We present a new idea of group support for authenticated key exchange that substantially increases the resilience of an underlaying probabilistic key pre-distribution scheme against the threat of node capturing. We also propose a new method for automatic protocol generation which utilizes Evolutionary Algorithms (EA). The approach is verified on the automatic generation of secrecy amplification protocols for wireless sensor networks. All human-designed secrecy amplification protocols proposed so far were re-invented by the method. A new protocol with better fraction of secure links was evolved. An alternative construction of secrecy amplification protocol was designed which exhibits only linear (instead of exponential) increase of needed messages when the number of communication neighbours is growing. As a message transmission is a battery expensive operation, this more efficient protocol can significantly save this resource.

LOBS: Load Balancing for Similarity Peer-to-Peer Structures

by David Novák, Pavel Zezula, June 2007, 36 pages.

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


The real-life experience with the similarity search shows that this task is both difficult and very expensive in terms of processing time. The peer-to-peer structures seem to be a suitable solution for content-based retrieval in huge data collections. In these systems, the computational load generated by a query traffic is highly skewed which degrades the searching performance. Since no current load-balancing techniques are designed for this task, we propose LOBS -- a novel and general system for load-balancing in peer-to-peer structures with time-consuming searching. LOBS is based on the following principles: measuring the computational load of the peers, separation of the logical and the physical level of the system, and detailed analysis of the load source to exploit either data relocation or data replication.

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.


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.


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.


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.

Responsible contact: unix(atsign)fi(dot)muni(dot)cz