<p>If I understand your model correctly, then it's enough for you that all runs either get stuck in accepting states, or get stuck in non-accepting states.
If this is the case, you can also use deterministic weak Buchi automata, which are more expressive than $satefy\cup co-safety$.</p>

CC BY-SA 3.0
2013-02-13T09:31:20.317Z
2013-02-13T21:16:56.977Z
2013-02-13T21:16:56.977Z
Shaull
<p>I am doing implicit Buchi determination for LTL logic in hardware where the combinational logic represents the set of states. </p>

<p>But instead of using acceptance states, I am using final state (as in NFA). Using this approach it seems that I can synthesize all co-safety  and safety properties.  </p>

<p>Is my assumption wrong?</p>

<p><strong>In their paper "Model-checking for safety properties" Orna kupferman and vardi prove that finite alternating automata which is obtained by redefining the set of accepting states as empty states can monitor all the informative prefixes for safety, co-sfety properties. So in my algorithm I construct Buchi automata for LTL property(negation) and define the accepatnce set as the empty set(unconditionally accepting state) in it.   So my question can be reframed as "Is the assumption that the definition of acceptance set as empty in alternating automaton is equivalent to defining acceptance set in Buchi automata as empty and hence the Buchi automata recognizes all the prefixes recognized by finite alternating automata"?
Thanks for all the suggestions and reply.<em>*</em>**</strong> </p>

CC BY-SA 3.0
2013-01-16T05:58:18.640Z
@Sylvain, your comment can be an answer.
Kaveh
CC BY-SA 3.0
2013-02-13T16:27:39.340Z
the question is not clear to me. If your final states means "once I reach it I won", then this is call a reachability objective, which is very different from safety.
Denis
CC BY-SA 3.0
2013-02-14T12:25:42.850Z
I think it may depend on how you construct the Buchi automaton.
If you have an alternating automaton without accepting states (except $\top$), then if you apply the Miyano-Hayashi alternation removal, you end up with a nondeterministic Buchi automaton, where still all the state are not accepting, except one accepting sink. So in this sense, I think that the answer is "yes".
However, if you use the Vardi-Wolper construction to obtain the Buchi automaton, this is not so certain, since this construction behaves differently in some aspects.
Shaull
CC BY-SA 3.0
2013-02-20T06:58:38.660Z
I figured the same...thanks for the reply @Shaull
pratibha sawhney
CC BY-SA 3.0
2012-10-09T13:08:17.640Z
What is the difference between a final state and an accepting state. What assumption are you referring to?
Dave Clarke
CC BY-SA 3.0
2012-10-09T14:22:53.473Z
Are your words infinite?  If so, how are you using a final state?  Maybe you should define your model and domain explicitly.
John K.
CC BY-SA 3.0
2012-10-11T11:27:36.940Z
Yes, my words are infinite. But as I have to construct deterministic finite machine to recognize them, so i have restricted my set of properties(safety and weak co-safety) properties which can be recognized by Buchi automaton which have unconditionally accepting state(with a true loop).  So my assumption is that  for all safety properties(also weak until properties) such automaton exists. Am i correct in my assumption?? any comments would be highly appreciated - pratibha @Pal GD
pratibha sawhney
CC BY-SA 3.0
2012-10-21T11:11:10.900Z
Your assumption is correct: safety languages can be recognized by Büchi automata with all states accepting.  See for instance the book _Infinite Words_ by Perrin and Pin.
Sylvain
<lo.logic><fl.formal-languages><automata-theory><linear-temporal-logic>
Implicit Non-deterministic Buchi determinization
pratibha sawhney
# Implicit Non-deterministic Buchi determinization

(Asked by: username_0 on 2012-10-09)

I am doing implicit Buchi determination for LTL logic in hardware where the combinational logic represents the set of states.

But instead of using acceptance states, I am using final state (as in NFA). Using this approach it seems that I can synthesize all co-safety and safety properties.

Is my assumption wrong?

**In their paper "Model-checking for safety properties" Orna kupferman and vardi prove that finite alternating automata which is obtained by redefining the set of accepting states as empty states can monitor all the informative prefixes for safety, co-sfety properties. So in my algorithm I construct Buchi automata for LTL property(negation) and define the accepatnce set as the empty set(unconditionally accepting state) in it. So my question can be reframed as "Is the assumption that the definition of acceptance set as empty in alternating automaton is equivalent to defining acceptance set in Buchi automata as empty and hence the Buchi automata recognizes all the prefixes recognized by finite alternating automata"?
Thanks for all the suggestions and reply.*\**\*\***

**Tags:** lo.logic, fl.formal-languages, automata-theory, linear-temporal-logic

> **Comments:**
> **username_4**: What is the difference between a final state and an accepting state. What assumption are you referring to?  
> **username_5**: Are your words infinite?  If so, how are you using a final state?  Maybe you should define your model and domain explicitly.  
> **username_0**: Yes, my words are infinite. But as I have to construct deterministic finite machine to recognize them, so i have restricted my set of properties(safety and weak co-safety) properties which can be recognized by Buchi automaton which have unconditionally accepting state(with a true loop).  So my assumption is that  for all safety properties(also weak until properties) such automaton exists. Am i correct in my assumption?? any comments would be highly appreciated - pratibha @Pal GD  
> **username_6**: Your assumption is correct: safety languages can be recognized by Büchi automata with all states accepting.  See for instance the book _Infinite Words_ by Perrin and Pin.  
> **username_1**: @username_6, your comment can be an answer.  
> **username_2**: the question is not clear to me. If your final states means "once I reach it I won", then this is call a reachability objective, which is very different from safety.  
> **username_3**: I think it may depend on how you construct the Buchi automaton. If you have an alternating automaton without accepting states (except $\top$), then if you apply the Miyano-Hayashi alternation removal, you end up with a nondeterministic Buchi automaton, where still all the state are not accepting, except one accepting sink. So in this sense, I think that the answer is "yes". However, if you use the Vardi-Wolper construction to obtain the Buchi automaton, this is not so certain, since this construction behaves differently in some aspects.  
> **username_0**: I figured the same...thanks for the reply @username_3  

---

## 1 answers

### Answer by username_3 on 2013-02-13. Score: 2

If I understand your model correctly, then it's enough for you that all runs either get stuck in accepting states, or get stuck in non-accepting states.
If this is the case, you can also use deterministic weak Buchi automata, which are more expressive than $satefy\cup co-safety$.


---

