%0 Journal Article
%T Checking Temporal Duration Properties of Timed Automata
%A Dang Van Hung
%A <br>李勇
%J 计算机科学技术学报
%D 2002
%I 
%X In this paper, the problem of checking a timed automaton for a Duration Calculus formula of the form Temporal Duration Property is addressed. It is shown that Temporal Duration Properties are in the class of discretisable real-time properties of Timed Automata, and an algorithm is given to solve the problem based on linear programming techniques and the depth-first search method in the integral region graph of the automaton. The complexity of the algorithm is in the same class as that of the solution of the reachability problem of timed automata.
%K model checking
%K duration calculus
%K timed automata<br>时控自动化
%K 持续时间计算
%K 模型检测算法
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=F57FEF5FAEE544283F43708D560ABF1B&aid=31D4F41DD72ED693324970587613948A&yid=C3ACC247184A22C1&vid=BCA2697F357F2001&iid=B31275AF3241DB2D&sid=2B25C5E62F83A049&eid=2B25C5E62F83A049&journal_id=1000-9000&journal_name=计算机科学技术学报&referenced_num=0&reference_num=12