# Technical Reports

## A list with abstracts sorted by year - 2009

### A Calculus of Coercive Subtyping

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

#### Abstract:

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.

### Decidable Race Condition for HMSC

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

#### Abstract:

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

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

### Faster Algorithm for Mean-Payoff Games

by *
Jakub Chaloupka,
Luboš Brim,
* October 2009, 11 pages.

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

#### Abstract:

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.

### On the Memory Consumption of Probabilistic Pushdown Automata

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

#### Abstract:

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.

### An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata

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

#### Abstract:

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.

### CUDA accelerated LTL Model Checking

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

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

#### Abstract:

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

### Quantitative Model Checking of Systems with Degradation (Full Paper).

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

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

#### Abstract:

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

### Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete

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

#### Abstract:

Modal transition systems (MTS), a specification

### Verification Manager: Automating the Verification Process

by *
Radek Pelánek,
Václav Rosecký,
* March 2009, 17 pages.

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

#### Abstract:

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

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

Responsible contact: unixfimunicz