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 described behaviours, and are often considered as a design error. While there is a quadratic-time algorithm detecting races in Basic Message Sequence Charts (BMSCs), the problem is undecidable for High-level Message Sequence Charts (HMSCs). To improve this negative situation for HMSCs, we introduce two new notions: a new concept of race called trace-race and an extension of the HMSC formalism with open coregions, i.e. coregions that can extend over more than one BMSC. We present three arguments showing benefits of our notions over the standard notions of race and HMSC. First, every trace-race-free HMSC is also race-free. Second, every race-free HMSC can be equivalently expressed as a trace-race-free HMSC with open coregions. Last, the trace-race detection problem for HMSC with open coregions is decidable and PSPACE-complete (the problem is in P if the number of processes and gates is fixed).

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

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. We study the computation of both the distribution of the memory consumption and its expectation. For the distribution, we show that a naive method incurs an exponential blow-up, and that it can be avoided using linear equation systems. We also suggest a possibly even faster approximation method. Given epsilon>0, these methods allow to compute bounds on the memory consumption that are exceeded with a probability of at most epsilon. For the expected memory consumption, we show that whether it is infinite can be decided in polynomial time for stateless pPDA (pBPA) and in polynomial space for pPDA. We also provide an iterative method for approximating the expectation. We show how to compute error bounds of our approximation method and analyze its convergence speed. We prove that our method converges linearly, i.e., the number of accurate bits of the approximation is a linear function of the number of iterations.

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, a SIMD-like hardware architecture became easily accessible for many users who have their computers equipped with modern NVIDIA GPU cards with CUDA technology. In this paper we redesign the maximal accepting predecessors algorithm [7] for LTL model checking in terms of matrix-vector product in order to accelerate LTL model checking on many-core GPU platforms. Our experiments demonstrate that using the NVIDIA CUDA technology results in a significant computation speedup.

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 automaton may be infinite, which we deal with by introducing a normal form of the Büchi automata and normalizing procedure. We also show that the newly introduced formalism can be used to distinguish MDPs indistinguishable by any LTL, PCTL or even PCTL* formula.

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 formalism introduced more than 20 years ago, has recently received a considerable attention in several different areas. Many of the fundamental questions related to MTSs have already been answered. However, the problem of the exact computational complexity of thorough refinement checking between two finite MTSs remained unsolved.

We settle down this question by showing EXPTIME-completeness of thorough refinement checking on finite MTSs. The upper-bound result relies on a novel algorithm running in single exponential time providing a direct goal-oriented way to decide thorough refinement. If the right-hand side MTS is moreover deterministic, or has a fixed size, the running time of the algorithm becomes polynomial. The lower-bound proof is achieved by reduction from the acceptance problem of alternating linear bounded automata and the problem remains EXPTIME-hard even if the left-hand side MTS is fixed.

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 on a concept of a verification manager. The manager automates some step of the verification process and enables efficient parallel combination of different verification techniques. We describe a realization of this concept for explicit model checking and discuss practical experience. Particularly, we discuss the problem of selection of input problems for evaluation of this kind of tool.

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 automata (or, equivalently, 1-exit recursive state machines), where the winning objective is specified by a regular set of target configurations and a qualitative probability constraint ‘>0’ or ‘=1’. The goal of one player is to maximize the probability of reaching the target set so that the constraint is satisfied, while the other player aims at the opposite. We show that the winner in such games can be determined in NP intersection co-NP. Further, we prove that the winning regions for both players are regular, and we design algorithms which compute the associated finite-state automata. Finally, we show that winning strategies can be synthesized effectively.