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 条
  • [21] Bounded model checking for past LTL
    Benedetti, M
    Cimatti, A
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2003, 2619 : 18 - 33
  • [22] MODEL CHECKING USING NET UNFOLDINGS
    ESPARZA, J
    SCIENCE OF COMPUTER PROGRAMMING, 1994, 23 (2-3) : 151 - 195
  • [23] Diagnosability Verification with Parallel LTL-X Model Checking Based on Petri Net Unfoldings
    Madalinski, Agnes
    Khomenko, Victor
    2010 CONFERENCE ON CONTROL AND FAULT-TOLERANT SYSTEMS (SYSTOL'10), 2010, : 398 - 403
  • [24] Measuring Progress of Probabilistic LTL Model Checking
    Cormie-Bowins, Elise
    van Breugel, Franck
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (85): : 33 - 47
  • [25] LTL model checking for modular Petri nets
    Latvala, T
    Mäkelä, M
    APPLICATIONS AND THEORY OF PETRI NETS 2004, PROCEEDINGS, 2004, 3099 : 298 - 311
  • [26] Tuning SAT solvers for LTL Model Checking
    Kheireddine, Anissa
    Renault, Etienne
    Baarir, Souheib
    2022 29TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, APSEC, 2022, : 259 - 268
  • [27] LTL Model Checking of Interval Markov Chains
    Benedikt, Michael
    Lenhardt, Rastislav
    Worrell, James
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 32 - 46
  • [28] LTL model checking for communicating concurrent programs
    Adrien Pommellet
    Tayssir Touili
    Innovations in Systems and Software Engineering, 2020, 16 : 161 - 179
  • [29] LINEAR ENCODINGS OF BOUNDED LTL MODEL CHECKING
    Biere, Armin
    Heljanko, Keijo
    Junttila, Tommi
    Latvala, Timo
    Schuppan, Viktor
    LOGICAL METHODS IN COMPUTER SCIENCE, 2006, 2 (05)
  • [30] Scalable shared memory LTL model checking
    Barnat J.
    Brim L.
    Ročkai P.
    International Journal on Software Tools for Technology Transfer, 2010, 12 (02) : 139 - 153
12345