Evrostos: the rLTL verifier
Evrostos: the rLTL verifier
复制标题
Evrostos：rLTL 验证器
DOI：
10.1145/3302504.3311812
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Tabuada, Paulo
中科院分区：
文献类型：
--
作者：
Anevlavis, Tzanis;Neider, Daniel;Phillipe, Matthew;Tabuada, Paulo
健壮性线性时态逻辑(RLTL)是为了将健壮性的概念融入到线性时间时态逻辑(LTL)规范中而设计的。从技术上讲，健壮性是通过5个不同的真值在逻辑rLTL中形式化的，这导致了相关模型检测问题的时间复杂性的增加。一般而言，rLTL公式的模型检验依赖于构造一个大小为5|φ|的广义Büchi自动机，其中|φ|表示rLTL公式φ的长度。最近的研究表明，当要进行模型检验的公式来自rLTL的片段时，该自动机的大小可以减少到3|φ|(甚至更小)。在本文中，我们介绍了这段代码中的第一个模型检查公式工具Evrostos。我们还基于文献中报道的模型和LTL公式进行了几项实证研究，证实了对上述片段的rLTL模型检查会产生时间开销，从而使rLTL的验证切实可行。
Robust Linear Temporal Logic (rLTL) was crafted to incorporate the notion of robustness into Linear-time Temporal Logic (LTL) specifications. Technically, robustness was formalized in the logic rLTL via 5 different truth values and it led to an increase in the time complexity of the associated model checking problem. In general, model checking an rLTL formula relies on constructing a generalized Büchi automaton of size 5 | φ | where | φ | denotes the length of an rLTL formula φ. It was recently shown that the size of this automaton can be reduced to 3 | φ | (and even smaller) when the formulas to be model checked come from a fragment of rLTL. In this paper, we introduceEvrostos,the first tool for model checking formulas in this fragment. We also present several empirical studies, based on models and LTL formulas reported in the literature, confirming that rLTL model checking for the aforementioned fragment incurs in a time overhead that makes the verification of rLTL practical.
登录
查看更多内容
稳健的 omega-regular 软件综合理论
DOI：
10.1145/2539036.2539044
发表时间：
2013
期刊：
ACM Trans. Embed. Comput. Syst.
影响因子：
--
作者：
R. Majumdar;Elaine Render;P. Tabuada
通讯作者：
P. Tabuada
对未建模的间歇性干扰具有鲁棒性的安全控制器的综合
DOI：
10.1109/cdc.2016.7799416
发表时间：
2016
期刊：
2016 IEEE 55th Conference on Decision and Control (CDC)
影响因子：
--
作者：
E. Dallal;D. Neider;P. Tabuada
通讯作者：
P. Tabuada
自动空中交通管制系统协调协议的正式规范和验证
DOI：
10.1016/j.scico.2014.04.002
发表时间：
2012
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
Yang Zhao;Kristin Yvonne Rozier
通讯作者：
Kristin Yvonne Rozier
验证 rLTL 公式：现在比以往更快！
DOI：
10.1109/cdc.2018.8619014
发表时间：
2018
期刊：
2018 IEEE Conference on Decision and Control (CDC
影响因子：
--
作者：
Anevlavis, Tzanis;Philippe, Matthew;Neider, Daniel;Tabuada, Paulo
通讯作者：
Tabuada, Paulo
DOI：
10.1243/09544100jaero546
发表时间：
2010-01-01
影响因子：
1.1
作者：
Erzberger, H.;Heere, K.
通讯作者：
Heere, K.