Technical Reports

A List by Author: Jakub Chaloupka

e-mail:

xchalou1(a)fi.muni.cz

Z-reachability Problem for Games on 2-dimensional Vector Addition Systems with States is in P

by Jakub Chaloupka, A full version of the paper presented at Workshop on Reachability Problems 2010 August 2010, 36 pages.

FIMU-RS-2010-06. Available as Postscript, PDF.

Abstract:

We consider a two-player infinite game with zero-reachability objectives played on a 2-dimensional vector addition system with states (VASS), the states of which are divided between the two players. Brázdil, Janèar, and Kuèera (2010) have shown that for k > 0, deciding the winner in a game on k-dimensional VASS is in (k-1)-EXPTIME. In this paper, we show that, for k = 2, the problem is in P, and thus improve the EXPTIME upper bound.

Using Strategy Improvement to Stay Alive

by Lubo¹ Brim, Jakub Chaloupka, March 2010, 48 pages.

FIMU-RS-2010-03. Available as Postscript, PDF.

Abstract:

We design a novel algorithm for solving Mean-Payoff Games (MPGs). Besides solving an MPG in the usual sense, our algorithm computes more information about the game, information that is important with respect to applications. The weights of the edges of an MPG can be thought of as a gained/consumed energy -- depending on the sign. For each vertex, our algorithm computes the minimum amount of initial energy that is sufficient for player Max to ensure that in a play starting from the vertex, the energy level never goes below zero. Our algorithm is not the first algorithm that computes the minimum sufficient initial energies, but according to our experimental study it is the fastest algorithm that computes them. The reason is that it utilizes the strategy improvement technique which is very efficient in practice.

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.

Distributed Memory LTL Model Checking Based on Breadth First Search

by Jiøí Barnat, Lubo¹ Brim, Jakub Chaloupka, September 2004, 57 pages.

FIMU-RS-2004-07. Available as Postscript, PDF.

Abstract:

We propose a parallel distributed memory on-the-fly algorithm for enumerative LTL model checking. The algorithm is designed for network of workstations communicating via MPI. The detection of cycles (faulty runs) effectively employs the so called back-level edges. In particular, a parallel level synchronized breadth first search of the graph is performed to discover all back-level edges and for each level the back-level edges are checked in parallel by a nested search procedure to confirm or refute the presence of a cycle. Several optimizations of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed. Experimental evaluation of the algorithm is presented.