Jitka Stříbrná

October 1, 1998

Current address

Vojanova 599/44 400 07 Ústí nad Labem Czech Republic

Tel: +420-47-550 3948 Email: js@dcs.ed.ac.uk http://www.dcs.ed.ac.uk/home/js

Personal data

Gender: female Date of birth: 28 July 1971 Place of birth: Nymburk, Czechoslovakia Nationality: Czech

Education

1994 - 1998 University of Edinburgh, Laboratory for Foundations of Computer Science (LFCS). Was working towards a Ph.D. under the supervision of Mark Jerrum. Submitted a dissertation thesis Decidability and complexity of equivalences for simple process algebras.

1989 - 1994 Charles University, Department of Computer Science. Obtained B.Sc. and M.Sc. in theoretical computer science. Thesis On the borderline between combinatorics and logics supervised by Jan Kratochvíl (in Czech).

Publications

Decidability of strong bisimulation of Basic Parallel Processes using Hilbert’s basis theorem, Proceedings of Infinity’97: 2nd International Workshop on Verification of Infinite State Systems, ENTCS 9, 1997.

Hardness results for weak bisimilarity of simple process algebras, Proceedings of MFCS workshop on concurrency, to appear in ENTCS.

Decidability and complexity of equivalences for simple process algebras, PhD thesis, University of Edinburgh, 1998.

Research interests

• logic: classical and modal logics, mainly in connection with description of properties of systems, decidability and model checking

• computational complexity: in connection with decidability and feasibility of decision procedures for various process equivalences

• concurrency: theoretical aspects of concurrency, such as process algebras and process calculi, various equivalences on processes and their properties, decidability, etc.

• language and automata theory

• recursion theory and set theory

Teaching

• tutored a course on Algorithms and Data Structures for third-year computer science students at the Edinburgh University

• was involved in ‘Girls Get Smart’ project - designed to help thirteen and fourteen-year old girls to become more familiar with the Internet and with web page design

• teaching languages (in particular English and Czech)

Skills and interests

• some programming experience in Pascal, C++, ML and Prolog; basic knowledge of UNIX

• languages (I speak fluently Czech and English, on a conversational level Russian and German and I have basic knowledge of French, Spanish and Italian)

• among other interests belong dance, sports and travel

Meetings attended

• August 1998 - MFCS/CLS ’98 and workshop on concurrency in Brno, Czech Republic

• July 1997 - international colloquium Icalp’97 and workshop Infinity’97 in Bologna, Italy

• August 1996 - international conference Concur’96 and workshop Infinity’96 in Pisa, Italy

• November 1995 - workshop on Games, Processes and Logic at the Newton Institute in Cambridge, England

Presentations

• MFCS workshop on concurrency in Brno - presented the paper Hardness results for weak bisimilarity of simple process algebras

• Infinity’97 in Bologna - presented the paper Decidability of strong bisimulation of Basic Parallel Processes using Hilbert’s basis theorem

• May 1997, the Wednesday club meetings at LFCS, Edinburgh - presented the same paper Award

In 1994 I was awarded a four-year Wolfson scholarship for students from Eastern Europe to do a Ph.D. in LFCS at the Edinburgh University.

References

Dr. Mark Jerrum, LFCS, Department of Computer Science, Edinburgh University, King’s Buildings, Mayfield Road, Edinburgh EH9 3JZ, Scotland. email: mrj@dcs.ed.ac.uk

Dr. Jan Kratochvíl, Department of Applied Mathematics, Charles University, Malostranské náměstí 25, 118 00 Praha 1, Czech Republic. email: honza@kam.ms.mff.cuni.cz

Dr. Julian Bradfield, LFCS, Department of Computer Science, Edinburgh University, King’s Buildings, Mayfield Road, Edinburgh EH9 3JZ, Scotland. email: jcb@dcs.ed.ac.uk Extended Thesis Abstract

In my thesis I follow up on work of Christensen, Esparza, Hirshfeld, Hüttel, Jančar, Jerrum, Moller, Stirling and others that investigated the decidability questions for strong or weak bisimilarity on some simple classes of processes, in particular Basic Process Algebra processes and Basic Parallel processes. Strong bisimilarity and its weakening weak bisimilarity, due to Milner, are two important equivalence notions that relate systems which perform the same behaviour (in the latter case external or observable behaviour). BPA-processes are the process theory equivalent of context-free grammars with processes being constructed as sequential composition of atoms. Basic Parallel processes (introduced by Christensen) are the parallel equivalent of BPA-processes being defined as parallel composition of atoms.

We can define the notion of (weak) bisimilarity in two different ways. One way is starting from smaller relations that satisfy a certain bisimulation condition and then taking the union of all such relations; we call this approach coinductive. The other way is to start from above, from a relation containing all pairs of processes and then form a chain of smaller relations by eliminating pairs that do not satisfy a certain expansion condition. The sought after bisimulation relation is then obtained as an intersection of all such relations. We call these relations approximants and this procedure the inductive definition. Intuitively, we can index these approximants by ordinal numbers starting from 0 (which corresponds to the universal binary relation on processes) and we adopt the notation ∼_{α}, resp. ≈_{α}, for strong, resp. weak, bisimulation approximants. In the case of strong bisimulation and BPA or BPP there is an important fact which gives rise to a straightforward procedure for semideciding non-bisimilarity: ∼ = ⋂_{n∈ω} ∼_{n}. However, this is no longer true for weak bisimulation and hence the following question arises: what is the least ordinal number α (most likely different for BPA and BPP) such that ≈ = ≈_{α}? I have attempted to find an answer to this question with the following results:

• for BPA I have found a lower bound on α which is ω^{ω} by constructing pairs of BPA-processes D_{i}, D′_{i} such that for every i, D_{i} ≈_{ω^{i}} D′_{i} and D_{i} ≉ D′_{i}

• in the case of BPP, there are pairs of processes P_{i}, P′_{i} such that P_{i} ≈_{ω+i} P′_{i} and P_{i} ≉ P′_{i} from which we can deduce that the lower bound on α is ω · 2; I have proved that ω · 2 is also the upper bound for some restricted classes of BPP and also BPA

There is some further analysis of approximants and I also investigate alternative definitions of approximants and their relation to decidability of weak bisimilarity of BPP.

Although we do not know whether weak bisimilarity is decidable in the case of general BPA and BPP we may try to estimate the lower bound on a prospective decision procedure. This can be done using the reduction technique. The core of the technique is the following: we take a problem P which is complete for some complexity class C and find a feasible (polynomial) encoding of instances of P into instances of our problem. Then we can deduce that our problem is at least C-hard, i.e. any prospective algorithm solving this problem will have complexity at least C. I demonstrate the following reductions: KNAPSACK is reduced onto weak bisimilarity of BPP and BPA which implies that the latter is at least NP-hard. Next I describe the reductions of TOT (the totality problem for regular expressions) onto weak bisimilarity of BPA which makes the weak bisimilarity decision problem PSPACE-hard.

The final part of my thesis concentrates on strong bisimulation for BPP. Although it is a well known fact that strong bisimilarity is decidable, the decision procedure is non-elementary and doesn’t even have a primitive recursive upper bound. Since for a special subclass of normed BPP there is a polynomial decision procedure (due to Hirshfeld, Jerrum and Moller) and there is no evidence that any complex problem can be encoded into the decidability problem for BPP, it seems plausible that at least there could be an exponential decision procedure for general processes. That was a motivation for the new approach towards deciding bisimilarity of BPP. The method draws parallels between process theory and polynomial algebra, and uses important facts from computational algebra, in particular the notion of Gröbner bases and the algorithm for checking membership in polynomial ideals. We can encode basic parallel process as power products over the field F_{2} and then we express a bisimulation condition using polynomial ideals. Finally we apply the Hilbert’s basis theorem which ensures that this condition is finite and hence decidable since it reduces to membership test.