Propositional formula to FSM to Kripke

Question

Given a propositional formula, for example R=!(next(p)&next(q)->(a|o)&(q|p))

How can I convert this to the FSM diagram and then to Kripke structure?

Answer 1

FSM to Kripke

Let's start with the FSM → Kripke transformation. That's slide 8 in the Transition System chapter.

State variables: Each of the new Kripke states represents an FSM state, an input and an output. Simplified speaking, the FSM states variable, FSM input variables and FSM output variables together become the new Kripke state variables.

Transitions: A Kripke states inherits those transitions of the corresponding FSM state that have the input and output variables of the new Kripke state. It is important that the transitions get copied multiple times as we don't know anything about the input and output variables of the successor state.
Example: FSM state {q} has a transition with input a, output o to {p}.
Then the state {q,a,o} gets four transitions going to the four states {p}, {p,a}, {p,o}, {p,a,o}.

Now we only need to talk about the initial states. The initial states of the Kripke structure are those states that correspond to initial states of the FSM. There are two things to take care of:

1. Each initial FSM is represented by multiple initial states of the Kripke structure (with different values for input and output)
2. We remove initial states of the Kripke structure that have no outgoing transitions (deadends)

Symbolic FSM to FSM diagram

The symbolic representation is discussed on slide 54. The symbolic representation consists of two formulas. One described the transitions and one the initial states. Each state in the diagram represents one valuation of the state variables. So if your states variables are p and q, you get the states {}, {p}, {q}, {p,q}. In the transition formula, we also have input variables (in your example a), and output variables (in your example o). Then we also have the variables for the successor (vulgo: right side) states. In your example, they are p', q' (or as the online tool would say: next(p), next(q)).

Let's look at your example:

R = !(next(p)&next(q)->(a|o)&(q|p)) = …

For better readability, we replace the negated implication and apply De Morgan:

… = next(p)&next(q) & !((a|o)&(q|p)) = next(p)&next(q) & ( !(a|o) | !(q|p) ) = next(p)&next(q) & ( (!a & !o) | (!q & !p) ) = …

Now we multiply out

= (next(p) & next(q) & !a & !o) | (next(p)&next(q) & !q & !p)

Let's look at for example at the valuation with p, q, next(p), next(q) true and a, o false. We don't satisfy the right co-clause but we do satisfy the left co-clause. Great! So we know that there is a self-loop at {p,q} reading !a and outputting !o. Great!

We can continue reading the transition relation like that. All transitions lead to the state {p,q}. All of the four states have this transition to {p,q} reading !a and outputting !o. From the state {} to {p,q} there are four transition, one for each possible valuation of a and o.

If we now knew the formula for the initial states, we could mark all states that correspond to a satisfying assignment as initial states.

Source Code:

\documentclass[10pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{tikz}
\usetikzlibrary{arrows,automata,positioning}

\begin{document}
  \begin{tikzpicture}[shorten >=1pt,node distance=3cm,auto]
  \tikzstyle{state}=[minimum size=1.2 cm,draw,shape=circle]
      \node[state]  (nix){$\{\}$};
      \node[state, right of=nix] (p){$\{p\}$};
      \node[state,below of=nix]  (pq){$\{p,q\}$};
      \node[state,right of=pq] (q){$\{q\}$};
      \path[->]
        (p) edge node {$\neg a, \neg o$} (pq)
        (nix) edge node {$\ast$} (pq)
        (pq) edge [loop left] node  {$\neg a, \neg o$} (pq)
        (q) edge node {$\neg a, \neg o$} (pq)
    ;
  \end{tikzpicture}
\end{document}

Answer 2

In addition to Martin's answer, a good alternative to handle problems like these is to first compute for the possible states the corresponding instance of the transition relation, and from there the satisfying variable assignments. 

In the example, it seems that we have state variables p,q, input variable a, and output variable o even thought that is not clear from the question. If so, I would then compute the following instances of the transition relation R:

• p=0&q=0: thus, R becomes !(next(p)&next(q)->0) which is next(p)&next(q)
• p=0&q=1: thus, R becomes !(next(p)&next(q)->(a|o)) which is next(p)&next(q)&!a&!o
• p=1&q=0: thus, R becomes same as in p=0&q=1
• p=1&q=1: thus, R becomes same as in p=0&q=1

This means that we have the following transitions in the FSM:

• (p=0,q=0) --(a=*,o=*)--> (p=1,q=1)
• (p=0,q=1) --(a=0,o=0)--> (p=1,q=1)
• (p=1,q=0) --(a=0,o=0)--> (p=1,q=1)
• (p=1,q=1) --(a=0,o=0)--> (p=1,q=1)

You can use a teaching tool to check your computations, which also draws the FSM:

In case you also have initial states, it is wise to first compute the instantiated transition relation for those, and then for the next states reached from there to avoid unnecessary work on unreachable states.

To obtain the Kripke structure, you have to consider for each state the possible situations it can react to as Martin already described. A situation is thereby a combination of the state, input and output variables. In the given example, these are quite many transitions among the possible 16 states, but the transitions can be easily described as above for the FSM:

• (p=0,q=0,a=*,o=*) --> (p=1,q=1,a=*,o=*)
• (p=0,q=1,a=0,o=0) --> (p=1,q=1,a=*,o=*)
• (p=1,q=0,a=0,o=0) --> (p=1,q=1,a=*,o=*)
• (p=1,q=1,a=0,o=0) --> (p=1,q=1,a=*,o=*)

If you tell the above mentioned teaching tool that p,q,a,o are state variables and that there are no input variables, it will compute the Kripke structure for you.