Technical Reports

A List by Author: Jitka Støíbrná

e-mail:

js(a)fi.muni.cz

home page:

https://www.fi.muni.cz/usr/stribrna/

Distributed LTL Model-Checking in SPIN

by Jiøí Barnat, Lubo¹ Brim, Jitka Støíbrná, December 2000, 19 pages.

FIMU-RS-2000-10. Available as Postscript, PDF.

Abstract:

Distributed version of the SPIN model checker has not been extended to allow distributed model-checking of LTL formulas. This paper explores the possibility of performing nested depth first search algorithm in distributed SPIN. A distributed version of the algorithm is presented, and its complexity is discussed.

Some Remarks on Weak Bisimilarity of BPA-Processes

by Ivana Èerná, Jitka Støíbrná, December 2000, 26 pages.

FIMU-RS-2000-09. Available as Postscript, PDF.

Abstract:

The purpose of this work is to examine the decidability problem of weak bisimilarity for BPA-processes. It has been known that strong bisimilarity, which may be considered a special case of weak bisimilarity, where the internal (silent) action tau is treated equally to observable actions, is decidable for BPA-processes. For strong bisimilarity, these processes are finitely branching and so for two non-bisimilar processes there exists a level n that distinguishes the two processes. Additionally, from the decidability of whether two processes are equivalent at a given level n, semidecidability of strong non-bisimilarity directly follows. We examine the following two closely related approaches to semidecidability of strong equivalence:

1. construction of a (finite) bisimulation or expansion tree,
2. construction of a finite Caucal base.

We have attempted to find out if any of the above mentioned approaches could be generalized to (semi)decide weak bisimilarity. Our findings indicate that a direct generalization is not sufficient and an efficient (semi)decision procedure cannot be obtained in this way.

Approximating Weak Bisimulation on Basic Process Algebra

by Jitka Støíbrná, This work has been presented at MFCS`99. September 1999, 18 pages.

FIMU-RS-99-05. Available as Postscript, PDF.

Abstract:

The maximal strong and weak bisimulations on any class of processes can be obtained as the limits of decreasing chains of binary relations, approximants. In the case of strong bisimulation and Basic Process Algebras this chain has length at most omega which enables semidecidability of strong bisimilarity. We show that it is not so for weak bisimulation where the chain can grow much longer, and discuss the implications this has for the problem of (semi)decidability of weak bisimilarity.