计算机软件新技术-计算机科学国家重点实验联合学术研讨会

演讲人:李广元

题目: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.