|
- Journal
Articles:
- with Luca
Alberucci: On
Modal µ-Calculus
and
Gödel-Löb
Logic. Studia Logica: 91, 145-169 (2009)
Abstract:
"We show that the modal µ-calculus over GL collapses to the modal
fragment by showing that the fixpoint formula is reached after two
iterations and answer to a question posed by van Benthem in
[vBe06]. Further, we introduce the modal µ∼-calculus by
allowing fixpoint constructors for any formula where the fixpoint
variable appears guarded but not necessarily positive and show that
this calculus over GL collapses to the modal fragment, too. The latter
result allows us a new proof of the
de Jongh, Sambin Theorem and provides a simple algorithm to construct
the fixpoint formula."
- with Luca
Alberucci: The
Modal μ-Calculus Hierarchy on Restricted Classes of Transition
Systems. The Journal of Symbolic Logic:
74(4), 1367-1400 (2009)
Abstract:
"We discuss the strictness of the modal µ-calculus hierarchy over
some restricted classes of transition systems. First, we show
that the hierarchy is strict over reflexive frames. By proving the
finite model
theorem for reflexive systems the same results holds for finite models.
Second, we prove that over transitive systems the hierarchy collapses
to the alternation-free fragment. In order to do this the finite model
theorem
for transitive transition systems is also proved. Further, we verify
that if symmetry is added to transitivity the hierarchy collapses
to the purely modal fragment."
- Papers in
Refereed Conferences:
- with Jacques
Duparc: Describing
the
Wadge
Hierarchy
for
the
Alternation
Free
Fragment
of
μ-Calculus
(I):
The
Levels
Below
ω_1
in:
Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Löwe (eds.):
Logic and Theory of
Algorithms, Fourth Conference on Computability in
Europe, CiE 2008, Athens, Greece, June 2008, Proceedings.
Springer
LNCS 5028, 2008
Abstract:
"The height of the Wadge Hierarchy
for the Alternation Free Fragment of
µ-calculus is known to be at least ϵ_0 . It was conjectured that
the height is exactly ϵ_0 . We make a first step towards the proof of
this conjecture by showing that there is no ∆^µ_2 definable set in
between the levels ω^ω and ω_1 of the Wadge Hierarchy of Borel
Sets."
- with Jacques
Duparc: A
Playful Glance at Hierarchical Questions for Two-Way Alternating
Automata
In: Margaret Archibald, Vasco Brattka, Valentin Goranko, Benedikt
Löwe (eds.): Infinity in Logic
and Computation, Revised Selected Papers of the International
Conference
Infinity in Computation and Logic, Cape Town, South Africa, November
2007. Springer LNAI 5489, 2009
Abstract:
"Two-way alternating automata were introduced by Vardi in order to
study the satisfiability problem for the modal µ-calculus
extended with backwards modalities.
In this paper, we present a very simple proof by way of Wadge
games of the strictness of the hierarchy of Motowski indices of two-way
alternating automata over trees."
- with
Jacques Duparc and Filip
Murlak: Linear Game Automata -
Decidable Hierarchy Problems for Stripped-Down Alternating Tree
Automata [full
version
on
HAL]. In: Erich
Graedel, Reinhard Kahle (eds.): CSL
09. Springer LNCS 5771, pp. 225-239
Abstract:
"For deterministic tree automata, classical hierarchies, like
Mostowski-Rabin (or index) hierarchy, Borel hierarchy, or Wadge
hierarchy, are known to be decidable. However, when it comes to
non-deterministic tree automata, none of these hierarchies is
even close to be understood. Here we make a second attempt in paving
the way towards a clear understanding of tree automata. We concentrate
on the class of linear game automata (LGA), and prove within this new
context, that all corresponding hierarchies mentioned
above—Mostowski-Rabin, Borel, and Wadge—are decidable. The class LGA is
obtained by taking linear tree automata with alternation restricted to
the choice of path in the input tree. Despite their simplicity, LGA
recognize sets of arbitrary high Borel rank. The actual richness of LGA
is revealed by the height of their Wadge hierarchy: (ω^ω)^ω"
- with
J. Cabessa,
J.
Duparc and F. Murlak: The
Wadge
Hierarchy
of
Max-Regular
Languages. In:
Ravi Kannan and K. Narayan Kumar (eds.): IARCS Annual Conference on Foundations of
Software Technology and Theoretical Computer Science (FSTTCS 2009).
Leibniz
International
Proceedings
in
Informatics,
vol.
4,
2009,
pp.
121-132
Abstract:
"Recently, Mikolaj Bojanczyk introduced a class of max-regular
languages, an extension of regular languages of infinite words
preserving many of its usual properties. This new class can be
seen as a different way of generalizing the notion of regularity from
finite to infinite words. This paper compares regular and
max-regular languages in terms of topological complexity. It is proved
that up to Wadge equivalence the classes coincide. Moreover, when
restricted to $\mathbf{\Delta}^0_2$-languages, the classes
contain virtually the same languages. On the other hand,
separating examples of arbitrary complexity exceeding
$\mathbf{\Delta}^0_2$ are constructed."
- with Balder
ten
Cate: Characterizing EF over Infinite Trees
and Modal Logic on
Transitive Graphs. MFCS 2011: 290-302.
Abstract:
"We provide several effective equivalent characterizations of $\EF$
(the modal
logic of the descendant relation) on arbitrary trees. More
specifically, we prove that, for $\EF$-bisimulation invariant
properties of trees, being definable by an $\EF$ formula, being a
Borel set, and being definable in weak monadic second order logic, all
coincide. The proof builds upon a known algebraic characterization of
$\EF$ for the case of \emph{finitely branching} trees due to
Boja\'nczyk and Idziaszek. We furthermore obtain characterizations of
modal logic on transitive Kripke structures as a fragment of weak
monadic second order logic and of the mu-calculus."
- with
J.
Duparc and F. Murlak: Definable
Operations
On
Weakly Recognizable Sets of Trees (full
version). In: FSTTCS 2011.
Abstract:
"Alternating automata on infinite trees induce operations on languages
which do not preserve natural equivalence relations, like having the
same Mostowski–Rabin index, the same Borel rank, or being continuously
reducible to each other (Wadge equivalence). In order to prevent this,
alternation needs to be restricted to the choice of direction in the
tree. For weak alternating automata with restricted alternation a small
set of computable operations generates all definable operations, which
implies that the Wadge degree of a given automaton is computable. The
weak index and the Borel rank coincide, and are computable. An
equivalent automaton of minimal index can be computed in polynomial
time (if the productive states of the automaton are given)."
- Thesis:
- [T1]
(University of Lausanne & University of Bordeaux 1) A Study on the
Expressive Power of Some Fragments of the Modal Mu-Calculus
Abstract:
"In this work we study the complexity of some fragments of the modal
$\mu$-calculus from two points of view: the syntactical and the
topological. In the first part of the dissertation we adopt the
syntactical point of view in order to study the behavior of this
formalism on some restricted classes of models. Among other results, we
show that on transitive transition systems, every $\mu$-formula is
logically equivalent to an alternation free formula. For what concerns
the topological point of view, we first prove that on transitive
models, the modal logic is exactly the Borel fragment of the modal
$\mu$-calculus. Then we provide an effective description of the Borel
and Wadge hierarchies of a sub-fragment of the alternation free
fragment of the $\mu$-calculus on binary trees. Finally we verify that
for this fragment the syntactical point of view and topological point
of view coincide. "
|
|
|