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

Improve this question
$\endgroup$
2
  • 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
    Commented Jul 29, 2015 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
    Commented Jul 29, 2015 at 19:37

2 Answers 2

Reset to default
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.

Improve this answer
$\endgroup$
3
  • $\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
    Commented Aug 6, 2015 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
    Commented Aug 13, 2015 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
    Commented Sep 4, 2015 at 14:17
2
$\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

Improve this answer
$\endgroup$
8
  • $\begingroup$ Thanks for the intersting answer and papers - I haven't heard of hyperproperties before (+1). $\endgroup$
    – DaveBall aka user750378
    Commented Aug 5, 2015 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
    Commented Aug 5, 2015 at 13:27
  • $\begingroup$ How would you define linear-time properties? Do you mean trace properties as in sets of traces? $\endgroup$
    – Markus
    Commented Aug 6, 2015 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
    Commented Aug 6, 2015 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
    Commented Aug 16, 2015 at 15:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.