- e-mail:
- rehak(a)fi.muni.cz
- home page:
- http://www.fi.muni.cz/~xrehak/

by *
Tomáš Brázdil,
Holger Hermanns,
Jan Krčál,
Jan Křetínský,
Vojtěch Řehák,
* A full version of the paper presented at conference FSTTCS 2012. November 2012, 52 pages.

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

Interactive Markov chains (IMC) are compositional behavioral models extending both labeled transition systems and continuous-time Markov chains. IMC pair modeling convenience - owed to compositionality properties - with effective verification algorithms and tools - owed to Markov properties. Thus far however, IMC verification did not consider compositionality properties, but considered closed systems. This paper discusses the evaluation of IMC in an open and thus compositional interpretation. For this we embed the IMC into a game that is played with the environment. We devise algorithms that enable us to derive

by *
Tomáš Brázdil,
Jan Krčál,
Jan Křetínský,
Antonín Kučera,
Vojtěch Řehák,
* A full version of the paper presented at CONCUR 2010. August 2010, 39 pages.

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

We consider two-player stochastic games over real-time probabilistic

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

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

by *
Jindřich Babica,
Vojtěch Řehák,
Petr Slovák,
Pavel Troubil,
Martin Zavadil,
* May 2007, 33 pages.

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

Message Sequence Charts (MSC) are a useful formalism for formalization of

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