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 条
  • [31] Efficient Translation of LTL to Büchi Automata
    殷翀元
    罗贵明
    Tsinghua Science and Technology, 2009, 14 (01) : 75 - 82
  • [32] Efficient Realizability Checking by Modularization of LTL Specifications
    Ito, Sohei
    Osari, Kenji
    Shimakawa, Masaya
    Hagihara, Shigeki
    Yonezaki, Naoki
    COMPUTER JOURNAL, 2022, 65 (10): : 2801 - 2814
  • [33] Flash memory efficient LTL model checking
    Edelkamp, S.
    Sulewski, D.
    Barnat, J.
    Brim, L.
    Simecek, P.
    SCIENCE OF COMPUTER PROGRAMMING, 2011, 76 (02) : 136 - 157
  • [34] Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
    Brunner, Julian
    Lammich, Peter
    NASA FORMAL METHODS, NFM 2016, 2016, 9690 : 307 - 321
  • [35] First order Büchi automata and their application to verification of LTL specifications
    Zhang, Wenhui
    Journal of Logical and Algebraic Methods in Programming, 2025, 142
  • [36] Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
    Julian Brunner
    Peter Lammich
    Journal of Automated Reasoning, 2018, 60 : 3 - 21
  • [37] An extension of first-order LTL with rules with application to runtime verification
    Havelund, Klaus
    Peled, Doron
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2021, 23 (04) : 547 - 563
  • [38] An extension of first-order LTL with rules with application to runtime verification
    Klaus Havelund
    Doron Peled
    International Journal on Software Tools for Technology Transfer, 2021, 23 : 547 - 563
  • [39] Go2Pins: A Framework for the LTL Verification of Go Programs
    Kirszenberg, Alexandre
    Martin, Antoine
    Moreau, Hugo
    Renault, Etienne
    MODEL CHECKING SOFTWARE (SPIN 2021), 2021, 12864 : 140 - 156
  • [40] Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
    Brunner, Julian
    Lammich, Peter
    JOURNAL OF AUTOMATED REASONING, 2018, 60 (01) : 3 - 21
12345