A List by Author: Jitka Stříbrná
- home page:
Distributed LTL Model-Checking in SPIN
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
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:
- construction of a (finite) bisimulation or expansion tree,
- construction of a finite Caucal base.
Approximating Weak Bisimulation on Basic Process Algebra
by Jitka Stříbrná, This work has been presented at MFCS`99. September 1999, 18 pages.
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.
Please install a newer browser for this site to function properly.