Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(8)
Boolean Operation
Decision Problem
Finite State Automata
Infinite Word
Linear Time
Model Checking
Satisfiability
Visibly Pushdown Automata
Subscribe
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/9783540744078_32,Laura Bozzelli
Edit
Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages
(
Citations: 3
)
BibTex

RIS

RefWorks
Download
Laura Bozzelli
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 2Exptimecomplete. Due to this high complexity, we introduce a new class of alternating automata called alternating jump automata (AJA). AJA extend classical alternating finitestate automata over infinite words by also allowing nonlocal moves. A nonlocal forward move leads a copy of the automaton from a call input position to the matchingreturn position. We also allow local and nonlocal backward moves. We show that oneway AJA and twoway 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 modelchecking for parity twoway AJA are Exptimecomplete. Finally, we consider a lineartime fixpoint calculus which subsumes the full lineartime μ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 twoway AJA, and vice versa. As a consequence
satisfiability
and pushdown
model checking
for this logic are Exptimecomplete.
Conference:
International Conference on Concurrency Theory  CONCUR
, pp. 476491, 2007
DOI:
10.1007/9783540744078_32
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.
(
www.springerlink.com
)
(
www.springerlink.com
)
(
dx.doi.org
)
(
www.informatik.unitrier.de
)
More »
Citation Context
(3)
...a formula in a temporal logic over nested words like CaRet [4], NWTL [2], and μNWTL [
10
], is translated into a languageequivalent NWA...
...We omit the details of this transformation construction since it is similar to a construction in [
10
] for socalled 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 lineartime μcalculus [8] by next modalities for the calls and returns in nested words...
Christian Dax
,
et 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 Arenas
,
et al.
Regular Languages of Nested Words: Fixed Points, Automata, and Synchro...
...For finite words, we propose a translation of CCaRet 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 exponentialtime blowup...
...For finite words, we propose a translation of CCaRet 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 exponentialtime blowup...
...Alternating jump (finitestate) 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
References
(17)
A fixpoint calculus for local and global program flows
(
Citations: 17
)
Rajeev Alur
,
Swarat Chaudhuri
,
P. Madhusudan
Conference:
ACM SIGPLANSIGACT Symposium on Principles of Programming Languages  POPL
, pp. 153165, 2006
Languages of Nested Trees
(
Citations: 15
)
Rajeev Alur
,
Swarat Chaudhuri
,
P. Madhusudan
Conference:
Computer Aided Verification  CAV
, pp. 329342, 2006
A Temporal Logic of Nested Calls and Returns
(
Citations: 77
)
Rajeev Alur
,
Kousha Etessami
,
P. Madhusudan
Conference:
Tools and Algorithms for Construction and Analysis of Systems  TACAS
, pp. 467481, 2004
Visibly pushdown languages
(
Citations: 148
)
Rajeev Alur
,
P. Madhusudan
Conference:
ACM Symposium on Theory of Computing  STOC
, pp. 202211, 2004
Adding Nesting Structure to Words
(
Citations: 59
)
Rajeev Alur
,
P. Madhusudan
Conference:
Developments in Language Theory  DLT
, pp. 113, 2006
Sort by:
Citations
(3)
Alternation Elimination for Automata over Nested Words
(
Citations: 1
)
Christian Dax
,
Felix Klaedtke
Conference:
Foundations of Software Science and Computation Structure  FoSSaCS
, pp. 168183, 2011
Regular Languages of Nested Words: Fixed Points, Automata, and Synchronization
Marcelo Arenas
,
Pablo Barceló
,
Leonid Libkin
Journal:
Theory of Computing Systems / Mathematical Systems Theory  MST
, vol. 49, no. 3, pp. 639670, 2011
The Complexity of CaRet + Chop
(
Citations: 1
)
Laura Bozzelli
Conference:
International Workshop on Temporal Representation and Reasoning  TIME
, pp. 2331, 2008