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.
- 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 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.