1
$\begingroup$

This question is specifically about the paper "Guarded Fixed Point Logic" by Gradel and Walukiewicz. Among other things they prove the decidability of the satisfiability problem for Fixpoint Loosely Guarded Fragment of First-Order Logic.

They see tableaux as input trees for alternating two-way automata.

Their proof follows these steps:

1) For any given sentence $\psi$, one can algorithmically build an alternating two-way automaton $\mathcal{A}_\psi$ such that $\mathcal{A}_\psi$ accepts $T$ iff $T$ is a tableau for $\psi$.

2) For any given sentence $\psi$, one can algorithmically build an alternating two-way automaton $\mathcal{A}_\psi$ such that $\mathcal{A}_\psi$ accepts $T$ iff $T$ is a tableau that represents a model for $\psi$.

3) Their alternating two-way automata are closed under intersection and have decidable emptiness problem.

They don’t talk about accepting conditions for their alternating two-way automata. Rather, they directly define acceptance in terms of games and winning strategies. I would like to:

1) See the accepting conditions for their alternating two-way automata explicitly stated without talking about games.

2) Know why the number of constants that we need to build the tableaux is bound by $2\cdot$ (width of $\psi$). Does this mean that if the initial sentence is satisfiable, then it has a model of size $\leq 2\cdot$ (width of $\psi$)?

3) Know what could be dropped or modified if one in interested only in the Loosely Guarded Fragment of First-Order Logic WITHOUT FIXPOINTS.

Hope someone is interested too.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

The considered automaton model A2A (two-way alternating tree automaton) is similar to an Alternating Turing Machine, with the following differences:

  • The automaton runs on a rooted tree, whose nodes are labeled, and each node has an arbitrary (finite) number of children,
  • The automaton does not modify the input tree,
  • The automaton can choose its next state, and to remain in the same node of the tree, or to move to some neighbor, but cannot specify in which direction it moves. Therefore, if the state is an existential state, the automaton accepts if it accepts after moving in some direction; if the state is a universal state, the automaton accepts if it accepts after moving in each direction.
  • The runs are infinite, and the accepting condition is described by the parity condition (an infinite run is considered accepting if the smallest state $\Omega(q)$ appearing infinitely often is even).

To understand how the last condition is formally implemented, it is actually useful to think in terms of a game played by two players (the existential and universal player).

Various kinds of alternating automata are a standard notion in automata theory – see e.g.

  • "Automata on Infinite Trees" by Christof Loding
  • "Automata on Infinite Objects" by Wolfgang Thomas.
Improve this answer
$\endgroup$
2
  • $\begingroup$ (Part 1) Thank you for the answer. I would also like to have an intuitive reading of the accepting condition. If I understand correctly: - a move for the existential player means going down one node (i.e. type) in the tree (i.e. tableau). That in turn means “exhibiting a witness” for an existential formula. - a move for the universal player means staying on the same node but changing state. That in turn means “testing an already proposed witness” on an universal formula. $\endgroup$
    – Alberto
    Commented Sep 2, 2016 at 13:17
  • $\begingroup$ (Part 2) Now I have trouble relating the formal definition of parity accepting condition with the intuitive idea of "the existential player can always propose a new witness element and the universal player can test all witnesses without finding a contradiction”. $\endgroup$
    – Alberto
    Commented Sep 2, 2016 at 13:18

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .