Technical Reports
A list with abstracts sorted by year - 2004
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.
Abstract:
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.
Abstract:
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.
Abstract:
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.
Abstract:
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.
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.
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.
Abstract:
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.
Abstract:
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.
Abstract:
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.
Abstract:
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.
Abstract:
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.
Abstract:
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.
