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.


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.


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.


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.


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.


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.


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.


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.


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.


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.