by Hynek Mlnařík, December 2006, 43 pages.
FIMU-RS-2006-10. Available as Postscript, PDF.
We present new imperative quantum programming language LanQ which was designed to support combination of quantum and classical programming and basic process operations -- process creation and interprocess communication. The language can thus be used for implementing both classical and quantum algorithms and protocols. Its syntax is similar to that of C language what makes it easy to learn for existing programmers. In this paper, we present operational semantics of the language. We provide an example run of a quantum random number generator.
by Ivana Černá, Pavlína Vařeková, Barbora Zimmerová, October 2006, 25 pages.
FIMU-RS-2006-08. Available as Postscript, PDF.
The paper introduces a Component-interaction automata language, which was designed for modelling of component interactions in hierarchical component-based software systems. The language supports modelling of important interaction attributes of such systems, and hence provides a rich base for further application of formal methods. Component-interaction automata provide a flexible form of component composition which can respect architectural assembly of the system, communication mechanisms, and other specifics of component-based systems. This allows the language to capture interactions in many different kinds of componentbased systems (built on different component models for instance). This paper provides a detailed study of the language including discussion of its practical application
by Stanislav Bartoň, Pavel Zezula, A full version of the paper presented at IEEE MCD 2006. September 2006, 22 pages.
FIMU-RS-2006-07. Available as Postscript, PDF.
An own design of an indexing structure for general graph structured data called rhoIndex that allows an effective processing of special path queries is presented. These special queries represent for example a search for all paths lying between two arbitrary vertices limited to a certain path length. The rhoIndex is a multilevel balanced tree structure where each node is created with a certain graph transformation and described by modified adjacency matrix. Hence, rhoIndex indexes all the paths to a predefined length linclusive. The search algorithm is then able to find all the paths shorter than or having the length land some of the paths longer then the predefined llying between any two vertices in the indexed graph. The designed search algorithm exploits a special graph structure, a transcription graph, to compute the result using the rhoIndex . We also present an experimental evaluation of the process of creating the rhoIndex on graphs with different sizes and also a complexity evaluation of the search algorithm that uses the rhoIndex.
by Ondřej Výborný, September 2006, 19 pages.
FIMU-RS-2006-06. Available as Postscript, PDF.
The past few years have confirmed the increasing importance of the preservation of the privacy of an individual due to the number of methods by which private information can be misused. At the same time, since vast amounts of data are easily available, data mining is taking on a greater role in the processing thereof, placing techniques that can satisfy strict legal and public requirements on the processing of sensitive data in great demand.
by Laura Bozzelli, Mojmír Křetínský, Vojtěch Řehák, Jan Strejček, A full version of the paper presented at FSTTCS 2006. November 2006, 27 pages.
FIMU-RS-2006-05. Available as Postscript, PDF.
We establish a decidability boundary of the model checking problem for infinite-state systems defined by Process Rewrite Systems (PRS) or weakly extended Process Rewrite Systems (wPRS), and properties described by basic fragments of action-based Linear Temporal Logic (LTL). It is known that the problem for general LTL properties is decidable for Petri nets and for pushdown processes, while it is undecidable for PA processes. As our main result, we show that the problem is decidable for wPRS if we consider properties defined by formulae with only modalities strict eventually and strict always. Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality until or the fragment with modalities next and infinitely often.
by Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, Jana Tůmová, September 2006, 19 pages.
FIMU-RS-2006-04. Available as Postscript, PDF.
Probabilistic processes are used to model concurrent programs that exhibit uncertainty. The state explosion problem for probabilistic systems is more critical than in the non-probabilistic case. In the paper we propose a cluster-based algorithm for qualitative LTL model checking of finite state Markov decision processes. We use the automata approach which reduces the model checking problem to the question of existence of an accepting end component. The algorithm uses repeated reachability which systematically eliminates states that cannot belong to any accepting end component. A distinguished feature of the distributed algorithm is that its complexity meets the complexity of the best known sequential algorithm.
by Radek Pelánek, October 2006, 39 pages.
FIMU-RS-2006-03. Available as Postscript, PDF.
We present BEEM - BEnchmarks for Explicit Model checkers. This benchmark set includes more than 50 models together with correctness properties (both safety and liveness). The benchmark set is accompanied by an comprehensive web
The report describes the rationale beyond the form of the benchmark set, the design of the web portal and the main aspects of its realization, and also an example of an experimental analysis over the benchmark set: an analysis of a performance of sequential and distributed reachability.
The address of the web portal is http://anna.fi.muni.cz/models .
by Tomáš Brázdil, Václav Brožek, Vojtěch Forejt, Antonín Kučera, A full version of the paper presented at LICS 2006. September 2006, 37 pages.
FIMU-RS-2006-02. Available as Postscript, PDF.
We consider stochastic turn-based games where the