A Kripke structure M = (S, I, R, L) models a mutual exclusion protocol. S = {s0, s1, s2, s3}, I = {s0}. What does the labeling function L contribute that the states and transitions alone do not?
AL defines which transitions are valid
BL assigns observable properties to states (e.g., 'process 1 is in its critical section'), enabling temporal logic formulas about those properties to be evaluated
CL determines the initial states
DL specifies the order in which states are explored
States and transitions define the system's behavior — what can happen. The labeling function L maps each state to the atomic propositions true in that state, creating the bridge between the system model and the specification language. Without L, the model checker has no way to evaluate a formula like AG(not (cs1 and cs2)) because it wouldn't know which states satisfy cs1 or cs2. L is the semantic interpretation of propositions in the model.
Question 2 True / False
In a Kripke structure, the transition relation R must be total — every state must have at least one successor.
TTrue
FFalse
Answer: True
Totality of R is a standard requirement in Kripke structures for temporal logic. If a state had no successors, infinite computation paths through that state would be undefined, and temporal operators like G (globally) and F (eventually) would lose their meaning. In practice, if a system can halt or deadlock, this is modeled by adding a self-loop from the terminal state to itself, making the system stutter in the terminal state forever rather than having no successor.
Question 3 Short Answer
How does a Kripke structure for a concurrent system with two processes relate to the individual Kripke structures of each process?
Think about your answer, then reveal below.
Model answer: The composite Kripke structure is the synchronous or asynchronous product of the individual structures. In asynchronous composition, each state is a pair (s1, s2) of component states, and a transition occurs when either component takes a step (interleaving). The state space is the Cartesian product S1 x S2, and the labeling is the union of component labels. This product construction is the source of state explosion: n components with k states each yield up to k^n composite states.
Composition is both the power and the curse of Kripke-structure-based model checking. It naturally models concurrency (all possible interleavings are encoded in the product), but the exponential blowup in state count is the state explosion problem. Symbolic representations (BDDs, SAT) and abstraction techniques exist specifically to handle these composite structures without explicitly enumerating every product state.