El objetivo de esta tesis es abordar distintos problemas algebraicos acerca de algunas subvariedades de las álgebras de De Morgan Heyting y de las álgebras pseudocomplementadas de Kleene utilizando dualidades topológicas tipo Priestley correspondientes a dichas variedades. Se investiga la sucesión de subvariedades SDHn de las álgebras de De Morgan Heyting caracterizadas por la identidad xn(1*) = x(n+1)(1*) definidas por H.P. Sankappanavar en [26]. Se obtienen condiciones necesarias y sufi- cientes sobre el espacio de filtros primos para que un álgebra de De Morgan Heyting pertenezca a la variedad SDH1 y se caracterizan las álgebras subdirectamente irreducibles y simples de dicha variedad. Todos estos resultados son extendidos para las álgebras finitas en el caso general SDHn. La clase de las álgebras de Boole es un ejemplo familiar de álgebras de Heyting y es bien conocido que existe una correspondencia entre las subálgebras de un álgebra de Boole y ciertas relaciones de equivalencia definidas sobre su espacio Booleano (ver, por ejemplo [13]). En esta tesis se extiende esta correspondencia tanto para la clase de las álgebras de Heyting como para la clase de las álgebras de De Morgan Heyting, es decir, se caracterizan las subálgebras de las álgebras de Heyting y de De Morgan Heyting definiendo ciertas relaciones de equivalencia sobre los espacios topológicos de sus respectivas representaciones tipo Priestley. Como caso particular de este resultado, se obtiene la caracterización para subálgebras maximales de las álgebras de Heyting finitas dada por M. Adams en [2]. Se estudian las álgebras subdirectamente irreducibles en la variedad PCDM de las álgebras pseudocomplementadas de De Morgan a través de sus pm-espacios. Se introduce la noción de body de un álgebra L 2 PCDMy se caracteriza completamente Body(L) cuando L es subdirectamente irreducible, directamente indescomponible o simple. Como consecuencia de esto, en el caso particular de las álgebras pseudocomplementadas de Kleene, surgen naturalmente tres subvariedades de la misma para las cuales se determinan identidades que las caracterizan. Se define la subvariedad BPK, de particular interés ya que sus álgebras subdirectamente irreducibles son suma ordinal de álgebras de Boole y cadenas, realizándose un estudio de la misma. Se determina completamente el reticulado de sus subvariedades y se encuentran bases ecuacionales para cada una de ellas. Una de estas subvariedades, llamada BPK0 es aquella cuyos miembros subdirectamente irreducibles son de la forma B B, donde B es un álgebra de Boole. La última parte de la tesis está destinada al estudio de la variedad BPK0 resolviéndose problemas tales como la obtención de las álgebras libres con una cantidad finita de generadores libres y la descripción completa del reticulado de cuasivariedades junto con una base de cuasi-identidades para cada cuasivariedad. / The objective of this thesis is to study several algebraic problems regarding some subvarieties of De Morgan Heyting algebras and pseudocomplemented Kleene algebras using the corresponding Priestley dualities as a main tool. We focus on the sequence of subvarieties SDHn, which consist of the De Morgan Heyting algebras characterized by the identity xn(1*) =x(n+1)(1*), as defined by H. P. Sankappanavar in [26]. We give necessary and suficient conditions on the space of prime filters for a De Morgan Heyting algebra to belong to the variety SDH1. We also characterize the subdirectly irreducible and simple members of this variety. These results are all further extended for finite algebras in the general case of the varieties SDHn. The class of Boolean algebras is a familiar example of Heyting algebras and it is well known that there exists a correspondence between subalgebras of a Boolean algebra and certain equivalence relations on its Boolean space (see, for example, [13]). In this thesis, we extend this correspondence both for the class of Heyting algebras and for the class of De Morgan Heyting algebras, that is, we characterize the subalgebras of a Heyting algebra and a De Morgan Heyting algebra by defining certain equivalence relations on their respective Priestley spaces. The characterization of maximal subalgebras in finite Heyting algebras given by M. Adams in [2] follows now as a special case of our characterization. We also study the subdirectly irreducible members of the variety PCDM of pseudocomplemented De Morgan algebras in terms of their pm-spaces. We introduce the notion of body of an algebra L 2 PCDM and characterize completely the body of L when L is subdirectly irreducible, directly indecomposable or simple. As a consequence of this, in the case of pseudocomplemented Kleene algebras, three special subvarieties arise naturally, for which we give explicit identities that characterize them. We also define the variety BPK which is of particular interest because its subdirectly irreducible algebras are ordinal sums of Boolean algebras and chains. We study this variety in depth. We determine the whole subvariety lattice and find explicit equational bases for each of the subvarieties. The subdirectly irreducible members of one of these subvarieties, called BPK0, are of the form B B, where B is a Boolean algebra. The last part of this thesis is devoted to the study of this variety: we characterize the finitely generated free algebras and give a full description of the quasivariety lattice as well as the corresponding quasi-equational basis for each of the quasivarieties.

Tableau d'honneur de la Faculté des études supérieures et postdoctorales, 2006-2007 / L’algèbre de Kleene est la théorie algébrique des automates finis et des expressions régulières. Récemment, Kozen a proposé un cadre de travail basé sur l’algèbre de Kleene avec tests (une variante de l’algèbre de Kleene) pour vérifier qu’un programme satisfait une politique de sécurité spécifiée par un automate de sécurité. Malheureusement, cette approche ne permet pas de vérifier des propriétés de vivacité pour les programmes réactifs (programmes qui s’exécutent à l’infini). Le but de ce mémoire est d’étendre la méthode de vérification de programmes proposée par Kozen pour enlever cette limitation. Pour y arriver, nous développons la théorie de l’oméga-algèbre (une extension de l’algèbre de Kleene qui prend en compte les exécutions infinies) qui constitue la majeure partie de ce mémoire. En particulier, nous présentons des résultats de complétude concernant la théorie de Horn de cette algèbre. / Kleene algebra is the algebraic theory of finite automata and regular expressions. Recently, Kozen has proposed a framework based on Kleene algebra with tests (a variant of Kleene algebra) for verifying that a program satisfies a security policy specified by a security automaton. Unfortunately, this approach does not allow to verify liveness properties for reactive programs (programs that execute forever). The goal of this thesis is to extend the framework proposed by Kozen for program verification to remove this limitation. For that, we develop the theory of omega algebra, an extension of Kleene algebra suitable for reasoning about nonterminating executions. The main part of this thesis is about omega algebra. In particular, we show some completeness results about the Horn theory of omega algebra.

Les algèbres de relations apparaissent naturellement dans de nombreux cadres, en informatique comme en mathématiques. Elles constituent en particulier un formalisme tout à fait adapté à la sémantique des programmes impératifs. Les algèbres de Kleene constituent un point de départ : ces algèbres jouissent de résultats de décidabilités très satisfaisants, et admettent une axiomatisation complète. L'objectif de cette thèse a été d'étendre les résultats connus sur les algèbres de Kleene à des extensions de celles-ci.Nous nous sommes tout d'abord intéressés à une extension connue : les algèbres de Kleene avec converse. La décidabilité de ces algèbres était déjà connue, mais l'algorithme prouvant ce résultat était trop compliqué pour être utilisé en pratique. Nous avons donné un algorithme plus simple, plus efficace, et dont la correction est plus facile à établir. Ceci nous a permis de placer ce problème dans la classe de complexité PSpace-complete.Nous avons ensuite étudié les allégories de Kleene. Sur cette extension, peu de résultats étaient connus. En suivant des résultats sur des algèbres proches, nous avons établi l'équivalence du problème d'égalité dans les allégories de Kleene à l'égalité de certains ensembles de graphes. Nous avons ensuite développé un modèle d'automate original (les automates de Petri), basé sur les réseaux de Petri, et avons établi l'équivalence de notre problème original avec le problème de comparaison de ces automates. Nous avons enfin développé un algorithme pour effectuer cette comparaison dans le cadre restreint des treillis de Kleene sans identité. Cet algorithme utilise un espace exponentiel. Néanmoins, nous avons pu établir que la comparaison d'automates de Petri dans ce cas est ExpSpace-complète. Enfin, nous nous sommes intéressés aux algèbres de Kleene Nominales. Nous avons réalisé que les descriptions existantes de ces algèbres n'étaient pas adaptées à la sémantique relationnelle des programmes. Nous les avons donc modifiées pour nos besoins, et ce faisant avons trouvé diverses variations naturelles de ce modèle. Nous avons donc étudié en détails et en Coq les ponts que l'on peut établir entre ces variantes, et entre le modèle “classique” et notre nouvelle version / Algebras of relations appear naturally in many contexts, in computer science as well as in mathematics. They constitute a framework well suited to the semantics of imperative programs. Kleene algebra are a starting point: these algebras enjoy very strong decidability properties, and a complete axiomatisation. The goal of this thesis was to export known results from Kleene algebra to some of its extensions. We first considered a known extension: Kleene algebras with converse. Decidability of these algebras was already known, but the algorithm witnessing this result was too complicated to be practical. We proposed a simpler algorithm, more efficient, and whose correctness is easier to establish. It allowed us to prove that this problem lies in the complexity class PSpace-complete.Then we studied Kleene allegories. Few results were known about this extension. Following results about closely related algebras, we established the equivalence between equality in Kleene allegories and equality of certain sets of graphs. We then developed an original automaton model (so-called Petri automata), based on Petri nets. We proved the equivalence between the original problem and comparing these automata. In the restricted setting of identity-free Kleene lattices, we also provided an algorithm performing this comparison. This algorithm uses exponential space. However, we proved that the problem of comparing Petri automata lies in the class ExpSpace-complete.Finally, we studied Nominal Kleene algebras. We realised that existing descriptions of these algebra were not suited to relational semantics of programming languages. We thus modified them accordingly, and doing so uncovered several natural variations of this model. We then studied formally the bridges one could build between these variations, and between the existing model and our new version of it. This study was conducted using the proof assistant Coq

Ulm, Univ., Diss., 2007.

No description available.

The main result of this thesis is the generalization of the Kleene-theorem to formal tree-series over commutative semirings (the Kleene theorem states the coincidence between rational and recognizable formal languages). To this end weighted tree-languages are introduced and the Kleene-theorem is proved for them. The desired result for formal tree-series is then obtained through application of a homomorphism that relates weighted tree-languages with formal tree-series. In the second part of the thesis the connections to the theorie of Iteration-theories are discovered. In particular it is shown there that the grove-theory of formal tree-series forms a partial iteration-theory. / Hauptresultat dieser Arbeit ist die Verallgemeinerung des Satzes von Kleene über die Koinzidenz der rationalen und der erkennbaren Sprachen auf den Fall der formalen Baumreihen über kommutativen Semiringen. Zu diesem Zweck werden gewichtete Baumsprachen eingeführt, da sich diese ählich den klassischen Baumsprachen verhalten. Der Satz von Kleene wird also zunächst auf den Fall der gewichteten Baumsprachen verallgemeinert. Das erstrebte Resultat wird dann durch Anwendung eines Homomorphismus', der gewichteten Baumsprachen formle Baumreihen zuordnet, erhalten. Im zweiten Teil der Arbeit werden Kreuzverbindungen zur Theorie der Iterationstheorien aufgezeigt. Insbesondere wird z.B. gezeigt, dass die Grovetheorie der formalen Baumreihen eine partielle Iterationstheorie bildet.

Cette thèse introduit différentes méthodes de vérification (ou model-checking) sur des modèles de systèmes à pile. En effet, les systèmes à pile (pushdown systems) modélisent naturellement les programmes séquentiels grâce à une pile infinie qui peut simuler la pile d'appel du logiciel. La première partie de cette thèse se concentre sur la vérification sur des systèmes à pile de la logique HyperLTL, qui enrichit la logique temporelle LTL de quantificateurs universels et existentiels sur des variables de chemin. Il a été prouvé que le problème de la vérification de la logique HyperLTL sur des systèmes d'états finis est décidable ; nous montrons que ce problème est en revanche indécidable pour les systèmes à pile ainsi que pour la sous-classe des systèmes à pile visibles (visibly pushdown systems). Nous introduisons donc des algorithmes d'approximation de ce problème, que nous appliquons ensuite à la vérification de politiques de sécurité. Dans la seconde partie de cette thèse, dans la mesure où la représentation de la pile d'appel par les systèmes à pile est approximative, nous introduisons les systèmes à surpile (pushdown systems with an upper stack) ; dans ce modèle, les symboles retirés de la pile d'appel persistent dans la zone mémoire au dessus du pointeur de pile, et peuvent être plus tard écrasés par des appels sur la pile. Nous montrons que les ensembles de successeurs post* et de prédécesseurs pre* d'un ensemble régulier de configurations ne sont pas réguliers pour ce modèle, mais que post* est toutefois contextuel (context-sensitive), et que l'on peut ainsi décider de l'accessibilité d'une configuration. Nous introduisons donc des algorithmes de sur-approximation de post* et de sous-approximation de pre*, que nous appliquons à la détection de débordements de pile et de manipulations nuisibles du pointeur de pile. Enfin, dans le but d'analyser des programmes avec plusieurs fils d'exécution, nous introduisons le modèle des réseaux à piles dynamiques synchronisés (synchronized dynamic pushdown networks), que l'on peut voir comme un réseau de systèmes à pile capables d'effectuer des changements d'états synchronisés, de créer de nouveaux systèmes à piles, et d'effectuer des actions internes sur leur pile. Le problème de l'accessibilité étant naturellement indécidable pour un tel modèle, nous calculons une abstraction des chemins d'exécutions entre deux ensembles réguliers de configurations. Nous appliquons ensuite cette méthode à un processus itératif de raffinement des abstractions. / In this thesis, we propose different model-checking techniques for pushdown system models. Pushdown systems (PDSs) are indeed known to be a natural model for sequential programs, as they feature an unbounded stack that can simulate the assembly stack of an actual program. Our first contribution consists in model-checking the logic HyperLTL that adds existential and universal quantifiers on path variables to LTL against pushdown systems (PDSs). The model-checking problem of HyperLTL has been shown to be decidable for finite state systems. We prove that this result does not hold for pushdown systems nor for the subclass of visibly pushdown systems. Therefore, we introduce approximation algorithms for the model-checking problem, and show how these can be used to check security policies. In the second part of this thesis, as pushdown systems can fail to accurately represent the way an assembly stack actually operates, we introduce pushdown systems with an upper stack (UPDSs), a model where symbols popped from the stack are not destroyed but instead remain just above its top, and may be overwritten by later push rules. We prove that the sets of successors post* and predecessors pre* of a regular set of configurations of such a system are not always regular, but that post* is context-sensitive, hence, we can decide whether a single configuration is forward reachable or not. We then present methods to overapproximate post* and under-approximate pre*. Finally, we show how these approximations can be used to detect stack overflows and stack pointer manipulations with malicious intent. Finally, in order to analyse multi-threaded programs, we introduce in this thesis a model called synchronized dynamic pushdown networks (SDPNs) that can be seen as a network of pushdown processes executing synchronized transitions, spawning new pushdown processes, and performing internal pushdown actions. The reachability problem for this model is obviously undecidable. Therefore, we compute an abstraction of the execution paths between two regular sets of configurations. We then apply this abstraction framework to a iterative abstraction refinement scheme.

The main result of this thesis is the generalization of the Kleene-theorem to formal tree-series over commutative semirings (the Kleene theorem states the coincidence between rational and recognizable formal languages). To this end weighted tree-languages are introduced and the Kleene-theorem is proved for them. The desired result for formal tree-series is then obtained through application of a homomorphism that relates weighted tree-languages with formal tree-series. In the second part of the thesis the connections to the theorie of Iteration-theories are discovered. In particular it is shown there that the grove-theory of formal tree-series forms a partial iteration-theory. / Hauptresultat dieser Arbeit ist die Verallgemeinerung des Satzes von Kleene über die Koinzidenz der rationalen und der erkennbaren Sprachen auf den Fall der formalen Baumreihen über kommutativen Semiringen. Zu diesem Zweck werden gewichtete Baumsprachen eingeführt, da sich diese ählich den klassischen Baumsprachen verhalten. Der Satz von Kleene wird also zunächst auf den Fall der gewichteten Baumsprachen verallgemeinert. Das erstrebte Resultat wird dann durch Anwendung eines Homomorphismus', der gewichteten Baumsprachen formle Baumreihen zuordnet, erhalten. Im zweiten Teil der Arbeit werden Kreuzverbindungen zur Theorie der Iterationstheorien aufgezeigt. Insbesondere wird z.B. gezeigt, dass die Grovetheorie der formalen Baumreihen eine partielle Iterationstheorie bildet.