Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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

share|improve this question
What is the difference between a final state and an accepting state. What assumption are you referring to? –  Dave Clarke 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. –  Pål GD 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 –  pratibha sawhney 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. –  Sylvain Oct 21 '12 at 11:11
@Sylvain, your comment can be an answer. –  Kaveh Jan 16 '13 at 5:58
show 3 more comments

1 Answer 1

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

share|improve this answer
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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