In essence, a (finite) labelled transition system in which every state has at least one transition (“left total”).

Notes related to Kripke structure

Büchi automaton, Model checking, Temporal logic

Papers related to Kripke structure

• Software model checking [jhala:compsurv:2009]
• Relational test tables: A practical specification language for evolution and security [weigl:arxiv:2019]