Abstract: The model of simple batch systems is the foundation of its performance evaluation, simulation, scheduling,and control research. This paper introduced a mathematical model named batch automata for simple batch systems, andgave an algorithm for translating a batch automata into a Kripke structure, and completed the model checking of batch system based on the Kripke structure to verify the reasonable property, i. e.，both fair and efficiency.

Key words: Simple batch systems,Model checking,Kripke structure,Automata