patternMinor
What exactly state is in Model Checking
Viewed 0 times
whatcheckingstateexactlymodel
Problem
So I finally realized the difference between transition systems and automata, and now am closer to understanding Model Checking. One of the last pieces is understanding what exactly "state" is in Model Checking.
It is mentioned that you create a Kripke Structure, which is pretty much just a state-transition system. But the thing is, I don't know what exactly the states are.
In my confusion, I think I see 3 or 4 different interpretations of states in regards to Model Checking.
There is a problem with (1). Specifically, you may perform an action, and yet the value of all your atomic propositions stay the same. So it seems there is a distinction between "state as in a program step" and "state as in a set of atomic propositions". In scheduling/planning, I think this is how they conceive of states, as CFG nodes along with some Atomic Propositions.
There is a problem with (2) as well. You can create all kinds of combinations of Atomic Propositions, like even creating a Power Set of every number and combination. I wonder if these "objects" are actually called states, or if I am confusing something here. If they are states, then states are completely independent of the program CFG, though it might be correlated in some cases. Also in this case, states can be nested, because you can have states part of larger and larger sets.
My feeling about (3) is that this is what Finite State Automata and other automata typically use for state. But it seems like in some places Model Checking might be defining states as labels instead of more complex objects like (1) and (2) or even (4).
In reactive systems state is considered the "whole application state", meaning the valuations of the state variables. I don't think this is what Model Checkin
It is mentioned that you create a Kripke Structure, which is pretty much just a state-transition system. But the thing is, I don't know what exactly the states are.
In my confusion, I think I see 3 or 4 different interpretations of states in regards to Model Checking.
- States are steps in a Control-Flow Graph (CFG).
- States are combinations of Boolean Variables or Atomic Propositions.
- States are just identifiers or labels.
- States are the values of the variables (any data variable, Boolean or not).
There is a problem with (1). Specifically, you may perform an action, and yet the value of all your atomic propositions stay the same. So it seems there is a distinction between "state as in a program step" and "state as in a set of atomic propositions". In scheduling/planning, I think this is how they conceive of states, as CFG nodes along with some Atomic Propositions.
There is a problem with (2) as well. You can create all kinds of combinations of Atomic Propositions, like even creating a Power Set of every number and combination. I wonder if these "objects" are actually called states, or if I am confusing something here. If they are states, then states are completely independent of the program CFG, though it might be correlated in some cases. Also in this case, states can be nested, because you can have states part of larger and larger sets.
My feeling about (3) is that this is what Finite State Automata and other automata typically use for state. But it seems like in some places Model Checking might be defining states as labels instead of more complex objects like (1) and (2) or even (4).
In reactive systems state is considered the "whole application state", meaning the valuations of the state variables. I don't think this is what Model Checkin
Solution
My vote is on (4) from an intuition point of view.
I just started learning this recently so take this with a grain of salt but as mentioned by D.W. the set of states can be anything you want. It is an abstract concept. However, it is natural to think of states as being valuations of the variables in the system. For example, we may think of the current state of the solar system as the current values of all variables of interest to us, such as all positions and velocities of the 8 planets in it.
Seeing it this way has another advantage. If we take the atomic propositions to be formulas of the form $x = v$ where $x$ is a variable and $v$ is a value, then the labeling function is simply the identity function: $L(S) = S$, and an atomic proposition $P$ is true in state $S$ iff $P \in S$.
The fact that the state space becomes the power set of all n-tuples of valuations of variables is not really a downside. Many of these states would simply be unreachable in any practical Kripke structure. As for your concern about states being "nested", first of all note that $S_1 \subset S_2$ means that they are actually different states. Secondly, if $S_1 \subseteq S_2$, then you have the property that anything true in $S_1$ is also true in $S_2$!
In fact, as far as I have seen, this is the interpretation used in many of the practical uses of Kripke structures that I have seen, such as in model checking in the context of formal verification.
I just started learning this recently so take this with a grain of salt but as mentioned by D.W. the set of states can be anything you want. It is an abstract concept. However, it is natural to think of states as being valuations of the variables in the system. For example, we may think of the current state of the solar system as the current values of all variables of interest to us, such as all positions and velocities of the 8 planets in it.
Seeing it this way has another advantage. If we take the atomic propositions to be formulas of the form $x = v$ where $x$ is a variable and $v$ is a value, then the labeling function is simply the identity function: $L(S) = S$, and an atomic proposition $P$ is true in state $S$ iff $P \in S$.
The fact that the state space becomes the power set of all n-tuples of valuations of variables is not really a downside. Many of these states would simply be unreachable in any practical Kripke structure. As for your concern about states being "nested", first of all note that $S_1 \subset S_2$ means that they are actually different states. Secondly, if $S_1 \subseteq S_2$, then you have the property that anything true in $S_1$ is also true in $S_2$!
In fact, as far as I have seen, this is the interpretation used in many of the practical uses of Kripke structures that I have seen, such as in model checking in the context of formal verification.
Context
StackExchange Computer Science Q#93363, answer score: 4
Revisions (0)
No revisions yet.