Model checking is a powerful technique for analyzing reach ability and temporal properties of finite state systems. Model-checking finite state systems has been well-studied and there are well known efficient algorithms for this problem. However these algorithms may not terminate when applied directly to in finite state systems. Counter systems are a class of in fininite state systems where the domain of counter values is possibly in finite. Many practical systems like cache coherence protocols, broadcast protocols etc, can naturally be modeled as counter systems. In this thesis we identify a class of counter systems, and propose a new technique to check whether a system from this class satires’ a given CTL formula. The key novelty of our approach is a way to use existing reach ability analysis techniques to answer both \until" and \global" properties; also our technique for \global" properties is different from previous techniques that work on other classes of counter systems, as well as other classes of in finite state systems. We also provide some results by applying our approach to several natural examples, which illustrates the scope of our approach.

Model checking is a fully-automatic formal verification method that has been extremely successful in validating and verifying safety-critical systems in the past three decades. In the past fifteen years, there has been a lot of work in extending many model checking algorithms over finite-state systems to finitely representable infinitestate systems. Unlike in the case of finite systems, decidability can easily become a problem in the case of infinite-state model checking. In this thesis, we present generic and specific techniques that can be used to derive decidability with near-optimal computational complexity for various model checking problems over infinite-state systems. Generic techniques and specific techniques primarily differ in the way in which a decidability result is derived. Generic techniques is a “top-down” approach wherein we start with a Turing-powerful formalismfor infinitestate systems (in the sense of being able to generate the computation graphs of Turing machines up to isomorphisms), and then impose semantic restrictions whereby the desired model checking problem becomes decidable. In other words, to show that a subclass of the infinite-state systems that is generated by this formalism is decidable with respect to the model checking problem under consideration, we will simply have to prove that this subclass satisfies the semantic restriction. On the other hand, specific techniques is a “bottom-up” approach in the sense that we restrict to a non-Turing powerful formalism of infinite-state systems at the outset. The main benefit of generic techniques is that they can be used as algorithmic metatheorems, i.e., they can give unified proofs of decidability of various model checking problems over infinite-state systems. Specific techniques are more flexible in the sense they can be used to derive decidability or optimal complexity when generic techniques fail. In the first part of the thesis, we adopt word/tree automatic transition systems as a generic formalism of infinite-state systems. Such formalisms can be used to generate many interesting classes of infinite-state systems that have been considered in the literature, e.g., the computation graphs of counter systems, Turing machines, pushdown systems, prefix-recognizable systems, regular ground-tree rewrite systems, PAprocesses, order-2 collapsible pushdown systems. Although the generality of these formalisms make most interesting model checking problems (even safety) undecidable, they are known to have nice closure and algorithmic properties. We use these nice properties to obtain several algorithmic metatheorems over word/tree automatic systems, e.g., for deriving decidability of various model checking problems including recurrent reachability, and Linear Temporal Logic (LTL) with complex fairness constraints. These algorithmic metatheorems can be used to uniformly prove decidability with optimal (or near-optimal) complexity of various model checking problems over many classes of infinite-state systems that have been considered in the literature. In fact, many of these decidability/complexity results were not previously known in the literature. In the second part of the thesis, we study various model checking problems over subclasses of counter systems that were already known to be decidable. In particular, we consider reversal-bounded counter systems (and their extensions with discrete clocks), one-counter processes, and networks of one-counter processes. We shall derive optimal complexity of various model checking problems including: model checking LTL, EF-logic, and first-order logic with reachability relations (and restrictions thereof). In most cases, we obtain a single/double exponential reduction in the previously known upper bounds on the complexity of the problems.

Dans cette thèse, nous nous attachons à étudier des classes de graphes infinis et leurs propriétés, Notamment celles de vérification de modèles, d'accessibilité et de langages reconnus.Nous définissons une notion d'arbres de piles ainsi qu'une notion liée de réécriture suffixe, permettant d'étendre à la fois les automates à piles d'ordre supérieur et la réécriture suffixe d'arbres de manière minimale. Nous définissons également une notion de reconnaissabilité sur les ensembles d'opérations à l'aide d'automates qui induit une notion de reconnaissabilité sur les ensembles d'arbres de piles et une notion de normalisation des ensembles reconnaissables d'opérations analogues à celles existant sur les automates à pile d'ordre supérieur. Nous montrons que les graphes définis par ces systèmes de réécriture suffixe d'arbres de piles possèdent une FO-théorie décidable, en montrant que ces graphes peuvent être obtenu par une interprétation à ensembles finis depuis un graphe de la hiérarchie à piles.Nous nous intéressons également au problème d'algébricité des langages de traces des systèmes à compteurs et au problème lié de la stratifiabilité d'un ensemble semi-linéaire. Nous montrons que dans le cas des polyèdres d'entiers, le problème de stratifiabilité est décidable et possède une complexité coNP-complète. Ce résultat nous permet ensuite de montrer que le problème d'algébricité des traces de systèmes à compteurs plats est décidable et coNP-complet. Nous donnons également une nouvelle preuve de la décidabilité des langages de traces des systèmes d'addition de vecteurs, préalablement étudié par Schwer / In this thesis, we study classes of infinite graphs and their properties,especially the model-checking problem, the accessibility problem and therecognised languages.We define a notion of stack trees, and a related notionof ground rewriting, which is an extension of both higher-order pushdownautomata and ground tree rewriting systems. We also define a notion ofrecognisability on the sets of ground rewriting operations through operationautomata. This notion induces a notion of recognisability over sets of stacktrees and a normalisation of recognisable sets of operations, similar to theknown notions over higher-order pushdown automata. We show that the graphsdefined by these ground stack tree rewriting systems have a decidableFO-theory, by exhibiting a finite set interpretation from a graph defined bya higher-order automaton to a graph defined by a ground stack tree rewritingsystem.We also consider the context-freeness problem for counter systems, andthe related problem of stratifiability of semi-linear sets. We prove thedecidability of the stratifiability problem for integral polyhedra and that itis coNP-complete. We use this result to show that the context-freeness problemfor flat counter systems is as well coNP-complete. Finally, we give a new proofof the decidability of the context-freeness problem for vector additionsystems, previously studied by Schwer