Timed Automata (TA) are a very popular modeling formalism for systems with time-sensitive properties. A common task is to verify if a network of TA satisfies a given property, usually expressed in Linear Temporal Logic (LTL), or in a subset of Timed Computation Tree Logic (TCTL). In this paper, we build upon the TACK bounded model checker for TA, which supports a signal-based semantics of TA and the richer Metric Interval Temporal Logic (MITL). TACK encodes both the TA network and property into a variant of LTL, Constraint LTL over clocks (CLTLoc). The produced CLTLoc formula can then be solved by tools such as Zot, which transforms CLTLoc properties into the input logics of Satisfiability Modulo Theories (SMT) solvers. We present a novel method that preserves TACK's encoding of MITL properties while encoding the TA network directly into the SMT solver language, making use of both the BitVector logic and the logic of real arithmetics. We also introduce several optimizations that allow us to significantly outperform the CLTLoc encoding in many practical scenarios.
翻译:Timed Automata (TA) 是一个非常流行的具有时间敏感性特性的系统模式化模型。 一个共同的任务是验证TA网络是否满足了通常以线性时空逻辑(LTL)表达的某个属性,或者在时间计算树逻辑(TCTL)的一个子集中表达的某个属性。 在本文中,我们以TA的 TACK 捆绑模式检查器为基础,支持TA 和较富的Metric Interval Temallogic (MITL) 的基于信号的语义。 TACK 将 TA 网络和属性编码为时钟(CLTL) 的变体。 生成的 CLTLoc 公式可以通过Zot 等工具来解决, 将 CLTOLoc 属性转化为可满足 Medisficable Medlo Theories (SMTMT) 解算器的输入逻辑。 我们提出了一个新的方法, 保存TACK的数学编码, 同时将 TA 网络直接编码为 SMTTL 解算器的变体语言, 也让我们大量的BBIVLOCLT 的逻辑也允许许多实际的逻辑。