Relating word and tree automata (Q2576943): Difference between revisions

From MaRDI portal
Importer (talk | contribs)
Created a new Item
 
ReferenceBot (talk | contribs)
Changed an Item
 
(5 intermediate revisions by 4 users not shown)
Property / author
 
Property / author: Shmuel Safra / rank
Normal rank
 
Property / reviewed by
 
Property / reviewed by: Aleksej Dmitrievich Korshunov / rank
Normal rank
 
Property / author
 
Property / author: Shmuel Safra / rank
 
Normal rank
Property / reviewed by
 
Property / reviewed by: Aleksej Dmitrievich Korshunov / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1016/j.apal.2005.06.009 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W2044854034 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4539644 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5525343 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4733398 / rank
 
Normal rank
Property / cites work
 
Property / cites work: “Sometimes” and “not never” revisited / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3739111 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4385542 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Deciding full branching time logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4518423 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Complementing deterministic Büchi automata in polynomial time / rank
 
Normal rank
Property / cites work
 
Property / cites work: The complexity of verification / rank
 
Normal rank
Property / cites work
 
Property / cites work: Automated Technology for Verification and Analysis / rank
 
Normal rank
Property / cites work
 
Property / cites work: From linear time to branching time / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4542592 / rank
 
Normal rank
Property / cites work
 
Property / cites work: An automata-theoretic approach to branching-time model checking / rank
 
Normal rank
Property / cites work
 
Property / cites work: Decision problems forω-automata / rank
 
Normal rank
Property / cites work
 
Property / cites work: Efficient minimization of deterministic weak \(\omega\)-automata / rank
 
Normal rank
Property / cites work
 
Property / cites work: Testing and generating infinite sequences by a finite automaton / rank
 
Normal rank
Property / cites work
 
Property / cites work: Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra / rank
 
Normal rank
Property / cites work
 
Property / cites work: On syntactic congruences for \(\omega\)-languages / rank
 
Normal rank
Property / cites work
 
Property / cites work: FINITE STATE PROCESSES, Z-TEMPORAL LOGIC AND THE MONADIC THEORY OF THE INTEGERS / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4381391 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4205072 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Decidability of Second-Order Theories and Automata on Infinite Trees / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5616162 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The complexity of propositional linear temporal logics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Deciding Equivalence of Finite Tree Automata / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4385530 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Generalized finite automata theory with an application to a decision problem of second-order logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Automata-theoretic techniques for modal logics of programs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Reasoning about infinite computations / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3948585 / rank
 
Normal rank
links / mardi / namelinks / mardi / name
 

Latest revision as of 14:32, 11 June 2024

scientific article
Language Label Description Also known as
English
Relating word and tree automata
scientific article

    Statements

    Relating word and tree automata (English)
    0 references
    0 references
    0 references
    0 references
    29 December 2005
    0 references
    A Büchi word automaton is \(A=\langle\Sigma,Q,\delta,Q_0,F\rangle\), where \(\Sigma\) is the input alphabet, \(Q\) is a finite set of states, \(\delta:Q\times\Sigma\rightarrow 2^Q\) is a transition function, \(Q_0\subseteq Q\) is the set of initial states and \(F\subseteq Q\) is the set of accepting states. If \(A\) has several initial states or the transition function may specify many possible transmissions for each state and letter, \(A\) is nondeterministic. If \(| Q_0| =1\) and \(\delta\) is such that, for every \(q\in Q\) and \(\sigma\in\Sigma\), we have that \(| \delta(q,\sigma)| \leq 1\), then \(A\) is a deterministic automaton. A Büchi tree automaton is \(U=\langle\Sigma,Q,\delta,Q_0,F\rangle\), where \(\Sigma,Q,\delta,Q_0\) and \(F\) are as in Büchi word automata, and \(\delta:Q\times\Sigma\rightarrow 2^{Q\times Q}\) is a (nondeterministic) transition function. Let \(T\) be the infinite binary tree. A run of \(U\) on an input \(\Sigma\)-labeled tree \(V\) is a \(Q\)-labeled tree \(r\) such that \(r(\varepsilon)\in Q_0\) and for every \(x\in T\) we have that \(\langle r(x,0), r(x,1)\rangle\in \delta(r(x),V(x))\). Given a run \(r\) and a path \(\pi\subset T\), let \[ \inf (r| n) =\{q\in Q: \text{ for infinitely many } x\in\pi,\text{ we have } r(x)= q\}. \] A run \(r\) is accepting iff for each path \(\pi\subset T\) there exists a state in \(F\) that \(r\) visits infinitely often along \(\pi\). Rabin word automata are identical to Büchi word automata, only that the acceptance condition \(F\subseteq 2^{Q\times Q}\) is a set \(\{\langle G_1,B_1\rangle,\dots, \langle G_k,B_k\rangle\}\) of pairs of subsets of \(Q\), and a run \(r\) is accepting iff there is \(1\leq i\leq k\) such that \(\inf (r)\cap G_i \neq \emptyset\). Rabin tree automata are indentical to Büchi tree automata, except that a run is accepting iff for each path \(\pi\subset T\), there is \(1\leq i\leq k\) such that \(\inf (r| n)\cap G_i \neq\emptyset\) and \(\inf (r| n)\cap B_i \neq\emptyset\). For a word language \(L\subseteq \Sigma^\omega\), the derived language of \(L\), denoted by \(L_\Delta\), is the set of all trees all of whose paths are labeled with words in \(L\). It is shown that a word language \(L\) is recognizable by a nondeterministic Büchi word automaton but not recognizable by a deterministic Büchi word automaton iff \(L\) is recognizable by a nondeterministic Rabin tree automaton. Let \(U\) be a Büchi tree automaton that recognizes \(L_\Delta\). The authors construct a deterministic Büchi word automaton \(A\) that recognizes \(L\). For \(U\) with \(n\) states, the automaton \(A\) has almost \(2^{n+1}\) states.
    0 references
    tree automata
    0 references
    word automata
    0 references
    expressive power
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers