A list with abstracts sorted by year - 2005
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.
Data storage, especially long-time data storage, is one of the biggest IT/ICT topics discussed in this field today. This document deals with basic classification of electronic data, highlights its specifics versus standard documents and contains overview of elementary requirements on its availability, integrity, confidentiality and storage duration, as well as accessibility time. Together with requirements, this document discusses cornerstones
Reachability Relations and Sampled Semantics of Timed Systems
by Pavel Krčál, Radek Pelánek, A full version of the paper presented at conference FSTTCS 2005. December 2005, 31 pages.
FIMU-RS-2005-09. Available as Postscript, PDF.
Timed systems can be considered with two types of semantics -- dense time semantics and discrete time semantics. The most typical examples of both of them are real semantics and sampled semantics (i.e., discrete semantics with a fixed time step epsilon). In this work, we study different
Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances
by Javier Esparza, Antonín Kučera, Richard Mayr, A full version of the paper presented at LICS 2005. July 2005, 26 pages.
FIMU-RS-2005-07. Available as Postscript, PDF.
Probabilistic pushdown automata (pPDA) have been identified as a natural model
Refining the Undecidability Border of Weak Bisimilarity
by Mojmír Křetínský, Vojtěch Řehák, Jan Strejček, A full version of the paper presented at INFINITY 2005. August 2005, 20 pages.
FIMU-RS-2005-06. Available as Postscript, PDF.
Weak bisimilarity is one of the most studied behavioural equivalences. This
Tool for robust stochastic parsing using optimal maximum coverage
by Vladimír Kadlec, Jean-Cédric Chappelier, Martin Rajman, This report was also submitted as Technical Report No. 2004112 at Swiss Federal Institute of Technology (EPFL), Lausanne (Switzerland), October, 2004. April 2005, 16 pages.
FIMU-RS-2005-05. Available as Postscript, PDF.
This report presents a robust syntactic parser that is able to return
Under-Approximation Generation using Partial Order Reduction
by Luboš Brim, Ivana Černá, Pavel Moravec, Jiří Šimša, A full version of the paper submitted to conference CAV05 February 2005, 21 pages.
FIMU-RS-2005-04. Available as Postscript, PDF.
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.
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.
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.
We consider qualitative and quantitative model-checking problems
Please install a newer browser for this site to function properly.