0
$\begingroup$

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

Improve this question
$\endgroup$
8
  • 1
    $\begingroup$ What is the difference between a final state and an accepting state. What assumption are you referring to? $\endgroup$
    – Dave Clarke
    Oct 9, 2012 at 13:08
  • $\begingroup$ Are your words infinite? If so, how are you using a final state? Maybe you should define your model and domain explicitly. $\endgroup$
    – Pål GD
    Oct 9, 2012 at 14:22
  • $\begingroup$ 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 $\endgroup$
    – pratibha sawhney
    Oct 11, 2012 at 11:27
  • 2
    $\begingroup$ 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. $\endgroup$
    – Sylvain
    Oct 21, 2012 at 11:11
  • $\begingroup$ @Sylvain, your comment can be an answer. $\endgroup$
    – Kaveh
    Jan 16, 2013 at 5:58

1 Answer 1

Reset to default
2
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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