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

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,
Václav Brožek,
Krishnendu Chatterjee,
Vojtěch Forejt,
Antonín Kučera,
* A full version of the paper presented at conference LICS 2011. April 2011, 32 pages.

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

We study Markov decision processes (MDPs) with multiple

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 *
Tomáš Brázdil,
Petr Jančar,
Antonín Kučera,
* A full version of the paper presented at ICALP 2010. February 2010, 38 pages.

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

We consider two-player turn-based games with zero-reachability and zero-safety objectives generated by extended vector addition systems with states. Although the problem of deciding the winner in such games is undecidable in general, we identify several decidable and even tractable subcases of this problem obtained by restricting the number of counters and/or the sets of target configurations.

by *
Tomáš Brázdil,
Vojtěch Forejt,
Jan Krčál,
Jan Křetínský,
Antonín Kučera,
* A full version of the paper presented at FST&TCS 2009. October 2009, 46 pages.

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

We study continuous-time stochastic games with

by *
Tomáš Brázdil,
Javier Esparza,
Stefan Kiefer,
* A full version of the paper presented at FSTTCS 2009 October 2009, 52 pages.

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

We investigate the problem of evaluating memory consumption for systems modelled by probabilistic pushdown automata (pPDA). The space needed by a run of a pPDA is the maximal height reached by the stack during the run. The problem is motivated by the investigation of depth-first computations that play an important role for space-efficient schedulings of multithreaded programs.

by *
Václav Brožek,
Tomáš Brázdil,
Antonín Kučera,
Jan Obdržálek,
* A full version of the paper presented at STACS 2009. May 2009, 37 pages.

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

We consider a class of infinite-state stochastic games generated by stateless pushdown

by *
Tomáš Brázdil,
Václav Brožek,
Jan Holeček,
Antonín Kučera,
* A full version of the paper presented at LPAR 2008 September 2008, 31 pages.

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

We show that several basic discounted properties of probabilistic

by *
Tomáš Brázdil,
Vojtěch Forejt,
Antonín Kučera,
* A full version of the paper presented at ICALP 2008. December 2008, 48 pages.

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

We show that controller synthesis and verification problems for

by *
Tomáš Brázdil,
Vojtěch Forejt,
Jan Křetínský,
Antonín Kučera,
* A full version of the paper presented at LICS 2008. June 2008, 34 pages.

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

We study the satisfiability problem for qualitative PCTL

by *
Tomáš Brázdil,
Vojtěch Forejt,
* A full version of the paper presented at CONCUR 2007 July 2007, 28 pages.

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

We consider a class of finite

by *
Tomáš Brázdil,
Václav Brožek,
Vojtěch Forejt,
Antonín Kučera,
* A full version of the paper presented at LICS 2006. September 2006, 37 pages.

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

We consider stochastic turn-based games where the
*highly undecidable*, even

by *
Tomáš Brázdil,
Antonín Kučera,
Oldřich Stražovský,
* A full version of the paper presented at STACS 2005. February 2005, 33 pages.

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

We consider qualitative and quantitative model-checking problems

by *
Tomáš Brázdil,
Antonín Kučera,
Oldřich Stražovský,
* A full version of the paper presented at CONCUR`04. September 2004, 26 pages.

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

We prove that probabilistic bisimilarity is decidable over