VCD: A Visual Formalism for Specification of Heterogeneous Software Architectures

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) for high-level design of heterogeneous systems is presented in this paper. The language is based on a state-transition operational semantics, which allows application of formal methods to software design. Formal definition of VCD is included in the paper. Moreover, an example of use of the language is also given.

Characteristic Patterns for LTL

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 in fragments of LTL where the nesting depths of X and U modalities are bounded by given constants. This brings further results about various LTL fragments. We also propose a generic method for decomposing LTL formulae into an equivalent disjunction of ``semantically refined" LTL formulae, and indicate how this result can be used to improve the functionality of existing LTL model-checkers.

Accepting Predecessors are Better than Back Edges in Distributed LTL Model Checking

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.

Deeper Connections between LTL and Alternating Automata

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 into a language equivalent A1W automata has been introduced in [MSS88]. The inverse translation has been developed independently in [Roh97] and [LT00]. We improve the latter translation and present deeper connections between LTL and A1W automata. Using these translations we identify the classes of A1W automata equivalent to LTL fragments given by bounds on nesting depths of temporal operators (see, e.g., [Wil99,KS02]) and the fragments of Until-Release hierarchy [CP03].

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.


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.

Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems

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 probabilistic extensions of BPA and BPP processes. For normed subclasses of probabilistic BPA and BPP processes we obtain polynomial-time algorithms. Further, we show that probabilistic bisimilarity between probabilistic pushdown automata and finite-state systems is decidable in exponential time. If the number of control states in PDA is bounded by a fixed constant, then the algorithm needs only polynomial time.

A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications

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 problem of comparing an arbitrary transition system to some finite-state specification can be reduced to a model checking problem against simple modal formulae. As an application, we derive decidability of several regular equivalence problems for well-known families of infinite-state systems.

An Effective Characterization of Properties Definable by LTL Formulae with a Bounded Nesting Depth of the Next-Time Operator

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 without any next-time operator if and only if the property is stutter invariant. It is also known that the problem whether a given LTL property is stutter invariant is PSPACE-complete. We extend these results to fragments of LTL obtained by restricting the nesting depth of the next-time operator to a given n. Some interesting facts about the logic LTL follow as simple corollaries.

Model Checking Probabilistic Pushdown Automata

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 automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model checking for this class of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for general PCTL and the subclass of stateless pPDA. Finally, we consider the class of properties definable by deterministic Buchi automata, and show that both qualitative and quantitative model checking for pPDA is decidable.

Application-Level Firewall Protection Profile for High Robustness Environments-Initial Considerations

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. They either permit or block the exchange of data between networks. The ability to permit or block the transfer of data means firewalls can be used to selectively allow access to the resources it protects. Firewalls of varying security levels have been created to provide security that is adequate to the sensitivity of the data being protected. Firewalls are often formally evaluated to certify what level of security they are suitable for. They are evaluated against so-called security evaluation criteria -- standardised descriptions of security measures. Common Criteria (CC) is the current global standard for evaluations. Firewall security attributes are described in a Protection Profile (PP) that defines an implementation-independent set of security requirements and objectives for a category of products or systems that meet similar consumers needs for IT security. Our project set out to produce a summary of security issues for an Application-Level Firewall Protection Profile (PP) for a High Robustness Environment. We started our work with the Basic-Level Firewall PP, the Medium-Level Firewall PP and the High-Level Mail Guard PP. The two firewall PPs and the Mail Guard PP are compared to give an insight into what the issues concerning the High-Level Firewall PP are. This High-Level Firewall PP is then discussed in terms of its major principles.

A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata

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 between pushdown automata and finite-state automata. The abstract part of the method is applicable to every process equivalence which is a right PDA congruence. Practical usability of the method is demonstrated on selected equivalences which are conceptual representatives of the whole spectrum. In particular, special attention is devoted to bisimulation-like equivalences (including weak, early, delay, branching, and probabilistic bisimilarity), and it is also shown how the method applies to simulation-like and trace-like equivalences. The generality does not lead to the loss of efficiency; the algorithms obtained by applying our method are essentially time-optimal and sometimes even polynomial. The list of particular results obtained by our method includes items which are first of their kind.