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