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]