Questions about temporal logic.

Question

Hi,

1. In the past exams, the order of precedence wasn't specified. What binds stronger propositional logic operator or temporal operator?
2. Is it safe to assume an E before a path formula, which has no path, so if just Gb is given then it is equivalent to EGb? 

Answer 1

The precedences in the teaching tools are as follows:

    LOWEST
    1. EQV
    2. IMP
    3. OR
    4. XOR
    5. AND
    6. X G F PG GF PWX PSX E A <> [] <:> [:] mu.x nu.x
    HIGHEST

Note that we do not have to specify precedences for the binary temporal operators since these have to be written with brackets which makes their syntax unambiguous. The same holds for the conditional operator. Note that the mu and nu operators are bind highest, so that it is best to write brackets after them like mu x.(...).

The formulas Gb and EGb are different formulas. The former is a path formula that should be interpreted on a path, the latter is a state formula that shall be evaluated on a state. So, it is not safe to consider them same.

Comments

So how can i understand the formula (EGa) WB (Ga)? The second Ga doesn't make sense without a path being given ? Is this formula valid?  EGa WB EGa does not hold in my opinion. Is this the same with EGa WB Ga?

---

First, [p WB p] is equivalent to G¬p, since p cannot hold before p holds, so we can only satisfy [p WB p] with the exceptional case where G¬p holds. Hence, also [(Gp) WB (Gp)] will be equivalent to G¬Gp which is GF¬p.

Second, I can image a path in a structure where [(EGa) WB (Ga)] holds. Consider the following structure

    vars a;
    init 0;
    labels 0:a; 1:a; 2:; 3:a;
    transitions 0->1; 0->2; 1->1; 2->3; 3->3;

You can easily check that EGa holds on states 0,1,3 and that [(EGa) WB (Ga)] holds on the path 0->2->3->3... since EGa already holds in state 0 while the Ga only becomes true from state 3 onwards.

Third, [(EGa) WB (EGa)] could only be satisied when G¬(EGa), i.e., GAF¬a holds, which is possible on the single path of the following structure:

    vars a;
    init 0;
    labels 0:;
    transitions 0->0;

So be careful with the branching time!

---

Thank you for your answer,  I still don't understand about which path Ga talks? In my opinion Ga does not make sense if it does not have an underlying path? Does it talk about any path starting at an initial state?

---

Ga is a path formula, and to discuss it, we need a path to talk about it, right. In my example above for [(EGa) WB (Ga)], I considered the path 0->2->3->3...  and Ga holds on that path from state 3 onwards. However, EGa holds on states 0,1,3 and therefore also on state 0, i.e., the first state on that path. That is so, since the path used to justify EGa there is another path, namely, 0->1->1...

---

just to be clear, as Ga is a path formula and EGa is a state formula, [(EGa) WB (Ga)] is a path formula, which as you said needs a path to talk about. So the formula [(EGa) WB (Ga)] implicilty stands for E[[(EGa) WB (Ga)]], to show it is satisfiable you chose so,s1,s1,s1... for the inner path(innermost) as this satisfies Ga and s0,s2,s3,s3... for the outermost path as it satisfies Ga later?

---

Right, that is the case.

---

Thank you for all your answers. So i should imagine an E before a path formula ? I

---

For satisfiability, yes, you can do so, but when it comes to evaluating the formula on a structure, then no, since one is a state formula and the other one is a path formula.