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.
Abstract:
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.
Abstract:
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.
Abstract:
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.
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.
