题目：Model Checking Time-Constraint LTL Properties for Timed Automata
摘要：Time-constraint LTL is an extension of propositional linear temporal logic(LTL) with atomic clock constraints added as atomic formulas. It can be regarded as a linear-time version of the requirement specification language used in the model checker of Uppaal. This talk will describe an automata-theoretic approach via automata emptiness for model checking time-constraint LTL properties of timed automata. We will show that time-constraint LTL formulas can be translated into time-constraint Buchi automata, which are a special subclass of timed Buchi automata. By combining this translation procedure with our previous zone-based emptiness checking procedure for timed Buchi automata, a tool for model checkingtime-constraint LTL properties for timed automata has been implemented.