- e-mail:
- brim(a)fi.muni.cz
- home page:
- http://www.fi.muni.cz/usr/brim/

by *
Jiří Barnat,
Petr Bauch,
Luboš Brim,
Milan Češka,
* July 2010, 24 pages.

**FIMU-RS-2010-10.**
Available as *Postscript*,
**PDF**.

The problem of decomposition of a directed graph into its strongly connected

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,
Milan Češka,
Tomáš Lamr,
* June 2009, 18 pages.

**FIMU-RS-2009-05.**
Available as *Postscript*,
**PDF**.

Recent technological developments made available various many-core hardware platforms. For example,

by *
Nikola Beneš,
Luboš Brim,
Ivana Černá,
Jiří Sochor,
Pavlína Vařeková,
Barbora Zimmerová,
* July 2008, 21 pages.

**FIMU-RS-2008-07.**
Available as *Postscript*,
**PDF**.

Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL incorporates both states and events to express important properties of component-based software systems.

by *
Jiří Barnat,
Luboš Brim,
Pavel Šimeček,
* January 2007, 20 pages.

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

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.

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

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.

by *
Luboš Brim,
Ivana Černá,
Pavel Moravec,
Jiří Šimša,
* A full version of the paper submitted to conference CAV05 February 2005, 21 pages.

**FIMU-RS-2005-04.**
Available as *Postscript*,
**PDF**.

We propose a new on-the-fly approach which combines partial order reduction with the under-approximation technique for falsification and verification of LTL-X properties. It uses sensitivity relation and modified ample conditions to generate a reduced state space that is not fully stutter equivalent to the original one and it checks the desired property using representatives. Widening of under-approximations is fully automatic and does not rely on any supporting mechanisms like theorem-provers or SAT solvers.

by *
Luboš Brim,
Ivana Černá,
Pavel Moravec,
Jiří Šimša,
* A full version of the paper accepted to the conference FMCAD 2004. November 2004, 22 pages.

**FIMU-RS-2004-09.**
Available as *Postscript*,
**PDF**.

We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations communicating via MPI. The detection of accepting cycles is based on computing maximal accepting predecessors and the subsequent decomposition of the graph into independent predecessor subgraphs induced by maximal accepting predecessors. Several optimizations of the basic algorithm are presented and the influence of the ordering on the algorithm performance is discussed. Experimental implementation of the algorithm shows promising results.

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.

by *
Luboš Brim,
Ivana Černá,
Lukáš Hejtmánek,
* This is a full version of the paper presented at PARCO 2003. July 2003, 14 pages.

**FIMU-RS-2003-04.**
Available as *Postscript*,
**PDF**.

Several new parallel algorithms for the single source shortest paths

by *
Luboš Brim,
Jitka Crhová,
Karen Yorav,
* This is a full version of the paper presented at PDMC`02. October 2002, 22 pages.

**FIMU-RS-2002-08.**
Available as *Postscript*,
**PDF**.

In this work we discuss the problem of performing distributed CTL model

by *
Luboš Brim,
Ivana Černá,
Pavel Krčál,
Radek Pelánek,
* This is a full version of the paper presented at SOFSEM 2001. November 2001, 22 pages.

**FIMU-RS-2001-09.**
Available as *Postscript*,
**PDF**.

A distributed algorithm for the single-source shortest path problem for directed graphs with arbitrary edge lengths is proposed. The new algorithm is based on relaxations and uses reverse search for inspecting edges and thus avoids using any additional data structures. At the same time the algorithm uses a novel way to recognize a reachable negative-length cycle in the graph which facilitates the scalability of the algorithm.

by *
Luboš Brim,
Ivana Černá,
Pavel Krčál,
Radek Pelánek,
* This is a full version of the paper presented at FST&TCS 2001. May 2001, 19 pages.

**FIMU-RS-2001-01.**
Available as *Postscript*,
**PDF**.

A distributed algorithm for single source shortest path

by *
Jiří Barnat,
Luboš Brim,
Jitka Stříbrná,
* December 2000, 19 pages.

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

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.

by *
Jean-Marie Jacquet,
Luboš Brim,
David Gilbert,
Mojmír Křetínský,
* December 1999, 62 pages.

**FIMU-RS-99-08.**
Available as *Postscript*,
**PDF**.

Concurrent constraint programming is classically based on asynchronous communication via a shared store. In previous work, we presented a new version of the ask and tell primitives which features synchronicity, our approach being based on the idea of telling new information just in the case that a concurrently running process is asking for it. We turn in this paper to a semantic study of this new framework, called Scc.

It is first shown to be different in nature from classical concurrent constraint programming and from CCS, a classical reference in traditional concurrency theory. This suggests the interest of new semantics for Scc. To that end, an operational semantics reporting the steps of the computations is presented. A denotational semantics is then proposed. It uses monotonic sequences of labelled pairs of input-output states, possibly containing gaps, and ending - according to the logic programming tradition - with marks reporting success or failure. This denotational semantics is proved to be correct with respect to the operational semantics as well as fully abstract.