by Jiří Barnat, Luboš Brim, Jitka Stříbrná, December 2000, 19 pages.
FIMU-RS-2000-10. Available as Postscript, PDF.
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.
by Ivana Černá, Jitka Stříbrná, December 2000, 26 pages.
FIMU-RS-2000-09. Available as Postscript, PDF.
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:
by Jitka Stříbrná, This work has been presented at MFCS`99. September 1999, 18 pages.
FIMU-RS-99-05. Available as Postscript, PDF.
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.