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.