# Implicit Non-deterministic Buchi determinization

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.***

• What is the difference between a final state and an accepting state. What assumption are you referring to? Oct 9 '12 at 13:08
• Are your words infinite? If so, how are you using a final state? Maybe you should define your model and domain explicitly. Oct 9 '12 at 14:22
• 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 Oct 11 '12 at 11:27
• 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. Oct 21 '12 at 11:11
• @Sylvain, your comment can be an answer. Jan 16 '13 at 5:58

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$.