Forbidding and enforcing systems (fe-systems) provide a new way of defining classes of structures based on boundary conditions. Forbidding and enforcing systems on formal languages were inspired by molecular reactions and DNA computing. Initially, they were used to define new classes of languages (fe-families) based on forbidden subwords and enforced words. This paper considers a metric on languages and proves that the metric space obtained is homeomorphic to the Cantor space. This work studies Chomsky classes of families as subspaces and shows they are neither closed nor open. The paper investigates the fe-families as subspaces and proves the necessary and sufficient conditions for the fe-families to be open. Consequently, this proves that fe-systems define classes of languages different than Chomsky hierarchy. This work shows a characterization of continuous functions through fe-systems and includes results about homomorphic images of fe-families. This paper introduces a new notion of connecting graphs and a new way to study classes of graphs. Forbidding-enforcing systems on graphs define classes of graphs based on forbidden subgraphs and enforced subgraphs. Using fe-systems, the paper characterizes known classes of graphs, such as paths, cycles, trees, complete graphs and k-regular graphs. Several normal forms for forbidding and enforced sets are stated and proved. This work introduces the notion of forbidding and enforcing to posets where fe-systems are used to define families of subsets of a given poset, which in some sense generalizes language fe-systems. Poset fe-systems are, also, used to define a single subset of elements satisfying the forbidding and enforcing constraints. The latter generalizes graph fe-systems to an extent, but defines new classes of structures based on weak enforcing. Some properties of poset fe-systems are investigated. A series of normal forms for forbidding and enforcing sets is presented. This work ends with examples illustrating the computational potential of fe-systems. The process of cutting DNA by an enzyme and ligating is modeled in the setting of language fe-systems. The potential for use of fe-systems in information processing is illustrated by defining the solutions to the k-colorability problem.

In this thesis we investigate the expressive power of several logics over finite trees. In particular we want to understand precisely the expressive power of first-order logic over finite trees. Because we study many logics, we proceed by comparison to a logic that subsumes them all and serves as a yardstick: monadic second-order logic. Each logic we consider is a fragment of monadic second-order logic. MSO is linked to the theory of formal languages. To each logical formula corresponds a tree language, which is the language of trees satisfying this formula. Furthermore, given a logic we can associate a class of tree languages: the class of languages definable by a formula of this logic. In the setting of finite trees MSO corresponds exactly to the class of regular tree languages. Given a logic, we actually look for a decidable characterization of the class of languages defined in this logic. By decidable characterization, we mean an algorithm for solving the following problem: given as input a finite tree automaton, decide if the recognized language belongs to the class in question. We will actually obtain our decidable characterizations by exhibiting for each class a set of closure properties such that a language is in the class under investigation if and only if it satisfies these closure properties. Each such closure property is then shown to be decidable. Stating and proving such closure properties usually yields a solid understanding of the expressive power of the corresponding logic. The main open problem in this research area is to obtain a decidable characterization for the class of tree languages that are definable in first-order logic. We provide decidable characterizations for several fragments of FO. First we provide three decidable characterizations for classes of regular languages of trees of bounded rank. The first class we consider is the class of languages definable in the temporal logic EF+F^-1. It essentially navigates the trees using two modalities for moving to a descendant node or an ancestor node. The second class we consider is the class of trees of bounded rank definable using one quantifier alternation. The last class, is the class of languages definable using a boolean combination of existential first order formulas. In the setting of forests, we investigate the class of languages definable in first-order logic using only two variables and two prediactes corresponding respectively to the ancestor and following sibling relations. We provide a characterization for this logic. The last class for which we provide a decidable characterization is the class of locally testable language (LT). A language L is in LT if membership in L depends only on the presence or absence of neighborhoods of a certain fixed size in the tree. We define notions of LT for both unranked trees and trees of bounded rank by adapting the definition of neighborhood to each setting. Then we provide a decidable characterization for both notions of LT.

Formal methods provide means for rigorously specifying the desired behaviour of a hardware or software system, making a precise model of its actual behaviour, and then verifying whether that actual behaviour corresponds to the specification.<br><br> My habiliation thesis reports on various contributions to this realm, where my main interest has been on algorithmic aspects. This is motivated by the observation that asymptotic worst-case complexity, often used to characterize the difficulty of algorithmic problems, is only loosely related to the difficulty encountered in solving those problems in practice.<br><br> The two main types of system I have been working on are pushdown systems and Petri nets. Both are fundamental notions of computation, and both offer, in my opinion, particularly nice opportunities for combining theory and algorithmics.<br><br> Pushdown systems are finite automata equipped with a stack; since the height of the stack is not bounded, they represent a class of infinite-state systems that model programs with (recursive) procedure calls. Moreover, we shall see that specifying authorizations is another, particularly interesting application of pushdown systems.<br><br> While pushdown systems are primarily suited to express sequential systems, Petri nets model concurrent systems. My contributions in this area all concern unfoldings. In a nutshell, the unfolding of a net N is an acyclic version of N in which loops have been unrolled. Certain verification problems, such as reachability, have a lower complexity on unfoldings than on general Petri nets.

Lindenmayer (L) systems form a class of interesting computational formalisms due to their parallel nature, the various circumstances under which they operate, the restrictions imposed on language acceptance, and other attributes. These systems have been extensively studied in the Formal Languages literature. In the past decade a new type of Lindenmayer system had been proposed: Watson-Crick Lindenmayer Systems. These systems are essentially a marriage between Developmental systems and DNA Computing. At their heart they are Lindenmayer systems augmented with a complementary relation amongst elements in the system just as the base pairs of DNA strands can be complementary with respect to one another. When conditions and a mechanism for 'switching' the state of a computation to it's complementary version are provided then these systems can become surprisingly more powerful than the L systems which form their backbone. This dissertation explores the computational power of new variants of Watson-Crick L systems. It is found that many of these systems are Computationally-Complete. These investigations differ from prior ones in that the systems under consideration have extended alphabets and usually Regular Triggers for complementation are considered as opposed to Context-Free Triggers investigated in previous works. / Thesis (Master, Computing) -- Queen's University, 2010-12-06 18:29:23.584

The work presented in this thesis discusses various formalisms for representing the addition of order-controlling and order-relaxing mechanisms to existing formal language models. An immediate example is shuffle expressions, which can represent not only all regular languages (a regular expression is a shuffle expression), but also features additional operations that generate arbitrary interleavings of its argument strings. This defines a language class which, on the one hand, does not contain all context-free languages, but, on the other hand contains an infinite number of languages that are not context-free. Shuffle expressions are, however, not themselves the main interest of this thesis. Instead we consider several formalisms that share many of their properties, where some are direct generalisations of shuffle expressions, while others feature very different methods of controlling order. Notably all formalisms that are studied here have a semi-linear Parikh image, are structured so that each derivation step generates at most a constant number of symbols (as opposed to the parallel derivations in for example Lindenmayer systems), feature interesting ordering characteristics, created either by derivation steps that may generate symbols in multiple places at once, or by multiple generating processes that produce output independently in an interleaved fashion, and are all limited enough to make the question of efficient parsing an interesting and reasonable goal. This vague description already hints towards the formalisms considered; the different classes of mildly context-sensitive devices and concurrent finite-state automata. This thesis will first explain and discuss these formalisms, and will then primarily focus on the associated membership problem (or parsing problem). Several parsing results are discussed here, and the papers in the appendix give a more complete picture of these problems and some related ones.

Nous étudions dans cette thèse la notion de quasipériodicité,introduite par Apostolico et Ehrenfeucht au début des années 1990,puis étendue aux mots infinis par Solomon Marcus au début des années2000. Un mot (fini ou infini) w est quasipériodique s'il peut êtrecouvert par des occurrences, éventuellement chevauchantes, d'un autremot, fini, appelé sa quasipériode. En 2006, Monteil etMarcus ont introduit la notion plus forte de quasipériodicitémulti-échelles : le fait d'avoir une infinité de quasipériodes.Dans un premier temps, nous étudions la quasipériodicité des motsinfinis bidimensionnels. Nous montrons que, contrairement au casunidimensionnel où la quasipériodicité ne force aucune propriété fortedes mots infinis, il existe des quasipériodes q qui forcent les mots2D q-quasipériodiques à être d'entropie nulle. Nous montrons égalementque la quasipériodicité multi-échelles en deux dimensions forcel'existence de fréquences uniformes pour les facteurs.Dans un deuxième temps, nous donnons des résultats sur les motsinfinis en une dimension. Nous donnons notament une approchepermettant de déterminer les quasipériodes d'un mot infini à partir deses facteurs carrés et de ses facteurs spéciaux. Nous montrons ensuiteque la famille des mots périodiques, ainsi que celle des mots standardsturmiens, peuvent être caractérisées en termes de quasipériodicitémulti-échelles. / We study the notion of quasiperiodicity, introduced by Apostolico and Ehrenfeucht at the beginning of the 1990's, then extended to infinite words by Solomon Marcus at the beginning of the 2000's. A (finite or infinite) word w is quasiperiodic if it can be covered by occurrences, possibly overlapping, of another finite word, call its quasiperiod. In 2006, Monteil and Marcus introduced a stronger notion: multi-scale quasiperiodicity, the property of having infinitely many quasiperiods.First we study quasiperiodicity of two-dimensional infinite words. We show that, by contrast with the one-dimensional case where quasiperiodicity do not force any property on infinite words, there exist quasiperiods q which force 2D q-quasiperiodic words to have zero entropy. We also show that multi-scale quasiperiodicity in two dimension force the existence of uniform frequencies for factors.Then we give results on infinite words in one dimension. Most notably we give a method to determine the quasiperiods of an infinite words from its square and special factors. We show that the family of periodic words and standard Sturmian words are characterizable in terms of multi-scale quasiperiodicity.

Apesar das novas e efetivas técnicas de engenharia de software, os projetos de desenvolvimento de sistemas estão propensos a ter os mesmos problemas que acometem o software de apoio à gestão. Entrega com atraso, acima do orçamento e não suprindo as reais necessidades dos usuários finais ou da organização que está financiando o desenvolvimento do sistema, são os principais problemas. Esse último problema é o que mais afeta o desenvolvimento de sistemas e é um desafio para que o desenvolvimento personalizado seja uma solução real para várias empresas. Este trabalho apresenta uma proposta de método de gestão que auxilie a comunicação entre as atividades associadas à engenharia de requisitos e as atividades associadas à modelagem dos processos de negócio. Essa abordagem concerne à gestão e tratamento de requisitos de sistemas baseando-se em técnicas de engenharia de processos de negócios e de engenharia de requisitos, no processo unificado de desenvolvimento de software e na utilização de linguagens semi-formais e formais de modelagem, UML e SysML respectivamente. O método pretende mitigar os efeitos dos problemas de comunicação existentes entre os diversos integrantes de um projeto, com especial atenção para a comunicação entre a equipe de requisitos do projeto e os stakeholders responsáveis pela aceitação e aprovação do sistema. A pesquisa, com o apoio da apresentação de dois casos que ilustram o método de gestão proposto, permite concluir que é possível tornar mais efetiva e produtiva a comunicação entre os diversos envolvidos com o projeto, podendo resultar em um processo mais eficiente para a aceitação dos requisitos junto aos stakeholders. / Despite new and effective software engineering techniques, system development projects are likely to have the same problems that affect the management support software. Delivery delay, above budget and not fitting the real needs of end users or the organization that is funding the system development, are the most common problems. The latter problem is the one that most affects the systems development and is a challenge for the custom development to be a real solution to several companies. This work presents a proposal for a management method to help the communication between the activities associated with the engineering requirements and the activities associated with business processes modeling. This approach, concerns to the systems requirements treatment and management, is based on business processes engineering and requirements engineering, in software development unified process and in the use of semi-formal and formal modeling languages as UML and SysML, respectively. The method seeks to mitigate the effects of the communication problems among the project members, with special attention to the communication between the project requirements team and the stakeholders responsible for the system acceptance and adoption. The research, supported by the presentation of two cases which illustrates the proposed management method, has concluded that it is possible to make more effective and productive communication among members related with the project, which may result a more efficient process for the stakeholders requirement acceptance.

No description available.

Cette thèse adresse les problèmes d'universalité et de complétude computationelle pour plusieurs modèles de calcul inspirés par la biologie. Il s'agit principalement des systèmes d'insertion/effacement, réseaux de processeurs évolutionnaires, ainsi que des systèmes de réécriture de multi-ensembles. Les résultats décrits se classent dans deux catégories majeures : l'étude de la puissance de calcul des opérations d'insertion et d'effacement avec ou sans mécanismes de contrôle, et la construction des systèmes de réécriture de multi-ensembles universels de petite taille. Les opérations d'insertion et d'effacement consistent à rajouter ou supprimer une sous-chaîne dans une chaîne de caractères dans un contexte donné. La motivation pour l'étude de ces opérations vient de la biologie, ainsi que de la linguistique et de la théorie des langages formels. Dans la première partie de ce manuscrit nous examinons des systèmes d'insertion/effacement correspondant à l'édition de l'ARN, un processus qui insère ou supprime des fragments de ces molécules. Une particularité importante de l'édition de l'ARN est que le endroit auquel se font les modifications est déterminé par des séquences de nucléotides se trouvant toujours du même côté du site de modification. En termes d'insertion et d'effacement, ce phénomène se modéliserait par des règles possédant le contexte uniquement d'un seul côté. Nous montrons qu'avec un contexte gauche de deux caractères il est possible d'engendrer tous les langages rationnels. D'autre part, nous prouvons que des contextes plus longs n'augmentent pas la puissance de calcul du modèle. Nous examinons aussi les systèmes d’insertion/effacement utilisant des mécanismes de contrôle d’application des règles et nous montrons l'augmentation de la puissance d'expression. Les opérations d'insertion et d'effacement apparaissent naturellement dans le domaine de la sécurité informatique. Comme exemple on peut donner le modèle des grammaires gauchistes (leftist grammar), qui ont été introduites pour l'étude des systèmes critiques. Dans cette thèse nous proposons un nouvel instrument graphique d'analyse du comportement dynamique de ces grammaires. La deuxième partie du manuscrit s'intéresse au problème d'universalité qui consiste à trouver un élément concret capable de simuler le travail de n'importe quel autre dispositif de calcul. Nous commençons par le modèle de réseaux de processeurs évolutionnaires, qui abstrait le traitement de l'information génétique. Nous construisons des réseaux universels ayant un petit nombre de règles. Nous nous concentrons ensuite sur les systèmes de réécriture des multi-ensembles, un modèle qui peut être vu comme une abstraction des réactions biochimiques. Pour des raisons historiques, nous formulons nos résultats en termes de réseaux de Petri. Nous construisons des réseaux de Petri universels et décrivons des techniques de réduction du nombre de places, de transitions et d'arcs inhibiteurs, ainsi que du degré maximal des transitions. Une bonne partie de ces techniques repose sur une généralisation des machines à registres introduite dans cette thèse et qui permet d'effectuer plusieurs tests et opérations en un seul changement d'état / The present thesis considers the problems of computational completeness and universality for several biologically-inspired models of computation: insertion-deletion systems, networks of evolutionary processors, and multiset rewriting systems. The presented results fall into two major categories: study of expressive power of the operations of insertion and deletion with and without control, and construction of universal multiset rewriting systems of low descriptional complexity. Insertion and deletion operations consist in adding or removing a subword from a given string if this subword is surrounded by some given contexts. The motivation for studying these operations comes from biology, as well as from linguistics and the theory of formal languages. In the first part of the present work we focus on insertion-deletion systems closely related to RNA editing, which essentially consists in inserting or deleting fragments of RNA molecules. An important feature of RNA editing is the fact that the locus the operations are carried at is determined by certain sequences of nucleotides, which are always situated to the same side of the editing site. In terms of formal insertion and deletion, this phenomenon is modelled by rules which can only check their context on one side and not on the other. We show that allowing one-symbol insertion and deletion rules to check a two-symbol left context enables them to generate all regular languages. Moreover, we prove that allowing longer insertion and deletion contexts does not increase the computational power. We further consider insertion-deletion systems with additional control over rule applications and show that the computational completeness can be achieved by systems with very small rules. The motivation for studying insertion-deletion systems also comes from the domain of computer security, for the purposes of which a special kind of insertion-deletion systems called leftist grammars was introduced. In this work we propose a novel graphical instrument for visual analysis of the dynamics of such systems. The second part of the present thesis is concerned with the universality problem, which consists in finding a fixed element able to simulate the work any other computing device. We start by considering networks of evolutionary processors (NEPs), a computational model inspired by the way genetic information is processed in the living cell, and construct universal NEPs with very few rules. We then focus on multiset rewriting systems, which model the chemical processes running in the biological cell. For historical reasons, we formulate our results in terms of Petri nets. We construct a series of universal Petri nets and give several techniques for reducing the numbers of places, transitions, inhibitor arcs, and the maximal transition degree. Some of these techniques rely on a generalisation of conventional register machines, proposed in this thesis, which allows multiple register checks and operations to be performed in a single state transition

Dans cette thèse nous étudions le pouvoir d'expression de plusieurs logiques sur les arbres finis. En particulier, nous cherchons à obtenir une compréhension précise du pouvoir d'expression de la logique du premier ordre sur les arbres finis. Nous étudions un nombre important de logiques- pour cette raison nous procédons par comparaison avec une logique qui les contient et nous sert de référence: la logique monadique du second-ordre. Chaque logique que nous considérons est un fragment de la logique monadique du second ordre. MSO est liée à la théorie des langages formels. A chaque formule logique correspond un langage d'arbre: celui des arbres satisfaisant la formule. De plus, étant donné une logique nous pouvons lui associer une classe de langages d'arbres: la classe des langages définissables par une formule de cette logique. Dans le cadre des arbres finis, MSO correspond exactement à la classe des langages réguliers. Étant donné une logique, nous cherchons en fait à obtenir une caractérisation décidable de la classe de langages définissable par celle-ci. Par caractérisation décidable nous entendons un algorithme résolvant le problème suivant: pour un automate d'arbre finis, décider si le langage appartient à la classe en question. Nos caractérisations décidables sont en fait obtenue en exhibant pour chaque classe un ensemble de propriétés de clôture vérifiées par un langage si et seulement si celui-ci appartient à la classe en question. Nous montrons ensuite que chaque propriété de clôture est décidable. Énoncer et prouver de telles propriétés de clôture permet généralement d'obtenir une bonne compréhension du pouvoir de la logique correspondante. Le problème ouvert principal de ce domaine de recherche est l'obtention d'une caractérisation décidable pour la logique du premier ordre. Nous présentons des caractérisation décidables pour plusieurs fragment de FO. Nous commençons par la présentation de trois caractérisations décidable pour des classes de langages d'arbres de rang borné. La première classe que nous considérons est celle des langages définissables par la logique EF + F-1. Cette logique permet de naviguer dans l'arbre en se déplaçant soit vers un ancêtre, soit vers un descendant. La second classe est celle des arbres de rang borné définissables par la logique du premier ordre en n'utilisant qu'une seule alternance de quantificateurs. La dernière classe est celle des langages définissables par une combinaison booléenne de formules existentielles du premier ordre. Dans le cadre des forêts, nous étudions la classe des langages définissable par la logique du premier ordre à deux variables et deux prédicats correspondants respectivement à la relation ancêtre et la relation frère suivant. Nous présentons une caractérisation pour cette logique. La dernière classe pour laquelle nous présentons une caractérisation décidable est celle des langages localement testables (LT). UN langage est dans LT si l'appartenance d'un arbre à celui-ci ne dépends que des voisinages d'une certaine taille fixée dans l'arbre. / In this thesis we investigate the expressive power of several logics over finite trees. In particular we want to understand precisely the expressive power of first-order logic over finite trees. Because we study many logics, we proceed by comparison to a logic that subsumes them all and serves as a yardstick: monadic second-order logic. Each logic we consider is a fragment of monadic second-order logic. MSO is linked to the theory of formal languages. To each logical formula corresponds a tree language, which is the language of trees satisfying this formula. Furthermore, given a logic we can associate a class of tree languages: the class of languages definable by a formula of this logic. In the setting of finite trees MSO corresponds exactly to the class of regular tree languages. Given a logic, we actually look for a decidable characterization of the class of languages defined in this logic. By decidable characterization, we mean an algorithm for solving the following problem: given as input a finite tree automaton, decide if the recognized language belongs to the class in question. We will actually obtain our decidable characterizations by exhibiting for each class a set of closure properties such that a language is in the class under investigation if and only if it satisfies these closure properties. Each such closure property is then shown to be decidable. Stating and proving such closure properties usually yields a solid understanding of the expressive power of the corresponding logic. The main open problem in this research area is to obtain a decidable characterization for the class of tree languages that are definable in first-order logic. We provide decidable characterizations for several fragments of FO. First we provide three decidable characterizations for classes of regular languages of trees of bounded rank. The first class we consider is the class of languages definable in the temporal logic EF+F^-1. It essentially navigates the trees using two modalities for moving to a descendant node or an ancestor node. The second class we consider is the class of trees of bounded rank definable using one quantifier alternation. The last class, is the class of languages definable using a boolean combination of existential first order formulas. In the setting of forests, we investigate the class of languages definable in first-order logic using only two variables and two prediactes corresponding respectively to the ancestor and following sibling relations. We provide a characterization for this logic. The last class for which we provide a decidable characterization is the class of locally testable language (LT). A language L is in LT if membership in L depends only on the presence or absence of neighborhoods of a certain fixed size in the tree. We define notions of LT for both unranked trees and trees of bounded rank by adapting the definition of neighborhood to each setting. Then we provide a decidable characterization for both notions of LT.