# Technical Reports

## A List by Author: Antonín Kučera

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

### 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

### 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

### 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

### Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

by *
Javier Esparza,
Antonín Kučera,
Richard Mayr,
* A full version of the paper presented at LICS 2005. July 2005, 26 pages.

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

#### Abstract:

Probabilistic pushdown automata (pPDA) have been identified as a natural model

### 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

### 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

### 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

### A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications

by *
Antonín Kučera,
Philippe Schnoebelen,
* A full version of the paper presented at CONCUR`04. June 2004, 32 pages.

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

#### Abstract:

We introduce a generic family of behavioral relations for which the

### 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

### Model Checking Probabilistic Pushdown Automata

by *
Javier Esparza,
Antonín Kučera,
Richard Mayr,
* A full version of the paper presented at LICS`04. July 2004, 34 pages.

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

#### Abstract:

We consider the model checking problem for probabilistic pushdown

### A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata

by *
Antonín Kučera,
Richard Mayr,
* A full version of the paper presented at IFIP TCS 2004. April 2004, 38 pages.

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

#### Abstract:

We propose a generic method for deciding semantic equivalences

### Pre-Proceedings of INFINITY 2002

by *
Antonín Kučera,
Richard Mayr,
* August 2002, 153 pages.

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

#### Abstract:

This volume contains pre-proceedings of 4th International

### 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

### Why is Simulation Harder Than Bisimulation?

by *
Antonín Kučera,
Richard Mayr,
* A full version of the paper presented at CONCUR`02 June 2002, 26 pages.

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

#### Abstract:

Why is deciding simulation preorder (and simulation equivalence)

### On the Complexity of Semantic Equivalences for Pushdown Automata and BPA

by *
Antonín Kučera,
Richard Mayr,
* A full version of the paper presented at MFCS`02. May 2002, 32 pages.

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

#### Abstract:

We study the complexity of comparing pushdown automata (PDA) and context-free

### On Simulation-Checking with Sequential Systems

by *
Antonín Kučera,
* This is a full version of the paper accepted for ASIAN 2000. September 2000, 34 pages.

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

#### Abstract:

We present new complexity results for simulation-checking and model-checking with infinite-state systems generated by pushdown automata and their proper subclasses of one-counter automata and one-counter nets (one-counter nets are "weak" one-counter automata computationally equivalent to Petri nets with at most one unbounded place).

As for simulation-checking, we show the following: a) simulation equivalence between pushdown processes and finite-state processes is EXPTIME-complete; b) simulation equivalence between processes of one-counter automata and finite-state processes is coNP-hard; c) simulation equivalence between processes of one-counter nets and finite-state processes is in P (to the best of our knowledge, it is the first (and rather tight) polynomiality result for simulation with infinite-state processes).

As for model-checking, we prove that a) the problem of simulation-checking between processes of pushdown automata (or one-counter automata, or one-counter nets) and finite-state processes are polynomially reducible to the model-checking problem with a fixed formula F = nu X. [z]<z> X of the modal mu-calculus. Consequently, model-checking with F is EXPTIME-complete for pushdown processes and coNP-hard for processes of one-counter automata; b) model-checking with a fixed formula <>[a]<>[b]ff of the logic EF (a simple fragment of CTL) is NP-hard for processes of OC nets, and model-checking with another fixed formula []<a>[]<b>tt of EF is coNP-hard. Consequently, model-checking with any temporal logic which can express these simple formulae is computationally hard even for the (very simple) sequential processes of OC-nets.

### Efficient Verification Algorithms for One-Counter Processes

by *
Antonín Kučera,
* This is a full version of the paper presented at ICALP 2000. March 2000, 24 pages.

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

#### Abstract:

We study the problem of strong/weak bisimilarity between processes of one-counter automata and finite-state processes. We show that the problem of weak bisimilarity between processes of one-counter nets (which are "weak" one-counter automata) and finite-state processes is DP-hard (in particular, it means that the problem is both NP and co-NP hard). The same technique is used to demonstrate co-NP hardness of strong bisimilarity between processes of one-counter nets. Then we design an algorithm which decides weak bisimilarity between processes of one-counter automata and finite-state processes in time which is polynomial for most "practical" instances, giving a characterization of all hard instances as a byproduct. Moreover, we show how to efficiently compute a rather tight bound for the time which is needed to solve a given instance. Finally, we prove that the problem of strong bisimilarity between processes of one-counter automata and finite-state processes is in P.

### A Logical Viewpoint on Process-Algebraic Quotients

by *
Antonín Kučera,
Javier Esparza,
* This is a full and revised version of a paper which previously appeared in Proceedings of CSL`99. January 2000, 26 pages.

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

#### Abstract:

We study the following problem: Given a transition system T and its quotient T/~ under an equivalence ~, which are the sets L, L` of Hennessy-Milner formulae such that: if f belongs to L and T satisfies f, then T/~ satisfies f; if f belongs to L` and T/~ satisfies f, then T satisfies f.

### Bisimilarity of Processes with Finite-state Systems

by *
Petr Jančar,
Antonín Kučera,
* These results will be presented at INFINITY`97 workshop. May 1997, 19 pages.

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

#### Abstract:

We describe a general method for deciding bisimilarity for pairs of processes where one process has finitely many states. We apply this method to pushdown processes and to PA processes. We also demonstrate that the mentioned problem is undecidable for `state-extended` PA processes.

### How to Parallelize Sequential Processes

by *
Antonín Kučera,
* Accepted to the 8th International Conference on Concurrency Theory (CONCUR`97). December 1996, 24 pages.

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

#### Abstract:

A process is prime if it cannot be decomposed into a parallel product of nontrivial processes. We characterize all non-prime normed BPA processes together with their decompositions in terms of normal forms which are designed in this paper. Then we show that it is decidable whether a given normed BPA process is prime and if not, its decomposition can be effectively constructed. This brings other positive decidability results. Finally, we prove that bisimilarity is decidable in a large subclass of normed PA processes.

### Comparing Expressibility of Normed BPA and Normed BPP Processes

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

#### Abstract:

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.

### Regularity is Decidable for Normed PA Processes in Polynomial Time

by *
Antonín Kučera,
* This paper is going to be presented at FST&TCS`96 conference, LNCS 1180, Springer-Verlag. February 1996, 17 pages.

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

#### Abstract:

A process X is regular if it is bisimilar to a process X` with finitely many states. We prove that regularity of normed PA processes is decidable and we present a practically usable polynomial-time algorithm. Moreover, if the tested normed PA process X is regular then the process X` can be effectively constructed. It implies decidability of bisimulation equivalence for any pair of processes such that one process is a normed PA process and the other process has finitely many states.

Responsible contact: unixfimunicz