We construct the model by four layer abstraction: state, transition, action, and labeling abstraction, which are described below.