Technical Reports

A list with abstracts sorted by year - 2000

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:

1. construction of a (finite) bisimulation or expansion tree,
2. 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.