Tell me more ×
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.
up vote 9 down vote favorite
2

I am looking for a general technique which can help me to prove not just that Buchi automata is more expressive model than LTL, but that the specific formula can/can't be expressed in LTL.

For example, "$p$ occurs at least on even positions" can be described by the following Buchi automata: $({q_0, q_1}, \Sigma, \delta, q_0, \{q_0\})$ where $\delta(q_1, *) = q_0$ and $\delta(q_0, p) = q_1$.

I've read that that automata can't be expressed in LTL, but I don't understand how to formally prove it.

Thanks.

share|improve this question
Funny. I was looking at those slides today also. – Dave Clarke♦ Mar 11 '12 at 17:46

3 Answers

up vote 6 down vote accepted

First you need to know what you want to express and how you are going to express it. For instance, you can represent a property as a set of infinite traces.

The properties definable by Buechi automata are the $\omega$-regular languages. The properties definable by LTL formulae are the star-free regular languages. The star-free languages are a strict subset of the $\omega$-regular languages.

Section 5.1 of Principles of Model Checking by Baier and Katoen is a good, elementary starting point. If you want general proof techniques there are a variety of ways to proceed. One general technique that appeals to me is to use games. The first player is trying to show two structures can be distinguished with an LTL formula. The second shows they are the same. Two structures are LTL equivalent if the second player has a winning strategy. So, if you take two structures which are not isomorphic but the second player has a winning strategy, then, there is no LTL formula to distinguish between the two.

An Until Hierarchy and Other Applications of an Ehrenfeucht-Fraisse Game for Temporal Logic, K. Etessami and Th. Wilke.

There are algorithms for checking if a given $\omega$-regular language is star-free. Unfortunately these are usually couched inside the proofs of theorems.

Logical definability on infinite traces, Werner Ebinger and Anca Muscholl

I'll dig around a bit more and try to find a more algorithmic presentation.

share|improve this answer
I am sorry if I wasn't clear enough. I skimmed through 5.1 of Principles of Model Checking and I didn't find any new information. I know what LTL is and how to express properties with it. I also know that there are certain properties you can not express in LTL (e.g. $\omega$-regular languages are more expressive). I know that LTL formula can be converted to Buchi automata. I, however, don't know how to prove that a specific Buchi-automata can NOT be converted to LTL. – Daniil Mar 12 '12 at 14:18
So if I prove that a specific property can be expressed only in non-star-free regular language it follows that the property can not be expressed in LTL. So I am looking for a techniques to prove that for specific properties. – Daniil Mar 12 '12 at 14:21
The problem of deciding if an $\omega$-regular language is star-free is decidable. The algorithm counts as a general proof technique. I'm trying to find a reference that precisely answers your question. The references I included above are not exact, but I hope they are insightful. – Vijay D Mar 12 '12 at 21:03
I have a small reservation with using EF games for this purpose, because if one is to actually write down a detailed proof covering all cases, they quickly become difficult to manage. Hence the interest of algebraic methods on $\omega$-words. (They are however good for convincing oneself that a particular property is not expressible in LTL, and in more abstract proofs.) – Sylvain Mar 12 '12 at 22:48
I, personally prefer algebraic techniques. My intuition is terrible in general and I found algebraic techniques lead me to fewer red herrings and shorter proofs. However, from paper rejections and presentations, I have the impression majority of computer scientists prefer games or relational (bisimulation, etc) proof techniques. – Vijay D Mar 13 '12 at 5:18
up vote 7 down vote

I would suggest using the characterization of first-order languages by counter-free Büchi automata: see e.g. V. Diekert and P. Gastin, First-order definable languages. In Logic and Automata: History and Perspectives, Texts in Logic and Games 2, pages 261--306. Amsterdam University Press, 2008. http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf

PS: over finite words, this BEATCS column is also very helpful: J.-E. Pin, Logic on Words, http://hal.archives-ouvertes.fr/hal-00020073.

share|improve this answer
up vote 4 down vote

I think the best way to be convinced of the fact that there is no LTL formula for this language is via $\omega$-semigroups.

Indeed, there is a theorem, that you can find in Diekert/Gastin or Pin, stating that the LTL-definable language have an aperiodic minimal $\omega$-semigroup.

Given a regular language L on infinite words (via an automaton for instance), the minimal $\omega$-semigroup S recognizing L can be computed. To do this, consider the semigroup generated by transition matrices of the automaton, and then minimize it. Then you can test S for aperiodicity : just iterate all the elements $x\in S$ and check that there is always an $n$ such that $x^n=x^{n+1}$.

This gives you an algorithm for LTL-definability.

share|improve this answer

Your Answer

 
discard

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.