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.