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 条

[21] Is LTL model-checking effective for Diagnosability Verification?
Tuxi, Thiago M.
Carvalho, Lilian K.
Nunes, Eduardo V. L.
Da Cunha, Antonio E. C.
IFAC PAPERSONLINE, 2020, 53 (04): : 256 - 262
[22] LTL and LDL on Finite Traces: Reasoning, Verification, and Synthesis
De Giacomo, Giuseppe
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (218):
[23] Accelerated Runtime Verification of LTL Specifications with Counting Semantics
Medhat, Ramy
Bonakdarpour, Borzoo
Fischmeister, Sebastian
Joshi, Yogi
RUNTIME VERIFICATION, (RV 2016), 2016, 10012 : 251 - 267
[24] Decentralized Runtime Verification of LTL Specifications in Distributed Systems
Mostafa, Menna
Bonakdarpour, Borzoo
2015 IEEE 29TH INTERNATIONAL PARALLEL AND DISTRIBUTED PROCESSING SYMPOSIUM (IPDPS), 2015, : 494 - 503
[25] Formal Modeling and Verification of Cloud Elasticity with Maude and LTL
Khebbeb, Khaled
Hameurlain, Nabil
Belala, Faiza
NEW TRENDS IN MODEL AND DATA ENGINEERING, 2019, 1085 : 64 - 77
[26] RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification
Geske, Maren
Jasper, Marc
Steffen, Bernhard
Howar, Falk
Schordan, Markus
van de Pol, Jaco
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: DISCUSSION, DISSEMINATION, APPLICATIONS, ISOLA 2016, PT II, 2016, 9953 : 787 - 803
[27] Verification of automatically generated pattern-based LTL specifications
Salamah, Salamah
Gates, Ann Q.
Kreinovich, Vladik
Roach, Steve
HASE 2007: 10TH IEEE HIGH ASSURANCE SYSTEMS ENGINEERING SYMPOSIUM, PROCEEDINGS, 2007, : 341 - 348
[28] Past Time LTL Runtime Verification for Microcontroller Binary Code
Reinbacher, Thomas
Brauer, Joerg
Horauer, Martin
Steininger, Andreas
Kowalewski, Stefan
FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, 2011, 6959 : 37 - +
[29] LTL Verification of Online Executions with Sensing in Bounded Situation Calculus
De Giacomo, Giuseppe
Lesperance, Yves
Patrizi, Fabio
Vassos, Stavros
21ST EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE (ECAI 2014), 2014, 263 : 369 - +
[30] Construction and Verification of PLC-Programs by LTL-Specification
Kuzmin, E. V.
Sokolov, V. A.
Ryabukhin, D. A.
AUTOMATIC CONTROL AND COMPUTER SCIENCES, 2015, 49 (07) : 453 - 465

← 1 2 3 4 5 →