Technical Reports

A list with abstracts sorted by year - 2006

Operational Semantics of Quantum Programming Language LanQ

by Hynek Mlnaøík, December 2006, 43 pages.

FIMU-RS-2006-10. Available as Postscript, PDF.

Abstract:

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.

Component-Interaction Automata Modelling Language

by Ivana Èerná, Pavlína Vaøeková, Barbora Zimmerová, October 2006, 25 pages.

FIMU-RS-2006-08. Available as Postscript, PDF.

Abstract:

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 and comparison with related work. We intend to use this language as a framework for verifying coordination errors, checking of reconfiguration correctness, and formal analysis of component interactions in component-based systems, which is our ongoing and future work.

rhoIndex, Designing and Evaluating an Indexing Structure for Graph Structured Data

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.

Abstract:

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.

Privacy Preserving Data Mining, State-of-the-Art

by Ondøej Výborný, September 2006, 19 pages.

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

Abstract:

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. This paper presents the state-of-the-art in privacy preserving data mining and also proposes an alternative classification of privacy preserving techniques based on several points of view on privacy.

On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems

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.

Abstract:

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.

Distributed Qualitative LTL Model Checking of Markov Decision Processes

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.

Abstract:

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.

Web Portal for Benchmarking Explicit Model Checkers

by Radek Pelánek, October 2006, 39 pages.

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

Abstract:

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 portal, which provides detailed information about all models. The web portal also includes information about state spaces and facilities selection of models for experiments.

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 .

Stochastic Games with Branching-Time Winning Objectives

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.

Abstract:

We consider stochastic turn-based games where the winning objectives are given by formulae of the branching-time logic PCTL. These games are generally not determined and winning strategies may require memory and/or randomization. Our main results concern history-dependent strategies. In particular, we show that the problem whether there exists a history-dependent winning strategy in 1.5-player games is highly undecidable, even for objectives formulated in the L(F^{=5/8},F^{=1},F^{>0},G^{=1}) fragment of PCTL. On the other hand, we show that the problem becomes decidable (and in fact EXPTIME-complete) for the L(F^{=1},F^{>0},G^{=1}) fragment of PCTL, where winning strategies require only finite memory. This result is tight in the sense that winning strategies for L(F^{=1},F^{>0},G^{=1},G^{>0}) objectives may already require infinite memory.