%0 Journal Article
%T Region Construction Method for Timed Automaton<br>一种基于时间自动机的域构造方法
%A QIAN Jun-yan
%A ZHAO Ling-zhong
%A <br>钱俊彦
%A 赵岭忠
%J 计算机应用研究
%D 2005
%I 
%X 模型检验是一种重要的形式化自动验证技术，通过状态空间搜索来保证软硬件设计的正确性。由于TCTL不是针对时间自动机，而是针对有限状态变迁系统的，从而无法使用TCTL直接对时间自动机进行模型检验。给出了一种从时间自动机到有限状态变迁系统的方法，并在不改变时间自动机的语义上，使时间自动机等价后的域状态数尽可能少，在一定程度上有效地解决了状态空间爆炸问题。
%K Model Checking
%K Timed Automaton
%K TCTL<br>模型检验
%K 时间自动机
%K TCTL
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=A9D9BE08CDC44144BE8B5685705D3AED&aid=47DB60E18FEED5C9&yid=2DD7160C83D0ACED&vid=BC12EA701C895178&iid=DF92D298D3FF1E6E&sid=68D88C2FCF9C3098&eid=09ABD5535D9B6D45&journal_id=1001-3695&journal_name=计算机应用研究&referenced_num=0&reference_num=6