论文研究-一种基于时间自动机的域构造方法.pdf

模型检验是一种重要的形式化自动验证技术，通过状态空间搜索来保证软硬件设计的正确性。由于TCTL不是针对时间自动机，而是针对有限状态变迁系统的，从而无法使用TCTL直接对时间自动机进行模型检验。给出了一种从时间自动机到有限状态变迁系统的方法，并在不改变时间自动机的语义上，使时间自动机等价后的域状态数尽可能少，在一定程度上有效地解决了状态空间爆炸问题。