What exactly state is in Model Checking

Question

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.

1. States are steps in a Control-Flow Graph (CFG).
2. States are combinations of Boolean Variables or Atomic Propositions.
3. States are just identifiers or labels.
4. 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 Checking means when they talk about state.

So my question is, what exactly state is in Model Checking. Until today I have always imagined it as CFG nodes like in (1), in which case there is a relatively small number of them. But now I am starting to think they are more like (2), independent of CFG nodes. I can't tell yet. Program changing/running and state changing are things that almost always happen together. But I'm confused, thinking maybe the states in a state-transition graph / Kripke Structure are really just an abstract collection of Boolean Variables or Atomic Propositions. Please let me know if I am wrong.

Answer 1

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.

Answer 2

A Kripke structure is a mathematical formalism. Formally, a state in a Kripke structure is just a piece of mathematics; it is an element of the set $S$. It's up to us what interpretation we put on it.

Sure, there are some applications where we model a CFG as a Kripke structure, and we let the state represent the current location in the control-flow graph (i.e., the state represents the value of the program counter). That's a modelling decision we make. There's nothing that says we have to do it that way; it's a choice we can make, or not make, according to whatever is useful for our purposes.

Perhaps the key distinction here is between a piece of mathematics and a piece of the real world; the difference between the real-world system and a mathematical model of it; and the correspondence between the two. There are many ways you might be able to model a real-world system. Conversely, there are many ways you might be able to interpret a mathematical structure and use it to model real-world systems.