17

I am looking for an easy example of two transition systems that are LTL equivalent, but not trace equivalent.

I have read the proof of Trace Equivalence being finer than LTL Equivalence in the book "Principles of Model Checking" (Baier/Katoen) but I'm not sure I really understand it. I am unable to picture it, is there maybe a simple example that can visualize the difference?

Kaveh
  • 21,577
  • 8
  • 82
  • 183
magnattic
  • 173
  • 7
  • thanks for creating the tag, apparently not many questions here regarding this kind of logic – magnattic Apr 03 '11 at 17:55
  • This is the end of logic I don't know much about, or I would have tried to be more helpful than just fixing the tag. :) – Neel Krishnaswami Apr 03 '11 at 17:57
  • 3
    Might I recommend expanding the acronym in the title. This will help others find the question and answers and might also help bring your question to the attention of those who can provide good responses. – Marc Hamann Apr 03 '11 at 19:01
  • 1
    not to mention google searches :) – Suresh Venkat Apr 03 '11 at 19:20
  • 5
    @Marc: Using the acronym LTL is absolutely standard - modal logicians like their brief names (think B, D4.3, KL, &c.). I think the title shouldn't be expanded, given that we have the tag. – Charles Stewart Apr 04 '11 at 06:44
  • @Charles Stewart: I understand that point of view. If we are using LTL as an atomic technical term rather than as an acronym, then it is what it is. Given the range of topics covered here, though, I still worry about ending up in TLA (three-letter acronym) soup. ;-) – Marc Hamann Apr 04 '11 at 13:38
  • @atticae @Charles: Let me revise my suggestion based on Charles input. S4, for example, is a well understood term in modal logic, but outside of a specifically ML context I would probably refer to it as "S4 modal logic", or the like. I wonder if something similar is appropriate here, even if to some it would seem redundant. – Marc Hamann Apr 04 '11 at 13:47
  • 1
    The question is still not very well defined: are you allowing infinite Kripke structures? Do you consider mixed (maximal) finite and infinite traces, or only allow infinite ones? I am asking because AFAICR Baier & Katoen only consider the case of finite Kripke structures and infinite traces, which rule out Dave's answer below. – Sylvain Apr 04 '11 at 14:12
  • @Sylvain: Dave deleted his answer. – Dave Clarke Apr 04 '11 at 21:03
  • @Sylvain: My apologies, I am still pretty new to the whole field. But as you said, I think I would need an example in the constraints of the book, so finite Kripke stuctures and infinite traces. I didnt even consider infinite Kripke structures, but in the book it clearly says that they are working with Transition Systems without terminal states. Sorry for my english btw. :) I will start a bounty in the hopes for someone to come up with an easy example, if there is one. – magnattic Apr 05 '11 at 22:16
  • And regarding the abbreviation topic: When searching for the topic in google I also looked for "LTL" instead the whole term. Might just be me though, if you think it should be expanded, feel free to edit the title. – magnattic Apr 05 '11 at 22:20
  • 1
    @atticae: with finite total Kripke structures (and thus infinite traces), I'd expect LTL equivalence and trace equivalence to be the same thing... I'll think about it. – Sylvain Apr 06 '11 at 08:41
  • I would post the proof from the book here, but I guess that would violate copyright or something? – magnattic Apr 06 '11 at 11:23
  • @atticae: The proof is straightforward, it's the counterexample to the other direction we are struggling with. In short the proof says that if two systems do not satisfy the same LTL formula, then there is one formula satisfied by one system but not by the other. By definition, this means that there is a trace in the first system that satisfies the first formula, but this trace does not occur in the second system. Hence the two systems are not trace equivalent. – Dave Clarke Apr 06 '11 at 12:07
  • I would guess that if two transition systems satisfy the same LTL formulas, then they are isomorphic, and thus trace equivalent. Two finite structures satisfy the same set of First-order sentences(i.e., formulas without variables) iff they are isomorphic. By Kamp's theorem (See www.cs.toronto.edu/~libkin/csc2428/Lecture7.ps for a proof), LTL is equivalent to FO-logic, in the sense that for every LTL sentence $\varphi$ there is a FO sentence $\phi$ with the same models and vice versa. Thus if two TS are LTL-equiv, they are FO-equiv and thus isomorphic. But I might be missing someth. – Mateus de Oliveira Oliveira Apr 07 '11 at 22:18
  • Is the author really saying that trace equivalence is strictly finner than LTL equivalence? Corollary 3.18 of the book states: TS is equiv to TS' iff they satisfy the same LT properties, in support of Sylvain's comment. I mean in this case LTL equiv, would also be finer than trace equiv. – Mateus de Oliveira Oliveira Apr 07 '11 at 22:26
  • @Mateus LT = "Linear Time" properties, that is, sets of traces. It shouldn't be confused with LTL properties, which are specified by LTL formulas. Also, you have to be very careful when you throw around "isomorphic". Isomorphic as what? As first order structures? Does that imply that they are trace equivalent? – Mark Reitblatt Apr 08 '11 at 17:59
  • @Dave Ok, after reviewing B&K, they consider both infinite and finite transition systems. – Mark Reitblatt Apr 10 '11 at 01:55
  • @Mateus: Kamp's theorem is for FO with an order relation not FO over an arbitrary signature. You cannot refer to the edge-relation of the transition system, which is required to specify the structure up to isomorphism. – Vijay D Apr 11 '11 at 21:12
  • @Vijay, thanks for the explanation. I wasn't sure if there was not a way to express the edge relation of the transition system. – Mateus de Oliveira Oliveira Apr 12 '11 at 05:46

2 Answers2

9

Reading Baier and Katoen closely, they are considering both finite and infinite transition systems. See page 20 of that book for definitions.

First, take the simple transition system $EVEN$:

EVEN

Lemma: No LTL formula recognizes the language $L_{even} = $Traces$(EVEN)$. A string $c \in L_{even}$ iff $c_i = a$ for even $i$. See Wolper '81. You can prove this by first showing that no LTL formula with $n$ "next-time" operators can distinguish the strings of the form $p^i\neg p p^\omega$ for $i> n$, by a simple induction.

Consider the following (infinite, non-deterministic) transition system $NOTEVEN$. Note that there are two different initial states:

enter image description here

Its traces are precisely $\{a,\neg a\}^\omega - L_{even}$.

Corollary to the Lemma: If $NOTEVEN \vDash \phi$ then $EVEN \not\vDash \neg\phi$

Now, consider this simple transition system $TOTAL$:

Total TS

Its traces are clearly $\{a,\neg a\}^\omega$.

Thus, $NOTEVEN$ and $TOTAL$ are not trace equivalent. Suppose they were LTL inequivalent. Then we would have an LTL formula $\phi$ such that $NOTEVEN \vDash \phi$ and $TOTAL \not\vDash \phi$. But then, $EVEN\vDash \neg\phi$. This is a contradiction.

Thanks to Sylvain for catching a stupid bug in the first version of this answer.

Mark Reitblatt
  • 1,690
  • 15
  • 20
  • Hmm, this isn't perfectly clear. Should I make the steps around the contradiction more explicit? The transition systems also aren't as pretty as they could be... – Mark Reitblatt Apr 10 '11 at 04:15
  • You are mis-interpreting the $L_\text{even}$ language: the system you are proposing is equivalent to the formula $a\wedge\mathsf{G}((a\to\mathsf{X}\neg a)\wedge(\neg a\to\mathsf{X}a))$. The correct system should have a nondeterministic choice in the initial, $a$-labeled state $q_0$ between going to a state $q_1$ labeled by $a$ and one $q_2$ not labeled by $a$. Both $q_1$ and $q_2$ have transitions returning to $q_0$. – Sylvain Apr 10 '11 at 19:00
  • @Sylvain you are correct. I tried to simplify, and I ended up breaking it! Let me fix that up. – Mark Reitblatt Apr 10 '11 at 21:03
  • Can't you "reverse" the argument, so that the two systems you compare in the end are $\mathit{EVEN}$ and $\mathit{TOTAL}$ instead of $\mathit{NOTEVEN}$ and $\mathit{TOTAL}$? – Sylvain Apr 11 '11 at 14:35
  • The formula $a$ distinguishes between $EVEN$ and $NOTEVEN$. – Vijay D Apr 11 '11 at 14:48
  • @Vijay No, the issue is distinguishing between $TOTAL$ and $NOTEVEN$. Both $EVEN$ and $NOTEVEN$ satisfy the formula $a$. However, incorporating Sylvain's suggestion did break the argument. I needed the "bad" language to be a singleton. I can fix it with a string that counts (not unlike Antti's anwer below), but I don't have time to change it right this moment. And I'd like to stick in full proofs this time so that I don't have any other stupid mistakes. – Mark Reitblatt Apr 11 '11 at 15:11
  • Ah. I got confused thinking $EVEN$ and $NOTEVEN$ were proposed for equivalence. Does an empty state mean that the state is not labelled $a$? As $NOTEVEN$ has an initial state labelled $\neg a$, it does not satisfy $a$. – Vijay D Apr 11 '11 at 20:01
  • @Vijay Ahh, you're right. NOTEVEN doesn't satisfy $a$, mea culpa. – Mark Reitblatt Apr 11 '11 at 20:08
  • The problem with my proof suggestion is I didn't work it out! I see the problem with your answer too. I thought while writing that $TOTAL$ should only satisfy 'true'. Should have followed that through. – Vijay D Apr 11 '11 at 22:24
  • 1
    @Mark Reitblatt: From what do you reason that sentence in the end "But then, $EVEN\vDash \neg\phi$."? I cannot see an argumentation that leads to that point, which is essential to show the contradiction. – magnattic May 12 '12 at 14:49
3

If your LTL definition includes the "next" operator, then the following applies. You have two sets of traces $A$ and $B$ . Let $b$ be any finite prefix of a trace in $B$. $b$ must also be a finite prefix of a trace in $A$, because otherwise you can convert this to a formula that is just a series of next-operators that detects the difference. Therefore every finite prefix of a $B$-word needs to be a finite prefix of an $A$-word and vice versa. This means that if $A \not= B$, there needs to be a word in $b$ so that all its finite prefixes appear in $A$ but $b$ in itself does not appear in $A$. If $A$ and $B$ are generated by finite transition systems I think this is impossible. Assuming infinite transition systems, you can define

$A = \{a,b\}^\omega$ and $B = A \setminus \{w\}$ where $w$ is e.g. the infinite word $aba^2b^2a^3b^3a^4b^4\cdots$.

Any LTL formula that holds universally for $A$ will hold universally for $B$ because $B$ is a subset of $A$. Any LTL formula that holds for $B$ also holds for $A$; for the sake of contradiction, assume not, but that $\varphi$ holds for every element of $B$ (i.e. for every element of the universe expect for the word $w$) but not for $w$. Then $\neg\varphi$ evaluates to true on $w$ but not on any other word of the universe (and LTL is closed under negation), and there is no LTL formula that can be true only for $w$ as every Buchi automaton that accepts only one infinite word must be strictly cyclic whereas $w$ is not.

antti.huima
  • 295
  • 1
  • 8
  • Those are finite traces. Assuming you extend them to infinite traces with $a^\omega$ at the end, the formula $\neg (b\wedge X (b \wedge X G a))$ accepts the second set but rejects the first. – Mark Reitblatt Apr 08 '11 at 20:51
  • You're right, I wrote a new answer :) LOL, I remembered from my days in theoretical cs that LTL doesn't have the next operator :) – antti.huima Apr 09 '11 at 04:29
  • I think this does the trick. – Dave Clarke Apr 09 '11 at 09:02
  • I think it works too. – Mark Reitblatt Apr 09 '11 at 16:07
  • This answer isn't satisfactory. The OP was asking for transition systems, but the answer is about languages and justified in terms of Buchi automata and $\omega$-regular languages, which aren't in the text referenced. – Mark Reitblatt Apr 09 '11 at 23:34
  • I removed references to $\omega$-regularity. They weren't anyway needed. It is known that there is a Buchi automaton for every LTL formula so I think they can be used as a device. And there was no requirement that the transition systems would be finite. Finite transition systems generate trace sets that are as languages regular. I don't know if LTL equivalence = trace equivalence for trace sets generated by finite transition systems. If I would have to guess I would guess yes. – antti.huima Apr 10 '11 at 01:12
  • I can construct two Buchi automata that are LTL indistinguishable. It's fairly simple: it's basically the trick you use, but the "outside" language is $\omega$-regular and not LTL expressible. But doing it for transition systems seems to be trickier. – Mark Reitblatt Apr 10 '11 at 01:37
  • LTL equivalence = trace equivalence for finite transition systems. – Dave Clarke Apr 10 '11 at 08:00
  • Is LTL equivalence = trace equivalence also for finitely branching transition systems? The solution above can be easily implemented as a transition system if one $\aleph_0$ branch is allowed – antti.huima Apr 10 '11 at 17:10
  • Well ok Mark's answer also involves an $\aleph_0$ branch so I guess it's settled. – antti.huima Apr 11 '11 at 03:21