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:

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).