by *
David Šafránek,
Jiří Šimša,
* A full version of SOFSEM 2005 paper. December 2004, 25 pages.

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

A visual formalism called *Visual Coordination Diagrams* (VCD)

by *
Antonín Kučera,
Jan Strejček,
* A full version of the paper presented at Sofsem 2005. December 2004, 22 pages.

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

We give a new characterization of those languages that are definable

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 *
Radek Pelánek,
Jan Strejček,
* September 2004, 26 pages.

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

It is known that Linear Temporal Logic (LTL) has the same expressive power as alternating 1-weak automata (A1W automata, also called alternating linear automata or very weak alternating automata). A translation of LTL formulae

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 *
Tomáš Brázdil,
Antonín Kučera,
Oldřich Stražovský,
* A full version of the paper presented at CONCUR`04. September 2004, 26 pages.

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

We prove that probabilistic bisimilarity is decidable over

by *
Antonín Kučera,
Philippe Schnoebelen,
* A full version of the paper presented at CONCUR`04. June 2004, 32 pages.

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

We introduce a generic family of behavioral relations for which the

by *
Antonín Kučera,
Jan Strejček,
* May 2004, 11 pages.

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

It is known that an LTL property is expressible by an LTL formula

by *
Javier Esparza,
Antonín Kučera,
Richard Mayr,
* A full version of the paper presented at LICS`04. July 2004, 34 pages.

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

We consider the model checking problem for probabilistic pushdown

by *
Mark Kelly,
Václav Matyáš,
Ahmed Patel,
* April 2004, 43 pages.

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

Firewalls act as access control policy mediators between networks.

by *
Antonín Kučera,
Richard Mayr,
* A full version of the paper presented at IFIP TCS 2004. April 2004, 38 pages.

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

We propose a generic method for deciding semantic equivalences