# Technical Reports

## A List by Author: Jan Strejček

- e-mail:
- xstrejc(a)fi.muni.cz

### Decidable Race Condition for HMSC

by *
Vojtěch Řehák,
Petr Slovák,
Jan Strejček,
Loic Hélouet,
* December 2009, 30 pages.

**FIMU-RS-2009-10.**
Available as *Postscript*,
**PDF**.

#### Abstract:

Races in Message Sequence Charts may lead to a bad interpretation of

### On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems

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**.

#### Abstract:

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*.

### Refining the Undecidability Border of Weak Bisimilarity

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**.

#### Abstract:

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

### Characteristic Patterns for LTL

by *
Antonín Kučera,
Jan Strejček,
* A full version of the paper presented at Sofsem 2005. December 2004, 22 pages.

**FIMU-RS-2004-10.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We give a new characterization of those languages that are definable

### Deeper Connections between LTL and Alternating Automata

by *
Radek Pelánek,
Jan Strejček,
* September 2004, 26 pages.

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

#### Abstract:

It is known that Linear Temporal Logic (LTL) has the same expressive power as alternating 1-weak automata (A1W automata, also called alternating linear automata or very weak alternating automata). A translation of LTL formulae

### An Effective Characterization of Properties Definable by LTL Formulae with a Bounded Nesting Depth of the Next-Time Operator

by *
Antonín Kučera,
Jan Strejček,
* May 2004, 11 pages.

**FIMU-RS-2004-04.**
Available as *Postscript*,
**PDF**.

#### Abstract:

It is known that an LTL property is expressible by an LTL formula

### Process Rewrite Systems with Weak Finite-State Unit

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**.

#### Abstract:

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

### The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL

by *
Antonín Kučera,
Jan Strejček,
* A full version of the paper presented at CSL`02. July 2002, 24 pages.

**FIMU-RS-2002-03.**
Available as *Postscript*,
**PDF**.

#### Abstract:

It is known that LTL formulae without the `next` operator
*stutter-equivalence* of

### Constrained Rewrite Transition Systems

by *
Jan Strejček,
* December 2000, 30 pages.

**FIMU-RS-2000-12.**
Available as *Postscript*,
**PDF**.

#### Abstract:

We extend broadly studied rewrite transition systems with a mechanism for computing with partial information in the form similar to that one used in Concurrent Constraint Programming (CCP). Two new classes of transition systems (fcBPA and fcBPP) are introduced as this extension changes expressibility power of rewrite transition systems corresponding to BPA and BPP. The power of rewrite systems corresponding to other classes (FSA, PDA, PPDA, and PN) remains unchanged. The new classes are inserted to the hierarchy of standard process classes presented by Moller [Mol96].

Responsible contact: unixfimunicz