<p>Pierre Wolper defined in 1983 <em>extended temporal logic</em> (ETL, in <em>Information and Computation</em> 56, 72–99, <a href="http://dx.doi.org/10.1016/S0019-9958(83)80051-5" rel="nofollow">doi:10.1016/S0019-9958(83)80051-5</a>), where a temporal operator $\mathcal A(\varphi_1,\dots,\varphi_n)$ can be introduced for a finite-state automaton $\mathcal A$.  The formula is satisfied in an infinite word $u$ at position $i$, i.e. $u,i\models\mathcal A(\varphi_1,\dots,\varphi_n)$, if there exists a finite word $a_{i_1}\cdots a_{i_n}$ in the language of the automaton $\mathcal A$, such that for every $1\leq j\leq n$, $u, i+(j-1)\models\varphi_{i_j}$.  Extended temporal logic has the same expressive power as the linear-time $\mu$-calculus or MSO on infinite words, so it does not answer your question.</p>

<p>One can however go further and allow other languages instead of regular ones in the operator $\mathcal A(\dots)$.  Paul Gastin and Stéphane Demri consider the case of context-free languages at the end of their chapter <em>Specification and Verification using Temporal Logics</em> of <em>Modern applications of automata theory</em> (IISc Research Monographs 2, chapter 15, pages 457–494, World Scientific, 2012, <a href="http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-iis09.pdf" rel="nofollow">http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-iis09.pdf</a>).  You can certainly express non-lasso properties in such a logic.  It is shown by Gastin and Demri to have (highly) undecidable satisfiability and model-checking problems.</p>

CC BY-SA 3.0
2015-08-06T10:18:55.663Z
Thanks for the reference, looks quite helpful. I know already Extended CTL*, where Büchi automata can be used as temporal operator. So going beyond (omega-)regular temporal operators is an interesting next step. Now I wonder whether model checking of counterexamples that are more complex than a lasso is always undecidable. Maybe your reference will also help there...
DaveBall aka user750378
CC BY-SA 3.0
2015-08-13T11:55:26.477Z
Thanks, Sylvain, this is heading in the right direction (+50). I did, however, not find a linear time property ($\neq$ false) that only has counterexamples that are more complex than a lasso. I do not consider a finite counterexample being more complex than a lasso. Can you construct such a language with the counting languages of finite words given in your reference, like {a^n,b,c^n,d}?
DaveBall aka user750378
CC BY-SA 3.0
2015-09-04T14:17:17.203Z
@DaveBall what about the formula $\mathsf{G}(\mathcal{A}(p,\neg p))$ over a set of atomic propositions $\{p\}$ and with $\mathcal{A}$ a pushdown automaton for $\{a^nba^{m}\mid 0\leq n<m\}$?  If I'm not wrong, its models are the infinite words of the form $\{p\}^{n_1}\emptyset\{p\}^{n_2}\emptyset\{p\}^{n_3}\emptyset\cdots$ with $n_1<n_2<n_3<\cdots$.
Sylvain
CC BY-SA 3.0
2015-08-05T20:49:27.427Z
2015-08-05T20:49:27.427Z
Sylvain
<p>I think it depends on what you mean by linear-time temporal logics. If you mean temporal logics that have linear time semantics (i.e. cannot distinguish more than trace equivalence, a la van Glabbeek) then there are indeed logics that require counter examples that are not just lassos. HyperLTL is an example:</p>

<p><a href="https://www.react.uni-saarland.de/publications/CFKMRS14.html" rel="nofollow">https://www.react.uni-saarland.de/publications/CFKMRS14.html</a></p>

<p><a href="https://www.react.uni-saarland.de/publications/FR14.html" rel="nofollow">https://www.react.uni-saarland.de/publications/FR14.html</a></p>

CC BY-SA 3.0
2015-08-05T13:25:40.217Z
Thanks for the intersting answer and papers - I haven't heard of hyperproperties before (+1).
DaveBall aka user750378
CC BY-SA 3.0
2015-08-05T13:27:39.073Z
But in my question, I am looking for linear time properties without any relationship between multiple paths (hence no acceptance of your answer).
DaveBall aka user750378
CC BY-SA 3.0
2015-08-06T15:45:49.613Z
How would you define linear-time properties? Do you mean trace properties as in sets of traces?
Markus
CC BY-SA 3.0
2015-08-06T16:18:37.837Z
For me, a linear-time property decides for each trace individually whether the property is met (see def. 3.10 of Principles of Model Checking, Christel Baier and Joost-Pieter Katoen)
DaveBall aka user750378
CC BY-SA 3.0
2015-08-15T09:43:23.083Z
When a counterexample to a HyperLTL property consists of finitely many traces, then there is also a lasso shaped counterexample, right? For HyperLTL_2, the cited reference does use the LTL model checking method of Vardi&Wolper, which requires lassos.
DaveBall aka user750378
CC BY-SA 3.0
2015-08-16T15:58:39.427Z
Counterexamples to HyperLTL do not necessarily consist of finitely many traces; think of formulas with quantifier alternations. The algorithm indeed makes use of the fact that to determine the nonemptiness of a Büchi automaton, it suffices to search for lasso shaped paths, but the lasso does not correspond to a path in the system - The Büchi automaton is the result of several transformations.

Also for the more simple alternation-free HyperLTL$_2$, where counterexamples can be seen as pairs of paths, the counterexample is not a pair of lasso shaped paths, but a lasso shaped pair of paths.
Markus
CC BY-SA 3.0
2015-08-17T09:14:15.510Z
Thanks for your comment, Markus. So when you have a finite set of paths in your counterexample, you can construct a lasso-shaped set of paths from the set of lasso-shaped paths, but this no longer works for infinite sets of paths, right? Doesn't one existential path quantifier suffice for a counterexample to have infinitely many paths (in fact, all paths)?
DaveBall aka user750378
CC BY-SA 3.0
2015-08-19T22:40:56.807Z
I don't understand the first question on a formal level, so I'm hesitant to answer it. Concerning the second question: yes. This is probably a much more simple example than quantifier alternations in HyperLTL. CTL would suffice to define such a property. This opens, however, the question what counterexamples are exactly.
Markus
CC BY-SA 3.0
2015-07-31T03:13:11.413Z
2015-07-31T03:13:11.413Z
Markus
<p>Are there linear time temporal logics that can express some property $P_{nonlasso}$ that does have a counterexample, but none that is a lasso (or finite)? </p>

<hr>

<p>Details:</p>

<p>One advantage of model checking over other formal methods is their ability to return a counterexample, a (finite path or a) path in form of a lasso. This is sufficient up to (extended) Büchi automata, since an infinite accepting path can be transformed to a lasso that infitely visits some accepting state. </p>

<p>But is this still the case for more complex linear time logics? Or a non-linear time logic that does have counterexamples, e.g. ACTL*? Can the $\mu$-calculus or MCRL2 express such a linear time property $P_{nonlasso}$? </p>

<p>For instance, having the Kripke structure $s_1 \leftrightarrow init \leftrightarrow s_2$, can I express the counting property "repeat $(init \rightarrow s_1 \rightarrow init)^i \cdot (init \rightarrow s_2 \rightarrow init)^i$ for infinitely increasing $i$"? This path does have a very simple schema...</p>

<hr>

<p>Update: I am looking for linear time temporal logics without any relationship between multiple paths (see Makus's answer for other logics).</p>

CC BY-SA 3.0
2015-07-29T19:22:11.513Z
Any nonempty $\omega$-regular language will contain a word of the form $uv^\omega$, so you would need a logic which can describe non-$\omega$-regular languages. The linear $\mu$-calculus therefore won't do.
Klaus Draeger
CC BY-SA 3.0
2015-07-29T19:37:56.133Z
Thanks Klaus, that helps already. Since I have never gone beyond $\mu$-calculus, I have no idea what temporal logic or model checker there is left to investigate...
DaveBall aka user750378
<model-checking><temporal-logic><linear-temporal-logic>
Are there temporal logics linear time properties that only have counterexamples that are more complex than a lasso?
DaveBall aka user750378
# Are there temporal logics linear time properties that only have counterexamples that are more complex than a lasso?

(Asked by: username_0 on 2015-07-29)

Are there linear time temporal logics that can express some property $P\_{nonlasso}$ that does have a counterexample, but none that is a lasso (or finite)?

---

Details:

One advantage of model checking over other formal methods is their ability to return a counterexample, a (finite path or a) path in form of a lasso. This is sufficient up to (extended) Büchi automata, since an infinite accepting path can be transformed to a lasso that infitely visits some accepting state.

But is this still the case for more complex linear time logics? Or a non-linear time logic that does have counterexamples, e.g. ACTL\*? Can the $\mu$-calculus or MCRL2 express such a linear time property $P\_{nonlasso}$?

For instance, having the Kripke structure $s\_1 \leftrightarrow init \leftrightarrow s\_2$, can I express the counting property "repeat $(init \rightarrow s\_1 \rightarrow init)^i \cdot (init \rightarrow s\_2 \rightarrow init)^i$ for infinitely increasing $i$"? This path does have a very simple schema...

---

Update: I am looking for linear time temporal logics without any relationship between multiple paths (see Makus's answer for other logics).

**Tags:** model-checking, temporal-logic, linear-temporal-logic

> **Comments:**
> **username_1**: Any nonempty $\omega$-regular language will contain a word of the form $uv^\omega$, so you would need a logic which can describe non-$\omega$-regular languages. The linear $\mu$-calculus therefore won't do.  
> **username_0**: Thanks Klaus, that helps already. Since I have never gone beyond $\mu$-calculus, I have no idea what temporal logic or model checker there is left to investigate...  

---

## 2 answers

### Answer by username_2 on 2015-08-05. Score: 2 | Accepted answer

Pierre Wolper defined in 1983 *extended temporal logic* (ETL, in *Information and Computation* 56, 72–99, [doi:10.1016/S0019-9958(83)80051-5](http://dx.doi.org/10.1016/S0019-9958(83)80051-5)), where a temporal operator $\mathcal A(\varphi\_1,\dots,\varphi\_n)$ can be introduced for a finite-state automaton $\mathcal A$. The formula is satisfied in an infinite word $u$ at position $i$, i.e. $u,i\models\mathcal A(\varphi\_1,\dots,\varphi\_n)$, if there exists a finite word $a\_{i\_1}\cdots a\_{i\_n}$ in the language of the automaton $\mathcal A$, such that for every $1\leq j\leq n$, $u, i+(j-1)\models\varphi\_{i\_j}$. Extended temporal logic has the same expressive power as the linear-time $\mu$-calculus or MSO on infinite words, so it does not answer your question.

One can however go further and allow other languages instead of regular ones in the operator $\mathcal A(\dots)$. Paul Gastin and Stéphane Demri consider the case of context-free languages at the end of their chapter *Specification and Verification using Temporal Logics* of *Modern applications of automata theory* (IISc Research Monographs 2, chapter 15, pages 457–494, World Scientific, 2012, <http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-iis09.pdf>). You can certainly express non-lasso properties in such a logic. It is shown by Gastin and Demri to have (highly) undecidable satisfiability and model-checking problems.

> **Comments:**
> **username_0**: Thanks for the reference, looks quite helpful. I know already Extended CTL*, where Büchi automata can be used as temporal operator. So going beyond (omega-)regular temporal operators is an interesting next step. Now I wonder whether model checking of counterexamples that are more complex than a lasso is always undecidable. Maybe your reference will also help there...  
> **username_0**: Thanks, username_2, this is heading in the right direction (+50). I did, however, not find a linear time property ($\neq$ false) that only has counterexamples that are more complex than a lasso. I do not consider a finite counterexample being more complex than a lasso. Can you construct such a language with the counting languages of finite words given in your reference, like {a^n,b,c^n,d}?  
> **username_2**: @DaveBall what about the formula $\mathsf{G}(\mathcal{A}(p,\neg p))$ over a set of atomic propositions $\{p\}$ and with $\mathcal{A}$ a pushdown automaton for $\{a^nba^{m}\mid 0\leq n<m\}$?  If I'm not wrong, its models are the infinite words of the form $\{p\}^{n_1}\emptyset\{p\}^{n_2}\emptyset\{p\}^{n_3}\emptyset\cdots$ with $n_1<n_2<n_3<\cdots$.  

---

### Answer by username_3 on 2015-07-31. Score: 2

I think it depends on what you mean by linear-time temporal logics. If you mean temporal logics that have linear time semantics (i.e. cannot distinguish more than trace equivalence, a la van Glabbeek) then there are indeed logics that require counter examples that are not just lassos. HyperLTL is an example:

<https://www.react.uni-saarland.de/publications/CFKMRS14.html>

<https://www.react.uni-saarland.de/publications/FR14.html>

> **Comments:**
> **username_0**: Thanks for the intersting answer and papers - I haven't heard of hyperproperties before (+1).  
> **username_0**: But in my question, I am looking for linear time properties without any relationship between multiple paths (hence no acceptance of your answer).  
> **username_3**: How would you define linear-time properties? Do you mean trace properties as in sets of traces?  
> **username_0**: For me, a linear-time property decides for each trace individually whether the property is met (see def. 3.10 of Principles of Model Checking, Christel Baier and Joost-Pieter Katoen)  
> **username_0**: When a counterexample to a HyperLTL property consists of finitely many traces, then there is also a lasso shaped counterexample, right? For HyperLTL_2, the cited reference does use the LTL model checking method of Vardi&Wolper, which requires lassos.  
> **username_3**: Counterexamples to HyperLTL do not necessarily consist of finitely many traces; think of formulas with quantifier alternations. The algorithm indeed makes use of the fact that to determine the nonemptiness of a Büchi automaton, it suffices to search for lasso shaped paths, but the lasso does not correspond to a path in the system - The Büchi automaton is the result of several transformations.  Also for the more simple alternation-free HyperLTL$_2$, where counterexamples can be seen as pairs of paths, the counterexample is not a pair of lasso shaped paths, but a lasso shaped pair of paths.  
> **username_0**: Thanks for your comment, username_3. So when you have a finite set of paths in your counterexample, you can construct a lasso-shaped set of paths from the set of lasso-shaped paths, but this no longer works for infinite sets of paths, right? Doesn't one existential path quantifier suffice for a counterexample to have infinitely many paths (in fact, all paths)?  
> **username_3**: I don't understand the first question on a formal level, so I'm hesitant to answer it. Concerning the second question: yes. This is probably a much more simple example than quantifier alternations in HyperLTL. CTL would suffice to define such a property. This opens, however, the question what counterexamples are exactly.  

---

