Abstract:This paper proposes an event temporal logic (ETL) because there has been no suitable temporal logic that can directly describe the properties of event graph (EG) models. ETL takes events as its atomic propositions and has the abilities to describe the event canceling edge, the passing parameter values between events, time constraints and the priorities of coinstantaneous events, which can facilitate the description of properties for EGs. A model checking method for EG and ETL on the basis of theory of automata is also proposed in this paper to check whether properties hold for models, according to the accepted language is an empty set or not. The experimental results show ETL is powerful enough to describe EG models, and the model checking method for EG and ETL is effective.