Volume 11, Issue 4

2015


1. Expressive Path Queries on Graph with Data

Barcelo, Pablo ; Fontaine, Gaelle ; Lin, Anthony Widjaja.
Graph data models have recently become popular owing to their applications, e.g., in social networks and the semantic web. Typical navigational query languages over graph databases - such as Conjunctive Regular Path Queries (CRPQs) - cannot express relevant properties of the interaction between […]

2. Logic and Branching Automata

Nicolas, Bedon.
In this paper we study the logical aspects of branching automata, as defined by Lodaya and Weil. We first prove that the class of languages of finite N-free posets recognized by branching automata is closed under complementation. Then we define a logic, named P-MSO as it is a extension of monadic […]

3. The computability path ordering

Blanqui, Frédéric ; Jouannaud, Jean-Pierre ; Rubio, Albert.
This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation on terms obtained by lifting a precedence on function symbols. A first […]

4. Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic

Bozzano, Marco ; Cimatti, Alessandro ; Gario, Marco ; Tonetta, Stefano.
Autonomous critical systems, such as satellites and space rovers, must be able to detect the occurrence of faults in order to ensure correct operation. This task is carried out by Fault Detection and Identification (FDI) components, that are embedded in those systems and are in charge of […]

5. Quantitative information flow under generic leakage functions and adaptive adversaries

Boreale, M. ; Pampaloni, Francesca.
We put forward a model of action-based randomization mechanisms to analyse quantitative information flow (QIF) under generic leakage functions, and under possibly adaptive adversaries. This model subsumes many of the QIF models proposed so far. Our main contributions include the following: (1) we […]

6. Finite choice, convex choice and finding roots

Roux, Stéphane Le ; Pauly, Arno.
We investigate choice principles in the Weihrauch lattice for finite sets on the one hand, and convex sets on the other hand. Increasing cardinality and increasing dimension both correspond to increasing Weihrauch degrees. Moreover, we demonstrate that the dimension of convex sets can be […]

7. A decidable weakening of Compass Logic based on cone-shaped cardinal directions

Montanari, Angelo ; Puppis, Gabriele ; Sala, Pietro.
We introduce a modal logic, called Cone Logic, whose formulas describe properties of points in the plane and spatial relationships between them. Points are labelled by proposition letters and spatial relations are induced by the four cone-shaped cardinal directions. Cone Logic can be seen as a […]

8. Faster Existential FO Model Checking on Posets

Gajarský, Jakub ; Hliněný, Petr ; Obdržálek, Jan ; Ordyniak, Sebastian.
We prove that the model checking problem for the existential fragment of first-order (FO) logic on partially ordered sets is fixed-parameter tractable (FPT) with respect to the formula and the width of a poset (the maximum size of an antichain). While there is a long line of research into FO model […]

9. From nominal to higher-order rewriting and back again

Domínguez, Jesús ; Fernández, Maribel.
We present a translation function from nominal rewriting systems (NRSs) to combinatory reduction systems (CRSs), transforming closed nominal rules and ground nominal terms to CRSs rules and terms, respectively, while preserving the rewriting relation. We also provide a reduction-preserving […]

10. Problems in number theory from busy beaver competition

Michel, Pascal.
By introducing the busy beaver competition of Turing machines, in 1962, Rado defined noncomputable functions on positive integers. The study of these functions and variants leads to many mathematical challenges. This article takes up the following one: How can a small Turing machine manage to […]

11. FO Model Checking of Interval Graphs

Ganian, Robert ; Hlineny, Petr ; Kral, Daniel ; Obdrzalek, Jan ; Schwartz, Jarett ; Teska, Jakub.
We study the computational complexity of the FO model checking problem on interval graphs, i.e., intersection graphs of intervals on the real line. The main positive result is that FO model checking and successor-invariant FO model checking can be solved in time O(n log n) for n-vertex interval […]

12. Modular session types for objects

Gay, Simon J. ; Gesbert, Nils ; Ravara, António ; Vasconcelos, Vasco T..
Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class […]

13. Type Reconstruction for the Linear \pi-Calculus with Composite Regular Types

Padovani, Luca.
We extend the linear {\pi}-calculus with composite regular types in such a way that data containing linear values can be shared among several processes, if there is no overlapping access to such values. We describe a type reconstruction algorithm for the extended type system and discuss […]

14. Datalog Rewritings of Regular Path Queries using Views

Francis, Nadime ; Segoufin, Luc ; Sirangelo, Cristina.
We consider query answering using views on graph databases, i.e. databases structured as edge-labeled graphs. We mainly consider views and queries specified by Regular Path Queries (RPQ). These are queries selecting pairs of nodes in a graph database that are connected via a path whose sequence of […]

15. Structurally Cyclic Petri Nets

Frank, Drewes ; Jérôme, Leroux.
A Petri net is structurally cyclic if every configuration is reachable from itself in one or more steps. We show that structural cyclicity is decidable in deterministic polynomial time. For this, we adapt the Kosaraju's approach for the general reachability problem for Petri nets.

16. Bisimulation of Labelled State-to-Function Transition Systems Coalgebraically

Latella, Diego ; Massink, Mieke ; De Vink, Erik P.
Labeled state-to-function transition systems, FuTS for short, are characterized by transitions which relate states to functions of states over general semirings, equipped with a rich set of higher-order operators. As such, FuTS constitute a convenient modeling instrument to deal with process […]

17. Preservation and decomposition theorems for bounded degree structures

Harwath, Frederik ; Heimberg, Lucas ; Schweikardt, Nicole.
We provide elementary algorithms for two preservation theorems for first-order sentences (FO) on the class \^ad of all finite structures of degree at most d: For each FO-sentence that is preserved under extensions (homomorphisms) on \^ad, a \^ad-equivalent existential […]

18. A finer reduction of constraint problems to digraphs

Bulín, Jakub ; Delic, Dejan ; Jackson, Marcel ; Niven, Todd.
It is well known that the constraint satisfaction problem over a general relational structure A is polynomial time equivalent to the constraint problem over some associated digraph. We present a variant of this construction and show that the corresponding constraint satisfaction problem is […]

19. A Program Logic for Verifying Secure Routing Protocols

Chen, Chen ; Jia, Limin ; Xu, Hao ; Luo, Cheng ; Zhou, Wenchao ; Loo, Boon Thau.
The Internet, as it stands today, is highly vulnerable to attacks. However, little has been done to understand and verify the formal security guarantees of proposed secure inter-domain routing protocols, such as Secure BGP (S-BGP). In this paper, we develop a sound program logic for SANDLog-a […]

20. Computational Problems in Metric Fixed Point Theory and their Weihrauch Degrees

Neumann, Eike.
We study the computational difficulty of the problem of finding fixed points of nonexpansive mappings in uniformly convex Banach spaces. We show that the fixed point sets of computable nonexpansive self-maps of a nonempty, computably weakly closed, convex and bounded subset of a computable real […]

21. Type-based Self-stabilisation for Computational Fields

Damiani, Ferruccio ; Viroli, Mirko.
Emerging network scenarios require the development of solid large-scale situated systems. Unfortunately, the diffusion/aggregation computational processes therein often introduce a source of complexity that hampers predictability of the overall system behaviour. Computational fields have […]

22. Typed realizability for first-order classical analysis

Blot, Valentin.
We describe a realizability framework for classical first-order logic in which realizers live in (a model of) typed {\lambda}{\mu}-calculus. This allows a direct interpretation of classical proofs, avoiding the usual negative translation to intuitionistic logic. We prove that the usual terms of […]