- e-mail:
- mojmir(a)fi.muni.cz
- home page:
- http://www.fi.muni.cz/usr/kretinsky/

by *
Laura Bozzelli,
Mojmír Křetínský,
Vojtěch Řehák,
Jan Strejček,
* A full version of the paper presented at FSTTCS 2006. November 2006, 27 pages.

**FIMU-RS-2006-05.**
Available as *Postscript*,
**PDF**.

We establish a decidability boundary of the model checking problem for infinite-state systems defined by *Process Rewrite Systems* (PRS) or *weakly extended Process Rewrite Systems* (wPRS), and properties described by basic fragments of action-based *Linear Temporal Logic* (LTL). It is known that the problem for general LTL properties is decidable for Petri nets and for pushdown processes, while it is undecidable for PA processes. As our main result, we show that the problem is decidable for wPRS if we consider properties defined by formulae with only modalities *strict eventually* and *strict always*. Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality *until* or the fragment with modalities *next* and *infinitely often*.

by *
Mojmír Křetínský,
Vojtěch Řehák,
Jan Strejček,
* A full version of the paper presented at INFINITY 2005. August 2005, 20 pages.

**FIMU-RS-2005-06.**
Available as *Postscript*,
**PDF**.

Weak bisimilarity is one of the most studied behavioural equivalences. This

by *
Mojmír Křetínský,
Vojtěch Řehák,
Jan Strejček,
* This is a full version of the paper presented at INFINITY`03. September 2003, 23 pages.

**FIMU-RS-2003-05.**
Available as *Postscript*,
**PDF**.

Various classes of infinite-state processes are often specified by rewrite

by *
Jean-Marie Jacquet,
Luboš Brim,
David Gilbert,
Mojmír Křetínský,
* December 1999, 62 pages.

**FIMU-RS-99-08.**
Available as *Postscript*,
**PDF**.

Concurrent constraint programming is classically based on asynchronous communication via a shared store. In previous work, we presented a new version of the ask and tell primitives which features synchronicity, our approach being based on the idea of telling new information just in the case that a concurrently running process is asking for it. We turn in this paper to a semantic study of this new framework, called Scc.

It is first shown to be different in nature from classical concurrent constraint programming and from CCS, a classical reference in traditional concurrency theory. This suggests the interest of new semantics for Scc. To that end, an operational semantics reporting the steps of the computations is presented. A denotational semantics is then proposed. It uses monotonic sequences of labelled pairs of input-output states, possibly containing gaps, and ending - according to the logic programming tradition - with marks reporting success or failure. This denotational semantics is proved to be correct with respect to the operational semantics as well as fully abstract.

by *
Petr Jančar,
Mojmír Křetínský,
* Pre-proceedings of the MFCS`98 Workshop on Concurrency (the PS file is NOT provided, as it is too large (approx. 30MB); take pdf (3.5 MB) instead). July 1998, 209 pages.

**FIMU-RS-98-06.**
Available as *Postscript*,
**PDF**.

This volume contains the pre-proceedings of the MFCS`98 Workshop on Concurrency, which took place in Brno, Czech Republic, August 27-29, 1998, as a satellite event of the 23rd international symposium on Mathematical Foundations of Computer Science. It is composed of two invited papers delivered by Javier Esparza (Munich) and Faron Moller (Uppsala), and of 17 contributed papers selected out of 24 submissions. The revised (and full) version of the proceedings should appear as a volume of Electronic Notes in Theoretical Computer Science (Elsevier).

by *
Ivana Černá,
Mojmír Křetínský,
Antonín Kučera,
* This is a full version of the paper which is to be presented at CSL`96. June 1996, 28 pages.

**FIMU-RS-96-02.**
Available as *Postscript*,
**PDF**.

We compare the classes of behaviours (transition systems) which can be generated by normed BPA_{\tau} and normed BPP_{\tau} processes. We exactly classify the intersection of these two classes, i.e., the class of transition systems which can be equivalently (up to bisimilarity) described by the syntax of normed BPA_{\tau} and normed BPP_{\tau} processes. We provide such a characterisation for classes of normed BPA and normed BPP processes as well.

Next we show that it is decidable in polynomial time whether for a given normed BPA_{\tau} (or BPP_{\tau} respectively) process X there is some (unspecified) normed BPP_{\tau} (or BPA_{\tau} respectively) process X` such that X is bisimilar to X`. Moreover, if the answer is positive then our algorithms also construct the process X`. Simplified versions of the algorithms mentioned above for normed BPA and normed BPP are given too.

As an immediate (but important) consequence we also obtain the decidability of bisimilarity in the union of normed BPA_{\tau} and normed BPP_{\tau} processes.