Discussion of LTL Subsets for Efficient Verification

被引：0

作者：

Shimakawa, Masaya ^{[1
]}

Iwasaki, Yuji ^{[1
]}

Hagihara, Shigeki ^{[1
]}

Yonezaki, Naoki ^{[2
]}

机构：

[1] Tokyo Inst Technol, Grad Sch Informat Sci & Engn, Dept Comp Sci, Tokyo, Japan

[2] Open Univ Japan, Chiba, Japan

来源：

THEORY AND PRACTICE OF COMPUTATION | 2018年

关键词：

Linear Temporal Logic; omega-automata; Specification; Verification;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The verification of reactive system specifications can detect dangerous situations that may arise that were not anticipated while drawing up the specifications. However, such verification typically involves complex, intricate analyses. The most effective approach for avoiding this difficulty is to restrict the syntax of the specification language. In this paper, we discuss subsets of linear temporal logic (used in the formal specification description of reactive systems) in which the syntax is restricted to simplify the verification procedure.

引用

下载

页码：14 / 27

页数：14

共 50 条

[1] Efficient Scalable Verification of LTL Specifications
Baresi, Luciano
Kallehbasti, Mohammad Mehdi Pourhashem
Rossi, Matteo
2015 IEEE/ACM 37TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, VOL 1, 2015, : 711 - 721
[2] More efficient on-the-fly LTL verification with Tarjan's algorithm
Geldenhuys, J
Valmari, A
THEORETICAL COMPUTER SCIENCE, 2005, 345 (01) : 60 - 82
[3] Bounded verification of past LTL
Cimatti, A
Roveri, M
Sheridan, D
FORMAL METHODS IN COMPUTER-AIDED DESIGN, 2004, 3312 : 245 - 259
[4] Bounded verification of past LTL
Cimatti, A
Roveri, M
Sheridan, D
FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS, 2004, 3312 : 245 - 259
[5] Runtime Verification for LTL and TLTL
Bauer, Andreas
Leucker, Martin
Schallhart, Christian
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2011, 20 (04)
[6] Tarjan's algorithm makes on-the-fly LTL verification more efficient
Geldenhuys, J
Valmari, A
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2004, 2988 : 205 - 219
[7] Comparing LTL Semantics for Runtime Verification
Bauer, Andreas
Leucker, Martin
Schallhart, Christian
JOURNAL OF LOGIC AND COMPUTATION, 2010, 20 (03) : 651 - 674
[8] Verification of LTL on B event systems
Groslambert, Julien
B 2007: Formal Specification and Development in B, Proceedings, 2007, 4355 : 109 - 124
[9] Sampling polynomial trajectories for LTL verification
Selvaratnam, Daniel
Cantoni, Michael
Davoren, J. M.
Shames, Iman
THEORETICAL COMPUTER SCIENCE, 2022, 897 : 135 - 163
[10] Formal verification of LTL formulas for systemc designs
Grosse, D
Drechsler, R
PROCEEDINGS OF THE 2003 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS, VOL V: BIO-MEDICAL CIRCUITS & SYSTEMS, VLSI SYSTEMS & APPLICATIONS, NEURAL NETWORKS & SYSTEMS, 2003, : 245 - 248

← 1 2 3 4 5 →