# Technical Reports

## A list with abstracts sorted by year - all

### Attackers in Wireless Sensor Networks Will Be Neither Random nor Jumping -- Secrecy Amplification Case, Extended Version

by *
Radim Ošťádal,
Petr Švéda,
Václav Matyáš,
* September 2016, 20 pages.

**FIMU-RS-2016-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Partially compromised network is a pragmatic assumption in many real-life

### The Million-Key Question - Investigating the Origins of RSA Public Keys

by *
Petr Švenda,
Matus Nemec,
Peter Sekan,
Rudolf Kvasnovsky,
David Formanek,
David Komarek,
Václav Matyáš,
* August 2016, 83 pages.

**FIMU-RS-2016-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Can bits of an RSA public key leak information about design and implementation choices such as the prime generation algorithm? We analysed over 60 million freshly generated key pairs from 22 open- and closed-source libraries and from 16 different smartcards, revealing significant leakage. The bias introduced by different choices is sufficiently large to classify a probable library or smartcard with high accuracy based only on the values of public keys. Such a classification can be used to decrease

### Evaluation of the Impact of Question Difficulty on Engagement and Learning

by *
Jan Papoušek,
Vít Stanislav,
Radek Pelánek,
* April 2016, 13 pages.

**FIMU-RS-2016-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We study the impact of question difficulty on learners’ engagement and learning using an experiment with an open online educational system for adaptive practice of geography. The experiment shows that easy questions are better for short term engagement, whereas difficult questions are better for long term engagement and learning. These results stress the necessity of careful formalization of goals and optimization criteria of open online education systems. We also present disaggregation of overall results into specific contexts of practice and highlight the issue of attrition bias. This paper is an extended version of the paper presented at Intelligent Tutoring Systems conference.

### Towards Better Selective Forwarding And Delay Attacks Detection in Wireless Sensor Networks

by *
Martin Stehlik,
Václav Matyáš,
Andriy Stetsko,
* A full version of the paper presented at conference ICNSC 2016. April 2016, 30 pages.

**FIMU-RS-2016-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

A number of intrusion detection techniques have been proposed to detect different kinds of active attacks on wireless sensor networks (WSNs). Selective forwarding and delay attacks are two simple but effective attacks that can disrupt the communication in WSNs. In this work, we propose two parametrized collaborative intrusion detection techniques and optimize their parameters for a specific scenario using extensive simulations and multiobjective evolutionary algorithms. Moreover, we sample the whole search space to enable evaluation of evolution performance. The found optimized results are also compared to a simpler non-collaborative detection technique to demonstrate improvements of collaborative approach. We also evaluate the influence of changes of the number of malicious nodes on the intrusion detection performance. This technical report extends our paper presented at conference ICNSC 2016 by details of experiment settings and results.

### On Secrecy Amplification Protocols - Extended Version

by *
Radim Ošťádal,
Petr Švenda,
Václav Matyáš,
* A full version of the paper presented at conference WISTP 2015 June 2015, 34 pages.

**FIMU-RS-2015-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We review most important secrecy amplification protocols that are suitable for ad-hoc networks of devices with limited resources, providing additional resistance against various attacks on used cryptographic keys without necessity for asymmetric cryptography. We discuss and evaluate different designs as well as approaches to create new protocols. A special focus is given to suitability of these protocols with respect to different underlying key distribution schemes and also to open issues. This technical report provides details of our research that will be presented at the 9th WISTP International Conference on Information Security Theory and Practice (WISTP`2015), where a subset of this technical report will be published in this conference proceedings.

### On Clock-Aware LTL Properties of Timed Automata

by *
Peter Bezděk,
Nikola Beneš,
Vojtěch Havel,
Jiří Barnat,
Ivana Černá,
* A full version of the paper presented at conference ICTAC 2014. June 2014, 27 pages.

**FIMU-RS-2014-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We introduce the *Clock-Aware Linear Temporal Logic* (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a~timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed Büchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique.

### Probabilistic Bisimulation: Naturally on Distributions

by *
Holger Hermanns,
Jan Krčál,
Jan Křetínský,
* April 2014, 36 pages.

**FIMU-RS-2014-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

In contrast to the usual understanding of probabilistic systems as

### Traffic characteristics of common DoS tools

by *
Vit Bukac,
* April 2014, 83 pages.

**FIMU-RS-2014-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Denial of service (DoS) attacks is an ever growing threat to the availability of computer systems. Numerous solutions have been proposed both for DoS attacks detection and mitigation. However, their evaluation and mutual comparison is complicated due to scarcity of representative contemporary input data. In academia, proposed DoS detection systems are frequently evaluated with obsolete and in practice no longer used tools. Such discrepancy can lead to distinctly different detection efficiency in evaluation environment and real environment. To address this issue, we provide a comparative analysis of traffic features of DoS attacks that were generated by state-of-the-art standalone DoS attack tools. We list frequently used traffic features and verify their presence in analyzed attack traffic. Common denominator of all attack traffic is the presence of repeated similar yet independent operations. Therefore, we propose a new research area for the detection of DoS attacks the source end, based on repeated attack patterns recognition.

### Improving Intrusion Detection Systems for Wireless Sensor Networks

by *
Andriy Stetsko,
Tobias Smolka,
Václav Matyáš,
Martin Stehlik,
* March 2014, 29 pages.

**FIMU-RS-2014-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

A considerable amount of research has been undertaken in the field of intrusion detection in wireless sensor networks. Researchers proposed a number of relevant mechanisms, and it is not an easy task to select the right ones for a given application scenario. Even when a network operator knows what mechanism to use, it remains an open issue how to configure this particular mechanism in such a way that it is efficient for the particular needs. We propose a framework that optimizes the configuration of an intrusion detection system in terms of detection accuracy and memory usage. There is a variety of scenarios, and a single set of configuration values is not optimal for all of them. Therefore, we believe, such a framework is of a great value for a network operator who needs to optimize an intrusion detection system for his particular needs, e.g., attacker model, environment, node parameters.

### PRESEMT Phrase Model Generator

by *
Michalis Troullinos,
* November 2013, 18 pages.

**FIMU-RS-2013-3.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The PRESEMT (Pattern REcognition-based Statistically Enhanced MT)

### Phrase Aligner

by *
Michalis Troullinos,
* November 2013, 44 pages.

**FIMU-RS-2013-2.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The PRESEMT (Pattern REcognition-based Statistically Enhanced MT)

### Dynamic maintenance of an accepting run

by *
Florent Peres,
Ivana Černá,
* August 2013, 46 pages.

**FIMU-RS-2013-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Finding an infinite sequence of transitions (a run) going through some special states (called accepting) is of importance for fields like formal verification. Whereas finding such a sequence as been extensively studied, the problem of *maintaining* this sequence upon changes in the model or the specification has received less attention. In this work, we propose a solution to the maintenance of an accepting run when the transition system representing the product of the model and of the specification is changed, using the Tarjan`s algorithm as a base algorithm.

### Verification of Open Interactive Markov Chains

by *
Tomáš Brázdil,
Holger Hermanns,
Jan Krčál,
Jan Křetínský,
Vojtěch Řehák,
* A full version of the paper presented at conference FSTTCS 2012. November 2012, 52 pages.

**FIMU-RS-2012-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Interactive Markov chains (IMC) are compositional behavioral models extending both labeled transition systems and continuous-time Markov chains. IMC pair modeling convenience - owed to compositionality properties - with effective verification algorithms and tools - owed to Markov properties. Thus far however, IMC verification did not consider compositionality properties, but considered closed systems. This paper discusses the evaluation of IMC in an open and thus compositional interpretation. For this we embed the IMC into a game that is played with the environment. We devise algorithms that enable us to derive

### Parameter Identification and Model Ranking of Thomas Networks

by *
Hannes Klarner,
Adam Streck,
David Šafránek,
Juraj Kolcak,
Heike Siebert,
* A full version of the paper presented at conference CMSB 2012. November 2012, 39 pages.

**FIMU-RS-2012-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We propose a new methodology for identification and analysis of discrete gene networks as defined by Rene Thomas, supported by a tool chain: (i) given a Thomas network with partially known kinetic parameters, we reduce the number of acceptable parametrizations to those that fit time-series measurements and reflect other known constraints by an improved technique of coloured LTL model checking performing efficiently on Thomas networks in distributed environment; $(ii)$ we introduce classification of acceptable parametrizations to identify the most optimal ones; (iii) we propose a way of visualising parametrizations dynamics wrt time-series data. The methodology is validated on a rat neural development case study; (iv) finally we provide description of developed algorithms and evaluation of their performance.

### Modal Process Rewrite Systems

by *
Nikola Beneš,
Jan Křetínský,
* A full version of the paper presented at ICTAC 2012. June 2012, 25 pages.

**FIMU-RS-2012-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We consider modal transition systems with infinite state space generated by finite sets of rules. In particular, we extend process rewrite systems to the modal setting and investigate decidability of the modal refinement relation between systems from various subclasses. Since already simulation is undecidable for most of the cases, we focus on the case where either the refined or the refining process is finite. Namely, we show decidability for pushdown automata extending the non-modal case and surprising undecidability for basic parallel processes. Further, we prove decidability when both systems are visibly pushdown automata. For the decidable cases, we also provide complexities. Finally, we discuss a notion of bisimulation over MTS.

### Dual-Priced Modal Transition Systems with Time Durations

by *
Nikola Beneš,
Jan Křetínský,
Kim Guldstrand Larsen,
Mikael Moeller,
Jiří Srba,
* A full version of the paper presented at conference LPAR 2012. January 2012, 23 pages.

**FIMU-RS-2012-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Modal transition systems are a well-established specification formalism for a high-level modelling of component-based software systems. We present a novel extension of the formalism called modal transition systems with durations where time durations are modelled as controllable or uncontrollable intervals. We further equip the model with two kinds of quantitative aspects: each action has its own running cost per time unit, and actions may require several hardware components of different costs. We ask the question, given a fixed budget for the hardware components, what is the implementation with the cheapest long-run average reward. We give an algorithm for computing such optimal implementations via a reduction to a new extension of mean payoff games with time durations and analyse the complexity of the algorithm.

### Employing Subsequence Matching in Audio Data Processing

by *
Petr Volny,
David Novák,
Pavel Zezula,
* September 2011, 29 pages.

**FIMU-RS-2011-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We overview current problems of audio retrieval and time-series subsequence matching. We discuss the usage of subsequence matching approaches in audio data processing, especially in automatic speech recognition (ASR) area and we aim at improving performance of the retrieval process. To overcome the problems known from the time-series area like the occurrence of implementation bias and data bias we present a Subsequence Matching Framework as a tool for fast prototyping, building, and testing similarity search subsequence matching applications. The framework is build on top of MESSIF (Metric Similarity Search Implementation Framework) and thus the subsequence matching algorithms can exploit advanced similarity indexes in order to significantly increase their query processing performance. To prove our concept we provide a design of query-by-example spoken term detection type of application with the usage of phonetic posteriograms and subsequence matching approach.

### Parametric Modal Transition Systems

by *
Nikola Beneš,
Jan Křetínský,
Kim Guldstrand Larsen,
Mikael Moller,
Jiří Srba,
* A full version of the paper presented at ATVA 2011 July 2011, 24 pages.

**FIMU-RS-2011-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently

### Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes

by *
Tomáš Brázdil,
Václav Brožek,
Krishnendu Chatterjee,
Vojtěch Forejt,
Antonín Kučera,
* A full version of the paper presented at conference LICS 2011. April 2011, 32 pages.

**FIMU-RS-2011-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We study Markov decision processes (MDPs) with multiple

### Human Problem Solving: Sudoku Case Study

by *
Radek Pelánek,
* A full version of a paper presented at the 24th Florida Artificial Intelligence Research Society Conference January 2011, 21 pages.

**FIMU-RS-2011-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We discuss and evaluate metrics for difficulty rating of Sudoku puzzles. The correlation coefficient with human performance for our best metric is 0.95. The data on human performance were obtained from three web portals and they comprise thousands of hours of human solving over 2000 problems. We provide a simple computational model of human solving activity and evaluate it over collected data. Using the model we show that there are two sources of problem difficulty: complexity of individual steps (logic operations) and structure of dependency among steps. Beside providing a very good Sudoku-tuned metric, we also discuss a metric with few Sudoku-specific details, which still provides good results (correlation coefficient is 0.88). Hence we believe that the approach should be applicable to difficulty rating of other constraint satisfaction problems.

### Disjunctive Modal Transition Systems and Generalized LTL Model Checking

by *
Nikola Beneš,
Ivana Černá,
Jan Křetínský,
* November 2010, 44 pages.

**FIMU-RS-2010-12.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Modal transition systems (MTS) is a well established formalism used for specification and for abstract interpretation. We consider its disjunctive extension (DMTS) and we show that refinement problems for DMTS are not harder than in the case of MTS. There are two main results in the paper. Firstly, we give a solution to the common implementation and specification problems lowering the complexity from EXPTIME to PTIME. Secondly, we identify a fundamental error made in previous attempts at LTL model checking of MTS and provide algorithms for LTL model checking of MTS and DMTS. Moreover, we show how to apply this result to compositional verification and circumvent the general incompleteness of the MTS composition.

### Process Algebra for Modal Transition Systemses

by *
Nikola Beneš,
Jan Křetínský,
* A full version of the paper presented at MEMICS 2010. September 2010, 15 pages.

**FIMU-RS-2010-11.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The formalism of modal transition systems (MTS) is a well established framework for systems specification as well as abstract interpretation. Nevertheless, due to incapability to capture some useful features, various extensions have been studied, such as e.g. mixed transition systems or disjunctive MTS. Thus a need to compare them has emerged.

### Computing Strongly Connected Components in Parallel on CUDA (full version)

by *
Jiří Barnat,
Petr Bauch,
Luboš Brim,
Milan Češka,
* July 2010, 24 pages.

**FIMU-RS-2010-10.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The problem of decomposition of a directed graph into its strongly connected

### A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking

by *
Lasse Jacobsen,
Morten Jacobsen,
Mikael Moeller,
Jiří Srba,
* A full version of the paper presented at EPEW`10. August 2010, 34 pages.

**FIMU-RS-2010-09.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Many formal translations between time dependent models have been proposed over the years. While some of them produce timed bisimilar models, others preserve only reachability or (weak) trace equivalence. We suggest a general framework for arguing when a translation preserves Timed Computation Tree Logic (TCTL) or its safety fragment. The framework works at the level of timed transition systems, making it independent of the modeling formalisms and applicable to many of the translations published in the literature. Finally, we present a novel translation from extended Timed-Arc Petri Nets to Networks of Timed Automata and using the framework argue that it preserves the full TCTL. The translation has been implemented in the verification tool TAPAAL.

### Access Rights in Enterprise Full-text Search

by *
Jan Kasprzak,
Michal Brandejs,
Matěj Čuhel,
Tomáš Obšívač,
* A full version of the paper presented at ICEIS 2010 conference. July 2010, 19 pages.

**FIMU-RS-2010-08.**
Available as *Postscript*,
**PDF**.

#### Abstract:

One of the toughest problems to solve when

### Security of Biometric Authentication Systems -- Extended Version

by *
Václav Matyáš,
Zdeněk Říha,
* A full version of the paper presented at conference Computer Information Systems and Industrial Management Applications 2010 June 2010, 27 pages.

**FIMU-RS-2010-07.**
Available as *Postscript*,
**PDF**.

#### Abstract:

This technical report outlines our views of actual security

### Z-reachability Problem for Games on 2-dimensional Vector Addition Systems with States is in P

by *
Jakub Chaloupka,
* A full version of the paper presented at Workshop on Reachability Problems 2010 August 2010, 36 pages.

**FIMU-RS-2010-06.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We consider a two-player infinite game with zero-reachability objectives played on a 2-dimensional vector addition system with states (VASS), the states of which are divided between the two players. Brázdil, Jančar, and Kučera (2010) have shown that for k > 0, deciding the winner in a game on k-dimensional VASS is in

### Stochastic Real-Time Games with Qualitative Timed Automata Objectives

by *
Tomáš Brázdil,
Jan Krčál,
Jan Křetínský,
Antonín Kučera,
Vojtěch Řehák,
* A full version of the paper presented at CONCUR 2010. August 2010, 39 pages.

**FIMU-RS-2010-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We consider two-player stochastic games over real-time probabilistic

### Neighbor-Based Intrusion Detection for Wireless Sensor Networks

by *
Andriy Stetsko,
Lukáš Folkman,
Václav Matyáš,
* May 2010, 33 pages.

**FIMU-RS-2010-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The neighbor-based detection technique explores the principle that sensor nodes situated spatially close to each other tend to have similar behavior. A node is considered malicious if its behavior significantly differs from its neighbors. The detection technique is localized, unsupervised and adapts to changing network dynamics. Although the technique is promising, it has not been deeply researched in the context of wireless sensor networks yet. In this technical report we analyze symptoms of different attacks for the applicability of the neighbor-based technique. The analysis shows that the technique can be used for detection of selective forwarding, jamming and hello flood attacks. We implemented an intrusion detection system which employs the neighbor-based detection technique. The system was designed for and works on the TinyOS operating system running the Collection tree protocol. We evaluated accuracy of the technique in detection of selective forwarding, jamming and hello flood attacks. The results show that the neighbor-based detection technique is highly accurate, especially in the case when collaboration among neighboring nodes is used.

### Using Strategy Improvement to Stay Alive

by *
Luboš Brim,
Jakub Chaloupka,
* March 2010, 48 pages.

**FIMU-RS-2010-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We design a novel algorithm for solving Mean-Payoff Games

### Reachability Games on Extended Vector Addition Systems with States

by *
Tomáš Brázdil,
Petr Jančar,
Antonín Kučera,
* A full version of the paper presented at ICALP 2010. February 2010, 38 pages.

**FIMU-RS-2010-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We consider two-player turn-based games with zero-reachability and zero-safety objectives generated by extended vector addition systems with states. Although the problem of deciding the winner in such games is undecidable in general, we identify several decidable and even tractable subcases of this problem obtained by restricting the number of counters and/or the sets of target configurations.

### Human Problem Solving: Sokoban Case Study

by *
Petr Jarušek,
Radek Pelánek,
* April 2010, 25 pages.

**FIMU-RS-2010-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We describe a case study in human problem solving for a particular problem - a Sokoban puzzle. For the study we collected data using the Internet. In this way we were able to collect significantly larger data (2000 problems solved, 780 hours of problem solving activity) than in typical studies of human problem solving. Our analysis of collected data focuses on the issue of problem difficulty. We show that there are very large differences in difficulty of individual Sokoban problems and that these differences are not explained by previous research. To address this gap in understanding we describe an abstract computational model of human problem solving, a metric of a problem decomposition, and formalization of a state space bottleneck. We discuss how these concepts help us understand human problem solving activity and

### A Calculus of Coercive Subtyping

by *
Matej Kollár,
Ondřej Peterka,
Ondřej Ryšavý,
Libor Škarvada,
* November 2009, 17 pages.

**FIMU-RS-2009-11.**
Available as *Postscript*,
**PDF**.

#### Abstract:

This report deals with a type system that merges subtyping and dependent types. We define a calculus that instead of term overloading employs coercion mappings. This enables to detach the subtyping from other parts of the calculus, so that the mutual dependence between subtyping, typing and kinding can be reduced. We analyze basic properties of the calculus and show several examples that demonstrate the mechanism of coercive subtyping.

### Decidable Race Condition for HMSC

by *
Vojtěch Řehák,
Petr Slovák,
Jan Strejček,
Loic Hélouet,
* December 2009, 30 pages.

**FIMU-RS-2009-10.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Races in Message Sequence Charts may lead to a bad interpretation of

### Continuous-Time Stochastic Games with Time-Bounded Reachability

by *
Tomáš Brázdil,
Vojtěch Forejt,
Jan Krčál,
Jan Křetínský,
Antonín Kučera,
* A full version of the paper presented at FST&TCS 2009. October 2009, 46 pages.

**FIMU-RS-2009-09.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We study continuous-time stochastic games with

### Faster Algorithm for Mean-Payoff Games

by *
Jakub Chaloupka,
Luboš Brim,
* October 2009, 11 pages.

**FIMU-RS-2009-08.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We study some existing techniques for solving mean-payoff games (MPGs), improve them, and design a randomized algorithm for solving MPGs with currently the best expected complexity.

### On the Memory Consumption of Probabilistic Pushdown Automata

by *
Tomáš Brázdil,
Javier Esparza,
Stefan Kiefer,
* A full version of the paper presented at FSTTCS 2009 October 2009, 52 pages.

**FIMU-RS-2009-07.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We investigate the problem of evaluating memory consumption for systems modelled by probabilistic pushdown automata (pPDA). The space needed by a run of a pPDA is the maximal height reached by the stack during the run. The problem is motivated by the investigation of depth-first computations that play an important role for space-efficient schedulings of multithreaded programs.

### An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata

by *
Joakim Byg,
Kenneth Yrke Joergensen,
Jiří Srba,
* A full version of the paper presented at ICFEM`09. October 2009, 29 pages.

**FIMU-RS-2009-06.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Bounded timed-arc Petri nets with read-arcs were recently proven equivalent to net- works of timed automata, though the Petri net model cannot express urgent be- haviour and the described mutual translations are rather inefficient. We propose an extension of timed-arc Petri nets with invariants to enforce urgency and with transport arcs to generalise the read-arcs. We also describe a novel translation from the extended timed-arc Petri net model to networks of timed automata. The trans- lation is implemented in the tool TAPAAL and it uses UPPAAL as the verification engine. Our experiments confirm the efficiency of the translation and in some cases the translated models verify significantly faster than the native UPPAAL models do.

### CUDA accelerated LTL Model Checking

by *
Jiří Barnat,
Luboš Brim,
Milan Češka,
Tomáš Lamr,
* June 2009, 18 pages.

**FIMU-RS-2009-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Recent technological developments made available various many-core hardware platforms. For example,

### Quantitative Model Checking of Systems with Degradation (Full Paper).

by *
Jiří Barnat,
Ivana Černá,
Jana Tůmová,
* June 2009, 35 pages.

**FIMU-RS-2009-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

In this paper we describe a rather specialized quality of a system -- the degradation. We demonstrate systems that naturally incorporate degradation phenomenon and we show how these systems can be verified by adapting the standard automatabased approach to LTL model checking. We introduce Büchi Automata with Degradation Constraints (BADCs) to specify the desired properties of systems with degradation and we describe how these can be used for verification. A major obstacle in the verification process is that the synchronous product of the system and the Büchi

### Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete

by *
Nikola Beneš,
Jan Křetínský,
Kim Guldstrand Larsen,
Jiří Srba,
* A full version of the paper presented at conference ICTAC 2009. July 2009, 28 pages.

**FIMU-RS-2009-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Modal transition systems (MTS), a specification

### Verification Manager: Automating the Verification Process

by *
Radek Pelánek,
Václav Rosecký,
* March 2009, 17 pages.

**FIMU-RS-2009-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Although model checking is usually described as an automatic technique, the verification process with the use of model checker is far from being fully automatic. With the aim of automating the verification process, we elaborate

### Qualitative Reachability in Stochastic BPA Games

by *
Václav Brožek,
Tomáš Brázdil,
Antonín Kučera,
Jan Obdržálek,
* A full version of the paper presented at STACS 2009. May 2009, 37 pages.

**FIMU-RS-2009-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We consider a class of infinite-state stochastic games generated by stateless pushdown

### Verbalizing Visual Data for the Blind: Towards a More Complex Graphical Ontology

by *
Petr Peňáz,
* December 2008, 18 pages.

**FIMU-RS-2008-12.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The standard situational and picture descriptions, as produced by human professionals, are being compared to the existing proposals of a dialogue-based processing and graphical ontologies. The ontology proposed to build up verbal presentations of the graphics for sightless persons seems to be very suitable for unambiguous cases. In order to include more complex cases of the visual communication, the existing ontology should be extended. Constituent elements of the graphical ontology in a broader sense are:

- user`s perspective (user`s individual features, where the user is coming from to observe the picture, what he was doing before and what he is doing now while observing it),
- intentional perspective of the author of the picture (picture encoding key),
- functional perspective concerning the graphics (framework encoding key, relationship between the pictures in the same document, or in other documents related).

- remains partially unchanged even in the new context,
- needs reassessment, as to the rest (due to new ties and interpretation).

### Virtual Scene Designed as a Software Component

by *
Radek Oslejšek,
* A full version of the paper presented at WSCG 2008 December 2008, 17 pages.

**FIMU-RS-2008-11.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Graphics systems use many advanced techniques that enable to model and visualize a virtual scene with varying level of realism. Unfortunately, the huge collection of existing rendering algorithms significantly differ in the way how a virtual scene is processed. Concrete implementations therefore usually lead to monolithic solutions. In this paper we present a component-based virtual scene with unified interface exploitable by many rendering strategies. Moreover, proposed approach does not dictate internal implementation of the scene. One implementation can be therefore reused by many rendering algorithms and, vice versa, the scene can be easily replaced by another implementation, even at runtime.

### Detection and Annotation of Graphical Objects in Raster Images within the GATE Project

by *
Ivan Kopeček,
Radek Oslejšek,
Jaromír Plhák,
Fedor Tiršel,
* December 2008, 16 pages.

**FIMU-RS-2008-10.**
Available as *Postscript*,
**PDF**.

#### Abstract:

This report presents a brief outline of the GATE (= Graphics Accessible to Everyone) project architecture and an analysis of some problems and approaches connected to the detection and annotation of graphical objects in raster images. It also mentions some experiments concerning the object detection and annotation. Some examples and illustrations are presented as well.

### Discounted Properties of Probabilistic Pushdown Automata

by *
Tomáš Brázdil,
Václav Brožek,
Jan Holeček,
Antonín Kučera,
* A full version of the paper presented at LPAR 2008 September 2008, 31 pages.

**FIMU-RS-2008-08.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We show that several basic discounted properties of probabilistic

### Partial Order Reduction for State/Event LTL

by *
Nikola Beneš,
Luboš Brim,
Ivana Černá,
Jiří Sochor,
Pavlína Vařeková,
Barbora Zimmerová,
* July 2008, 21 pages.

**FIMU-RS-2008-07.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL incorporates both states and events to express important properties of component-based software systems.

### Model Checking of Control-User Component-Based Parametrised Systems

by *
Pavlína Vařeková,
Ivana Černá,
* A full version of the paper presented at conference CBSE 2008. July 2008, 27 pages.

**FIMU-RS-2008-06.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Many real component-based systems, so called Control-User systems, are composed of a stable part (control component) and a number of dynamic components of the same type (user components). Models of these systems are parametrised by the number of user components and thus potentially infinite. Model checking techniques can be used to verify only specific instances of the systems. This paper presents an

### Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives

by *
Tomáš Brázdil,
Vojtěch Forejt,
Antonín Kučera,
* A full version of the paper presented at ICALP 2008. December 2008, 48 pages.

**FIMU-RS-2008-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We show that controller synthesis and verification problems for

### Distributed System for Discovering Similar Documents

by *
Jan Kasprzak,
Michal Brandejs,
Miroslav Křipac,
Pavel Šmerk,
* A full version of the paper presented at the ICEIS 2008 converence (www.iceis.org). July 2008, 14 pages.

**FIMU-RS-2008-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

One of the drawbacks of e-learning methods such as Web-based submission

### The Satisfiability Problem for Probabilistic CTL

by *
Tomáš Brázdil,
Vojtěch Forejt,
Jan Křetínský,
Antonín Kučera,
* A full version of the paper presented at LICS 2008. June 2008, 34 pages.

**FIMU-RS-2008-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We study the satisfiability problem for qualitative PCTL

### Evaluation of State Caching and State Compression Techniques

by *
Radek Pelánek,
Václav Rosecký,
Jaroslav Šeděnka,
* February 2008, 19 pages.

**FIMU-RS-2008-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We study two techniques for reducing memory consumption of explicit model checking - state caching and state compression. In order to evaluate these techniques we review the literature, discuss trends in relevant research, and

### Estimating State Space Parameters

by *
Radek Pelánek,
Pavel Šimeček,
* January 2008, 21 pages.

**FIMU-RS-2008-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We introduce the problem of estimation of state space parameters, argue that it is an interesting and practically relevant problem, and study several simple estimation techniques. Particularly, we focus on estimation of the number of reachable states. We study techniques based on sampling of the state space and techniques that employ data mining techniques (classification trees, neural networks) over parameters of breadth-first search. We show that even through the studied techniques are not able to produce exact estimates, it is possible to obtain useful information about a state space by sampling and to use this information to automate the verification process.

### 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

### 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.

### 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

### 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

### 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

### 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.

### 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

### 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.

### 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

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
*highly undecidable*, even

### The Long Term Data Storage

by *
David C Hájíček,
Ivo Studenský,
* Introduction to Relevant Questions June 2005, 40 pages.

**FIMU-RS-2005-12.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Data storage, especially long-time data storage, is one of the biggest IT/ICT topics discussed in this field today. This document deals with basic classification of electronic data, highlights its specifics versus standard documents and contains overview of elementary requirements on its availability, integrity, confidentiality and storage duration, as well as accessibility time. Together with requirements, this document discusses cornerstones

### Reachability Relations and Sampled Semantics of Timed Systems

by *
Pavel Krčál,
Radek Pelánek,
* A full version of the paper presented at conference FSTTCS 2005. December 2005, 31 pages.

**FIMU-RS-2005-09.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Timed systems can be considered with two types of semantics -- dense time semantics and discrete time semantics. The most typical examples of both of them are real semantics and sampled semantics (i.e., discrete semantics with a fixed time step epsilon). In this work, we study different

### Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

by *
Javier Esparza,
Antonín Kučera,
Richard Mayr,
* A full version of the paper presented at LICS 2005. July 2005, 26 pages.

**FIMU-RS-2005-07.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Probabilistic pushdown automata (pPDA) have been identified as a natural model

### Refining the Undecidability Border of Weak Bisimilarity

by *
Mojmír Křetínský,
Vojtěch Řehák,
Jan Strejček,
* A full version of the paper presented at INFINITY 2005. August 2005, 20 pages.

**FIMU-RS-2005-06.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Weak bisimilarity is one of the most studied behavioural equivalences. This

### Tool for robust stochastic parsing using optimal maximum coverage

by *
Vladimír Kadlec,
Jean-Cédric Chappelier,
Martin Rajman,
* This report was also submitted as Technical Report No. 2004112 at Swiss Federal Institute of Technology (EPFL), Lausanne (Switzerland), October, 2004. April 2005, 16 pages.

**FIMU-RS-2005-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

This report presents a robust syntactic parser that is able to return

### Under-Approximation Generation using Partial Order Reduction

by *
Luboš Brim,
Ivana Černá,
Pavel Moravec,
Jiří Šimša,
* A full version of the paper submitted to conference CAV05 February 2005, 21 pages.

**FIMU-RS-2005-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We propose a new on-the-fly approach which combines partial order reduction with the under-approximation technique for falsification and verification of LTL-X properties. It uses sensitivity relation and modified ample conditions to generate a reduced state space that is not fully stutter equivalent to the original one and it checks the desired property using representatives. Widening of under-approximations is fully automatic and does not rely on any supporting mechanisms like theorem-provers or SAT solvers.

### On-the-fly State Space Reductions

by *
Radek Pelánek,
* February 2005, 22 pages.

**FIMU-RS-2005-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We present an overview of equivalences of finite state structures and discuss methods for computing reduced structures on-the-fly. We evaluate merits of these reductions on a large set of model checking case studies. It turns out that the achieved reduction can be significant, but that it is not so ``drastic" as sometimes claimed in the literature. We also propose some new reduction methods.

### Haptically Driven Travelling Through Conformational Space

by *
Igor Peterlík,
Aleš Křenek,
* This report is an extended version of a~paper accepted for presentation at the First Joint Eurohaptics Conference and Symposium on Haptic Interfaces for Virtual Environment and Teleoperator Systems, Pisa, Italy, 2005. January 2005, 22 pages.

**FIMU-RS-2005-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

After reviewing our generic framework of building haptic interactive models of environments which are computationally very expensive (so that their simulation cannot be used directly) we describe in detail the deployment of the framework in modelling conformational behaviour of flexible molecules. We conclude with description of first practical results which prove correctness of our approach, and shift the whole research towards more realistic applications.

### On the Decidability of Temporal Properties of Probabilistic Pushdown Automata

by *
Tomáš Brázdil,
Antonín Kučera,
Oldřich Stražovský,
* A full version of the paper presented at STACS 2005. February 2005, 33 pages.

**FIMU-RS-2005-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We consider qualitative and quantitative model-checking problems

### VCD: A Visual Formalism for Specification of Heterogeneous Software Architectures

by *
David Šafránek,
Jiří Šimša,
* A full version of SOFSEM 2005 paper. December 2004, 25 pages.

**FIMU-RS-2004-11.**
Available as *Postscript*,
**PDF**.

#### Abstract:

A visual formalism called *Visual Coordination Diagrams* (VCD)

### Characteristic Patterns for LTL

by *
Antonín Kučera,
Jan Strejček,
* A full version of the paper presented at Sofsem 2005. December 2004, 22 pages.

**FIMU-RS-2004-10.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We give a new characterization of those languages that are definable

### Accepting Predecessors are Better than Back Edges in Distributed LTL Model Checking

by *
Luboš Brim,
Ivana Černá,
Pavel Moravec,
Jiří Šimša,
* A full version of the paper accepted to the conference FMCAD 2004. November 2004, 22 pages.

**FIMU-RS-2004-09.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations communicating via MPI. The detection of accepting cycles is based on computing maximal accepting predecessors and the subsequent decomposition of the graph into independent predecessor subgraphs induced by maximal accepting predecessors. Several optimizations of the basic algorithm are presented and the influence of the ordering on the algorithm performance is discussed. Experimental implementation of the algorithm shows promising results.

### Deeper Connections between LTL and Alternating Automata

by *
Radek Pelánek,
Jan Strejček,
* September 2004, 26 pages.

**FIMU-RS-2004-08.**
Available as *Postscript*,
**PDF**.

#### Abstract:

It is known that Linear Temporal Logic (LTL) has the same expressive power as alternating 1-weak automata (A1W automata, also called alternating linear automata or very weak alternating automata). A translation of LTL formulae

### Distributed Memory LTL Model Checking Based on Breadth First Search

by *
Jiří Barnat,
Luboš Brim,
Jakub Chaloupka,
* September 2004, 57 pages.

**FIMU-RS-2004-07.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We propose a parallel distributed memory on-the-fly algorithm for enumerative LTL model checking. The algorithm is designed for network of workstations communicating via MPI. The detection of cycles (faulty runs) effectively employs the so called back-level edges. In particular, a parallel level synchronized breadth first search of the graph is performed to discover all back-level edges and for each level the back-level edges are checked in parallel by a nested search procedure to confirm or refute the presence of a cycle. Several optimizations of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed. Experimental evaluation of the algorithm is presented.

### Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems

by *
Tomáš Brázdil,
Antonín Kučera,
Oldřich Stražovský,
* A full version of the paper presented at CONCUR`04. September 2004, 26 pages.

**FIMU-RS-2004-06.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We prove that probabilistic bisimilarity is decidable over

### A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications

by *
Antonín Kučera,
Philippe Schnoebelen,
* A full version of the paper presented at CONCUR`04. June 2004, 32 pages.

**FIMU-RS-2004-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We introduce a generic family of behavioral relations for which the

### An Effective Characterization of Properties Definable by LTL Formulae with a Bounded Nesting Depth of the Next-Time Operator

by *
Antonín Kučera,
Jan Strejček,
* May 2004, 11 pages.

**FIMU-RS-2004-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

It is known that an LTL property is expressible by an LTL formula

### Model Checking Probabilistic Pushdown Automata

by *
Javier Esparza,
Antonín Kučera,
Richard Mayr,
* A full version of the paper presented at LICS`04. July 2004, 34 pages.

**FIMU-RS-2004-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We consider the model checking problem for probabilistic pushdown

### Application-Level Firewall Protection Profile for High Robustness Environments-Initial Considerations

by *
Mark Kelly,
Václav Matyáš,
Ahmed Patel,
* April 2004, 43 pages.

**FIMU-RS-2004-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Firewalls act as access control policy mediators between networks.

### A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata

by *
Antonín Kučera,
Richard Mayr,
* A full version of the paper presented at IFIP TCS 2004. April 2004, 38 pages.

**FIMU-RS-2004-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We propose a generic method for deciding semantic equivalences

### Object with Roles and VREcko system

by *
Lubomír Markovič,
* September 2003, 17 pages.

**FIMU-RS-2003-06.**
Available as *Postscript*,
**PDF**.

#### Abstract:

A model based on objects with roles concept is presented. It provides

### Process Rewrite Systems with Weak Finite-State Unit

by *
Mojmír Křetínský,
Vojtěch Řehák,
Jan Strejček,
* This is a full version of the paper presented at INFINITY`03. September 2003, 23 pages.

**FIMU-RS-2003-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Various classes of infinite-state processes are often specified by rewrite

### Parallel Algorithms for Detection of Negative Cycles

by *
Luboš Brim,
Ivana Černá,
Lukáš Hejtmánek,
* This is a full version of the paper presented at PARCO 2003. July 2003, 14 pages.

**FIMU-RS-2003-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Several new parallel algorithms for the single source shortest paths

### Relating Hierarchy of Linear Temporal Properties to Model Checking

by *
Ivana Černá,
Radek Pelánek,
* April 2003, 18 pages.

**FIMU-RS-2003-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The hierarchy of properties as overviewed by Manna and Pnueli relates language,

### Linear Binary Space Partitions and Hierarchy of Object Classes

by *
Petr Tobola,
Karel Nechvíle,
* April 2003, 21 pages.

**FIMU-RS-2003-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We consider the problem of constructing binary space partitions for the

### Modelling Dialogue Systems by Finite Automata

by *
Ivan Kopeček,
Libor Škarvada,
* March 2003, 13 pages.

**FIMU-RS-2003-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Based on finite state formalization, this paper deals with

### Distributed Explicit Fair Cycle Detection: Set Based Approach

by *
Ivana Černá,
Radek Pelánek,
* December 2002, 24 pages.

**FIMU-RS-2002-09.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The fair cycle detection problem is at the heart of both LTL and fair

### Using Assumptions to Distribute CTL Model Checking

by *
Luboš Brim,
Jitka Crhová,
Karen Yorav,
* This is a full version of the paper presented at PDMC`02. October 2002, 22 pages.

**FIMU-RS-2002-08.**
Available as *Postscript*,
**PDF**.

#### Abstract:

In this work we discuss the problem of performing distributed CTL model

### Improvements in a Dialogue Interface for Library System

by *
Luděk Bártek,
* October 2002, 6 pages.

**FIMU-RS-2002-07.**
Available as *Postscript*,
**PDF**.

#### Abstract:

This article describes methods and algorithms used to improve the

### Trustworthiness of Signed Data

by *
Petr Švéda,
* September 2002, 13 pages.

**FIMU-RS-2002-06.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Use of digital signatures is not as straightforward as one would like to see it. We have to be aware of the fact that computers sign all electronic documents on behalf of humans and only few computers can be considered as fully trustworthy. Visual representation of file formats can be dramatically changed by settings of a viewer or a text processor. Users cannot be absolutely sure that they sign only the data visible on their computer screen. Proprietary signature solutions are not fully compatible as there are no standards.

### Proceedings of Tools Day

by *
Ivana Černá,
* August 2002, 105 pages.

**FIMU-RS-2002-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

This volume contains proceedings of

### Pre-Proceedings of INFINITY 2002

by *
Antonín Kučera,
Richard Mayr,
* August 2002, 153 pages.

**FIMU-RS-2002-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

This volume contains pre-proceedings of 4th International

### The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL

by *
Antonín Kučera,
Jan Strejček,
* A full version of the paper presented at CSL`02. July 2002, 24 pages.

**FIMU-RS-2002-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

It is known that LTL formulae without the `next` operator
*stutter-equivalence* of

### Why is Simulation Harder Than Bisimulation?

by *
Antonín Kučera,
Richard Mayr,
* A full version of the paper presented at CONCUR`02 June 2002, 26 pages.

**FIMU-RS-2002-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Why is deciding simulation preorder (and simulation equivalence)

### On the Complexity of Semantic Equivalences for Pushdown Automata and BPA

by *
Antonín Kučera,
Richard Mayr,
* A full version of the paper presented at MFCS`02. May 2002, 32 pages.

**FIMU-RS-2002-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We study the complexity of comparing pushdown automata (PDA) and context-free

### How to Employ Reverse Search in Distributed Single Source Shortest Paths

by *
Luboš Brim,
Ivana Černá,
Pavel Krčál,
Radek Pelánek,
* This is a full version of the paper presented at SOFSEM 2001. November 2001, 22 pages.

**FIMU-RS-2001-09.**
Available as *Postscript*,
**PDF**.

#### Abstract:

A distributed algorithm for the single-source shortest path problem for directed graphs with arbitrary edge lengths is proposed. The new algorithm is based on relaxations and uses reverse search for inspecting edges and thus avoids using any additional data structures. At the same time the algorithm uses a novel way to recognize a reachable negative-length cycle in the graph which facilitates the scalability of the algorithm.

### Proceedings of the Third Learning Language in Logic Workshop

by *
Luboš Popelínský,
Miloslav Nepil,
* September 2001, 66 pages.

**FIMU-RS-2001-08.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The 3rd Learning Language in Logic (LLL) workshop held in August 8-9 in Strasbourg was the follow-up of the previous LLL workshops held in 1999 in Bled, Slovenia, and in 2000 in Lisboa, Portugal. The LLL workshop took place as a joint workshop of ILP`2001 conference. The program of the workshop split into two parts. Work-in-progress papers presented in Aug 8 afternoon are contained in this report.

### Control of the Hypertext System Audis Using the Dialogue

by *
Pavel Gaura,
* September 2001, 6 pages.

**FIMU-RS-2001-07.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The brief description of the blind user oriented hypertext system AUDIS and the principals of the dialogue approach to the system control are described in the paper. The emphasis is placed on the improvements to the control of the system using the dialogues. AUDIS is developed primarily as a support that would help visually impaired students to study various materials.

### A Comparison of Algorithms for Normed BPA Processes -- An Experimental Performance Evaluation

by *
Aleš Borek,
* September 2001, 13 pages.

**FIMU-RS-2001-06.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Three algorithms for deciding bisimilarity of normed BPA processes (two using bisimulation base and one using tableau) are evaluated. The evaluation is based on experimental results and some weak and strong points of algorithms with regard to practical use are being shown.

### Data Structures for Spatial Data Mining

by *
Petr Kuba,
* September 2001, 22 pages.

**FIMU-RS-2001-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

This report deals with spatial data structures for indexing and with their usability for knowledge discovery in spatial data. Huge amount of data processed in spatial data mining (or in data mining generally) requires using some indexing structures to speed up the mining process. Typical data types and operations used in geographic information systems are described in this paper. Then basic spatial data mining tasks and some spatial data mining systems are introduced. Finally, indexing spatial structures for both vector and metric spaces are described and structures used in some spatial data mining systems are presented.

### Dialogue Interfaces for Library Systems

by *
Pavel Cenek,
* June 2001, 15 pages.

**FIMU-RS-2001-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Basic principles and structure of a dialogue interface are introduced in the paper. Then features specific for library systems are described. Next part deals with the question how to use these features for the design of a dialogue interface for library systems. Finally some specific library systems are introduced and possibilities how to design a dialogue interface for them is discussed.

### Automatic Processing of Czech Inflectional and Derivative Morphology

by *
Radek Sedláček,
Pavel Smrž,
* This is an extended version of the paper which is going to be published in the Proceedings of the Fourth International Conference TSD 2001, LNAI 1902, Pilsen, Czech Republic, September 2001, Springer-Verlag. June 2001, 12 pages.

**FIMU-RS-2001-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

This paper deals with the effective implementation of the new Czech morphological analyser ajka which is based on the algorithmic description of the Czech formal morphology. First, we present two most important word-forming processes in Czech --- inflection and derivation. A brief description of the data structures used for storing morphological information as well as a discussion of the efficient storage of lexical items (stem bases of Czech words) is included too. Then, we describe the morphological analysis algorithm in details and finally, we bring some interesting features of the designed and implemented system ajka together with current statistic data.

### Finding Semantically Related Words in Large Corpora

by *
Pavel Smrž,
Pavel Rychlý,
* Slightly modified version of the paper published in the Proceedings of TSD 2001, Pilsen, Czech Republic. June 2001, 9 pages.

**FIMU-RS-2001-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The paper deals with the linguistic problem of fully automatic grouping of semantically related words. We discuss the measures of semantic relatedness of basic word forms and describe the treatment of collocations. Next we present the procedure of hierarchical clustering of a very large number of semantically related words and give examples of the resulting partitioning of data in the form of dendrogram. Finally we show a form of the output presentation that facilitates the inspection of the resulting word clusters.

### Distributed Shortest Paths for Directed Graphs with Negative Edge Lengths

by *
Luboš Brim,
Ivana Černá,
Pavel Krčál,
Radek Pelánek,
* This is a full version of the paper presented at FST&TCS 2001. May 2001, 19 pages.

**FIMU-RS-2001-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

A distributed algorithm for single source shortest path

### Bounding Volume Hierarchy Analysis (Case Study)

by *
Radek Oslejšek,
* December 2000, 12 pages.

**FIMU-RS-2000-13.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Bounding Volume Hierarchies are very popular structures for objects storage of virtual scenes. In this article various OO models of BVH are analysed and described using UML. The first part compares bounding volume hierarchy with virtual scene representation from point of view of their management. The second part is focused on relationships between class hierarchies of scene graph and BVH.

### Constrained Rewrite Transition Systems

by *
Jan Strejček,
* December 2000, 30 pages.

**FIMU-RS-2000-12.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We extend broadly studied rewrite transition systems with a mechanism for computing with partial information in the form similar to that one used in Concurrent Constraint Programming (CCP). Two new classes of transition systems (fcBPA and fcBPP) are introduced as this extension changes expressibility power of rewrite transition systems corresponding to BPA and BPP. The power of rewrite systems corresponding to other classes (FSA, PDA, PPDA, and PN) remains unchanged. The new classes are inserted to the hierarchy of standard process classes presented by Moller [Mol96].

### High Performance Computing in JAVA -- Fact or Fiction?

by *
Václav Dvořák,
Lubomír Markovič,
* December 2000, 20 pages.

**FIMU-RS-2000-11.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The intent of this article is to give an overview of possibilities for building distributed/parallel applications in the JAVA language and to judge the suitability of some of them for high performance computing. In the first part different approaches and libraries are presented and in the second part of this article, RMI, HORB and CORBA libraries are compared to direct communication over sockets. Gauss-Jordan algorithm for computation a system of linear equations was used to test these libraries.

### Distributed LTL Model-Checking in SPIN

by *
Jiří Barnat,
Luboš Brim,
Jitka Stříbrná,
* December 2000, 19 pages.

**FIMU-RS-2000-10.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Distributed version of the SPIN model checker has not been extended to allow distributed model-checking of LTL formulas. This paper explores the possibility of performing nested depth first search algorithm in distributed SPIN. A distributed version of the algorithm is presented, and its complexity is discussed.

### Some Remarks on Weak Bisimilarity of BPA-Processes

by *
Ivana Černá,
Jitka Stříbrná,
* December 2000, 26 pages.

**FIMU-RS-2000-09.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The purpose of this work is to examine the decidability problem of weak bisimilarity for BPA-processes. It has been known that strong bisimilarity, which may be considered a special case of weak bisimilarity, where the internal (silent) action tau is treated equally to observable actions, is decidable for BPA-processes. For strong bisimilarity, these processes are finitely branching and so for two non-bisimilar processes there exists a level n that distinguishes the two processes. Additionally, from the decidability of whether two processes are equivalent at a given level n, semidecidability of strong non-bisimilarity directly follows. We examine the following two closely related approaches to semidecidability of strong equivalence:

- construction of a (finite) bisimulation or expansion tree,
- construction of a finite Caucal base.

### Biometric Authentication Systems

by *
Zdeněk Říha,
Václav Matyáš,
* November 2000, 44 pages.

**FIMU-RS-2000-08.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Biometrics is the name of a security hype these days. Although biometrics are not completely new, they are becoming more and more popular nowadays. The first part of the technical report explains the principle of biometric systems and describes various biometric techniques. In the second part security issues of biometric systems are discussed.

### On Disambiguation in Czech Corpora

by *
Luboš Popelínský,
Tomáš Pavelek,
Tomáš Ptáčník,
* October 2000, 26 pages.

**FIMU-RS-2000-07.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Lemma disambiguation means finding the basic word form, typically nominative singular for nouns or infinitive for verbs. We developed a multistrategy method for lemma disambiguation of unannotated text. The method is based on a combination of inductive logic programming and instance-based learning. We present results of the most important subtasks of lemma disambiguation for Czech language. Although no expert knowledge on Czech grammar has been used the accuracy reaches 90% with a fraction of words remaining ambiguous. We also display first results of tag disambiguation.

### Ways to the High-Resolution Cytometry Network

by *
Pavel Matula,
Petr Matula,
Michal Kozubek,
* October 2000, 14 pages.

**FIMU-RS-2000-06.**
Available as *Postscript*,
**PDF**.

#### Abstract:

This paper concerns fundamental tasks solved in the Laboratory of High-Resolution Cytometry in Brno and present and planned techniques for solving these tasks. The current research is aimed at 2-D and 3-D analysis of FISH-stained interphase nuclei, metaphase spreads and tissues. Both basic research and clinical applications are performed. The research is mostly performed using high-resolution cytometry technique developed in our laboratory. Two instruments capable of automated image acquisition from microscope slides have been developed. The acquired images are analysed by computer. The present image analysis system has some drawbacks. Therefore, development of a new system has started. The new system will be based on the client-server architecture and is called High-Resolution Cytometry Network.

### On Simulation-Checking with Sequential Systems

by *
Antonín Kučera,
* This is a full version of the paper accepted for ASIAN 2000. September 2000, 34 pages.

**FIMU-RS-2000-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We present new complexity results for simulation-checking and model-checking with infinite-state systems generated by pushdown automata and their proper subclasses of one-counter automata and one-counter nets (one-counter nets are "weak" one-counter automata computationally equivalent to Petri nets with at most one unbounded place).

As for simulation-checking, we show the following: a) simulation equivalence between pushdown processes and finite-state processes is EXPTIME-complete; b) simulation equivalence between processes of one-counter automata and finite-state processes is coNP-hard; c) simulation equivalence between processes of one-counter nets and finite-state processes is in P (to the best of our knowledge, it is the first (and rather tight) polynomiality result for simulation with infinite-state processes).

As for model-checking, we prove that a) the problem of simulation-checking between processes of pushdown automata (or one-counter automata, or one-counter nets) and finite-state processes are polynomially reducible to the model-checking problem with a fixed formula F = nu X. [z]<z> X of the modal mu-calculus. Consequently, model-checking with F is EXPTIME-complete for pushdown processes and coNP-hard for processes of one-counter automata; b) model-checking with a fixed formula <>[a]<>[b]ff of the logic EF (a simple fragment of CTL) is NP-hard for processes of OC nets, and model-checking with another fixed formula []<a>[]<b>tt of EF is coNP-hard. Consequently, model-checking with any temporal logic which can express these simple formulae is computationally hard even for the (very simple) sequential processes of OC-nets.

### Linear BSP Trees for Sets of Hyperrectangles with Low Directional Density

by *
Petr Tobola,
Karel Nechvíle,
* September 2000, 27 pages.

**FIMU-RS-2000-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We consider the problem of constructing of binary space partitions (BSP) for a set S of n hyperrectangles in arbitrary dimensional space. If the set S fulfills the low directional density condition defined in this paper then the resultant BSP has O(n) size and it can be constructed in O(n log^2 n) time in R^3. The low directional density condition defines a new class of objects which we are able to construct a linear BSP for. The method is quite simple and it should be appropriate for practical implementation.

### Efficient Verification Algorithms for One-Counter Processes

by *
Antonín Kučera,
* This is a full version of the paper presented at ICALP 2000. March 2000, 24 pages.

**FIMU-RS-2000-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We study the problem of strong/weak bisimilarity between processes of one-counter automata and finite-state processes. We show that the problem of weak bisimilarity between processes of one-counter nets (which are "weak" one-counter automata) and finite-state processes is DP-hard (in particular, it means that the problem is both NP and co-NP hard). The same technique is used to demonstrate co-NP hardness of strong bisimilarity between processes of one-counter nets. Then we design an algorithm which decides weak bisimilarity between processes of one-counter automata and finite-state processes in time which is polynomial for most "practical" instances, giving a characterization of all hard instances as a byproduct. Moreover, we show how to efficiently compute a rather tight bound for the time which is needed to solve a given instance. Finally, we prove that the problem of strong bisimilarity between processes of one-counter automata and finite-state processes is in P.

### Logical Markup from RTF

by *
Michal Chocholáč,
* February 2000, 20 pages.

**FIMU-RS-2000-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The paper is an overview of ways how to get logical structure from documents created by proprietary word-processors and stored into an RTF file. It describes and evaluates all steps of conversion process from RTF to SGML/XML. One of the submitted ways is demonstrated on a simple example. All used tools exist and are publicly available.

### A Logical Viewpoint on Process-Algebraic Quotients

by *
Antonín Kučera,
Javier Esparza,
* This is a full and revised version of a paper which previously appeared in Proceedings of CSL`99. January 2000, 26 pages.

**FIMU-RS-2000-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We study the following problem: Given a transition system T and its quotient T/~ under an equivalence ~, which are the sets L, L` of Hennessy-Milner formulae such that: if f belongs to L and T satisfies f, then T/~ satisfies f; if f belongs to L` and T/~ satisfies f, then T satisfies f.

### Timetabling with Annotations

by *
Hana Rudová,
Luděk Matyska,
* December 1999, 17 pages.

**FIMU-RS-99-09.**
Available as *Postscript*,
**PDF**.

#### Abstract:

One of the peculiarities of university timetabling problems lies in their huge complexity and the easy transition between complex constrained system to an over-constrained one. The Faculty of Informatics timetabling problem represents very complex scheduling and resource allocation problem as individual timetable for every student has to be scheduled with respect to course pre-enrollment informations. Variables` annotations were proposed to define preferences of variables in constraints and they serve as a source for computing variable ordering in optimization problems where the search space is too large to be fully traversed and explored. Annotations suggest a route through this space which leads quickly to at least sub-optimal solutions. Annotations may even help to find preferred solutions first as they instantiate preferred values in the domain of variables as soon as possible.

### A Fully Abstract Semantics for a Version of Synchronous Concurrent Constraint Programming

by *
Jean-Marie Jacquet,
Luboš Brim,
David Gilbert,
Mojmír Křetínský,
* December 1999, 62 pages.

**FIMU-RS-99-08.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Concurrent constraint programming is classically based on asynchronous communication via a shared store. In previous work, we presented a new version of the ask and tell primitives which features synchronicity, our approach being based on the idea of telling new information just in the case that a concurrently running process is asking for it. We turn in this paper to a semantic study of this new framework, called Scc.

It is first shown to be different in nature from classical concurrent constraint programming and from CCS, a classical reference in traditional concurrency theory. This suggests the interest of new semantics for Scc. To that end, an operational semantics reporting the steps of the computations is presented. A denotational semantics is then proposed. It uses monotonic sequences of labelled pairs of input-output states, possibly containing gaps, and ending - according to the logic programming tradition - with marks reporting success or failure. This denotational semantics is proved to be correct with respect to the operational semantics as well as fully abstract.

### Linear BSP Tree in the Plane for Set of Segments with Low Directional Density

by *
Petr Tobola,
Karel Nechvíle,
* A full version of the paper which appeared in Proceedings WSCG`99. September 1999, 20 pages.

**FIMU-RS-99-07.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We introduce a new BSP tree construction method for set of segments in the plane. Our algorithm is able to create BSP tree of linear size in the time O(n log^3 n) for set of segments with low directional density (i.e. it holds for arbitrary segment s_i from such set, that a line created as extension of this segment doesn`t intersect too many other segments from the set in a near neighbourhood of s_i) and a directional constant delta belonging to this set.

### On Birkhoff`s Aesthetic Measure of Vases

by *
Tomáš Staudek,
* September 1999, 8 pages.

**FIMU-RS-99-06.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The report discusses contribution of Birkhoff`s aesthetic measure to formal aesthetic evaluation of regular geometrical objects, namely Chinese vases. Characteristics of aesthetic measure function are considered in order to verify correctness of such application and extended Birkhoff`s aesthetic measure is then introduced.

### Approximating Weak Bisimulation on Basic Process Algebra

by *
Jitka Stříbrná,
* This work has been presented at MFCS`99. September 1999, 18 pages.

**FIMU-RS-99-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The maximal strong and weak bisimulations on any class of processes can be obtained as the limits of decreasing chains of binary relations, approximants. In the case of strong bisimulation and Basic Process Algebras this chain has length at most omega which enables semidecidability of strong bisimilarity. We show that it is not so for weak bisimulation where the chain can grow much longer, and discuss the implications this has for the problem of (semi)decidability of weak bisimilarity.

### CED -- Program for Corpora Editing

by *
Marek Veber,
* September 1999, 9 pages.

**FIMU-RS-99-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The article is concerned with editing of corpora, tagged corpora in particular. It introduces a corpus editor (program ced) and a software library for work with corpora. The following functions are described: Journaling of changes, document editing, working with a list of localities in the course of making aggregate corrections, co-operating with a corpus manager, independence of the physical corpora`s data storage.

### Corpus-based Rules for Czech Verb Discontinuous Constituents

by *
Eva Žáčková,
Karel Pala,
* This is an adapted version of the paper accepted for printing in the Proceedings of TSD`99. August 1999, 6 pages.

**FIMU-RS-99-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

In this paper we present a method for extracting general structures of the verb groups from a tagged and fully disambiguated corpus and consecutive exploitation of these structures for the building a formal grammar in the Prolog DCG fashion. Our goal is to apply them as a rules for the analysis of the Czech verb groups in the non-disambiguated grammatically tagged Czech corpus texts. The problem of the recognition of verb discontinuous constituents in Czech is also approached and obtained statistical data are presented.

### Complexity Issues of the Pattern Equations in Idempotent Semigroups

by *
Ondřej Klíma,
Jiří Srba,
* August 1999, 14 pages.

**FIMU-RS-99-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

A pattern equation is a word equation of the form X=A where X is a sequence of variables and A is a sequence of constants. The problem whether X=A has a solution in a free idempotent semigroup (free band) is shown to be NP--complete.

### On the Pattern Equations

by *
Ivana Černá,
Ondřej Klíma,
Jiří Srba,
* This is a full version of the paper accepted to SOFSEM`99. July 1999, 11 pages.

**FIMU-RS-99-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Word equation in a special form X=A, where X is a sequence of variables and A is a sequence of constants, is considered. The problem whether X=A has a solution over a free monoid (PATTERN EQUATION problem) is shown to be NP--complete. It is also shown that disjunction of a special type equation systems and conjunction of the general ones can be eliminated. Finally, the case of stuttering equations where the word identity is read modulo xx=x is mentioned.

### Object-oriented Graphics Architectures for Global Illumination

by *
Jiří Sochor,
Radek Oslejšek,
* December 1998, 17 pages.

**FIMU-RS-98-08.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The paper presents several examples of object-oriented graphics architectures derived from OO Testbed for Global Illumination. A new architecture based on explorer-with-map paradigm is described and projected on serial HW architecture of Cohen&Demetrecsu.

### Certification

by *
Zdeněk Říha,
* December 1998, 43 pages.

**FIMU-RS-98-07.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Certifications are specific procedures which compare references with measurements that allow a party to bind an attribute to an unknown party. There are three main types of methods that have been proposed to deal with this concern: directory methods, based on Certification Authorities: X.509 (e.g. SSL, PKIX), referral methods, based on "introducers" of keys (e.g. PGP), and collaborative methods (e.g. SKIP). All of them are described in the report.

### MFCS`98 Workshop on Concurrency - Preproceedings

by *
Petr Jančar,
Mojmír Křetínský,
* Pre-proceedings of the MFCS`98 Workshop on Concurrency (the PS file is NOT provided, as it is too large (approx. 30MB); take pdf (3.5 MB) instead). July 1998, 209 pages.

**FIMU-RS-98-06.**
Available as *Postscript*,
**PDF**.

#### Abstract:

This volume contains the pre-proceedings of the MFCS`98 Workshop on Concurrency, which took place in Brno, Czech Republic, August 27-29, 1998, as a satellite event of the 23rd international symposium on Mathematical Foundations of Computer Science. It is composed of two invited papers delivered by Javier Esparza (Munich) and Faron Moller (Uppsala), and of 17 contributed papers selected out of 24 submissions. The revised (and full) version of the proceedings should appear as a volume of Electronic Notes in Theoretical Computer Science (Elsevier).

### Comparing the Classes BPA and BPA with Deadlocks

by *
Jiří Srba,
* This is a full version of the paper accepted to MFCS`98. June 1998, 36 pages.

**FIMU-RS-98-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The class of BPA (or context-free) processes has been intensively studied and bisimilarity and regularity appeared to be decidable. We extend these processes with a deadlocking state into BPA_delta systems. We show that the BPA_delta class is more expressive w.r.t. bisimulation equivalence but it remains language equivalent to BPA. We prove that bisimilarity and regularity remain decidable in the BPA_delta class. Finally we give a characterisation of those BPA_delta processes which can be equivalently (up to bisimilarity) described within the "pure" BPA syntax.

### Constraints with Variables` Annotations

by *
Hana Rudová,
* This is an extended version of the paper accepted for presentation at ECAI-98. May 1998, 14 pages.

**FIMU-RS-98-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Variables` annotations in over-constrained problems are proposed and described in order to express preferences for optimal solution selection using preferences on variables. The basic interpretation of variables` annotations is presented and correspondence with hierarchical CSP and possibilistic CSP is described. An algorithm for solving systems of constraints with variables` annotations using mappings to hierarchy is designed. The potential application areas are also mentioned.

### Programmed Learning & Hypertext

by *
Jaroslav Pelikán,
* May 1998, 6 pages.

**FIMU-RS-98-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The history of programmed learning and its main principles. The advantages and disadvantages of programmed learning and hypertext systems. The integration of programmed learning and hypertext. The proposal, structure and realization of an electronic textbook. The main advantages of such a textbook.

### Off-line Recognition of Cursive Handwritten Czech Text

by *
Pavel Smrž,
Štěpán Hrbáček,
Michal Martinásek,
* February 1998, 8 pages.

**FIMU-RS-98-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

In this paper a part of the system for recognising off-line cursive Czech text is presented. Recently, various systems for recognition of cursive English text has been developed, however, to our knowledge no method has been presented yet for Czech, a language rich in diacritic marks. This paper deals with preprocessing which is different for Czech and English handwritten texts. For finding the letter boundaries a method based on minimising a heuristic cost function has been used.

### The Architecture of the Blind User Oriented Hypertext AUDIS

by *
Ivan Kopeček,
* February 1998, 7 pages.

**FIMU-RS-98-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The architecture of the blind user oriented hypertext AUDIS developed at the Faculty of Informatics, Masaryk University Brno, is described in the paper. AUDIS is developed primarily as a support, which would help visually impaired students to study various materials. It can also serve as an Internet browser.

### DESAM - Approaches to Desambiguation

by *
Karel Pala,
Pavel Rychlý,
Pavel Smrž,
* December 1997, 12 pages.

**FIMU-RS-97-09.**
Available as *Postscript*,
**PDF**.

#### Abstract:

This paper deals with Czech desambiguated corpus DESAM. It is a tagged corpus which was manually desambiguated and can be used in various applications. We discuss the structure of the corpus, tools used for its managing, linguistic applications, and also possible use of machine learning techniques relying on the desambiguated data. Possible ways of developing procedures for complete automatic desambiguation are considered.

### Stepping Stones to an Information Society

by *
Jiří Zlatuška,
* A revised version of an invited talk presented at SOFSEM`97 conference. December 1997, 30 pages.

**FIMU-RS-97-08.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The information revolution is radically transforming many patterns along which society and enterprises have traditionally worked. These changes do not bring just minor technological improvements, but indeed a fundamental transformation of our industry-based society into an information-based one. The changes are most visible and documented within the business world, but the synergy between technological and social shifts does not stop there. In this paper we try to identify and summarize key trends and challenges which this development puts before us.

### PHC Format Description

by *
Pavel Frýda,
Ivan Kopeček,
* November 1997, 6 pages.

**FIMU-RS-97-07.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The paper contains the presentation of a data format for phonetic corpora called PHC format and proposal of library of utilities designed for manipulation with PHC format.

### Bisimulation Equivalence is Decidable for One-Counter Processes

by *
Petr Jančar,
* Accepted for presentation at the 24th International Colloquium on Automata, Languages, and Programming (ICALP`97). May 1997, 13 pages.

**FIMU-RS-97-06.**
Available as *Postscript*,
**PDF**.

#### Abstract:

It is shown that bisimulation equivalence is decidable for the processes generated by (nondeterministic) pushdown automata where the pushdown behaves like a counter, in fact. Also regularity, i.e. bisimulation equivalence with some finite-state process, is shown to be decidable for the mentioned processes.

### Navigation and Information System for Visually Impaired People

by *
Ivan Kopeček,
Pavel Smrž,
* May 1997, 7 pages.

**FIMU-RS-97-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Orientation is one of the most important problems of visually impaired people. The aim of this paper is to suggest a contribution to the solution of this problem using computer technology. The basic idea is the detection of motion and orientation using sensors and consequent position identification. The detected trajectory is compared with a map and is corrected by means of the algorithm described in the paper. Some problems concerning sensor detection of human motion are also discussed. Based on the determined position other relevant information is provided to the user of system (information describing the neighbourhood of the actual position, optimal way to the chosen destination, possible warnings).

### An Algorithm on Interpolating between Two Shapes of a Molecule

by *
Aleš Křenek,
* Accepted for the SCCG`97 in Bratislava. May 1997, 10 pages.

**FIMU-RS-97-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Conformational behaviour analysis produces a sequence of shapes of a molecule which are only the key points on the entire path. They differ from one another significantly and an interpolation is necessary to achieve a smooth visualization. However, standard interpolation techniques cannot be used. We introduce a hypothesis on the nature of the shape changes and derive an interpolation algorithm. Conditions required for proper function as well as some ideas how to overcome the algorithm`s drawbacks are presented.

### Towards Adjusting Informatics Education to Information Era

by *
Jozef Gruska,
Roland Vollmar,
* A slightly extended version of the invited paper for IFIP TC3 WG3.2 Workshop "Informatics as a discipline and in other disciplines: What is in common?" May 1997, 33 pages.

**FIMU-RS-97-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Since the very beginning of the modern computing era, the scientific and educational community in informatics has been in a continuous search for a proper philosophy, viewpoints, aims, contents, methods and tools. Advances in software, communication and hardware have played by that search the most influencing role, with theory advances having only secondary and declining impacts - in spite of the remarkable success of theory, quite well recognized by the community at large.

The recent developments and advances in computing, communication and informatization of the society point out strongly, that horizons of the field are much broader, and its impacts on the society are far larger than anticipated even by strong optimists. This brings new and strong impetus to reconsider again the aims, scope, contents and methods of education in informatics and in other areas.

In the paper we analyze: (a) needs to change education in informatics; (b) the current situation in informatics education; (c) a framework for a new approach; (d) steps to be done; (3) two case studies.

### Bisimilarity of Processes with Finite-state Systems

by *
Petr Jančar,
Antonín Kučera,
* These results will be presented at INFINITY`97 workshop. May 1997, 19 pages.

**FIMU-RS-97-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We describe a general method for deciding bisimilarity for pairs of processes where one process has finitely many states. We apply this method to pushdown processes and to PA processes. We also demonstrate that the mentioned problem is undecidable for `state-extended` PA processes.

### Lower Bound of Distance in 3D

by *
Petr Konečný,
Karel Zikan,
* This article is going to be presented at WSCG`97 in Pilsen. January 1997, 16 pages.

**FIMU-RS-97-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The term "collision detection" refers to the task of determining whether, in a given set of objects, any two intersect. If they do, then common collision detection systems return either one such pair or all such pairs. The term "proximity computation" refers to a more general task where we determine the nearest or the "most overlapping" pairs of objects. In the article, we present a new method to rapidly compute lower bounds of distances. The lower bound decreases the complexity of collision detection (or proximity computation) by computing "candidates" of collision, i.e., pairs of objects that might intersect. It estimates the lower bound of their distance and rejects pairs that are too far from each other to collide.

### How to Parallelize Sequential Processes

by *
Antonín Kučera,
* Accepted to the 8th International Conference on Concurrency Theory (CONCUR`97). December 1996, 24 pages.

**FIMU-RS-96-05.**
Available as *Postscript*,
**PDF**.

#### Abstract:

A process is prime if it cannot be decomposed into a parallel product of nontrivial processes. We characterize all non-prime normed BPA processes together with their decompositions in terms of normal forms which are designed in this paper. Then we show that it is decidable whether a given normed BPA process is prime and if not, its decomposition can be effectively constructed. This brings other positive decidability results. Finally, we prove that bisimilarity is decidable in a large subclass of normed PA processes.

### Word Hy-phen-a-tion by Neural Networks

by *
Pavel Smrž,
Petr Sojka,
* August 1996, 10 pages.

**FIMU-RS-96-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We are discussing our experiments we made when learning feedforward neural network to find possible hyphenation points in all words of given language. Neural networks show to be a good device for solving this difficult problem. The structure of the multilayer neural network used is given, together with a discussion about training sets, influence of input coding and results of experiments done for the Czech language. We end up with pros and cons of our approach tested - hybrid architecture suitable for a multilingual system.

### Comparing Expressibility of Normed BPA and Normed BPP Processes

by *
Ivana Černá,
Mojmír Křetínský,
Antonín Kučera,
* This is a full version of the paper which is to be presented at CSL`96. June 1996, 28 pages.

**FIMU-RS-96-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We compare the classes of behaviours (transition systems) which can be generated by normed BPA_{\tau} and normed BPP_{\tau} processes. We exactly classify the intersection of these two classes, i.e., the class of transition systems which can be equivalently (up to bisimilarity) described by the syntax of normed BPA_{\tau} and normed BPP_{\tau} processes. We provide such a characterisation for classes of normed BPA and normed BPP processes as well.

Next we show that it is decidable in polynomial time whether for a given normed BPA_{\tau} (or BPP_{\tau} respectively) process X there is some (unspecified) normed BPP_{\tau} (or BPA_{\tau} respectively) process X` such that X is bisimilar to X`. Moreover, if the answer is positive then our algorithms also construct the process X`. Simplified versions of the algorithms mentioned above for normed BPA and normed BPP are given too.

As an immediate (but important) consequence we also obtain the decidability of bisimilarity in the union of normed BPA_{\tau} and normed BPP_{\tau} processes.

### Regularity is Decidable for Normed PA Processes in Polynomial Time

by *
Antonín Kučera,
* This paper is going to be presented at FST&TCS`96 conference, LNCS 1180, Springer-Verlag. February 1996, 17 pages.

**FIMU-RS-96-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

A process X is regular if it is bisimilar to a process X` with finitely many states. We prove that regularity of normed PA processes is decidable and we present a practically usable polynomial-time algorithm. Moreover, if the tested normed PA process X is regular then the process X` can be effectively constructed. It implies decidability of bisimulation equivalence for any pair of processes such that one process is a normed PA process and the other process has finitely many states.

### Notes on Compound Word Hyphenation in TeX

by *
Petr Sojka,
* August 1995, 12 pages.

**FIMU-RS-95-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

The problems of the automatic compound word and discretionary hyphenation in TeX are discussed. These hyphenation points have to be marked manually in the TeX source file so far. Several methods how to tackle with these problems are observed. The results obtained from experiments with German wordlist are discussed.

### WiM: A Study on the Top-Down ILP Program

by *
Luboš Popelínský,
* August 1995, 18 pages.

**FIMU-RS-95-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

In the area of the inductive synthesis of logic programs it is the small number of examples which is crucial. We show that the classical MIS-like architecture can be adapted using techniques described in ILP literature so that we reach very good results if to compare with other ILP systems. We describe the top-down ILP program WiM and the results obtained through it. WiM needs from 2 to 4 examples for most of the ILP benchmark predicates. Even though it is interactive, not more that one membership query is enough to receive the correct target program. WiM has higher efficiency of learning as well as smaller dependency on the quality of the example set in comparison to some of ILP programs. The quality of learning has been tested both on good examples and on randomly chosen example sets.

### Smoothing Integral Transforms for Molecular Mechanics Force Fields

by *
Petr Mejzlík,
* April 1995, 16 pages.

**FIMU-RS-95-02.**
Available as *Postscript*,
**PDF**.

#### Abstract:

A new class of methods, based on a special type of smoothing integral transforms, has recently been developed to solve problems concerning conformational optimization in computational chemistry. These methods do not apply an optimization procedure directly to the original potential function, but tracs low minima through a sequence of transformed potential functions with decreasing level of smoothing. This work studies the integral smoothing transforms in general and applies the theory to a class of potential functions which are typically used by molecular mechanics and related methods for computations with large molecules. It also addresses the problems of computational complexity of the transforms and their approximations.

### On Biases in Inductive Data Engineering

by *
Jana Kuklová,
Luboš Popelínský,
* March 1995, 7 pages.

**FIMU-RS-95-01.**
Available as *Postscript*,
**PDF**.

#### Abstract:

An utilization of inductive reasoning [Flene94] in the database area looks promising [Agar93], [DeRae92], [DeRae93], [Flach93], [Kivi92], [Savnik93], [Manni93]. Inductive data engineering, as introduced in [Flach93], means a process of restructuring database by means of induction.

In our work we focus on exploitation of inductive logic programming for database schema design [Roll92]. We propose modifications of INDEX, described in [Flach93], namely new biases for narrowing search space, as well as stopping criterion

In this article the case of single relation is described.

Responsible contact: unixfimunicz