Amusement is now a major application domain of computers and
entertainment software has a certain degree of importance to
consumers.  The target of this thesis is entertainment software with
interactive stories that dynamically branch according to users'
actions.  Script languages for describing such scenarios usually tend
to be rather _ad hoc_ and naive, which often leads to bugs in those
scenarios.  This thesis proposes a scenario description language with
clear and simple syntax and semantics, which enables systematic
verification of consistency conditions of complex scenarios.  The
language is based on a state transition model with a finite number of
variables varying over a finite number of values, where a scenario is
described as a set of commands that (1) are guarded by conditions over
the value of variables, (2) may branch over user input, and (3) modify
the value of variables.  Our automatic scenario checker traces every
possibility of the user input in parallel.  Since this parallelism is
highly fine-grained, the checker makes use of StackThreads, a generic
library for fine-grained multi-threading.  It also exploits shortcuts
and confluence found in a given scenario in order to reduce the number
of states to explore.