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.
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
by Lubo¹ Brim, Jakub Chaloupka, March 2010, 48 pages.
FIMU-RS-2010-03. Available as Postscript, PDF.
We design a novel algorithm for solving Mean-Payoff Games
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 Jiųķ Barnat, Lubo¹ Brim, Jakub Chaloupka, September 2004, 57 pages.
FIMU-RS-2004-07. Available as Postscript, PDF.
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.