Technical Reports
A List by Author: Milan Češka
- e-mail:
- xceska(a)fi.muni.cz
Computing Strongly Connected Components in Parallel on CUDA (full version)
by Jiří Barnat, Petr Bauch, Luboš Brim, Milan Češka, July 2010, 24 pages.
FIMU-RS-2010-10. Available as Postscript, PDF.
Abstract:
The problem of decomposition of a directed graph into its strongly connected
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,
Distributed Qualitative LTL Model Checking of Markov Decision Processes
by Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, Jana Tůmová, September 2006, 19 pages.
FIMU-RS-2006-04. Available as Postscript, PDF.
Abstract:
Probabilistic processes are used to model concurrent programs that exhibit uncertainty. The state explosion problem for probabilistic systems is more critical than in the non-probabilistic case. In the paper we propose a cluster-based algorithm for qualitative LTL model checking of finite state Markov decision processes. We use the automata approach which reduces the model checking problem to the question of existence of an accepting end component. The algorithm uses repeated reachability which systematically eliminates states that cannot belong to any accepting end component. A distinguished feature of the distributed algorithm is that its complexity meets the complexity of the best known sequential algorithm.
Responsible contact:
vedaXDjbU2LSW@fiQ1T5fpnNE.muni8CVI=SRv5.cz
Please install a newer browser for this site to function properly.