Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userSafety alternating automata on data words
127
0
0.0
(
0
)
Added by
Ranko Lazic
Publication date
2010
fields
Informatics Engineering
and research's language is
English
Authors
Ranko Lazic
Ask ChatGPT about the research
No Arabic abstract
A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. Safety one-way alternating automata with one register on infinite data words are considered, their nonemptiness is shown EXPSPACE-complete, and their inclusion decidable but not primitive recursive. The same complexity bounds are obtained for satisfiability and refinement, respectively, for the safety fragment of linear temporal logic with freeze quantification. Dropping the safety restriction, adding past temporal operators, or adding one more register, each causes undecidability.
rate research
Read More
A data tree is an unranked ordered tree whose every node is labelled by a letter from a finite alphabet and an element (datum) from an infinite set, where the latter can only be compared for equality. The article considers alternating automata on data trees that can move downward and rightward, and have one register for storing data. The main results are that nonemptiness over finite data trees is decidable but not primitive recursive, and that nonemptiness of safety automata is decidable but not elementary. The proofs use nondeterministic tree automata with faulty counters. Allowing upward moves, leftward moves, or two registers, each causes undecidability. As corollaries, decidability is obtained for two data-sensitive fragments of the XPath query language.
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $bigwedge_{i=1}^n mathbf{G}mathbf{F} varphi_i vee mathbf{F}mathbf{G} psi_i$, where $varphi_i$ and $psi_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.
In this paper, we investigate statistics on alternating words under correspondence between ``possible reflection paths within several layers of glass and ``alternating words. For $v=(v_1,v_2,cdots,v_n)inmathbb{Z}^{n}$, we say $P$ is a path within $n$ glass plates corresponding to $v$, if $P$ has exactly $v_i$ reflections occurring at the $i^{rm{th}}$ plate for all $iin{1,2,cdots,n}$. We give a recursion for the number of paths corresponding to $v$ satisfying $v in mathbb{Z}^n$ and $sum_{igeq 1} v_i=m$. Also, we establish recursions for statistics around the number of paths corresponding to a given vector $vinmathbb{Z}^n$ and a closed form for $n=3$. Finally, we give a equivalent condition for the existence of path corresponding to a given vector $v$.
In [1], we introduced the weakly synchronizing languages for probabilistic automata. In this report, we show that the emptiness problem of weakly synchronizing languages for probabilistic automata is undecidable. This implies that the decidability result of [1-3] for the emptiness problem of weakly synchronizing language is incorrect.
Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper we describe a single exponential translation from limit-deterministic Buchi automata (LDBA) to DPA, and show that it can be concatenated with a recent efficient translation from LTL to LDBA to yield a double exponential, enquote{Safraless} LTL-to-DPA construction. We also report on an implementation, a comparison with the SPOT library, and performance on several sets of formulas, including instances from the 2016 SyntComp competition.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
