Author name cluster

Jan Krčál

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

Highlights Conference 2013 Conference Abstract

Compositional verification and optimization of interactive Markov chains

Holger Hermanns
Jan Krčál
Jan Kretinsky

We provide the first assume-guarantee reasoning for stochastic continuous-time systems. Interactive Markov chains (IMC) are compositional behavioural models similar to continuous-time Markov decision processes. Given a time-bounded property, an IMC component and a specification of the environment, we synthesize a scheduler optimizing the probability that the property is satisfied when the IMC is working in an unknown environment that satisfies the specification. In this talk we focus on a two-player continuous-time stochastic game model that we call controller-environment games that is the crucial step in the solution of the problem above.

PDF Details

I&C Journal 2013 Journal Article

Continuous-time stochastic games with time-bounded reachability

Tomáš Brázdil
Vojtěch Forejt
Jan Krčál
Jan Křetínský
Antonín Kučera

We study continuous-time stochastic games with time-bounded reachability objectives and time-abstract strategies. 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. Further, we show how to compute ε-optimal strategies in finite games and provide detailed complexity estimations. Moreover, we show how to compute ε-optimal strategies in infinite games with finite branching and bounded rates where the bound as well as the successors of a given state are effectively computable. Finally, we show how to compute optimal strategies in finite uniform games.

Details DOI

Highlights Conference 2013 Conference Abstract

Verification of open interactive Markov chains

Tomáš Brázdil
Holger Hermanns
Jan Krčál
Jan Kretinsky
Vojtĕch Řehák

We provide the first assume-guarantee reasoning for stochastic continuous-time systems. Interactive Markov chains (IMC) are compositional behavioural models similar to continuous-time Markov decision processes. Given a time-bounded property and an IMC component, we synthesize its scheduler optimizing the probability that the property is satisfied when the IMC is working in an unknown environment. We also give a specification formalism for IMC and consider unknown environments satisfying a given specification.

PDF Details