Technical Reports

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.

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.