Search

We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the model-checking problem is undecidable, but we show that decidability can be recovered by considering flat Kripke structures where each state belongs to at most one simple loop. Most decision procedures are based on results on (flat) counter systems where counters are used to implement the evaluation of counting operators., Comment: Extended version providing an additional appendix

Context-free processes (BPA) have been used for dataflow analysis in recursive procedures with applications in optimizing compilers (Proceedings of FOSSaCS’99, Lecture Notes in Computer Science, Vol. 1578, Springer, Berlin, 1999, pp. 14–30). We introduce a more refined model called BPA(Z) that can model not only recursive dependencies, but also the passing of an integer parameter to a subroutine. Moreover, this parameter can be tested against conditions expressible in Presburger arithmetic. This new and more expressive model can still be analyzed automatically. We define Z-input 1-CM, a new class of 1-counter machines (cm) that take integer numbers as input, to describe sets of configurations of BPA(Z). We show that the Post∗ (the set of successors) of a set of BPA(Z)-configurations described by a Z-input 1-CM can be effectively constructed. The Pre∗ (set of predecessors) of a regular set can be effectively constructed as well. However, the Pre∗ of a set described by a Z-input 1-CM cannot be represented by a Z-input 1-CM, in general, and has an undecidable membership problem. Then we develop a new temporal logic based on reversal-bounded counter machines (i.e. machines which use counters such that the change between increasing and decreasing mode of each counter is bounded (J. Assoc. Comput. Mach. 25 (1978) 116) that can be used to describe properties of BPA(Z) and show that the model-checking problem is decidable.

International audience; This paper describes an effective verification procedure for imperative programs that handle (balanced) tree-like data structures. Since the verification problem considered is undecidable, we appeal to a classical semi-algorithmic approach in which the user has to provide manually the loop invariants in order to check the validity of Hoare triples of the form {P}C{Q}, where P, Q are the sets of states corresponding to the pre- and post-conditions, and C is the program to be verified. We specify the sets of states (representing tree-like memory configurations) using a special class of tree automata named Tree Automata with Size Constraints (TASC). The main advantage of using TASC in program specifications is that they recognize non-regular sets of tree languages such as the AVL trees, the red-black trees, and in general, specifications involving arithmetic reasoning about the lengths (depths) of various (possibly all) paths in the tree. The class of TASC is closed under the operations of union, intersection and complement, and moreover, the emptiness problem is decidable, which makes it a practical verification tool. We validate our approach considering red-black trees and the insertion procedure, for which we verify that the output of the insertion algorithm is a {\em balanced} red-black tree, i.e. the longest path is at most twice as long as the shortest path.

International audience; Regular (tree) model checking (RMC) is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word or tree automata, and operations of the systems being examined as finite word or tree transducers. The reachability set is then computed by a repeated application of the transducers on the automata representing the currently known set of reachable configurations. In order to facilitate termination of RMC, various acceleration schemas have been proposed. One of them is a combination of RMC with the abstract-check-refine paradigm yielding the so-called abstract regular model checking (ARMC). ARMC has originally been proposed for word automata and transducers only and thus for dealing with systems with linear (or easily linearisable) structure. In this paper, we propose a generalisation of ARMC to the case of dealing with trees which arise naturally in a lot of modelling and verification contexts. In particular, we first propose abstractions of tree automata based on collapsing their states having an equal language of trees up to some bounded height. Then, we propose an abstraction based on collapsing states having a non-empty intersection (and thus "satisfying") the same bottom-up tree "predicate" languages. Finally, we show on several examples that the methods we propose give us very encouraging verification results.

International audience; In [22], it was shown that MSO logic for ordered unranked trees becomes undecidable if Presburger constraints are allowed at children of nodes. We now show that a decidable logic is obtained if we use a a modal fixpoint logic instead. We present an automata theoretic characterization of this logic by means of deterministic Pres-burger tree automata (PTA) and show how it can be used to express numerical document queries. Surprisingly, the complexity of satisfiability for the extended logic is asymptotically the same as for the original logic. The non-emptiness for PTAs is in general pspace-complete which is moderate given that it is already pspace-hard to test whether the complement of a regular expression is non-empty. We also identify a subclass of PTAs with a tractable non-emptiness problem. Further, to decide whether a tree t satisfies a formula $\phi$ is polynomial in the size of $\phi$ and linear in the size of t. A technical construction of independent interest is a linear time construction of a Presburger formula for the Parikh set of a finite automaton.

International audience; We propose abstract regular model checking as a new generic technique for verification of parametric and infinite-state systems. The technique combines the two approaches of regular model checking and verification by abstraction. We propose a general framework of the method as well as several concrete ways of abstracting automata or transducers, which we use for modelling systems and encoding sets of their states as usual in regular model checking. The abstraction is based on collapsing states of automata (or transducers) and its precision is being incrementally adjusted by analysing spurious counterexamples. We illustrate the technique on verification of a wide range of systems including a novel application of automata-based techniques to an example of systems with dynamic linked data structures

International audience; We consider the verification of non-recursive C programs manipulating dynamic linked data structures with possibly several next pointer selectors and with finite domain non-pointer data. We aim at checking basic memory consistency properties (no null pointer assignments, etc.) and shape invariants whose violation can be expressed in an existential fragment of a first order logic over graphs. We formalise this fragment as a logic for specifying bad memory patterns whose formulae may be translated to testers written in C that can be attached to the program, thus reducing the verification problem considered to checking reachability of an error control line. We encode configurations of programs, which are essentially shape graphs, in an original way as extended tree automata and we represent program statements by tree transducers. Then, we use the abstract regular tree model checking framework for a fully automated verification. The method has been implemented and successfully applied on several case studies.

International audience; This paper addresses the problem of parametric verification for a class of concurrent systems with resource sharing. The systems are composed of a parametric number of finite-state processes that are competing for exclusive access to a finite number of resources. Their access to resources is managed by a locker according to a FIFO policy distinguishing low-priority and high-priority resource requests. For such systems, we define a model based on automata with queues recording for each resource the identities of the waiting processes. Then, we address the parametric verification problem for the proposed model and the temporal logic LTL\X with global process quantification. We consider two different interpretation domains for the logic, namely the sets of finite and fair behaviours. In addition, we consider parametric verification of process deadlockability too. We establish several decidability results for different classes of the considered systems and properties by reducing their parametric verification problems to (finite-state) model-checking problems with finite numbers of processes.