We develop a sound foundation for model checking algorithms for the class of PRS-style BDI agents, by showing how a reachability graph for any given PRS-type agent can be constructed from the agent program, thus addressing a long-standing issue in the verification of BDI agents. Categories and Subject Descriptors I.2.11 [Artificial Intelligence]: Distributed Artificial Intelligence—Intelligent agents General Terms Theory, Verification Keywords Model checking, BDI agent architectures