The bale of grass, the goat and the tiger
Many versions of this problem are described in the Wikipedia page
on "River crossing puzzles".
John McCarthy (1927-2011), a pioneer of artificial intelligence and a
winner of the ACM Turing award in 1971, describes how the related problem of
"Missionaries and cannibals" can be generalized in many different ways in
his 1997 article
Elaborating MCP.
Model checking
A simple temporal logic model checking algorithm is described in the article:
There are many books on model checking and other logic-based techniques
for verifying systems:
-
Logic in computer science by Michael Huth and Mark Ryan,
Cambridge University Press, 2nd ed, 2004.
-
Model checking by Edmund Clarke, Orna Grumberg and Doron Peled,
MIT Press, 2000.
-
Principles of model checking by Christel Baier and Joost-Pieter Katoen,
MIT Press, 2008.
Implementing model checking
The papers below discuss implementation techniques used in
model checking. See also video lectures by Donald Knuth on
Computer Musings
(the lectures on BDDs and ZDDs).
-
R E Bryant,
Graph-based algorithms for boolean function manipulation,
IEEE Transactions on Computers, Aug 1986.
-
H R Andersen,
An introduction to binary decision diagrams, April 1998.
-
I Bahar, E Frohm, C Gaona, G Hachtel, E Macii, A Pardo and F Somenzi,
Algebraic decision diagrams and their applications,
Formal Methods in System Design, April/May 1997.
-
E M Clarke, K McMillan, X Zhao, M Fujita and J Yang,
Spectral transforms for large boolean functions with applications to
technology mapping,
Formal Methods in System Design, April/May 1997.
-
A Mishchenko,
An introduction to zero-suppressed binary decision diagrams, June 2001.