The formal definition of model checking is:

If M is a Kripke structure (i.e., a state transition graph) and φ a formula in temporal logic (i.e., a specification), then model checking is the problem of verifying M |= φ (i.e., whether or not φ is true in M).

In other words, "model checking" determines whether the structure M is a model for formula φ.

We often use model checking in the sense of "checking a model for properties", i.e., that a miniature representation or abstraction of a system of interest has properties indicated by a specification; while this makes sense, it is not how the inventors of model checking thought about it¹.

In this OP, please identify what M and φ are in FISC and MODIST, the two systems assigned for today. You are not expected to write M and φ formally, but rather just use clear prose. You will most likely want to devote two paragraphs to each system (one paragraph for M and one for φ).

¹ Model checking was invented by Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis. They jointly received the Turing Award in 2007 for their work.

---

Favorite OP5: Salman's OP