Fluent temporal logic for discrete-time event-based models
Fluent temporal logic for discrete-time event-based models
复制标题
基于离散时间事件的模型的流畅时序逻辑
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Sebastián Uchitel
中科院分区：
文献类型：
--
作者：
Emmanuel Letier;J. Kramer;J. Magee;Sebastián Uchitel
Fluent模型检查是一种自动化技术，用于验证基于事件的操作模型是否满足某些基于状态的声明性属性。基于事件和基于状态的形式主义之间的联系是通过“流”来定义的，“流”是状态谓词，其值由使流值分别变为真或假的起始事件和终止事件的发生来确定。本文扩展了流畅的时态逻辑与时间运营商建模的时间属性的离散时间基于事件的模型。它提出了两种方法，不同的属性模型的系统状态发生后，每个事件或在一个固定的时间率。定时属性的模型检查是通过将它们转换到现有的非定时框架中来实现的。
Fluent model checking is an automated technique for verifying that an event-based operational model satisfies some state-based declarative properties. The link between the event-based and state-based formalisms is defined through "fluents" which are state predicates whose value are determined by the occurrences of initiating and terminating events that make the fluents values become true or false, respectively.The existing fluent temporal logic is convenient for reasoning about untimed event-based models but difficult to use for timed models. The paper extends fluent temporal logic with temporal operators for modelling timed properties of discrete-time event-based models. It presents two approaches that differ on whether the properties model the system state after the occurrence of each event or at a fixed time rate. Model checking of timed properties is made possible by translating them into the existing untimed framework.