Technical Reports

A List by Author: Ivana Èerná

e-mail:

cerna(a)fi.muni.cz

home page:

https://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 automaton may be infinite, which we deal with by introducing a normal form of the Büchi automata and normalizing procedure. We also show that the newly introduced formalism can be used to distinguish MDPs indistinguishable by any LTL, PCTL or even PCTL* formula.

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.

The main contribution of the paper is a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.

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 algorithmic technique for verification of safety interaction properties of Control-User systems. The core of our verification method is a computation of a cutoff. If the system is proved to be correct for every number of user components lower than the cutoff then it is correct for any number of users. We present an on-the-fly model checking algorithm which integrates computation of a cutoff with the verification itself. Symmetry reduction can be applied during the verification to tackle the state explosion of the model. Applying the algorithm we verify models of several previously published component-based systems.

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 and comparison with related work. We intend to use this language as a framework for verifying coordination errors, checking of reconfiguration correctness, and formal analysis of component interactions in component-based systems, which is our ongoing and future work.

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 and for the negative cycle detection problems on directed graphs with real edge weights and given by adjacency list are developed, analysed, and experimentally compared. The algorithms are to be performed on clusters of workstations that communicate via a message passing mechanism.

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, topology, omega-automata, and linear temporal logic classifications of properties. We provide new characterisations of this hierarchy in terms of automata with Buchi, co-Buchi, and Streett acceptance condition and in terms of Until-Release alternation hierarchy. Afterwards, we analyse the complex ity of the model checking problem for particular classes of the hierarchy and thanks to the new characterisations we identify those linear time temporal properties for which the model checking problem can be solved more efficiently than in the general case.

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 CTL model checking. This paper presents a new distributed scalable algorithm for explicit fair cycle detection. Our method combines the simplicity of the distribution of explicitly presented data structure and the features of symbolic algorithm allowing for an efficient parallelisation. If a fair cycle (i.e. counterexample) is detected, then the algorithm produces a cycle, which is in general shorter than that produced by depth-first search based algorithms. Experimental results confirm that our approach outperforms that based on a direct implementation of the best sequential algorithm.

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 Tools Day, which was held as an affiliated event of CONCUR 2002 on August 24, 2002 in Brno, Czech Republic.

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 problem in an arbitrary directed graph which can contain negative length cycles is presented. The new algorithm is a label-correcting one and uses a novel way for detection of negative length cycles. It works on a network of processors with disjoint memory that communicate via message passing. Correctness of the algorithm is proved. The algorithm is work-efficient as its worst time complexity is O(n^3/p), where p is the number of processors.

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:

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

We have attempted to find out if any of the above mentioned approaches could be generalized to (semi)decide weak bisimilarity. Our findings indicate that a direct generalization is not sufficient and an efficient (semi)decision procedure cannot be obtained in this way.

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.