5
$\begingroup$

I was wondering about what could possibly be the motivation behind defining the deterministic looping automata? What puzzles me is that they accept a word iff they have a run on it!

I believe they are strongly related to DBWs. And i would like to see how.

My intuition: since we can assume W.l.o.g that each non-accepting state $q$ in a DBW $A$ has a loop of non-accepting states containing q. Maybe one can look at the $strongly$ $connected$ $components$ of $A_{rej}$, Where $A_{rej}$ denotes $A$ restricted to non-accepting states, as looping automata.

Relevant papers could help.

Note: i am new to research. In particular i have few knowledge about DBWs. Its more a reference than a question.

thanks.

$\endgroup$
  • $\begingroup$ What's a DBW? Which definition of looping automata are you using? $\endgroup$ – András Salamon Sep 29 '17 at 15:30
  • $\begingroup$ DBW $A=(\Sigma, Q, q_0, \delta, F)$ is deteriministic büchi automaton where $\delta$ is a partial function from $Q \times \Sigma$ to $Q$. And a deterministic looping automaton $A$ is defined exactly as the deterministic büchi automaton but all states are accepting. i.e., $F=Q$. $\endgroup$ – Bader Abu Radi Sep 29 '17 at 15:53
9
$\begingroup$

In a looping automaton, the transition function is not assumed to be total. That is, for a state $q$ and a letter $\sigma$, it could be the case that $\delta(q,\sigma)$ is undefined. Intuitively, this is the same as having a transition to a rejecting sink.

So they are "deterministic" in the sense that there is no non-determinism. But still, this means that for every word either there is a single run, or there are no runs. Thus, saying that a word is accepted iff it has a run on it is not a trivial acceptance condition.

The reason for studying these automata is that they correspond to safety properties. A safety property is a language $L$ such that for every word $w\notin L$, there exists some prefix $x$ of $w$ such that for every suffix $y$, $x\cdot y\notin L$. That is, once you read $x$, there is no way to get in the language. These properties are useful in practice, as they correspond to "system failure", in a way. That is, once something really bad happens, you can't recover.

Technically, these autoamta are useful because of their simple acceptance condition.

As for references, start here. Also, Orna Kupferman has several papers using these objects (but I suspect you already know that... :) )

$\endgroup$
  • $\begingroup$ Thanks for the thorough answer. And your suspicion seems to be correct :) $\endgroup$ – Bader Abu Radi Oct 1 '17 at 18:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.