Let's assume that I have an LTL formula and I want to convert it to a Buchi automaton. For which fragment of LTL, GBA is more succinct and for which fragment BA has the same size as GBA.


There is no precise answer to this.

  1. The smallest GBA for a given language is never larger than the smallest BA for a given language, simply by the fact that BAs are a special case of GBAs.
  2. It is easy to construct a language for which smaller GBA exist. Example would be (in LTL) $\mathsf{GF}(a \wedge b) \wedge \mathsf{GF}(a \wedge \neg b) \wedge \mathsf{GF}(\neg a \wedge b) \wedge \mathsf{GF}(\neg a \wedge \neg b)$ - a four-state GBA does the trick, but the BA needs more states to encode waiting for the next event (out of $a \wedge b$, $\ldots$, $\neg a \wedge \neg b$) to happen. So whatever fragment of LTL you build, this formula will not be contained therein. But if you now take a disjunction of this property with $\mathsf{GF}(a)$ and then with $\mathsf{GF}(\neg a)$, then the smallest BA and GBA have the same size (one state). So you cannot give a precise syntactic representation of such a fragment (without making a containment check at least PSPACE-hard).
  3. You can, of course, build an LTL fragment for which containment of the property in the fragment guarantees that the smallest GBA will not be larger than the smallest BA. You would get such a fragment, for example, by including the next-time operator as the only temporal operator in the fragment.
  4. In practice, it doesn't matter anyway. Due to the many different optimizations in LTL-to-BA and LTL-to-GBA tools, you cannot predict very well whether they will compute BAs that are just as small as GBAs.

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.