Author name cluster

Gaëlle Fontaine

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

I&C Journal 2018 Journal Article

Cycle detection in computation tree logic

Gaëlle Fontaine
Fabio Mogavero
Aniello Murano
Giuseppe Perelli
Loredana Sorrentino

We introduce Cycle- CTL ⋆, an extension of CTL ⋆ with cycle quantifications that are able to predicate over cycles. The introduced logic turns out to be very expressive. Indeed, we prove that it strictly extends CTL ⋆ and is orthogonal to μ Calculus. We also give an evidence of its usefulness by providing few examples involving non-regular properties. We extensively investigate both the model-checking and satisfiability problems for Cycle- CTL ⋆ and some of its variants/fragments.

Details DOI

GandALF Workshop 2016 Workshop Paper

Cycle Detection in Computation Tree Logic

Gaëlle Fontaine
Fabio Mogavero
Aniello Murano
Giuseppe Perelli
Loredana Sorrentino

Temporal logic is a very powerful formalism deeply investigated and used in formal system design and verification. Its application usually reduces to solving specific decision problems such as model checking and satisfiability. In these kind of problems, the solution often requires detecting some specific properties over cycles. For instance, this happens when using classic techniques based on automata, game-theory, SCC decomposition, and the like. Surprisingly, no temporal logics have been considered so far with the explicit ability of talking about cycles. In this paper we introduce Cycle-CTL*, an extension of the classical branching-time temporal logic CTL* along with cycle quantifications in order to predicate over cycles. This logic turns out to be very expressive. Indeed, we prove that it strictly extends CTL* and is orthogonal to mu-calculus. We also give an evidence of its usefulness by providing few examples involving non-regular properties. We investigate the model checking problem for Cycle-CTL* and show that it is PSPACE-Complete as for CTL*. We also study the satisfiability problem for the existential-cycle fragment of the logic and show that it is solvable in 2ExpTime. This result makes use of an automata-theoretic approach along with novel ad-hoc definitions of bisimulation and tree-like unwinding.

PDF Details DOI

LPAR Conference 2013 Conference Paper

Expressive Path Queries on Graphs with Data

Pablo Barceló
Gaëlle Fontaine
Anthony W. Lin

Abstract Graph data models have recently become popular owing to their applications, e. g. , in social networks, semantic web. Typical navigational query languages over graph databases — such as Conjunctive Regular Path Queries (CRPQs) — cannot express relevant properties of the interaction between the underlying data and the topology. Two languages have been recently proposed to overcome this problem: walk logic (WL) and regular expressions with memory (REM). In this paper, we begin by investigating fundamental properties of WL and REM, i. e. , complexity of evaluation problems and expressive power. We first show that the data complexity of WL is nonelementary, which rules out its practicality. On the other hand, while REM has low data complexity, we point out that many natural data/topology properties of graphs expressible in WL cannot be expressed in REM. To this end, we propose register logic, an extension of REM, which we show to be able to express many natural graph properties expressible in WL, while at the same time preserving the elementariness of data complexity of REMs. It is also incomparable in expressive power against WL.

Details

Highlights Conference 2013 Conference Abstract

Semantic acyclicity on graph databases

Pablo Barcelo
Gaëlle Fontaine
Miguel Romero
Moshe Y. Vardi

Unions of acyclic conjunctive queries (CQs) can be evaluated in linear time, as opposed to arbitrary CQs, for which the evaluation problem is NP-complete. It is known that evaluation of semantically acyclic unions of CQs - i. e. , unions of CQs that are equivalent to a union of acyclic ones - is tractable. We study the notion of semantic acyclicity in the context of graph databases and unions of conjunctive regular path queries (UCRPQs). We prove that checking whether a UCRPQ is semantically acyclic is decidable in 2ExpSpace and is ExpSpace-hard. We show that evaluation of semantically acyclic UCRPQs is fixed-parameter tractable.

PDF Details

MFCS Conference 2010 Conference Paper

Frame Definability for Classes of Trees in the µ -calculus

Gaëlle Fontaine
Thomas Place

Abstract We are interested in frame definability of classes of trees, using formulas of the μ -calculus. In this set up, the proposition letters (or in other words, the free variables) in the μ -formulas correspond to second order variables over which universally quantify. Our main result is a semantic characterization of the MSO definable classes of trees that are definable by a μ -formula. We also show that it is decidable whether a given MSO formula corresponds to a μ -formula, in the sense that they define the same class of trees.

Details

CSL Conference 2008 Conference Paper

Continuous Fragment of the mu-Calculus

Gaëlle Fontaine

Abstract In this paper we investigate the Scott continuous fragment of the modal μ -calculus. We discuss its relation with constructivity, where we call a formula constructive if its least fixpoint is always reached in at most ω steps. Our main result is a syntactic characterization of this continuous fragment. We also show that it is decidable whether a formula is continuous.

Details