Orbit decidability and the conjugacy problem for some extensions of groups

"Vegeu el resum a l'inici del document del fitxer adjunt."

Word Equations and Related Topics. Independence, Decidability and Characterizations

The three main topics of this work are independent systems and chains of word equations, parametric solutions of word equations on three unknowns, and unique decipherability in the monoid of regular languages. The most important result about independent systems is a new method giving an upper bound for their sizes in the case of three unknowns. The bound depends on the length of the shortest equation. This result has generalizations for decreasing chains and for more than three unknowns. The method also leads to shorter proofs and generalizations of some old results. Hmelevksii’s theorem states that every word equation on three unknowns has a parametric solution. We give a significantly simplified proof for this theorem. As a new result we estimate the lengths of parametric solutions and get a bound for the length of the minimal nontrivial solution and for the complexity of deciding whether such a solution exists. The unique decipherability problem asks whether given elements of some monoid form a code, that is, whether they satisfy a nontrivial equation. We give characterizations for when a collection of unary regular languages is a code. We also prove that it is undecidable whether a collection of binary regular languages is a code.

Higher-Order Concurrency: Expressiveness and Decidability Results

Higher-order process calculi are formalisms for concurrency in which processes can be passed around in communications. Higher-order (or process-passing) concurrency is often presented as an alternative paradigm to the first order (or name-passing) concurrency of the pi-calculus for the description of mobile systems. These calculi are inspired by, and formally close to, the lambda-calculus, whose basic computational step ---beta-reduction--- involves term instantiation. The theory of higher-order process calculi is more complex than that of first-order process calculi. This shows up in, for instance, the definition of behavioral equivalences. A long-standing approach to overcome this burden is to define encodings of higher-order processes into a first-order setting, so as to transfer the theory of the first-order paradigm to the higher-order one. While satisfactory in the case of calculi with basic (higher-order) primitives, this indirect approach falls short in the case of higher-order process calculi featuring constructs for phenomena such as, e.g., localities and dynamic system reconfiguration, which are frequent in modern distributed systems. Indeed, for higher-order process calculi involving little more than traditional process communication, encodings into some first-order language are difficult to handle or do not exist. We then observe that foundational studies for higher-order process calculi must be carried out directly on them and exploit their peculiarities. This dissertation contributes to such foundational studies for higher-order process calculi. We concentrate on two closely interwoven issues in process calculi: expressiveness and decidability. Surprisingly, these issues have been little explored in the higher-order setting. Our research is centered around a core calculus for higher-order concurrency in which only the operators strictly necessary to obtain higher-order communication are retained. We develop the basic theory of this core calculus and rely on it to study the expressive power of issues universally accepted as basic in process calculi, namely synchrony, forwarding, and polyadic communication.

Decidability for some justification logics with negative introspection

Justification logics are modal logics that include justifications for the agent's knowledge. So far, there are no decidability results available for justification logics with negative introspection. In this paper, we develop a novel model construction for such logics and show that justification logics with negative introspection are decidable for finite constant specifications.

A Logic and tool for local reasoning about security protocols

Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática

Combining open and closed world reasoning for the semantic web

Dissertação para obtenção do Grau de Doutor em Informática

Toward a Run-Time Verification Framework for Real-Time Safety-Critical Systems

Presented at SEMINAR "ACTION TEMPS RÉEL:INFRASTRUCTURES ET SERVICES SYSTÉMES". 10, Apr, 2015. Brussels, Belgium.

A game theoretical approach to the algebraic counterpart of the Wagner hierarchy

La hiérarchie de Wagner constitue à ce jour la plus fine classification des langages ω-réguliers. Par ailleurs, l'approche algébrique de la théorie de langages formels montre que ces ensembles ω-réguliers correspondent précisément aux langages reconnaissables par des ω-semigroupes finis pointés. Ce travail s'inscrit dans ce contexte en fournissant une description complète de la contrepartie algébrique de la hiérarchie de Wagner, et ce par le biais de la théorie descriptive des jeux de Wadge. Plus précisément, nous montrons d'abord que le degré de Wagner d'un langage ω-régulier est effectivement un invariant syntaxique. Nous définissons ensuite une relation de réduction entre ω-semigroupes pointés par le biais d'un jeu infini de type Wadge. La collection de ces structures algébriques ordonnée par cette relation apparaît alors comme étant isomorphe à la hiérarchie de Wagner, soit un quasi bon ordre décidable de largeur 2 et de hauteur ω. Nous exposons par la suite une procédure de décidabilité de cette hiérarchie algébrique : on décrit une représentation graphique des ω-semigroupes finis pointés, puis un algorithme sur ces structures graphiques qui calcule le degré de Wagner de n'importe quel élément. Ainsi le degré de Wagner de tout langage ω-régulier peut être calculé de manière effective directement sur son image syntaxique. Nous montrons ensuite comment construire directement et inductivement une structure de n''importe quel degré. Nous terminons par une description détaillée des invariants algébriques qui caractérisent tous les degrés de cette hiérarchie. Abstract The Wagner hierarchy is known so far to be the most refined topological classification of ω-rational languages. Also, the algebraic study of formal languages shows that these ω-rational sets correspond precisely to the languages recognizable by finite pointed ω-semigroups. Within this framework, we provide a construction of the algebraic counterpart of the Wagner hierarchy. We adopt a hierarchical game approach, by translating the Wadge theory from the ω-rational language to the ω-semigroup context. More precisely, we first show that the Wagner degree is indeed a syntactic invariant. We then define a reduction relation on finite pointed ω-semigroups by means of a Wadge-like infinite two-player game. The collection of these algebraic structures ordered by this reduction is then proven to be isomorphic to the Wagner hierarchy, namely a well-founded and decidable partial ordering of width 2 and height $\omega^\omega$. We also describe a decidability procedure of this hierarchy: we introduce a graph representation of finite pointed ω-semigroups allowing to compute their precise Wagner degrees. The Wagner degree of every ω-rational language can therefore be computed directly on its syntactic image. We then show how to build a finite pointed ω-semigroup of any given Wagner degree. We finally describe the algebraic invariants characterizing every Wagner degree of this hierarchy.

Automates à contraintes semilinéaires = Automata with a semilinear constraint

Cette thèse présente une étude dans divers domaines de l'informatique théorique de modèles de calculs combinant automates finis et contraintes arithmétiques. Nous nous intéressons aux questions de décidabilité, d'expressivité et de clôture, tout en ouvrant l'étude à la complexité, la logique, l'algèbre et aux applications. Cette étude est présentée au travers de quatre articles de recherche. Le premier article, Affine Parikh Automata, poursuit l'étude de Klaedtke et Ruess des automates de Parikh et en définit des généralisations et restrictions. L'automate de Parikh est un point de départ de cette thèse; nous montrons que ce modèle de calcul est équivalent à l'automate contraint que nous définissons comme un automate qui n'accepte un mot que si le nombre de fois que chaque transition est empruntée répond à une contrainte arithmétique. Ce modèle est naturellement étendu à l'automate de Parikh affine qui effectue une opération affine sur un ensemble de registres lors du franchissement d'une transition. Nous étudions aussi l'automate de Parikh sur lettres: un automate qui n'accepte un mot que si le nombre de fois que chaque lettre y apparaît répond à une contrainte arithmétique. Le deuxième article, Bounded Parikh Automata, étudie les langages bornés des automates de Parikh. Un langage est borné s'il existe des mots w_1, w_2, ..., w_k tels que chaque mot du langage peut s'écrire w_1...w_1w_2...w_2...w_k...w_k. Ces langages sont importants dans des domaines applicatifs et présentent usuellement de bonnes propriétés théoriques. Nous montrons que dans le contexte des langages bornés, le déterminisme n'influence pas l'expressivité des automates de Parikh. Le troisième article, Unambiguous Constrained Automata, introduit les automates contraints non ambigus, c'est-à-dire pour lesquels il n'existe qu'un chemin acceptant par mot reconnu par l'automate. Nous montrons qu'il s'agit d'un modèle combinant une meilleure expressivité et de meilleures propriétés de clôture que l'automate contraint déterministe. Le problème de déterminer si le langage d'un automate contraint non ambigu est régulier est montré décidable. Le quatrième article, Algebra and Complexity Meet Contrained Automata, présente une étude des représentations algébriques qu'admettent les automates contraints et les automates de Parikh affines. Nous déduisons de ces caractérisations des résultats d'expressivité et de complexité. Nous montrons aussi que certaines hypothèses classiques en complexité computationelle sont reliées à des résultats de séparation et de non clôture dans les automates de Parikh affines. La thèse est conclue par une ouverture à un possible approfondissement, au travers d'un certain nombre de problèmes ouverts.

Systems of Parallel Communicating Restarting Automata

In der vorliegenden Dissertation werden Systeme von parallel arbeitenden und miteinander kommunizierenden Restart-Automaten (engl.: systems of parallel communicating restarting automata; abgekürzt PCRA-Systeme) vorgestellt und untersucht. Dabei werden zwei bekannte Konzepte aus den Bereichen Formale Sprachen und Automatentheorie miteinander vescrknüpft: das Modell der Restart-Automaten und die sogenannten PC-Systeme (systems of parallel communicating components). Ein PCRA-System besteht aus endlich vielen Restart-Automaten, welche einerseits parallel und unabhängig voneinander lokale Berechnungen durchführen und andererseits miteinander kommunizieren dürfen. Die Kommunikation erfolgt dabei durch ein festgelegtes Kommunikationsprotokoll, das mithilfe von speziellen Kommunikationszuständen realisiert wird. Ein wesentliches Merkmal hinsichtlich der Kommunikationsstruktur in Systemen von miteinander kooperierenden Komponenten ist, ob die Kommunikation zentralisiert oder nichtzentralisiert erfolgt. Während in einer nichtzentralisierten Kommunikationsstruktur jede Komponente mit jeder anderen Komponente kommunizieren darf, findet jegliche Kommunikation innerhalb einer zentralisierten Kommunikationsstruktur ausschließlich mit einer ausgewählten Master-Komponente statt. Eines der wichtigsten Resultate dieser Arbeit zeigt, dass zentralisierte Systeme und nichtzentralisierte Systeme die gleiche Berechnungsstärke besitzen (das ist im Allgemeinen bei PC-Systemen nicht so). Darüber hinaus bewirkt auch die Verwendung von Multicast- oder Broadcast-Kommunikationsansätzen neben Punkt-zu-Punkt-Kommunikationen keine Erhöhung der Berechnungsstärke. Desweiteren wird die Ausdrucksstärke von PCRA-Systemen untersucht und mit der von PC-Systemen von endlichen Automaten und mit der von Mehrkopfautomaten verglichen. PC-Systeme von endlichen Automaten besitzen bekanntermaßen die gleiche Ausdrucksstärke wie Einwegmehrkopfautomaten und bilden eine untere Schranke für die Ausdrucksstärke von PCRA-Systemen mit Einwegkomponenten. Tatsächlich sind PCRA-Systeme auch dann stärker als PC-Systeme von endlichen Automaten, wenn die Komponenten für sich genommen die gleiche Ausdrucksstärke besitzen, also die regulären Sprachen charakterisieren. Für PCRA-Systeme mit Zweiwegekomponenten werden als untere Schranke die Sprachklassen der Zweiwegemehrkopfautomaten im deterministischen und im nichtdeterministischen Fall gezeigt, welche wiederum den bekannten Komplexitätsklassen L (deterministisch logarithmischer Platz) und NL (nichtdeterministisch logarithmischer Platz) entsprechen. Als obere Schranke wird die Klasse der kontextsensitiven Sprachen gezeigt. Außerdem werden Erweiterungen von Restart-Automaten betrachtet (nonforgetting-Eigenschaft, shrinking-Eigenschaft), welche bei einzelnen Komponenten eine Erhöhung der Berechnungsstärke bewirken, in Systemen jedoch deren Stärke nicht erhöhen. Die von PCRA-Systemen charakterisierten Sprachklassen sind unter diversen Sprachoperationen abgeschlossen und einige Sprachklassen sind sogar abstrakte Sprachfamilien (sogenannte AFL's). Abschließend werden für PCRA-Systeme spezifische Probleme auf ihre Entscheidbarkeit hin untersucht. Es wird gezeigt, dass Leerheit, Universalität, Inklusion, Gleichheit und Endlichkeit bereits für Systeme mit zwei Restart-Automaten des schwächsten Typs nicht semientscheidbar sind. Für das Wortproblem wird gezeigt, dass es im deterministischen Fall in quadratischer Zeit und im nichtdeterministischen Fall in exponentieller Zeit entscheidbar ist.

Algorithmic Complexity and Computability

High-level introduction for web science students, rather than for computer science students.

Expressiveness of Concurrent Languages

The aim of this thesis is to go through different approaches for proving expressiveness properties in several concurrent languages. We analyse four different calculi exploiting for each one a different technique. We begin with the analysis of a synchronous language, we explore the expressiveness of a fragment of CCS! (a variant of Milner's CCS where replication is considered instead of recursion) w.r.t. the existence of faithful encodings (i.e. encodings that respect the behaviour of the encoded model without introducing unnecessary computations) of models of computability strictly less expressive than Turing Machines. Namely, grammars of types 1,2 and 3 in the Chomsky Hierarchy. We then move to asynchronous languages and we study full abstraction for two Linda-like languages. Linda can be considered as the asynchronous version of CCS plus a shared memory (a multiset of elements) that is used for storing messages. After having defined a denotational semantics based on traces, we obtain fully abstract semantics for both languages by using suitable abstractions in order to identify different traces which do not correspond to different behaviours. Since the ability of one of the two variants considered of recognising multiple occurrences of messages in the store (which accounts for an increase of expressiveness) reflects in a less complex abstraction, we then study other languages where multiplicity plays a fundamental role. We consider the language CHR (Constraint Handling Rules) a language which uses multi-headed (guarded) rules. We prove that multiple heads augment the expressive power of the language. Indeed we show that if we restrict to rules where the head contains at most n atoms we could generate a hierarchy of languages with increasing expressiveness (i.e. the CHR language allowing at most n atoms in the heads is more expressive than the language allowing at most m atoms, with mdecidability and undecidability for problems like reachability and coverability.

A Finite Model Property for Gödel Modal Logics

A new semantics with the finite model property is provided and used to establish decidability for Gödel modal logics based on (crisp or fuzzy) Kripke frames combined locally with Gödel logic. A similar methodology is also used to establish decidability, and indeed co-NP-completeness for a Gödel S5 logic that coincides with the one-variable fragment of first-order Gödel logic.