LTL Model checking

Question

February 17, 2021 Problem 6b

1) In acceptence condition I get GF(q0 -> b) & GF(q1 | b)  but in the solution it is GF(b | q1) only. Is it related to fairness constraint? Can you please explain.

2) Can you please show me the TT of transition ¬q0 & ¬q1 & a & ¬b & ¬q0' & ¬q1' or any other method to quickly draw the kripke structure ?

Sept 2022 Problem 6a

3) Can you please show me the truth table for p,q,pq,{}

  3.1. where p=0 and q =1. I m landing at (p' <-> a) & (!b & q). I am getting a transition from s1 to s2 on giving input 'a' (considering p' <-> a).

 3.2 where p=1 and q=0. I m landing at (p')&(!(!b&q)) = p'&(b|q). I m confused with drawing the transistion for p'&(b|q).

I hope once these questions are explained we will reach a good clarity.

Answer 1

About 1): adding each fairness constraint obtained by the simple translation from LTL to automata (shown on pages 83-84) is also correct. However, that will always generate a nondeterministic generalized Büchi automaton which is hard to determinize. Thus, we often wish to use as few of these constraints as possible, and if we are lucky, none of them is required at all. Pages 92-94 therefore first explain that we can neglect the fairness constraint for positive occurrences of weak temporal operators and we can also neglect the fairness constraint for negative occurrences of strong temporal operators. Another improvement is given on slides 115-116 where instead of fairness constraints, one may use coBüchi constraints in some cases. That may enable simple determinization procedures.

About 2): The formula ¬q0 & ¬q1 & a & ¬b & ¬q0' & ¬q1' describes only a single transition which is a self-loop on state {} with input {a}. Hint: you can use https://es.cs.uni-kl.de/tools/teaching/SymbolicStateTrans.html to quickly generate state transition diagrams. In general, you have to consider the satisfying assignments of the formula, which means to compute its truth table or a BDD or something where you can read these from.