Technical Reports
A list with abstracts sorted by year - 2002
Distributed Explicit Fair Cycle Detection: Set Based Approach
by
Ivana Černá,
Radek Pelánek,
December 2002, 24 pages.
FIMU-RS-2002-09.
Available as Postscript,
PDF.
Abstract:
The fair cycle detection problem is at the heart of both LTL and fair
CTL model checking. This paper presents a new distributed scalable
algorithm for explicit fair cycle detection. Our method combines the
simplicity of the distribution of explicitly presented data structure
and the features of symbolic algorithm allowing for an efficient
parallelisation. If a fair cycle (i.e. counterexample) is detected,
then the algorithm produces a cycle, which is in general shorter than
that produced by depth-first search based algorithms. Experimental
results confirm that our approach outperforms that based on a direct
implementation of the best sequential algorithm.
Using Assumptions to Distribute CTL Model Checking
by
Luboą Brim,
Jitka Crhová,
Karen Yorav,
This is a full version of the paper presented at PDMC`02. October 2002, 22 pages.
FIMU-RS-2002-08.
Available as Postscript,
PDF.
Abstract:
In this work we discuss the problem of performing distributed CTL model
checking by splitting the given state space into several "partial state
spaces". The partial state space is modelled as a Kripke structure with
border states. Each computer involved in the distributed computation owns
a partial state space and performs a model checking algorithm on this
incomplete structure. To be able to proceed, the border states are
augmented by assumptions about the truth of formulas and the computers
exchange assumptions about relevant states as they compute more precise
information. In the paper we give the basic definitions and present the
distributed algorithm.
Improvements in a Dialogue Interface for Library System
by
Luděk Bártek,
October 2002, 6 pages.
FIMU-RS-2002-07.
Available as Postscript,
PDF.
Abstract:
This article describes methods and algorithms used to improve the
dialogue interface of Library system at Faculty of Informatics.
This interface has been developed to enhance the accessibility of
the system to the people with special needs as well as to enable
telephone access to the system in the near future.
Trustworthiness of Signed Data
by
Petr ©véda,
September 2002, 13 pages.
FIMU-RS-2002-06.
Available as Postscript,
PDF.
Abstract:
Use of digital signatures is not as straightforward as one would like to see it. We have to be aware of the fact that computers sign all electronic documents on behalf of humans and only few computers can be considered as fully trustworthy. Visual representation of file formats can be dramatically changed by settings of a viewer or a text processor. Users cannot be absolutely sure that they sign only the data visible on their computer screen. Proprietary signature solutions are not fully compatible as there are no standards.
The report reviews the problem of the document content interpretation. Introductory section reviews problems related to the use of digital signatures in practice. The second section briefly summarizes necessary cryptographic assumptions and gives an overview of signature functional properties. The third section discusses questions and possible ways of an interpretation of documents content. The fourth section suggests design principles for trustworthy electronic document structure.
Proceedings of Tools Day
by
Ivana Černá,
August 2002, 105 pages.
FIMU-RS-2002-05.
Available as Postscript,
PDF.
Abstract:
This volume contains proceedings of
Tools Day, which was held as an affiliated event
of CONCUR 2002 on August 24, 2002 in Brno, Czech Republic.
Pre-Proceedings of INFINITY 2002
by
Antonín Kučera,
Richard Mayr,
August 2002, 153 pages.
FIMU-RS-2002-04.
Available as Postscript,
PDF.
Abstract:
This volume contains pre-proceedings of 4th International
Workshop on Verification of Infinite-State Systems
(INFINITY 2002), held on August 24, 2002, in Brno,
Czech Republic.
The workshop was organized as a satellite event
of CONCUR 2002.
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL
by
Antonín Kučera,
Jan Strejček,
A full version of the paper presented at CSL`02. July 2002, 24 pages.
FIMU-RS-2002-03.
Available as Postscript,
PDF.
Abstract:
It is known that LTL formulae without the `next` operator
are invariant under the so-called
stutter-equivalence of
words. In this paper we extend this principle to general
LTL formulae with given nesting depths of the `next` and `until` operators. This allows us to prove the semantical strictness of three
natural hierarchies of LTL formulae, which are
parametrized either
by the nesting depth of just one of the two operators,
or by both of them. As another interesting corollary
we obtain an alternative
characterization of LTL languages, which are exactly the
regular languages closed under the generalized form of stutter equivalence. We also indicate how to tackle the state-space explosion problem with the help of presented results.
Why is Simulation Harder Than Bisimulation?
by
Antonín Kučera,
Richard Mayr,
A full version of the paper presented at CONCUR`02 June 2002, 26 pages.
FIMU-RS-2002-02.
Available as Postscript,
PDF.
Abstract:
Why is deciding simulation preorder (and simulation equivalence)
computationally harder than deciding bisimulation equivalence on
almost all known classes of processes? We try to answer this question
by describing two general methods that can be used to construct direct
one-to-one polynomial-time reductions from bisimulation equivalence to
simulation preorder (and simulation equivalence). These methods can
be applied to many classes of finitely generated transition systems,
provided that they satisfy certain abstractly formulated conditions.
Roughly speaking, our first method works for all classes of systems
that can test for `non-enabledness` of actions, while our second
method works for all classes of systems that are closed under
synchronization.
On the Complexity of Semantic Equivalences for Pushdown Automata and BPA
by
Antonín Kučera,
Richard Mayr,
A full version of the paper presented at MFCS`02. May 2002, 32 pages.
FIMU-RS-2002-01.
Available as Postscript,
PDF.
Abstract:
We study the complexity of comparing pushdown automata (PDA) and context-free
processes (BPA) to finite-state systems, w.r.t. strong and weak simulation
preorder/equivalence and strong and weak bisimulation equivalence.
We present a complete picture of the complexity of all these problems.
In particular, we show that strong and weak simulation preorder
(and hence simulation equivalence) is EXPTIME-complete between PDA/BPA and
finite-state systems in both directions. For PDA the lower bound even holds
if the finite-state system is fixed, while simulation-checking between
BPA and any fixed finite-state system is already polynomial.
Furthermore, we show that weak (and strong) bisimilarity between
PDA and finite-state systems is PSPACE-complete,
while strong (and weak) bisimilarity between two (normed)
PDAs is EXPTIME-hard.
