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 条
  • [41] Efficient model checking for LTL with partial order snapshots
    Niebert, Peter
    Peled, Doron
    THEORETICAL COMPUTER SCIENCE, 2009, 410 (42) : 4180 - 4189
  • [42] An Efficient Algorithm for Transforming LTL Formula to Buchi Automaton
    He, Anping
    Wu, Jinzhao
    Li, Lian
    INTERNATIONAL CONFERENCE ON INTELLIGENT COMPUTATION TECHNOLOGY AND AUTOMATION, VOL 1, PROCEEDINGS, 2008, : 1215 - +
  • [43] Efficient model checking for LTL with partial order snapshots
    Niebert, P
    Peled, D
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2006, 3920 : 272 - 286
  • [44] Efficient approach of translating LTL formulae into Buchi automata
    Shan, Laixiang
    Du, Xiaomin
    Qin, Zheng
    FRONTIERS OF COMPUTER SCIENCE, 2015, 9 (04) : 511 - 523
  • [45] Clustering objects on subsets of attributes - Discussion
    Hand, DJ
    Glasbey, C
    Husmeier, D
    Gower, JC
    van Houwelingen, HC
    Bugrien, JB
    Nason, G
    Critchley, F
    Hoff, PD
    McLachlan, GJ
    Bean, RW
    JOURNAL OF THE ROYAL STATISTICAL SOCIETY SERIES B-STATISTICAL METHODOLOGY, 2004, 66 : 839 - 849
  • [46] Regulation of T lymphocyte subsets - Discussion
    Dutton, RW
    Sher, A
    Mosmann, TR
    Romagnani, S
    Trinchieri, G
    Flavell, R
    Fitch, FW
    Mitchison, NA
    Locksley, RM
    Allen, PM
    Mason, DW
    Abbas, AK
    Swain, SL
    T CELL SUBSETS IN INFECTIOUS AND AUTOIMMUNE DISEASES, 1995, 195 : 80 - 85
  • [47] Runtime verification using the temporal description logic ALC-LTL revisited
    Baader, Franz
    Lippmann, Marcel
    JOURNAL OF APPLIED LOGIC, 2014, 12 (04) : 584 - 613
  • [48] Business Process Verification and Restructuring LTL Formula Based on Machine Learning Approach
    Horita, Hiroki
    Hirayama, Hideaki
    Hayase, Takeo
    Tahara, Yasuyuki
    Ohsuga, Akihiko
    COMPUTER AND INFORMATION SCIENCE, 2016, 656 : 89 - 102
  • [49] Multi-core Model Checking Algorithms for LTL Verification with Fairness Assumptions
    Ha, Xuan-Linh
    Quan, Thanh-Tho
    Liu, Yang
    Sun, Jun
    2013 20TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2013), VOL 1, 2013, : 547 - 552
  • [50] Memory-Efficient Tactics for Randomized LTL Model Checking
    Larsen, Kim
    Peled, Doron
    Sedwards, Sean
    VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS (VSTTE 2017), 2017, 10712 : 152 - 169
12345