Kripke Structures
A Kripke structure over a set of atomic propositions \(\texttt{AP}\) is a 4-tuple
\[ \texttt{K} = (S, I, \rightarrow, \lambda) \]
where:
- \(S\) is a finite set of states.
- \(I \subseteq S\) is the non-empty set of initial states.
\(\rightarrow \subseteq S \times S\) is a transition relation, such that \(\rightarrow\) is left-total, i.e.
\[\forall s \in S. \exists s^\prime \in S. (s, s^\prime) \in \rightarrow \]
- \(\lambda: S \rightarrow 2^{AP}\) is an interpretation (or labelling) function that maps each state to its set of valid atomic propositions.