How to define the Atomic Propositions in Model Checking

Question

The atomic propositions in Symbolic Model Checking form the state in the state-transition graph (the model $\mathcal{M}$ in Model Checking). The other part of Model Checking is the specification, which is usually some sort of temporal logic formula over the atomic propositions in the model.

My question is about the atomic propositions themselves. I have only seen a few rudimentary examples of them, such as $x = 20$ or $printer is busy$. These atomic propositions (I think) are stating a fact about the state of the program at that point in the system. You then use a temporal logic formula to see if the model holds under it. I am confused by how the atomic propositions are both defined and used.

First, how they are defined. I haven't seen anywhere a description on how you define these atomic propositions. That is my first question. I don't understand how stating $x > 100$ in a state in the model $\mathcal{M}$ means anything. I didn't have to prove it or anything. It was just stated as fact. Then the temporal logic formula comes along and is checked against it, but there's some disconnect there for me. The value was never proven correct in the first place. It's as if, in my program, I make an HTTP request and during the waiting period before a response, my atomic proposition is that $\mathtt{the\ sky\ is\ blue}$. Wondering why was it put there, how do I know that it is true. A better atomic proposition would be $\mathtt{the\ request\ was\ sent}$. But again, I don't see how the program/model/checker "knows" this. I don't see what is doing the verification that that statement is true.

So my question is basically, how you define atomic propositions in Symbolic Model Checking. What goes into them. How you are allowed to make such statements that seemingly aren't verified. I don't see how I can say anything about the state of the program without something else "checking" that yes $\mathtt{the\ request\ was\ actually\ sent}$. I understand that after we define this model, we have our specification formulas and check them against the model. But we never checked the model itself for accuracy, is what I'm trying to get at.

I feel like, after writing down, in a specific state, an atomic proposition, I would then need to write a unit test to verify that it was true for some input. Not sure what I'm missing.

Answer 1

Formal verification often involves at least three steps:

1. Make a formal model of the real-world system. (The formal model might be a state-transition graph or automaton, for example.)

2. Write down a specification that hopefully captures the real-world requirements.

3. Verify that the formal model of the system meets the specification.

Formal methods provides guarantees about step 3; if step 3 succeeds, then we know that the formal model meets the spec. It doesn't provide any guarantees about steps 1 or 2. If there is a bug in the model, that causes it to fail to accurately capture the behavior of the real-world system, then the result of the verification process becomes meaningless and all guarantees are off. So, you need some separate way to gain assurance in those steps.

The atomic propositions are part of that modelling process. Usually, there are some parts of the real-world system that we model in the state-transition graph and others that we don't. For instance, consider a traffic light. It has some sensors to sense presence of cars and pedestrians; some logic to determine what color light to show in each direction; and some actuators (light bulbs) to actually display those chosen colors. We might choose to model the logic in a formal model, and verify that the logic works properly. This verification process might not verify anything about the sensors or the actuators; it might just assume they are correct. That might be justified if, for instance, we think the logic is the part that is most likely to have subtle errors. Then you might have an atomic proposition for "sensor #1 detected a pedestrian at such-and-such cross-walk" ($p_1$) and an atomic proposition for "turn on the green light facing in the N direction" ($q_N$). Those atomic propositions represent the inputs or outputs to the logic, or facts about the state of the system. The spec then has to be stated in terms of the atomic propositions, e.g., "it should be impossible to have the green light turned on in the N direction and in the E direction" ($G (\neg q_N \lor \neg q_E)$).