by *
Matej Kollár,
Ondřej Peterka,
Ondřej Ryšavý,
Libor Škarvada,
* November 2009, 17 pages.

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

This report deals with a type system that merges subtyping and dependent types. We define a calculus that instead of term overloading employs coercion mappings. This enables to detach the subtyping from other parts of the calculus, so that the mutual dependence between subtyping, typing and kinding can be reduced. We analyze basic properties of the calculus and show several examples that demonstrate the mechanism of coercive subtyping.

by *
Vojtěch Řehák,
Petr Slovák,
Jan Strejček,
Loic Hélouet,
* December 2009, 30 pages.

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

Races in Message Sequence Charts may lead to a bad interpretation of

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 *
Jakub Chaloupka,
Luboš Brim,
* October 2009, 11 pages.

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

We study some existing techniques for solving mean-payoff games (MPGs), improve them, and design a randomized algorithm for solving MPGs with currently the best expected complexity.

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

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.

by *
Joakim Byg,
Kenneth Yrke Joergensen,
Jiří Srba,
* A full version of the paper presented at ICFEM`09. October 2009, 29 pages.

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

Bounded timed-arc Petri nets with read-arcs were recently proven equivalent to net- works of timed automata, though the Petri net model cannot express urgent be- haviour and the described mutual translations are rather inefficient. We propose an extension of timed-arc Petri nets with invariants to enforce urgency and with transport arcs to generalise the read-arcs. We also describe a novel translation from the extended timed-arc Petri net model to networks of timed automata. The trans- lation is implemented in the tool TAPAAL and it uses UPPAAL as the verification engine. Our experiments confirm the efficiency of the translation and in some cases the translated models verify significantly faster than the native UPPAAL models do.

by *
Jiří Barnat,
Luboš Brim,
Milan Češka,
Tomáš Lamr,
* June 2009, 18 pages.

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

Recent technological developments made available various many-core hardware platforms. For example,

by *
Jiří Barnat,
Ivana Černá,
Jana Tůmová,
* June 2009, 35 pages.

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

In this paper we describe a rather specialized quality of a system -- the degradation. We demonstrate systems that naturally incorporate degradation phenomenon and we show how these systems can be verified by adapting the standard automatabased approach to LTL model checking. We introduce Büchi Automata with Degradation Constraints (BADCs) to specify the desired properties of systems with degradation and we describe how these can be used for verification. A major obstacle in the verification process is that the synchronous product of the system and the Büchi

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 *
Radek Pelánek,
Václav Rosecký,
* March 2009, 17 pages.

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

Although model checking is usually described as an automatic technique, the verification process with the use of model checker is far from being fully automatic. With the aim of automating the verification process, we elaborate

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

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