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

  • $\begingroup$ Yes; there are some canonical theorems. Where have you looked? $\endgroup$ – Raphael Apr 12 '17 at 19:12
  • $\begingroup$ Could you please give me some references on those theorems? $\endgroup$ – Perissiane Apr 13 '17 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 '17 at 11:49

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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