# Technical Reports

## A List by Author: Tomáš Brázdil

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

### Verification of Open Interactive Markov Chains

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

#### Abstract:

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

### Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes

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

#### Abstract:

We study Markov decision processes (MDPs) with multiple

### Stochastic Real-Time Games with Qualitative Timed Automata Objectives

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

#### Abstract:

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

### Reachability Games on Extended Vector Addition Systems with States

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

#### Abstract:

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.

### Continuous-Time Stochastic Games with Time-Bounded Reachability

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

#### Abstract:

We study continuous-time stochastic games with

### On the Memory Consumption of Probabilistic Pushdown Automata

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

#### Abstract:

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.

### Qualitative Reachability in Stochastic BPA Games

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

#### Abstract:

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

### Discounted Properties of Probabilistic Pushdown Automata

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

#### Abstract:

We show that several basic discounted properties of probabilistic

### Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives

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

#### Abstract:

We show that controller synthesis and verification problems for

### The Satisfiability Problem for Probabilistic CTL

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

#### Abstract:

We study the satisfiability problem for qualitative PCTL

### Strategy Synthesis for Markov Decision Processes and Branching-Time Logics

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

#### Abstract:

We consider a class of finite

### Stochastic Games with Branching-Time Winning Objectives

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

#### Abstract:

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

### On the Decidability of Temporal Properties of Probabilistic Pushdown Automata

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

#### Abstract:

We consider qualitative and quantitative model-checking problems

### Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems

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

#### Abstract:

We prove that probabilistic bisimilarity is decidable over

Responsible contact: unixfimunicz