## 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
components is a fundamental graph problem inherently present in many
scientific and commercial applications. In this paper we show how existing
parallel algorithms can be reformulated in order to be accelerated by NVIDIA
CUDA technology. In particular, we design a new CUDA-aware procedure for pivot
selection and we redesign the parallel algorithms in order to allow for CUDA
accelerated computation. We also experimentally demonstrate that with a single
GTX 280 GPU card we can easily outperform optimal serial CPU implementation,
which is particularly interesting result as unlike the serial CPU case, the
asymptotic complexity of the parallel algorithms is not optimal.

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

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