有限精度时间自动机的模型检测方法及语言特征研究

时间自动机是实时系统最广泛使用的一种形式模型，有限精度时间自动机（FPTA）是时间自动机的一种变形。两者语法相同，后者以整值时钟解释和时钟序取代前者的实值时钟解释。在左闭右开时间约束下, 同一自动机在两种语义下的可达性是一致的。但FPTA定义的时间语言类具有较好的性质，该语言类关于布尔运算是封闭的，且语言包含问题是可判定的。.本课题主要从事FPTA的模型检测和语言特征的研究。1.在我们已有的基于延迟序列符号化表示的模型检测方法的基础上，通过与BDD等的结合，寻找新的符号化表示方法和更高效的模型检测算法；2. 尝试现有的一些状态空间归约技术及模型抽象方法在FPTA中的使用，并发展新的适合于FPTA的抽象与归约方法；3. 研究FPTA的语言特征，确定FPTA、时间自动机及tick-自动机这三种模型定义的时间语言类之间的关系、寻找与FPTA对应的时序逻辑系统。