Technical Reports

A List by Author: Jiøí Barnat

e-mail:

xbarnat(a)fi.muni.cz

home page:

https://www.fi.muni.cz/~xbarnat

On Clock-Aware LTL Properties of Timed Automata

by Peter Bezdìk, Nikola Bene¹, Vojtìch Havel, Jiøí Barnat, Ivana Èerná, A full version of the paper presented at conference ICTAC 2014. June 2014, 27 pages.

FIMU-RS-2014-04. Available as Postscript, PDF.

Abstract:

We introduce the Clock-Aware Linear Temporal Logic (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a~timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed Büchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique.

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.

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.

LTL model checking with I/O-Efficient Accepting Cycle Detection

by Jiøí Barnat, Lubo¹ Brim, Pavel ©imeèek, January 2007, 20 pages.

FIMU-RS-2007-01. Available as Postscript, PDF.

Abstract:

We show how to adopt existing non-DFS-based algorithm OWCTY for accepting cycle detection to the I/O efficient setting and compare the I/O efficiency and practical performance of the adopted algorithm to the existing I/O efficient LTL model checking approach of Edelkamp et al. We show that while the new algorithm exhibits similar I/O complexity with respect to the size of the graph, it avoids the quadratic increase in the size of the graph of the approach of Edelkamp et al. Therefore, the absolute numbers of I/O operations are significantly smaller and the algorithm exhibits better practical performance.

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.

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.

Distributed LTL Model-Checking in SPIN

by Jiøí Barnat, Lubo¹ Brim, Jitka Støíbrná, December 2000, 19 pages.

FIMU-RS-2000-10. Available as Postscript, PDF.

Abstract:

Distributed version of the SPIN model checker has not been extended to allow distributed model-checking of LTL formulas. This paper explores the possibility of performing nested depth first search algorithm in distributed SPIN. A distributed version of the algorithm is presented, and its complexity is discussed.