New algorithms and data structures for the emptiness problem of alternating automata
Nicolas Maquet, Jean-François Raskin · 2011
This work studies new algorithms and data structures that are useful in the context of program verification. As computers have become more and more ubiquitous in our modern societies, an increasingly large number of computer-based systems are considered safety-critical. Such systems are characterized by the fact that a failure or a bug (computer error in the computing jargon) could potentially cause large damage, whether in loss of life, environmental damage, or economic damage. For safety-critical systems, the industrial software engineering community increasingly calls for using techniques which provide some formal assurance that a certain piece of software is correct.One of the most successful program verification techniques is model checking, in which programs are typically abstracted by a finite-state machine. After this abstraction step, properties (typically in the form of some temporal logic formula) can be checked against the finite-state abstraction, with the help of automated tools. Alternating automata play an important role in this context, since many temporal logics on words and trees can be efficiently translated into those automata. This property allows for the reduction of model checking to automata-theoretic questions and is called the automata-theoretic approach to model checking. In this work, we provide three novel approaches for the analysis (emptiness checking) of alternating automata over finite and infinite words. First, we build on the successful framework of antichains to devise new algorithms for LTL satisfiability and model checking, using alternating automata. These algorithms combine antichains with reduced ordered binary decision diagrams in order to handle the exponentially large alphabets of the automata generated by the LTL translation. Second, we develop new abstraction and refinement algorithms for alternating automata, which combine the use of antichains with abstract interpretation, in order to handle ever larger instances of alternating automata. Finally, we define a new symbolic data structure, coined lattice-valued binary decision diagrams that is particularly well-suited for the encoding of transition functions of alternating automata over symbolic alphabets. All of these works are supported with empirical evaluations that confirm the practical usefulness of our approaches. / Ce travail traite de l'etude de nouveaux algorithmes et structures de donnees dont l'usage est destine a la verification de programmes. Les ordinateurs sont de plus en plus presents dans notre vie quotidienne et, de plus en plus souvent, ils se voient confies des tâches de nature critique pour la securite. Ces systemes sont caracterises par le fait qu'une panne ou un bug (erreur en jargon informatique) peut avoir des effets potentiellement desastreux, que ce soit en pertes humaines, degâts environnementaux, ou economiques. Pour ces systemes critiques, les concepteurs de systemes industriels pronent de plus en plus l'usage de techniques permettant d'obtenir une assurance formelle de correction.Une des techniques de verification de programmes les plus utilisees est le model checking, avec laquelle les programmes sont typiquement abstraits par une machine a etats finis. Apres cette phase d'abstraction, des proprietes (typiquement sous la forme d'une formule de logique temporelle) peuvent etres verifiees sur l'abstraction a espace d'etats fini, a l'aide d'outils de verification automatises. Les automates alternants jouent un role important dans ce contexte, principalement parce que plusieurs logiques temporelle peuvent etres traduites efficacement vers ces automates. Cette caracteristique des automates alternants permet de reduire le model checking des logiques temporelles a des questions sur les automates, ce qui est appele l'approche par automates du model checking. Dans ce travail, nous etudions trois nouvelles approches pour l'analyse (le test du vide) desautomates alternants sur mots finis et infinis. Premierement, nous appliquons l'approche par antichaines (utilisee precedemment avec succes pour l'analyse d'automates) pour obtenir de nouveaux algorithmes pour les problemes de satisfaisabilite et du model checking de la logique temporelle lineaire, via les automates alternants.Ces algorithmes combinent l'approche par antichaines avec l'usage des ROBDD, dans le but de gerer efficacement la combinatoire induite par la taille exponentielle des alphabets d'automates generes a partir de LTL. Deuxiemement, nous developpons de nouveaux algorithmes d'abstraction et raffinement pour les automates alternants, combinant l'usage des antichaines et de l'interpretation abstraite, dans le but de pouvoir traiter efficacement des automates de grande taille. Enfin, nous definissons une nouvelle structure de donnees, appelee LVBDD (Lattice-Valued Binary Decision Diagrams), qui permet un encodage efficace des fonctions de transition des automates alternants sur alphabets symboliques. Tous ces travaux ont fait l'objet d'implementations et ont ete valides experimentalement.