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

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

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

In contrast to the usual understanding of probabilistic systems as

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 *
Nikola Beneš,
Jan Křetínský,
* A full version of the paper presented at ICTAC 2012. June 2012, 25 pages.

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

We consider modal transition systems with infinite state space generated by finite sets of rules. In particular, we extend process rewrite systems to the modal setting and investigate decidability of the modal refinement relation between systems from various subclasses. Since already simulation is undecidable for most of the cases, we focus on the case where either the refined or the refining process is finite. Namely, we show decidability for pushdown automata extending the non-modal case and surprising undecidability for basic parallel processes. Further, we prove decidability when both systems are visibly pushdown automata. For the decidable cases, we also provide complexities. Finally, we discuss a notion of bisimulation over MTS.

by *
Nikola Beneš,
Jan Křetínský,
Kim Guldstrand Larsen,
Mikael Moeller,
Jiří Srba,
* A full version of the paper presented at conference LPAR 2012. January 2012, 23 pages.

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

Modal transition systems are a well-established specification formalism for a high-level modelling of component-based software systems. We present a novel extension of the formalism called modal transition systems with durations where time durations are modelled as controllable or uncontrollable intervals. We further equip the model with two kinds of quantitative aspects: each action has its own running cost per time unit, and actions may require several hardware components of different costs. We ask the question, given a fixed budget for the hardware components, what is the implementation with the cheapest long-run average reward. We give an algorithm for computing such optimal implementations via a reduction to a new extension of mean payoff games with time durations and analyse the complexity of the algorithm.

by *
Nikola Beneš,
Jan Křetínský,
Kim Guldstrand Larsen,
Mikael Moller,
Jiří Srba,
* A full version of the paper presented at ATVA 2011 July 2011, 24 pages.

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

Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently

by *
Nikola Beneš,
Ivana Černá,
Jan Křetínský,
* November 2010, 44 pages.

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

Modal transition systems (MTS) is a well established formalism used for specification and for abstract interpretation. We consider its disjunctive extension (DMTS) and we show that refinement problems for DMTS are not harder than in the case of MTS. There are two main results in the paper. Firstly, we give a solution to the common implementation and specification problems lowering the complexity from EXPTIME to PTIME. Secondly, we identify a fundamental error made in previous attempts at LTL model checking of MTS and provide algorithms for LTL model checking of MTS and DMTS. Moreover, we show how to apply this result to compositional verification and circumvent the general incompleteness of the MTS composition.

by *
Nikola Beneš,
Jan Křetínský,
* A full version of the paper presented at MEMICS 2010. September 2010, 15 pages.

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

The formalism of modal transition systems (MTS) is a well established framework for systems specification as well as abstract interpretation. Nevertheless, due to incapability to capture some useful features, various extensions have been studied, such as e.g. mixed transition systems or disjunctive MTS. Thus a need to compare them has emerged.

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,
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 *
Nikola Beneš,
Jan Křetínský,
Kim Guldstrand Larsen,
Jiří Srba,
* A full version of the paper presented at conference ICTAC 2009. July 2009, 28 pages.

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

Modal transition systems (MTS), a specification

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