You are here: Faculty of Informatics » Research and Development » Technical Reports » Abstracts by Year

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 scenarios. Secrecy amplification protocols provide a significant increase in the number of secure communication links by re-establishing new keys via different communication paths. Our paper shows that so far research in the area of secrecy amplification protocols for wireless sensor networks has been based on rather simplified foundations with respect to attacker models. The attacker does not behave randomly and different attacker capabilities and behaviour have to be considered. We provide means to experimental work with parametrisable attacker capabilities and behaviour in realistic simulations, and evaluate the impact of the realistic attacker properties on the performance of major amplification protocols. We also show which secrecy amplification protocols perform best in different attacker settings and help to select a protocol that exhibits good results in a prevalent number of inspected scenarios. This is the extended version of our paper that is to be presented at 15th International Conference on Cryptology and Network Security (CANS 16) in Milan, Italy, November 14-16, 2016.

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 the anonymity set of users of anonymous mailers or operators of linked Tor hidden services, to quickly detect keys from the same vulnerable library or to verify a claim of use of secure hardware by a remote party. The classification of the key origins of more than 10 million RSA-based IPv4 TLS keys and 1.4 million PGP keys also provides an independent estimation of the libraries that are most commonly used to generate the keys found on the Internet. Our broad inspection provides a sanity check and deep insight regarding which of the recommendations for RSA key pair generation are followed in practice, including closed-source libraries and smartcards. The inspection was not limited only to public part of a RSA keypair – the properties of private key were inspected including factorization of p-1 and p+1 for large number of 512-bit RSA keys followed by discussion of relevant factorization attacks.

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 stochastic processes, recently these systems have also been regarded as transformers of probabilities. In this paper, we give a natural definition of strong bisimulation for probabilistic systems corresponding to this view that treats probability distributions as first-class citizens. Our definition applies in the same way to discrete systems as well as to systems with uncountable state and action spaces. Several examples demonstrate that our definition refines the understanding of behavioural equivalences of probabilistic systems. In particular, it solves a longstanding open problem concerning the representation of memoryless continuous time by memoryfull continuous time. Finally, we give algorithms for computing this bisimulation not only for finite but also for classes of uncountably infinite systems.

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) project is intended to lead to a flexible and adaptable MT system, based on a language-independent method, whose principles ensure easy portability to new language pairs. This report describes the Phrase Model Generator (PMG) of the PRESEMT system. PMG supports two distinct operations. The first operation processes the output of Phrase Aligner Module to train a phrasing model for the SL of the specified language pair. The second operation makes use of the phrasing model established to parse any SL text input and split it into phrases in preparation for the translation process.

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) project is intended to lead to a flexible and adaptable MT system, based on a language-independent method, whose principles ensure easy portability to new language pairs. This report describes the Phrase aligner module (PAM) of the PRESEMT system. PAM processes the bilingual corpora by performing text alignment at word and phrase level within a language pair. It operates in offline manner, processing the set of parallel sentences so as to determine how phrases are transformed from SL to TL.

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 bounds on reachability probabilities that are assured to hold in any composition context.

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 known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcome many of the limitations and we investigate the computational complexity of modal refinement checking.

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 limit-average (or mean-payoff) functions. We consider two different objectives, namely, expectation and satisfaction objectives. Given an MDP with k reward functions, in the expectation objective the goal is to maximize the expected limit-average value, and in the satisfaction objective the goal is to maximize the probability of runs such that the limit-average value stays above a given vector. We show that under the expectation objective, in contrast to the single-objective case, both randomization and memory are necessary for strategies, and that finite-memory randomized strategies are sufficient. Under the satisfaction objective, in contrast to the single-objective case, infinite memory is necessary for strategies, and that randomized memoryless strategies are sufficient for epsilon-approximation, for all epsilon. We further prove that the decision problems for both expectation and satisfaction objectives can be solved in polynomial time and the trade-off curve (Pareto curve) can be epsilon-approximated in time polynomial in the size of the MDP and 1/epsilon, and exponential in the number of reward functions, for all epsilon>0. Our results also reveal flaws in previous work for MDPs with multiple mean-payoff functions under the expectation objective, correct the flaws and obtain improved results.

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. This technical report is a full version of a paper presented at the 24th Florida Artificial Intelligence Research Society Conference.

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. Therefore, we introduce transition systems with obligations as a general model encompassing all the aforementioned models, and equip it with a process algebra description. Using these instruments, we then compare the previously studied subclasses and characterize their relationships.

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 components is a fundamental graph problem inherently present in many scientific and commercial applications. In this paper we show how existing parallel algorithms can be reformulated in order to be accelerated by NVIDIA CUDA technology. In particular, we design a new CUDA-aware procedure for pivot selection and we redesign the parallel algorithms in order to allow for CUDA accelerated computation. We also experimentally demonstrate that with a single GTX 280 GPU card we can easily outperform optimal serial CPU implementation, which is particularly interesting result as unlike the serial CPU case, the asymptotic complexity of the parallel algorithms is not optimal.

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 deploying an enterprise-wide full-text search system is to handle the access rights of the documents and intranet web pages correctly and effectively. Post-processing the results of general-purpose full-text search engine (filtering out the documents inaccessible to the user who sent the query) can be an expensive operation, especially in large collections of documents. We discuss various approaches to this problem and propose a novel method which employs virtual tokens for encoding the access rights directly into the search index. We then evaluate this approach in an intranet system with several millions of documents and a complex set of access rights and access rules.

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 of biometric authentication and encryption systems. The attractiveness of some novel approaches like cryptographic key generation from biometric data is in some respect understandable, yet so far has lead to various shortcuts and compromises on security. The report starts with an introductory section that is followed by a section about variability of biometric characteristics, with a particular attention paid to biometrics used in large systems. The following sections then discuss the potential for biometric authentication systems, and for the use of biometrics in support of cryptographic applications as they are typically used in computer systems.

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 (k-1)-EXPTIME. In this paper, we show that, for k = 2, the problem is in P, and thus improve the EXPTIME upper bound.

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 processes where the winning objective is specified by a timed automaton. The goal of player I is to play in such a way that the play (a timed word) is accepted by the timed automaton with probability one. Player II aims at the opposite. We prove that whenever player I has a winning strategy, then she also has a strategy that can be specified by a timed automaton. The strategy automaton reads the history of a play, and the decisions taken by the strategy depend only on the region of the resulting configuration. We also give an exponential-time algorithm which computes a winning timed automaton strategy if it exists.

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 (MPGs). Besides solving an MPG in the usual sense, our algorithm computes more information about the game, information that is important with respect to applications. The weights of the edges of an MPG can be thought of as a gained/consumed energy -- depending on the sign. For each vertex, our algorithm computes the minimum amount of initial energy that is sufficient for player Max to ensure that in a play starting from the vertex, the energy level never goes below zero. Our algorithm is not the first algorithm that computes the minimum sufficient initial energies, but according to our experimental study it is the fastest algorithm that computes them. The reason is that it utilizes the strategy improvement technique which is very efficient in practice.

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 differences in problem difficulty.

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 described behaviours, and are often considered as a design error. While there is a quadratic-time algorithm detecting races in Basic Message Sequence Charts (BMSCs), the problem is undecidable for High-level Message Sequence Charts (HMSCs). To improve this negative situation for HMSCs, we introduce two new notions: a new concept of race called trace-race and an extension of the HMSC formalism with open coregions, i.e. coregions that can extend over more than one BMSC. We present three arguments showing benefits of our notions over the standard notions of race and HMSC. First, every trace-race-free HMSC is also race-free. Second, every race-free HMSC can be equivalently expressed as a trace-race-free HMSC with open coregions. Last, the trace-race detection problem for HMSC with open coregions is decidable and PSPACE-complete (the problem is in P if the number of processes and gates is fixed).

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 time-bounded reachability objectives. We show that each vertex in such a game has a value (i.e., an equilibrium probability), and we classify the conditions under which optimal strategies exist. Finally, we show how to compute optimal strategies in finite uniform games, and how to compute e-optimal strategies in finitely-branching games with bounded rates (for finite games, we provide detailed complexity estimations).

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. We study the computation of both the distribution of the memory consumption and its expectation. For the distribution, we show that a naive method incurs an exponential blow-up, and that it can be avoided using linear equation systems. We also suggest a possibly even faster approximation method. Given epsilon>0, these methods allow to compute bounds on the memory consumption that are exceeded with a probability of at most epsilon. For the expected memory consumption, we show that whether it is infinite can be decided in polynomial time for stateless pPDA (pBPA) and in polynomial space for pPDA. We also provide an iterative method for approximating the expectation. We show how to compute error bounds of our approximation method and analyze its convergence speed. We prove that our method converges linearly, i.e., the number of accurate bits of the approximation is a linear function of the number of iterations.

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, a SIMD-like hardware architecture became easily accessible for many users who have their computers equipped with modern NVIDIA GPU cards with CUDA technology. In this paper we redesign the maximal accepting predecessors algorithm [7] for LTL model checking in terms of matrix-vector product in order to accelerate LTL model checking on many-core GPU platforms. Our experiments demonstrate that using the NVIDIA CUDA technology results in a significant computation speedup.

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 automaton may be infinite, which we deal with by introducing a normal form of the B�chi automata and normalizing procedure. We also show that the newly introduced formalism can be used to distinguish MDPs indistinguishable by any LTL, PCTL or even PCTL* formula.

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 formalism introduced more than 20 years ago, has recently received a considerable attention in several different areas. Many of the fundamental questions related to MTSs have already been answered. However, the problem of the exact computational complexity of thorough refinement checking between two finite MTSs remained unsolved.

We settle down this question by showing EXPTIME-completeness of thorough refinement checking on finite MTSs. The upper-bound result relies on a novel algorithm running in single exponential time providing a direct goal-oriented way to decide thorough refinement. If the right-hand side MTS is moreover deterministic, or has a fixed size, the running time of the algorithm becomes polynomial. The lower-bound proof is achieved by reduction from the acceptance problem of alternating linear bounded automata and the problem remains EXPTIME-hard even if the left-hand side MTS is fixed.

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 on a concept of a verification manager. The manager automates some step of the verification process and enables efficient parallel combination of different verification techniques. We describe a realization of this concept for explicit model checking and discuss practical experience. Particularly, we discuss the problem of selection of input problems for evaluation of this kind of tool.

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 automata (or, equivalently, 1-exit recursive state machines), where the winning objective is specified by a regular set of target configurations and a qualitative probability constraint ‘>0’ or ‘=1’. The goal of one player is to maximize the probability of reaching the target set so that the constraint is satisfied, while the other player aims at the opposite. We show that the winner in such games can be determined in NP intersection co-NP. Further, we prove that the winning regions for both players are regular, and we design algorithms which compute the associated finite-state automata. Finally, we show that winning strategies can be synthesized effectively.

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

As to the third element, it is being demonstrated that the verbal expression of a picture which has been included in a document:

remains partially unchanged even in the new context,

needs reassessment, as to the rest (due to new ties and interpretation).

To display both information packages correctly to the user, the ontology must be complex enough to differentiate between formally identical questions and to answer them in a specific way according to the above-mentioned perspectives.

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 pushdown automata related both to terminating and non-terminating runs can be efficiently approximated up to an arbitrarily small given precision.

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.

The main contribution of the paper is a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.

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 algorithmic technique for verification of safety interaction properties of Control-User systems. The core of our verification method is a computation of a cutoff. If the system is proved to be correct for every number of user components lower than the cutoff then it is correct for any number of users. We present an on-the-fly model checking algorithm which integrates computation of a cutoff with the verification itself. Symmetry reduction can be applied during the verification to tackle the state explosion of the model. Applying the algorithm we verify models of several previously published component-based systems.

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 Markov decision processes with qualitative PECTL* objectives are 2-EXPTIME complete. More precisely, the algorithms are polynomial in the size of a given Markov decision process and doubly exponential in the size of a given qualitative PECTL* formula. Moreover, we show that if a given qualitative PECTL* objective is achievable by some strategy, then it is also achievable by an effectively constructible one-counter strategy, where the associated complexity bounds are essentially the same as above. For the fragment of qualitative PCTL objectives, we obtain EXPTIME completeness and the algorithms are only singly exponential in the size of the formula.

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 and evaluation of students` papers and essays is that it has become easier for students to plagiarize the work of other people. In this paper we present a computer-based system for discovering similar documents, which has been in use at Masaryk University in Brno since August 2006, and which will also be used in the forthcoming Czech national archive of graduate theses. We also focus on practical aspects of this system: achieving near real-time response to newly imported documents, and computational feasibility of handling large sets of documents on commodity hardware. We also show the possibilities and problems with parallelization of this system for running on a distributed cluster of computers.

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 (Probabilistic Computation Tree Logic), which is obtained from "ordinary" CTL by replacing the EX, AX, EU, and AU operators with their qualitative counterparts X>0, X=1, U>0, and U=1, respectively. As opposed to CTL, qualitative PCTL does not have a small model property, and there are even qualitative PCTL formulae which have only infinite-state models. Nevertheless, we show that the satisfiability problem for qualitative PCTL is EXPTIME-complete and we give an exponential-time algorithm which for a given formula computes a finite description of a model (if it exists), or answers "not satisfiable" (otherwise). We also consider the finite satisfiability problem and provide analogous results. That is, we show that the finite satisfiability problem for qualitative PCTL is EXPTIME-complete, and every finite satisfiable formula has a model of an exponential size which can effectively be constructed in exponential time. Finally, we give some results about the quantitative PCTL, where the numerical bounds in probability constraints can be arbitrary rationals between 0 and 1. We prove that the problem whether a given quantitative PCTL formula has a model of the branching degree at most k, where k > 1 is an arbitrary but fixed constant, is highly undecidable. We also show that every satisfiable formula F has a model with branching degree at most |F| + 2. However, this does not yet imply the undecidability of the satisfiability problem for quantitative PCTL, and we in fact conjecture the opposite.

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 perform experiments over a large benchmark set (more than 100 models). The conclusion of our evaluation is that it is more important to combine several simple techniques in an appropriate way rather than to tune a single sophisticated technique.

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 history and the level of the query-answer approximation. All proposed algorithms are tested on real data and medium-sized P2P networks consisting of tens of computers.

Key Distribution and Secrecy Amplification in Wireless Sensor Networks

by Petr �venda, V�clav Maty�, November 2007, 63 pages.

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

Abstract:

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

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

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

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

Abstract:

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

This report contains detailed description of the fundamentals and specific algorithms of LOBS, a theoretical analysis of its behaviour, and results of extensive experiments we conducted using a prototype implementation of LOBS. We tested LOBS with the peer-to-peer structure \mchord{} having a various number of peers. We used a real-life dataset and query sets of various distributions. The results show that LOBS is able to cope with any query-distribution and that it improves both the utilization of resources and the system performance of query processing. The costs of balancing are reasonable compared to the level of imbalance and are very small if the system has time to adapt to a query-traffic. The behaviour of LOBS is independent of the size of the network.

Strategy Synthesis for Markov Decision Processes and Branching-Time Logics

by Tom� Br�zdil, Vojt�ch Forejt, A full version of the paper presented at CONCUR 2007 July 2007, 28 pages.

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

Abstract:

We consider a class of finite $1\frac{1}{2}$-player games (Markov decision processes) where the winning objectives are specified in the branching-time temporal logic qPECTL$^*$ (an extension of the qualitative PCTL$^*$). We study decidability and complexity of existence of a winning strategy in these games. %The logic is more expressive than the qualitative fragment of PCTL$^*$. We identify a fragment of qPECTL$^*$ called detPECTL$^*$ for which the existence of a winning strategy is decidable in exponential time, and also the winning strategy can be computed in exponential time (if it exists). Consequently we show that every formula of qPECTL$^*$ can be translated to a formula of detPECTL$^*$ (in exponential time) so that the resulting formula is equivalent to the original one over finite Markov chains. From this we obtain that for the whole qPECTL$^*$, the existence of a winning finite-memory strategy is decidable in double exponential time. An immediate consequence is that the existence of a winning finite-memory strategy is decidable for the qualitative fragment of PCTL$^*$ in triple exponential time. We also obtain a single exponential upper bound on the same problem for the qualitative PCTL. Finally, we study the power of finite-memory strategies with respect to objectives described in the qualitative PCTL.

Formalisms and Tools for Design and Specification of Network Protocols

by Jind�ich Babica, Vojt�ch �eh�k, Petr Slov�k, Pavel Troubil, Martin Zavadil, May 2007, 33 pages.

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

Abstract:

Message Sequence Charts (MSC) are a useful formalism for formalization of network protocols early in their design phase. In this paper, we introduce the basics of MSC language and describe some of the possibilities for automatic location of "problematic" parts in the design. Focus is then given to different modifications of MSC design (FIFO behavior, bounded channels, etc. ) as well as formal checking of more complex design properties (MSC membership, realizability). Next, an introduction of Specification and Description Language (SDL) is presented. Possibilities of automatic synthesis of system design in MSC to an SDL model and it`s correctness verification are mentioned.

LTL model checking with I/O-Efficient Accepting Cycle Detection

by Ji�� Barnat, Lubo� Brim, Pavel �ime�ek, January 2007, 20 pages.

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

Abstract:

We show how to adopt existing non-DFS-based algorithm OWCTY for accepting cycle detection to the I/O efficient setting and compare the I/O efficiency and practical performance of the adopted algorithm to the existing I/O efficient LTL model checking approach of Edelkamp et al. We show that while the new algorithm exhibits similar I/O complexity with respect to the size of the graph, it avoids the quadratic increase in the size of the graph of the approach of Edelkamp et al. Therefore, the absolute numbers of I/O operations are significantly smaller and the algorithm exhibits better practical performance.

Operational Semantics of Quantum Programming Language LanQ

by Hynek Mlna��k, December 2006, 43 pages.

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

Abstract:

We present new imperative quantum programming language LanQ which was designed to support combination of quantum and classical programming and basic process operations -- process creation and interprocess communication. The language can thus be used for implementing both classical and quantum algorithms and protocols. Its syntax is similar to that of C language what makes it easy to learn for existing programmers. In this paper, we present operational semantics of the language. We provide an example run of a quantum random number generator.

Component-Interaction Automata Modelling Language

by Ivana �ern�, Pavl�na Va�ekov�, Barbora Zimmerov�, October 2006, 25 pages.

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

Abstract:

The paper introduces a Component-interaction automata language, which was designed for modelling of component interactions in hierarchical component-based software systems. The language supports modelling of important interaction attributes of such systems, and hence provides a rich base for further application of formal methods. Component-interaction automata provide a flexible form of component composition which can respect architectural assembly of the system, communication mechanisms, and other specifics of component-based systems. This allows the language to capture interactions in many different kinds of componentbased systems (built on different component models for instance). This paper provides a detailed study of the language including discussion of its practical application and comparison with related work. We intend to use this language as a framework for verifying coordination errors, checking of reconfiguration correctness, and formal analysis of component interactions in component-based systems, which is our ongoing and future work.

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

by Stanislav Barto�, Pavel Zezula, A full version of the paper presented at IEEE MCD 2006. September 2006, 22 pages.

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

Abstract:

An own design of an indexing structure for general graph structured data called rhoIndex that allows an effective processing of special path queries is presented. These special queries represent for example a search for all paths lying between two arbitrary vertices limited to a certain path length. The rhoIndex is a multilevel balanced tree structure where each node is created with a certain graph transformation and described by modified adjacency matrix. Hence, rhoIndex indexes all the paths to a predefined length linclusive. The search algorithm is then able to find all the paths shorter than or having the length land some of the paths longer then the predefined llying between any two vertices in the indexed graph. The designed search algorithm exploits a special graph structure, a transcription graph, to compute the result using the rhoIndex . We also present an experimental evaluation of the process of creating the rhoIndex on graphs with different sizes and also a complexity evaluation of the search algorithm that uses the rhoIndex.

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

by Ond�ej V�born�, September 2006, 19 pages.

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

Abstract:

The past few years have confirmed the increasing importance of the preservation of the privacy of an individual due to the number of methods by which private information can be misused. At the same time, since vast amounts of data are easily available, data mining is taking on a greater role in the processing thereof, placing techniques that can satisfy strict legal and public requirements on the processing of sensitive data in great demand. This paper presents the state-of-the-art in privacy preserving data mining and also proposes an alternative classification of privacy preserving techniques based on several points of view on privacy.

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

by Laura Bozzelli, Mojm�r K�et�nsk�, Vojt�ch �eh�k, Jan Strej�ek, A full version of the paper presented at FSTTCS 2006. November 2006, 27 pages.

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

Abstract:

We establish a decidability boundary of the model checking problem for infinite-state systems defined by Process Rewrite Systems (PRS) or weakly extended Process Rewrite Systems (wPRS), and properties described by basic fragments of action-based Linear Temporal Logic (LTL). It is known that the problem for general LTL properties is decidable for Petri nets and for pushdown processes, while it is undecidable for PA processes. As our main result, we show that the problem is decidable for wPRS if we consider properties defined by formulae with only modalities strict eventually and strict always. Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality until or the fragment with modalities next and infinitely often.

Distributed Qualitative LTL Model Checking of Markov Decision Processes

by Ji�� Barnat, Lubo� Brim, Ivana �ern�, Milan �e�ka, Jana T�mov�, September 2006, 19 pages.

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

Abstract:

Probabilistic processes are used to model concurrent programs that exhibit uncertainty. The state explosion problem for probabilistic systems is more critical than in the non-probabilistic case. In the paper we propose a cluster-based algorithm for qualitative LTL model checking of finite state Markov decision processes. We use the automata approach which reduces the model checking problem to the question of existence of an accepting end component. The algorithm uses repeated reachability which systematically eliminates states that cannot belong to any accepting end component. A distinguished feature of the distributed algorithm is that its complexity meets the complexity of the best known sequential algorithm.

Web Portal for Benchmarking Explicit Model Checkers

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

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

Abstract:

We present BEEM - BEnchmarks for Explicit Model checkers. This benchmark set includes more than 50 models together with correctness properties (both safety and liveness). The benchmark set is accompanied by an comprehensive web portal, which provides detailed information about all models. The web portal also includes information about state spaces and facilities selection of models for experiments.

The report describes the rationale beyond the form of the benchmark set, the design of the web portal and the main aspects of its realization, and also an example of an experimental analysis over the benchmark set: an analysis of a performance of sequential and distributed reachability.

The address of the web portal is http://anna.fi.muni.cz/models .

Stochastic Games with Branching-Time Winning Objectives

by Tom� Br�zdil, V�clav Bro�ek, Vojt�ch Forejt, Anton�n Ku�era, A full version of the paper presented at LICS 2006. September 2006, 37 pages.

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

Abstract:

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

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 applicable for their fulfillment. Besides these basic factors, you can also find here questions relevant for legislative and normative restrictions put on certain types of data. Finally, we discuss present-day approaches for data exchange and storage, and its usability for long-term storage.

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 aspects of sampled semantics. At first, we study reachability relations between configurations of a timed automaton and provide a novel effective characterization of reachability relations. This result is used for proving our main result --- decidability of non-emptiness of a timed automaton omega-language in some sampled semantics (this problem was previously wrongly classified as undecidable). Also, we study relations between real semantics and sampled semantics with respect to different behavioral equivalences. Finaly, we study decidability of reachability problem for stopwatch automata with sampled semantics.

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 for probabilistic programs with recursive procedure calls. Previous works considered the decidability and complexity of the model-checking problem for pPDA and various probabilistic temporal logics. In this paper we concentrate on computing the expected values and variances of various random variables defined over runs of a given probabilistic pushdown automaton. In particular, we show how to compute the expected accumulated reward and the expected gain for certain classes of reward functions. Using these results, we show how to analyze various quantitative properties of pPDA that are not expressible in conventional probabilistic temporal logics.

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 equivalence is undecidable for pushdown processes (PDA), process algebras (PA), and multiset automata (MSA, also known as parallel pushdown processes, PPDA). Its decidability is an open question for basic process algebras (BPA) and basic parallel processes (BPP). We move the undecidability border towards these classes by showing that the equivalence remains undecidable for weakly extended versions of BPA and BPP. Further, we show the results hold for even more restricted classes of normed BPA with finite constraint system and normed BPP with finite constraint system.

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 a ``correct" derivation tree even if the grammar cannot generate the input sentence. The following two steps solution is proposed: the finest corresponding most probable optimal maximum coverage is generated first, then the trees from this coverage are glued into one resulting tree. We discuss the implementation of this method with the SLP toolkit and libkp library.

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 for probabilistic pushdown automata (pPDA) and various temporal logics. We prove that the qualitative and quantitative model-checking problem for omega-regular properties and pPDA is in 2-EXPSPACE and 3-EXPTIME, respectively. We also prove that model-checking the qualitative fragment of the logic PECTL* for pPDA is in 2-EXPSPACE, and model-checking the qualitative fragment of PCTL for pPDA is in EXPSPACE. Furthermore, model-checking the qualitative fragment of PCTL is shown to be EXPTIME-hard even for stateless pPDA. Finally, we show that PCTL model-checking is undecidable for pPDA, and PCTL+ model-checking is undecidable even for stateless pPDA.

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) for high-level design of heterogeneous systems is presented in this paper. The language is based on a state-transition operational semantics, which allows application of formal methods to software design. Formal definition of VCD is included in the paper. Moreover, an example of use of the language is also given.

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 in fragments of LTL where the nesting depths of X and U modalities are bounded by given constants. This brings further results about various LTL fragments. We also propose a generic method for decomposing LTL formulae into an equivalent disjunction of ``semantically refined" LTL formulae, and indicate how this result can be used to improve the functionality of existing LTL model-checkers.

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 into a language equivalent A1W automata has been introduced in [MSS88]. The inverse translation has been developed independently in [Roh97] and [LT00]. We improve the latter translation and present deeper connections between LTL and A1W automata. Using these translations we identify the classes of A1W automata equivalent to LTL fragments given by bounds on nesting depths of temporal operators (see, e.g., [Wil99,KS02]) and the fragments of Until-Release hierarchy [CP03].

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 probabilistic extensions of BPA and BPP processes. For normed subclasses of probabilistic BPA and BPP processes we obtain polynomial-time algorithms. Further, we show that probabilistic bisimilarity between probabilistic pushdown automata and finite-state systems is decidable in exponential time. If the number of control states in PDA is bounded by a fixed constant, then the algorithm needs only polynomial time.

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 problem of comparing an arbitrary transition system to some finite-state specification can be reduced to a model checking problem against simple modal formulae. As an application, we derive decidability of several regular equivalence problems for well-known families of infinite-state systems.

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 without any next-time operator if and only if the property is stutter invariant. It is also known that the problem whether a given LTL property is stutter invariant is PSPACE-complete. We extend these results to fragments of LTL obtained by restricting the nesting depth of the next-time operator to a given n. Some interesting facts about the logic LTL follow as simple corollaries.

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 automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model checking for this class of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for general PCTL and the subclass of stateless pPDA. Finally, we consider the class of properties definable by deterministic Buchi automata, and show that both qualitative and quantitative model checking for pPDA is decidable.

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. They either permit or block the exchange of data between networks. The ability to permit or block the transfer of data means firewalls can be used to selectively allow access to the resources it protects. Firewalls of varying security levels have been created to provide security that is adequate to the sensitivity of the data being protected. Firewalls are often formally evaluated to certify what level of security they are suitable for. They are evaluated against so-called security evaluation criteria -- standardised descriptions of security measures. Common Criteria (CC) is the current global standard for evaluations. Firewall security attributes are described in a Protection Profile (PP) that defines an implementation-independent set of security requirements and objectives for a category of products or systems that meet similar consumers needs for IT security. Our project set out to produce a summary of security issues for an Application-Level Firewall Protection Profile (PP) for a High Robustness Environment. We started our work with the Basic-Level Firewall PP, the Medium-Level Firewall PP and the High-Level Mail Guard PP. The two firewall PPs and the Mail Guard PP are compared to give an insight into what the issues concerning the High-Level Firewall PP are. This High-Level Firewall PP is then discussed in terms of its major principles.

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 between pushdown automata and finite-state automata. The abstract part of the method is applicable to every process equivalence which is a right PDA congruence. Practical usability of the method is demonstrated on selected equivalences which are conceptual representatives of the whole spectrum. In particular, special attention is devoted to bisimulation-like equivalences (including weak, early, delay, branching, and probabilistic bisimilarity), and it is also shown how the method applies to simulation-like and trace-like equivalences. The generality does not lead to the loss of efficiency; the algorithms obtained by applying our method are essentially time-optimal and sometimes even polynomial. The list of particular results obtained by our method includes items which are first of their kind.

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 both theoretical and practical framework for construction of objects. In this model the objects with roles can dynamically change the interfaces they support. Some advantages of creating applications using this concept are discussed on an example of a system of virtual reality.

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 systems. We extend Mayr`s Process Rewrite Systems (PRS) by finite-state unit whose transition function satisfies some restrictions inspired by weak finite automata. We classify these models by their expressiveness and show how the hierarchy of new classes (w.r.t. bisimilarity) is related to both PRS hierarchy of Mayr and two other hierarchies of PRS extensions introduced in [JKM02, Str02].

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 and for the negative cycle detection problems on directed graphs with real edge weights and given by adjacency list are developed, analysed, and experimentally compared. The algorithms are to be performed on clusters of workstations that communicate via a message passing mechanism.

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, topology, omega-automata, and linear temporal logic classifications of properties. We provide new characterisations of this hierarchy in terms of automata with Buchi, co-Buchi, and Streett acceptance condition and in terms of Until-Release alternation hierarchy. Afterwards, we analyse the complex ity of the model checking problem for particular classes of the hierarchy and thanks to the new characterisations we identify those linear time temporal properties for which the model checking problem can be solved more efficiently than in the general case.

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 set P of d-dimensional objects in d-dimensional space. There are several classes of objects defined for such settings, which support design of effective algorithms. We extend the existing the de Berg hierarchy of classes by the definition of new classes derived from that one and we show desirability of such an extension. Moreover we propose a new algorithm, which works on generalized lambda-low density scenes (defined in this paper) and provides BSP tree of linear size. The tree can be constructed in O(n log^2 n) time and space, where n is the number of objects. Moreover, we can trade-off between size and balance of the BSP tree fairly simply.

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 the problem of modelling and automatic programming of dialogue systems. The approach presented here is based on finding an operator (a construction) that assigns a corresponding dialogue system to a dialogue corpus. It will be shown that this construction is universal, in the sense that each dialogue system can be obtained in this way, and some related issues (uniqueness, algorithmization and algorithmical complexity) will be briefly discussed. The theory is illustrated on a simple example. Some related problems are formulated.

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 CTL model checking. This paper presents a new distributed scalable algorithm for explicit fair cycle detection. Our method combines the simplicity of the distribution of explicitly presented data structure and the features of symbolic algorithm allowing for an efficient parallelisation. If a fair cycle (i.e. counterexample) is detected, then the algorithm produces a cycle, which is in general shorter than that produced by depth-first search based algorithms. Experimental results confirm that our approach outperforms that based on a direct implementation of the best sequential algorithm.

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 checking by splitting the given state space into several "partial state spaces". The partial state space is modelled as a Kripke structure with border states. Each computer involved in the distributed computation owns a partial state space and performs a model checking algorithm on this incomplete structure. To be able to proceed, the border states are augmented by assumptions about the truth of formulas and the computers exchange assumptions about relevant states as they compute more precise information. In the paper we give the basic definitions and present the distributed algorithm.

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 dialogue interface of Library system at Faculty of Informatics. This interface has been developed to enhance the accessibility of the system to the people with special needs as well as to enable telephone access to the system in the near future.

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.

The report reviews the problem of the document content interpretation. Introductory section reviews problems related to the use of digital signatures in practice. The second section briefly summarizes necessary cryptographic assumptions and gives an overview of signature functional properties. The third section discusses questions and possible ways of an interpretation of documents content. The fourth section suggests design principles for trustworthy electronic document structure.

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 Tools Day, which was held as an affiliated event of CONCUR 2002 on August 24, 2002 in Brno, Czech Republic.

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 Workshop on Verification of Infinite-State Systems (INFINITY 2002), held on August 24, 2002, in Brno, Czech Republic. The workshop was organized as a satellite event of CONCUR 2002.

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 are invariant under the so-called stutter-equivalence of words. In this paper we extend this principle to general LTL formulae with given nesting depths of the `next` and `until` operators. This allows us to prove the semantical strictness of three natural hierarchies of LTL formulae, which are parametrized either by the nesting depth of just one of the two operators, or by both of them. As another interesting corollary we obtain an alternative characterization of LTL languages, which are exactly the regular languages closed under the generalized form of stutter equivalence. We also indicate how to tackle the state-space explosion problem with the help of presented results.

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) computationally harder than deciding bisimulation equivalence on almost all known classes of processes? We try to answer this question by describing two general methods that can be used to construct direct one-to-one polynomial-time reductions from bisimulation equivalence to simulation preorder (and simulation equivalence). These methods can be applied to many classes of finitely generated transition systems, provided that they satisfy certain abstractly formulated conditions. Roughly speaking, our first method works for all classes of systems that can test for `non-enabledness` of actions, while our second method works for all classes of systems that are closed under synchronization.

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 processes (BPA) to finite-state systems, w.r.t. strong and weak simulation preorder/equivalence and strong and weak bisimulation equivalence. We present a complete picture of the complexity of all these problems. In particular, we show that strong and weak simulation preorder (and hence simulation equivalence) is EXPTIME-complete between PDA/BPA and finite-state systems in both directions. For PDA the lower bound even holds if the finite-state system is fixed, while simulation-checking between BPA and any fixed finite-state system is already polynomial. Furthermore, we show that weak (and strong) bisimilarity between PDA and finite-state systems is PSPACE-complete, while strong (and weak) bisimilarity between two (normed) PDAs is EXPTIME-hard.

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 problem in an arbitrary directed graph which can contain negative length cycles is presented. The new algorithm is a label-correcting one and uses a novel way for detection of negative length cycles. It works on a network of processors with disjoint memory that communicate via message passing. Correctness of the algorithm is proved. The algorithm is work-efficient as its worst time complexity is O(n^3/p), where p is the number of processors.

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.

We have attempted to find out if any of the above mentioned approaches could be generalized to (semi)decide weak bisimilarity. Our findings indicate that a direct generalization is not sufficient and an efficient (semi)decision procedure cannot be obtained in this way.

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: vedaXDjbU2LSW@fiQ1T5fpnNE.muni8CVI=SRv5.cz

Please install a newer browser for this site to function properly.

More information