How to define the Atomic Propositions in Model Checking
Formal verification often involves at least three steps: 


Make a formal model of the real-world system.  (The formal model might be a state-transition graph or automaton, for example.)
Write down a specification that hopefully captures the real-world requirements.
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)$).