(definition)
Definition: A nondeterministic finite state machine whose states are labeled with boolean variables, which are the evaluations of expressions in that state. It may be extended with fairness constraints.
See also model checking.
Author: PEB
If you have suggestions, corrections, or comments, please get in touch with Paul E. Black.
Entry modified Fri Dec 17 12:05:03 2004.
HTML page formatted Wed Oct 26 09:47:42 2005.
Cite this as:
Paul E. Black, "Kripke structure", from
Dictionary of Algorithms and Data
Structures, Paul E. Black, ed.,
NIST.
http://www.nist.gov/dads/HTML/kripkeStruct.html
