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

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

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.

by *
Florent Peres,
Ivana Černá,
* August 2013, 46 pages.

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

Finding an infinite sequence of transitions (a run) going through some special states (called accepting) is of importance for fields like formal verification. Whereas finding such a sequence as been extensively studied, the problem of *maintaining* this sequence upon changes in the model or the specification has received less attention. In this work, we propose a solution to the maintenance of an accepting run when the transition system representing the product of the model and of the specification is changed, using the Tarjan`s algorithm as a base algorithm.

by *
Nikola Beneš,
Ivana Černá,
Jan Křetínský,
* November 2010, 44 pages.

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

Modal transition systems (MTS) is a well established formalism used for specification and for abstract interpretation. We consider its disjunctive extension (DMTS) and we show that refinement problems for DMTS are not harder than in the case of MTS. There are two main results in the paper. Firstly, we give a solution to the common implementation and specification problems lowering the complexity from EXPTIME to PTIME. Secondly, we identify a fundamental error made in previous attempts at LTL model checking of MTS and provide algorithms for LTL model checking of MTS and DMTS. Moreover, we show how to apply this result to compositional verification and circumvent the general incompleteness of the MTS composition.

by *
Jiří Barnat,
Ivana Černá,
Jana Tůmová,
* June 2009, 35 pages.

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

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

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 *
Pavlína Vařeková,
Ivana Černá,
* A full version of the paper presented at conference CBSE 2008. July 2008, 27 pages.

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

Many real component-based systems, so called Control-User systems, are composed of a stable part (control component) and a number of dynamic components of the same type (user components). Models of these systems are parametrised by the number of user components and thus potentially infinite. Model checking techniques can be used to verify only specific instances of the systems. This paper presents an

by *
Ivana Černá,
Pavlína Vařeková,
Barbora Zimmerová,
* October 2006, 25 pages.

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

The paper introduces a Component-interaction automata language, which was designed for modelling of component interactions in hierarchical component-based software systems. The language supports modelling of important interaction attributes of such systems, and hence provides a rich base for further application of formal methods. Component-interaction automata provide a flexible form of component composition which can respect architectural assembly of the system, communication mechanisms, and other specifics of component-based systems. This allows the language to capture interactions in many different kinds of componentbased systems (built on different component models for instance). This paper provides a detailed study of the language including discussion of its practical application

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 *
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 *
Ivana Černá,
Radek Pelánek,
* April 2003, 18 pages.

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

The hierarchy of properties as overviewed by Manna and Pnueli relates language,

by *
Ivana Černá,
Radek Pelánek,
* December 2002, 24 pages.

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

The fair cycle detection problem is at the heart of both LTL and fair

by *
Ivana Černá,
* August 2002, 105 pages.

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

This volume contains proceedings of

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 *
Ivana Černá,
Jitka Stříbrná,
* December 2000, 26 pages.

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

The purpose of this work is to examine the decidability problem of weak bisimilarity for BPA-processes. It has been known that strong bisimilarity, which may be considered a special case of weak bisimilarity, where the internal (silent) action tau is treated equally to observable actions, is decidable for BPA-processes. For strong bisimilarity, these processes are finitely branching and so for two non-bisimilar processes there exists a level n that distinguishes the two processes. Additionally, from the decidability of whether two processes are equivalent at a given level n, semidecidability of strong non-bisimilarity directly follows. We examine the following two closely related approaches to semidecidability of strong equivalence:

- construction of a (finite) bisimulation or expansion tree,
- construction of a finite Caucal base.

by *
Ivana Černá,
Ondřej Klíma,
Jiří Srba,
* This is a full version of the paper accepted to SOFSEM`99. July 1999, 11 pages.

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

Word equation in a special form X=A, where X is a sequence of variables and A is a sequence of constants, is considered. The problem whether X=A has a solution over a free monoid (PATTERN EQUATION problem) is shown to be NP--complete. It is also shown that disjunction of a special type equation systems and conjunction of the general ones can be eliminated. Finally, the case of stuttering equations where the word identity is read modulo xx=x is mentioned.

by *
Ivana Černá,
Mojmír Křetínský,
Antonín Kučera,
* This is a full version of the paper which is to be presented at CSL`96. June 1996, 28 pages.

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

We compare the classes of behaviours (transition systems) which can be generated by normed BPA_{\tau} and normed BPP_{\tau} processes. We exactly classify the intersection of these two classes, i.e., the class of transition systems which can be equivalently (up to bisimilarity) described by the syntax of normed BPA_{\tau} and normed BPP_{\tau} processes. We provide such a characterisation for classes of normed BPA and normed BPP processes as well.

Next we show that it is decidable in polynomial time whether for a given normed BPA_{\tau} (or BPP_{\tau} respectively) process X there is some (unspecified) normed BPP_{\tau} (or BPA_{\tau} respectively) process X` such that X is bisimilar to X`. Moreover, if the answer is positive then our algorithms also construct the process X`. Simplified versions of the algorithms mentioned above for normed BPA and normed BPP are given too.

As an immediate (but important) consequence we also obtain the decidability of bisimilarity in the union of normed BPA_{\tau} and normed BPP_{\tau} processes.