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.

Non-failure analysis for logic programs

We provide a method whereby, given mode and (upper approximation) type information, we can detect procedures and goals that can be guaranteed to not fail (i.e., to produce at least one solution or not termínate). The technique is based on an intuitively very simple notion, that of a (set of) tests "covering" the type of a set of variables. We show that the problem of determining a covering is undecidable in general, and give decidability and complexity results for the Herbrand and linear arithmetic constraint systems. We give sound algorithms for determining covering that are precise and efiicient in practice. Based on this information, we show how to identify goals and procedures that can be guaranteed to not fail at runtime. Applications of such non-failure information include programming error detection, program transiormations and parallel execution optimization, avoiding speculative parallelism and estimating lower bounds on the computational costs of goals, which can be used for granularity control. Finally, we report on an implementation of our method and show that better results are obtained than with previously proposed approaches.

Accepting splicing systems with permitting and forbidding words

Abstract: In this paper we propose a generalization of the accepting splicingsystems introduced in Mitrana et al. (Theor Comput Sci 411:2414?2422,2010). More precisely, the input word is accepted as soon as a permittingword is obtained provided that no forbidding word has been obtained sofar, otherwise it is rejected. Note that in the new variant of acceptingsplicing system the input word is rejected if either no permitting word isever generated (like in Mitrana et al. in Theor Comput Sci 411:2414?2422,2010) or a forbidding word has been generated and no permitting wordhad been generated before. We investigate the computational power ofthe new variants of accepting splicing systems and the interrelationshipsamong them. We show that the new condition strictly increases thecomputational power of accepting splicing systems. Although there areregular languages that cannot be accepted by any of the splicing systemsconsidered here, the new variants can accept non-regular and even non-context-free languages, a situation that is not very common in the case of(extended) finite splicing systems without additional restrictions. We alsoshow that the smallest class of languages out of the four classes definedby accepting splicing systems is strictly included in the class of context-free languages. Solutions to a few decidability problems are immediatelyderived from the proof of this result.

Uniform Distributed Pushdown Automata Systems.

We consider here uniform distributed pushdown automata systems (UDPAS), namely distributed pushdown automata systems having all components identical pushdown automata. We consider here just a single protocol for activating/deactivating components, namely a component stays active as long as it can perform moves, as well as two ways of accepting the input word: by empty stacks (all components have empty stacks) or by final states (all components are in final states), when the input word is completely read. We mainly investigate the computational power of UDPAS accepting by empty stacks and a few decidability and closure properties of the families of languages they define. Some directions for further work and open problems are also discussed.

Algorithmique et complexité des systèmes à compteurs

Réalisé en cotutelle avec l'École normale supérieure de Cachan – Université Paris-Saclay

Proof theory for hybrid(ised) logics

Hybridisation is a systematic process along which the characteristic features of hybrid logic, both at the syntactic and the semantic levels, are developed on top of an arbitrary logic framed as an institution. In a series of papers this process has been detailed and taken as a basis for a speci cation methodology for recon gurable systems. The present paper extends this work by showing how a proof calculus (in both a Hilbert and a tableau based format) for the hybridised version of a logic can be systematically generated from a proof calculus for the latter. Such developments provide the basis for a complete proof theory for hybrid(ised) logics, and thus pave the way to the development of (dedicated) proof support.

Algorithmique et complexité des systèmes à compteurs

Réalisé en cotutelle avec l'École normale supérieure de Cachan – Université Paris-Saclay

Adicionando temporalidade à linguagem OWL 2 : um estudo a partir da linguagem tOWL e sua decibilidade

Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, Programa de Pós-Graducação em Informática, 2016.