Model checking LTL using net unforldings

被引：0
|
作者：
Wallner, F [1 ]
机构：
[1] Tech Univ Munich, Inst Informat, D-80290 Munich, Germany
来源：
COMPUTER AIDED VERIFICATION | 1998年 / 1427卷
关键词：
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
Net unfoldings are a well-studied partial order semantics for Petri nets. In this paper, we show that the finite prefix of an unfolding, introduced by McMillan, is suited for model checking linear-time temporal properties. The method is based on the so-called automata-theoretic approach to model checking. We propose a technique to treat this approach within the framework of safe Petri nets, and give an efficient algorithm for detecting the system runs violating a given specification.
引用
收藏
页码：207 / 218
页数：12
相关论文
共 50 条
  • [31] LTL model checking of self modifying code
    Touili, Tayssir
    Ye, Xin
    FORMAL METHODS IN SYSTEM DESIGN, 2022, 60 (02) : 195 - 227
  • [32] Program complexity of dynamic LTL model checking
    Kähler, D
    Wilke, T
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2003, 2803 : 271 - 284
  • [33] Yet another look at LTL model checking
    Schneider, K
    CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, 1999, 1703 : 321 - 325
  • [34] Truly on-the-fly LTL model checking
    Hammer, M
    Knapp, A
    Merz, S
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2005, 3440 : 191 - 205
  • [35] LTL Model Checking under Fairness in PROB
    Dobrikov, Ivaylo
    Leuschel, Michael
    Plagge, Daniel
    SOFTWARE ENGINEERING AND FORMAL METHODS: 14TH INTERNATIONAL CONFERENCE, SEFM 2016, 2016, 9763 : 204 - 211
  • [36] LTL Model-Checking for Malware Detection
    Song, Fu
    Touili, Tayssir
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 416 - 431
  • [37] Bounded LTL model checking with stable models
    Heljanko, K
    Niemelä, I
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2003, 3 : 519 - 550
  • [38] 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
  • [39] LTL Model Checking of Self Modifying Code
    Touili, Tayssir
    Ye, Xin
    2019 24TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2019), 2019, : 1 - 10
  • [40] Distributed LTL Model Checking with Hash Compaction
    Barnat, J.
    Havlicek, J.
    Rockai, P.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2013, 296 : 79 - 93
12345