Academic
Publications
Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages

Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages,10.1007/978-3-540-74407-8_32,Laura Bozzelli

Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages   (Citations: 3)
BibTex | RIS | RefWorks Download
We investigate various classes of alternating automata for visibly pushdown languages (VPL) over infinite words. First, we show that alternating visibly pushdown automata (AVPA) are exactly as expressive as their nondeterministic counterpart (NVPA) but basic decision problems for AVPA are 2Exptime-complete. Due to this high complexity, we introduce a new class of alternating automata called alternating jump automata (AJA). AJA extend classical alternating finite-state automata over infinite words by also allowing non-local moves. A non-local forward move leads a copy of the automaton from a call input position to the matching-return position. We also allow local and non-local backward moves. We show that one-way AJA and two-way AJA have the same expressiveness and capture exactly the class of VPL. Moreover, boolean operations for AJA are easy and basic decision problems such as emptiness, universality, and pushdown model-checking for parity two-way AJA are Exptime-complete. Finally, we consider a linear-time fixpoint calculus which subsumes the full linear-time μ-calculus (with both forward and backward modalities) and the logic CaRet and captures exactly the class of VPL. We show that formulas of this logic can be linearly translated into parity two-way AJA, and vice versa. As a consequence satisfiability and pushdown model checking for this logic are Exptime-complete.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...a formula in a temporal logic over nested words like CaRet [4], NWTL [2], and μNWTL [10], is translated into a language-equivalent NWA...
    • ...We omit the details of this transformation construction since it is similar to a construction in [10] for so-called jumping automata, which are very similar to our alternating automata when restricting their inputs to the graph representation of nested words...
    • ...In [10], Bozzelli introduces the temporal logic μNWTL, which extends the linear-time μ-calculus [8] by next modalities for the calls and returns in nested words...

    Christian Daxet al. Alternation Elimination for Automata over Nested Words

    • ...Alternating automata for nested words were introduced independently, and at about the same time, in [14]...
    • ...In this paper, we compare our automata model with the automata model introduced in [14] and, in particular, we use a result from [14] to prove that alternation can be eliminated in our case...
    • ...In this paper, we compare our automata model with the automata model introduced in [14] and, in particular, we use a result from [14] to prove that alternation can be eliminated in our case...
    • ...Proof We start by introducing the necessary terminology to state a result in [14] that is used to prove the theorem...
    • ...with ⊥ a special stack bottom symbol not contained in [14]...
    • ...1 It is important to notice that alternating visibly pushdown automata were introduced in [14] by considering a parity acceptance condition...
    • ...We reformulate here some of the results of [14] for alternating visibly pushdown automata with a Büchi acceptance condition...
    • ...Then Büchi AVPA A is said to accept an ω-word w if and only if there exists a run T of A over w such that for every infinite path ρ in T starting at the root, Inf (ρ) ∩ F = ∅. In [14], it is proved that:...
    • ...Theorem 4.11 [14] For every Büchi AVPA A of size n, there exists (and can be effectively constructed) an equivalent Büchi NVPA B of size 2 2...

    Marcelo Arenaset al. Regular Languages of Nested Words: Fixed Points, Automata, and Synchro...

    • ...For finite words, we propose a translation of C-CaRet formulas into equivalent NVPA, while for infinite words we exploit the class of alternating jump (finite‐state) automata (AJA) [6] which can be translated into equivalent NVPA [6] with a single exponential-time blow-up...
    • ...For finite words, we propose a translation of C-CaRet formulas into equivalent NVPA, while for infinite words we exploit the class of alternating jump (finite‐state) automata (AJA) [6] which can be translated into equivalent NVPA [6] with a single exponential-time blow-up...
    • ...Alternating jump (finite-state) automata (AJA) [6] operate on infinite words over a pushdown alphabet and capture exactly the class of VPL...
    • ...NVPA (resp., the AJA) of Theorem 3 (resp., Theorem 4) associated with ¬ϕ. By [3] (resp., [6]) this can be done in time polynomial in the size of M and polynomial (resp., singly exponential) in the size of P¬ϕ (rep., A¬ϕ)...

    Laura Bozzelli. The Complexity of CaRet + Chop

Sort by: