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

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

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

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

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

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

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.

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

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.

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

We show that several basic discounted properties of probabilistic

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

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.

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

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

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

We show that controller synthesis and verification problems for

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

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

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

We study the satisfiability problem for qualitative PCTL

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

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

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

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

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

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.