5
$\begingroup$

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

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – Klaus Draeger Jul 29 '15 at 19:22
  • $\begingroup$ 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... $\endgroup$ – DaveBall aka user750378 Jul 29 '15 at 19:37
2
+50
$\begingroup$

Pierre Wolper defined in 1983 extended temporal logic (ETL, in Information and Computation 56, 72–99, doi: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.

$\endgroup$
  • $\begingroup$ 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... $\endgroup$ – DaveBall aka user750378 Aug 6 '15 at 10:18
  • $\begingroup$ 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}? $\endgroup$ – DaveBall aka user750378 Aug 13 '15 at 11:55
  • $\begingroup$ @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$. $\endgroup$ – Sylvain Sep 4 '15 at 14:17
1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Thanks for the intersting answer and papers - I haven't heard of hyperproperties before (+1). $\endgroup$ – DaveBall aka user750378 Aug 5 '15 at 13:25
  • $\begingroup$ But in my question, I am looking for linear time properties without any relationship between multiple paths (hence no acceptance of your answer). $\endgroup$ – DaveBall aka user750378 Aug 5 '15 at 13:27
  • $\begingroup$ How would you define linear-time properties? Do you mean trace properties as in sets of traces? $\endgroup$ – Markus Aug 6 '15 at 15:45
  • $\begingroup$ 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) $\endgroup$ – DaveBall aka user750378 Aug 6 '15 at 16:18
  • 1
    $\begingroup$ 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. $\endgroup$ – Markus Aug 16 '15 at 15:58

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.