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 条
  • [1] LTL model checking probabilistic Petri net system
    Liu, Yang
    Miao, Huaikou
    International Journal of Advancements in Computing Technology, 2012, 4 (01) : 172 - 178
  • [2] Model checking LTL using constraint programming
    Esparza, J
    Melzer, S
    APPLICATION AND THEORY OF PETRI NETS 1997, 1997, 1248 : 1 - 20
  • [3] Diagnosability verification using LTL model checking
    Thiago M. Tuxi
    Lilian K. Carvalho
    Eduardo V. L. Nunes
    Antonio E. C. da Cunha
    Discrete Event Dynamic Systems, 2022, 32 : 399 - 433
  • [4] Diagnosability verification using LTL model checking
    Tuxi, Thiago M.
    Carvalho, Lilian K.
    Nunes, Eduardo V. L.
    da Cunha, Antonio E. C.
    DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2022, 32 (03): : 399 - 433
  • [5] LTL model checking for statecharts
    Qian, Junyan
    Xu, Baowen
    Journal of Computational Information Systems, 2007, 3 (06): : 2241 - 2248
  • [6] First-order LTL model checking using MDGs
    Wang, F
    Tahar, S
    Mohamed, OA
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2004, 3299 : 441 - 455
  • [7] Bringing LTL Model Checking to Biologists
    Ahmed, Zara
    Benque, David
    Berezin, Sergey
    Dahl, Anna Caroline E.
    Fisher, Jasmin
    Hall, Benjamin A.
    Ishtiaq, Samin
    Nanavati, Jay
    Piterman, Nir
    Riechert, Maik
    Skoblov, Nikita
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2017, 2017, 10145 : 1 - 13
  • [8] Simple bounded LTL model checking
    Latvala, T
    Biere, A
    Heljanko, K
    Junttila, T
    FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS, 2004, 3312 : 186 - 200
  • [9] Another look at LTL model checking
    Clarke, EM
    Grumberg, O
    Hamaguchi, K
    FORMAL METHODS IN SYSTEM DESIGN, 1997, 10 (01) : 47 - 71
  • [10] A Circuit Approach to LTL Model Checking
    Claessen, Koen
    Een, Niklas
    Sterin, Baruch
    2013 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD), 2013, : 53 - 60
12345