## A List by Author: Jan Krčál

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

### Probabilistic Bisimulation: Naturally on Distributions

by *
Holger Hermanns,
Jan Krčál,
Jan Křetínský,
* April 2014, 36 pages.

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

#### Abstract:

In contrast to the usual understanding of probabilistic systems as
stochastic processes, recently these systems have also been regarded
as transformers of probabilities. In this paper, we give a
natural definition of strong bisimulation for probabilistic
systems corresponding to this view that treats probability
distributions as first-class citizens. Our definition applies
in the same way to discrete systems as well as to systems with
uncountable state and action spaces. Several examples demonstrate
that our definition refines the understanding of behavioural
equivalences of probabilistic systems. In particular, it solves a
longstanding open problem concerning the representation of
memoryless continuous time by memoryfull continuous time. Finally,
we give algorithms for computing this bisimulation not only for
finite but also for classes of uncountably infinite systems.

### 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
bounds on reachability probabilities that are assured to hold in any composition context.

### 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
processes where the winning objective is specified by a timed
automaton. The goal of player I is to play in such a way that the
play (a timed word) is accepted by the timed automaton with probability
one. Player II aims at the opposite. We prove that whenever
player I has a winning strategy, then she also has a strategy that
can be specified by a timed automaton. The strategy automaton reads the
history of a play, and the decisions taken by the strategy depend only on
the region of the resulting configuration. We also give an
exponential-time algorithm which computes a winning timed automaton
strategy if it exists.

### 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
time-bounded reachability objectives. We show that each vertex in
such a game has a value (i.e., an equilibrium probability),
and we classify the conditions under which optimal strategies exist.
Finally, we show how to compute optimal strategies in finite uniform
games, and how to compute e-optimal strategies in
finitely-branching games with bounded rates (for finite games, we
provide detailed complexity estimations).