1
$\begingroup$

I am looking for the portion of LTL formula that can be expressed by deterministic buchi automata. Is there any classification of this such?

Improve this question
$\endgroup$
3
  • $\begingroup$ Yes; there are some canonical theorems. Where have you looked? $\endgroup$
    – Raphael ♦
    Apr 12, 2017 at 19:12
  • $\begingroup$ Could you please give me some references on those theorems? $\endgroup$
    – Perissiane
    Apr 13, 2017 at 10:25
  • $\begingroup$ Not at the moment, sorry. Since I learned about them in a course, I'd assume any book on either topic would include them. $\endgroup$
    – Raphael ♦
    Apr 13, 2017 at 11:49

1 Answer 1

Reset to default
4
$\begingroup$

You can define syntactic fragments of LTL that ensure that all properties expressible in these fragments are representable as DBAs. An example is given in the paper "A LTL Fragment for GR(1)-Synthesis". Also, the common fragment of ACTL and LTL only contains properties that are representable as DBAs.

But note that such a fragment will never be complete in the "if a formula is not in the fragment, then it is not representable as a DBA" sense. The reason is that if we have LTL formulas that are not representable as DBAs, then we may be able to combine them to a formula that is representable as DBA. For example, the properties "FG p | GF q" and "FG q | GF p" are both not expressible by DBA, but both their conjunction and their disjunction are.

Note that there are also DBAs that are not representable in LTL. So a fragment of LTL cannot be equiexpressive to DBAs.

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.