时间自动机状态空间的一个极小化构造方法

计算机工程与应用 ›› 2007, Vol. 43 ›› Issue (14): 30-33.

时间自动机状态空间的一个极小化构造方法

姬莉霞周清雷李占波苏锦祥

郑州大学软件技术学院郑州大学信息工程学院郑州大学软件技术学院郑州大学信息工程学院

收稿日期:2006-09-21 修回日期:1900-01-01 出版日期:2007-05-10 发布日期:2007-05-10
通讯作者: 姬莉霞

Minimizing the state space of timed automata

LiXia Ji Zhanbo Li JinXiang Su

Received:2006-09-21 Revised:1900-01-01 Online:2007-05-10 Published:2007-05-10
Contact: LiXia Ji

摘要/Abstract

摘要： 基于时间自动机的可达性分析是模型检测最常用的方法之一，但该方法饱受状态空间爆炸问题的困扰。本文对时间自动机的转换系统进行改进，提出了一个状态空间的极小化构造方法。该方法用位置和停留在该位置时的可能时钟值集合来表示状态，以此隐藏因时间流逝而引发的无穷状态，得到了改进的转换系统——时间段转换系统；并通过对转换可能发生时间的分析，去除无效转换；然后使用转换互模拟合并等价状态，实现了状态空间的极小化，有效地避免了状态空间爆炸。

关键词: 时间自动机, 转换系统, 可达性, 状态空间, 模型检测

Abstract: The reachability analysis based on timed automata is one of the most used methods for model checking. Its’ major weakness is the state-space-explosion problem. In this paper, we developed the traditional transition system and advanced a method of state space minimization. The method described the state by location and the possible set of clocks staying in this location. We name that as time segment transition system. It hid the infinite state which was brought by time elapsing. We removed the invalid transition by analyzing the possible occurring time of the transition. Then we minimized the transition system by utilizing the transition bisimulation, and avoided the state-space-explosion problem effectively.

Key words: timed automata, transition systems, reachability, state space, model checking

姬莉霞周清雷李占波苏锦祥. 时间自动机状态空间的一个极小化构造方法[J]. 计算机工程与应用, 2007, 43(14): 30-33.

LiXia Ji Zhanbo Li JinXiang Su. Minimizing the state space of timed automata[J]. Computer Engineering and Applications, 2007, 43(14): 30-33.

[1]	李艳，王阳阳，张红岩，武优西. 不可达顶点剪枝算法及其在最短路径中的应用[J]. 计算机工程与应用, 2020, 56(15): 51-57.
[2]	李艳东，朱玲，郭媛，于颖，赵丽娜. 电驱移动机器人多变量固定时间连续编队控制[J]. 计算机工程与应用, 2020, 56(15): 228-234.
[3]	陈晓倩，刘瑞祥. 基于最小二乘策略迭代的无人机航迹规划方法[J]. 计算机工程与应用, 2020, 56(1): 191-195.
[4]	蒋梦梦，周杰. 基于高维状态空间方法构建金融市场网络模型[J]. 计算机工程与应用, 2019, 55(10): 53-60.
[5]	李茜1，王峥1，马建芬1，李娜2. 轻量级移动支付协议公平性分析[J]. 计算机工程与应用, 2018, 54(19): 82-87.
[6]	裴常福1，王彬1，薛洁2，刘辉1，熊新1. 基于时间自动机的脑网络时空演化建模方法[J]. 计算机工程与应用, 2018, 54(14): 45-51.
[7]	李前利，江华. 命题μ-演算局部模型检测高效算法设计[J]. 计算机工程与应用, 2017, 53(9): 51-56.
[8]	宋英莉，刘宣宇，张凯举，施惠元，王倩. IMNMSSPC算法在盾构机土压平衡控制中的应用[J]. 计算机工程与应用, 2017, 53(4): 251-255.
[9]	朱文亮1，2，倪福生1，2，王素红3，尹飞3. 疏浚泥浆浓度最优控制跟踪器的设计与实现[J]. 计算机工程与应用, 2017, 53(21): 263-270.
[10]	马旭辉1，滑亚飞2，何忠贺2. 基于路网可达性的交通控制子区划分方法研究[J]. 计算机工程与应用, 2017, 53(17): 224-228.
[11]	秦嫚蔓，王峥，王莉. 基于SPIN的远程证明协议的形式化分析及改进[J]. 计算机工程与应用, 2017, 53(1): 34-38.
[12]	张驰，褚楚，唐颖军，陈升. 基于行为投影的Web服务组合行为兼容性研究[J]. 计算机工程与应用, 2016, 52(20): 46-51.
[13]	吕江华1，刘志锋1，徐亚涛2，周从华1. 基于属性的访问控制策略的正确性验证[J]. 计算机工程与应用, 2016, 52(18): 98-103.
[14]	朱文涛. 逻辑LTS预备模拟关系的判定算法[J]. 计算机工程与应用, 2016, 52(17): 41-48.
[15]	夏春蕊1，王瑞1，李晓娟1，关永1，张杰2，魏洪兴3. 动态环境下基于概率模型检测的路径规划方法[J]. 计算机工程与应用, 2016, 52(12): 5-11.