Is there an algorithm on how to check if two LTL expressions (represented as binary trees) are semantically equivalent? Since there are many smaller equivalences such as $a\Rightarrow b \equiv \neg a \vee b$ or $F(a) \equiv true U a$ as well as commutativity, distributivity, etc. that need to be considered. My initial idea was to create the truth table for both expressions and compare them. But then the temporal operators would not be taken into account. Creating and comparing the automaton for each expression sounds like it would be rather inefficient. Is there a better way to do this?

Basically i have a program which increases a variable by 1 in each iteration and resets it to 0 as soon as y becomes 8 (i.e. mod 8). It is a quite simple example but it still bugs me out because i cannot clarify if my LTL-formula is correct for the property "there is a value of y whose next value is 8". For this i came up with the: $$FX(y \doteq 8)$$ which means "somewhere in the future the next value of y is 8". Is it the correct LTL formula for my question (even though it is of course invalid for my application)?

Sistla/Clarke proved [SC82] that the LTL model-checking problem is PSpace-complete. Sometimes people write that this problem is "PSpace-hard in $|\phi|$" (e.g. [LP85]). What does this mean formally? How to prove that a decision problem that has several parameters (here, $\phi$ and system) is PSpace-hard in one of the parameters? I guess we would need to poly-time reduce some PSpace-complete problem to our problem with the unintereseting parameter being fixed, while the interesting parameter can vary. But the original proof of Sistla/Clarke [Lemma 4.4, SC82] does not do the thing above! In their proof, both parameters of the resulting LTL model-checking problem instance depend on $n$, where $n$ is the TM tape bound. Is there a proof that fixes one of the parameters?

I'm a little confused about some LTL syntax. When the Global and Future operator (GFx) or []<>x is used, what does it mean. In the lecture slides it is given as infinitely often. But I don't understand it. When used as FGx or <>[]x, I understand it as eventually in the future something will be true forever. E.g. eventually x will become 3 (x = 3) and x will stay as 3 forever. Can someone explain what GFx means?

Problem: Let $\varphi = \varphi_1 \land \varphi_2$ be Deterministic Buchi Automata (DBA) expressible LTL formulas. Let $A$, $A_1$ and $A_2$ be translated DBAs such that ${\cal{L}}(A) = {\cal{L}}(A_1) \cap {\cal{L}}(A_2)$. What can be said about the relation between the number of states in $A$ and that in the synchronous product $A_1 \otimes A_2$? Some background: I found two definitions of the Buchi product, the one given by Vardi in An Automata-Theoretic Approach to Linear Temporal Logic that uses $S = S_1 \times S_2 \times \{1, 2\}$ while the one demonstrated in this presentation uses $S = S_1 \times S_2 \times \{1, 2, 3\}$. Also, Ehlers has proposed an approach to minimize the DBA in this paper. However, I have been unsuccessful in finding any rigorous mathematical relation between the sizes of translated DBA $A$ and the minimal synchronous product of $A_1 \otimes A_2$. My question: I would like to know about - Any work regarding the size of Minimal DBA Product - Any work about the relation between the number of states. - How to construct the minimal DBA Product, given $A_1$ and $A_2$.

LTL works with Boolean propositions. People probably studied extensions to non-Boolean propositions... Do you know a good starting reference? (I am aware of STL, but it also seems to talk about clocks, is there a variant without clocks?) Update: the question is not about "true, false, maybe" but rather about LTL where we can refer to integers, for example. Example: one might want to write `G(i+1 == X(i))`, meaning that value `i` should increment.

Is there any general result to show that which automaton is more succinct? I have a set of LTL properties and I would like to know (show) which automaton is more efficient in term of state number and edge number.

Both Logic in Computer Science (Huth and Ryan, 2004) and Branching vs. Linear Time: Final Showdown (Vardi, 2002), state something to this effect (paraphrased): In LTL, X F p and F X p are equivalent, meaning "p is eventually true in some state that is not the current state". In CTL, AX AF p and AF AX p are not equivalent. AX AF p does mean the same as the above LTL formulas, but AF AX p means something different, which we leave as an exercise to the reader. Both works emphasize that the meaning of AF AX p is something very strange. From what I understand of CTL, AF AX p would mean "all paths from this state eventually reach a state where p is true in all next states", but that doesn't seem particularly strange. Am I correct in that understanding?

Need to prove equivalence for (or disprove equivalence for): $ \hspace{1cm}\square ϕ → \lozenge ψ ≡ ϕ\textsf{ U }(ψ ∨ ¬ϕ) \\ $ My current attempt using the LTL equivalnce rules to determine equivalence: $ \square ϕ → \lozenge ψ \\ ≡\ ¬\square ϕ \lor \lozenge ψ \hspace{1cm}(\textsf{"Mutual implication"} ϕ →ψ≡¬ϕ\lor ψ )\\ ≡ \lozenge ¬ϕ \lor \lozenge ψ \hspace{1cm}(\textsf{"Duality"} ¬\square≡\lozenge ¬ )\\ ≡ \lozenge (¬ϕ \lor ψ) \hspace{1cm}(\textsf{"Distributive law on"}\lozenge )\\ ≡true \textsf{ U} (¬ϕ \lor ψ) \hspace{1cm}(\textsf{"Def of"}\lozenge )\\ ≡true \textsf{ U} (ψ \lor ¬ϕ) \hspace{1cm}(\textsf{"Symmetry"}\lor)\\ $ After this I got stuck. I am not sure how to proceed from here to get the right side. Are other propositional logic rules allowed to be used in LTL, like for example identity disjunction?

I am new to this topic, Linear Time Temporal Logic and I am trying to prove this equivalence -- $\Box\Diamond f \Leftrightarrow \Diamond\Box f$ This is my take -- Basic definitions: $(\sigma, j) \models \Box f: \forall k \, [(k \ge j) \Rightarrow ((\sigma, k) \models f)]$ $(\sigma, j) \models \Diamond f: \exists k \, [(k \ge j) \Rightarrow ((\sigma, k) \models f)]$ Here, $(\sigma, j) \models f$ means $\sigma$ satisfies $f$ at $\sigma(j)$, for more details about this syntax, please see here. Now the LHS: $\begin{eqnarray} (\sigma, j) \models \Box \Diamond f & : & \forall k \, [(k \ge j) \Rightarrow ((\sigma, k) \models \Diamond f)]\\ & \equiv & \forall k \, [(k \ge j) \Rightarrow [\exists p \, [(p \ge k) \Rightarrow ((\sigma, p) \models f)]]]\\ & \equiv & \forall k \, [(k<j) \vee [\exists p \, [(p<k) \vee ((\sigma,p) \models f)]]]\\ & \equiv & \forall k \, \exists p \, [(k<j) \vee (p<k) \vee ((\sigma,p) \models f)]\\ & \equiv & \forall k \, \exists p \, [(p<k<j) \vee ((\sigma,p) \models f)]\\ \end{eqnarray} $ Again, the RHS: $\begin{eqnarray} (\sigma, j) \models \Diamond \Box f & : & \exists k \, [(k \ge j) \Rightarrow ((\sigma, k) \models \Box f)]\\ & \equiv & \exists k \, [(k \ge j) \Rightarrow [\forall p \, [(p \ge k) \Rightarrow ((\sigma, p) \models f)]]]\\ & \equiv & \exists k \, [(k<j) \vee [\forall p \, [(p<k) \vee ((\sigma,p) \models f)]]]\\ & \equiv & \exists k \, \forall p \, [(p<k<j) \vee ((\sigma,p) \models f)]\\ \end{eqnarray} $ Now if we look at the last line of the both sides, the statement $\forall k \, \exists p \, [(p<k<j) \vee ((\sigma,p) \models f)] \equiv \exists k \, \forall p \, [(p<k<j) \vee ((\sigma,p) \models f)]$ needs to be true to complete the proof, however intuitively, this is not true. What I am missing? How do I proceed? Any idea?