# Technical Reports

## A List by Author: Ivana Černá

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

### On Clock-Aware LTL Properties of Timed Automata

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

#### Abstract:

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.

### Dynamic maintenance of an accepting run

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

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

#### Abstract:

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.

### Disjunctive Modal Transition Systems and Generalized LTL Model Checking

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

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

#### Abstract:

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.

### Quantitative Model Checking of Systems with Degradation (Full Paper).

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

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

#### Abstract:

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

### Partial Order Reduction for State/Event LTL

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

#### Abstract:

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.

### Model Checking of Control-User Component-Based Parametrised 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**.

#### Abstract:

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

### Component-Interaction Automata Modelling Language

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

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

#### Abstract:

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

### Distributed Qualitative LTL Model Checking of Markov Decision Processes

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

#### Abstract:

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.

### Under-Approximation Generation using Partial Order Reduction

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

#### Abstract:

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.

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

### Parallel Algorithms for Detection of Negative Cycles

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

#### Abstract:

Several new parallel algorithms for the single source shortest paths

### Relating Hierarchy of Linear Temporal Properties to Model Checking

by *
Ivana Černá,
Radek Pelánek,
* April 2003, 18 pages.

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

#### Abstract:

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

### Distributed Explicit Fair Cycle Detection: Set Based Approach

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

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

#### Abstract:

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

### Proceedings of Tools Day

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

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

#### Abstract:

This volume contains proceedings of

### How to Employ Reverse Search in Distributed Single Source Shortest Paths

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

#### Abstract:

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.

### Distributed Shortest Paths for Directed Graphs with Negative Edge Lengths

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

#### Abstract:

A distributed algorithm for single source shortest path

### Some Remarks on Weak Bisimilarity of BPA-Processes

by *
Ivana Černá,
Jitka Stříbrná,
* December 2000, 26 pages.

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

#### Abstract:

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.

### On the Pattern Equations

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

#### Abstract:

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.

### Comparing Expressibility of Normed BPA and Normed BPP Processes

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

#### Abstract:

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.

Responsible contact: unixfimunicz