Are there temporal logics linear time properties that only have counterexamples that are more complex than a lasso? 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).
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.