VRS : S1 and S2 formula satisfiability Diagram Question ( LTL, CTL, CTL*)

Question

Hello,

I have some queries regarding the problem asked most of the time in exam related to LTL, CTL, CTL* stuff where one has to draw a Kripke structure to satisfy either formula.

Query 1 : Is there any way to verify our solution whether it is correct or not using tools ? ( As far as I know, there can be multiple solutions to a question). 

Query 2 : How to draw structures for formulas like F( a <-> b ) or G( a <-> b )?  Because if we expand a <-> b as (( !a or b) & ( !b or a)), either {a,b) or {!a,!b} can be satisfied. So Are the below structures correct?

Query 3 : Exam August 27th, 2019 Problem 7a, here formula has XX(....), Suppose I have XX(a), I will take first two states as empty and then third state will be a. 
 

But in solution provided, only s0 and s2 is considered, s1 is not considered. I am not able to understand this. 

Thanks in advance.

Answer 1

These kind of exercises ask for your intuition and understanding of the formulas even though there are also algorithms that could be used to decide the equivalence and satisfiability of LTL/CTL/CTL* formulas.

Answer to Query 1: In most cases, the structures do only have a single path. Here, CTL* and LTL become the same since the E and A quantifiers can only consider the only existing path. Hence, you can use the LTL tool for checking those formulas (see below).

There is no teaching tool for satisfiability of CTL*, but there is a preliminary tool that you can find under https://es.cs.uni-kl.de/tools/teaching/PreStructures.html. The tool computes a so-called pre-structure that consists of states and transitions that could satisfy the given formula. You need however check whether it is possible to satisfy the reachability constraints of the formula. Still, the computed structure is often of great help.

Answer to Query 2: As many formulas, the formulas F(a<->b)  or GF(a<->b) have more than one model, so that many answers are possible (in general also every bisimular structure to the given one could be used also). Since the LTL tool is only about satisfiability/validity of LTL formulas, you have to describe your single-path structure as an LTL formula. For your second example, this may look as follows:

    (!a & !b) & X(a & b) & X X G(a & !b) -> F(a<->b)

If you use https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html, it will tell you that the above LTL formula is valid and therefore is an example that satisfies F(a<->b). If you try the following

    (!a & !b) & X(a & b) & X X G(a & !b) -> G(a<->b)

you will get a counterexample (ignore the _q* variables and it is a path of your structure).

Answer to Query 3: Your idea to get rid of the XX using the two states you mentioned is fine! However, you need to make sure that from s2 onwards one of the formulas without the XX is true while the other (without the XX) is false. That is not the case with your example. Check the following:

    (!a & !b) & X(!a & !b) & X X G(a & !b) -> X X (G(a⊕b) ⊕ F(a<->b))

    (!a & !b) & X(!a & !b) & X X G(a & !b) -> X X ((G(a⊕b))∨(G(a<->b)))

Note that from s2 onwards, G(a⊕b) holds, and F(a<->b) is false. Thus, G(a⊕b) ⊕ F(a<->b) and also (G(a⊕b))∨(G(a<->b)) are both true.