# Kripke Structure

A finite state machine, whose states are labeled with boolean variables and whose next state is chosen nondeterministically. It may be extended with fairness constraints.