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

<p>PS: over finite words, this BEATCS column is also very helpful: J.-E. Pin, <em>Logic on Words</em>, <a href="http://hal.archives-ouvertes.fr/hal-00020073">http://hal.archives-ouvertes.fr/hal-00020073</a>.</p>

CC BY-SA 3.0
2012-03-11T18:21:47.643Z
2012-03-11T20:30:30.230Z
2012-03-11T20:30:30.230Z
Sylvain
<p>I think the best way to be convinced of the fact that there is no LTL formula for this language is via $\omega$-semigroups.</p>

<p>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.</p>

<p>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}$.</p>

<p>This gives you an algorithm for LTL-definability.</p>

CC BY-SA 3.0
2012-04-02T13:27:13.627Z
2012-04-02T13:27:13.627Z
Denis
<p>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. </p>

<p>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.</p>

<p>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.</p>

<blockquote>
  <p><a href="http://homepages.inf.ed.ac.uk/kousha/until_hier_ic.ps" rel="nofollow">An Until Hierarchy and Other Applications of an Ehrenfeucht-Fraisse Game for Temporal Logic</a>, K. Etessami and Th. Wilke.</p>
</blockquote>

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

<blockquote>
  <p><a href="http://www.sciencedirect.com/science/article/pii/0304397595001301" rel="nofollow">Logical definability on infinite traces</a>, Werner Ebinger and Anca Muscholl</p>
</blockquote>

<p>I'll dig around a bit more and try to find a more algorithmic presentation.</p>

CC BY-SA 3.0
2012-03-12T14:18:58.380Z
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
CC BY-SA 3.0
2012-03-12T14:21:07.957Z
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
CC BY-SA 3.0
2012-03-12T21:03:42.413Z
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
CC BY-SA 3.0
2012-03-12T22:48:05.907Z
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
CC BY-SA 3.0
2012-03-13T05:18:14.497Z
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
CC BY-SA 3.0
2015-07-04T21:27:47.083Z
Sorry for the slightly off-topic comment: can someone point to some reference on those "algebraic techniques" for $\omega$-words?
Nicola Gigante
CC BY-SA 3.0
2012-03-12T08:04:11.240Z
2012-03-12T21:01:34.670Z
2012-03-12T21:01:34.670Z
Vijay D
<p>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.</p>

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

<p>I've <a href="http://www.lsv.ens-cachan.fr/~markey/Teaching/ESSLLI06/tuesday.pdf">read</a> that that automata can't be expressed in LTL, but I don't understand how to formally prove it.</p>

<p>Thanks.</p>

CC BY-SA 3.0
2012-03-11T17:46:19.943Z
Funny. I was looking at those slides today also.
Dave Clarke
<lo.logic><automata-theory>
How to prove that a formula can not be expressed in LTL, but can be in Buchi automata?
Daniil
# How to prove that a formula can not be expressed in LTL, but can be in Buchi automata?

(Asked by: username_0 on 2012-03-11)

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](http://www.lsv.ens-cachan.fr/~markey/Teaching/ESSLLI06/tuesday.pdf) that that automata can't be expressed in LTL, but I don't understand how to formally prove it.

Thanks.

**Tags:** lo.logic, automata-theory
> **Comments:**
> **username_1**: Funny. I was looking at those slides today also.  

---

## 3 answers

### Answer by username_4 on 2012-03-12. Score: 9 | Accepted answer

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](http://homepages.inf.ed.ac.uk/kousha/until_hier_ic.ps), 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](http://www.sciencedirect.com/science/article/pii/0304397595001301), Werner Ebinger and Anca Muscholl

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

> **Comments:**
> **username_0**: 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.  
> **username_0**: 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.  
> **username_4**: 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.  
> **username_2**: 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.)  
> **username_4**: 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.  
> **username_5**: Sorry for the slightly off-topic comment: can someone point to some reference on those "algebraic techniques" for $\omega$-words?  

---

### Answer by username_2 on 2012-03-11. Score: 7

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


---

### Answer by username_3 on 2012-04-02. Score: 4

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.


---

