On Signal Temporal Logic
On Signal Temporal Logic
复制标题
论信号时态逻辑
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Alexandre Donzé
中科院分区：
文献类型：
--
作者：
Alexandre Donzé
时间逻辑（TL）是一种流行的形式主义，被引入系统设计[PNU77]，作为一种指定反应性系统可接受行为的语言。传统上，通过演绎方法[MP95]或算法方法（模型检查[CGP99，QS82]），它已用于正式验证。在此框架中，所讨论的行为通常是离散的，即状态和/或事件的序列。近年来，几种趋势提出了使用TL的替代方法。
Temporal Logic (TL) is a popular formalism, introduced into systems design [Pnu77] as a language for specifying acceptable behaviors of reactive systems. Traditionally, it has been used for formal verification, either by deductive methods [MP95], or algorithmic methods (Model Checking [CGP99,QS82]). In this framework, the behaviors in question are typically discrete, that is, sequences of states and/or events. In recent years, several trends suggest alternative ways to use TL.