Liveness characterization for GFC systems (Ⅱ)

被引:0
作者
曹存
机构
[1] China
[2] Institute of Computing Technology
[3] Beijing 100080
[4] Chinese Academy of Sciences
关键词
free-choice net; liveness; generalized free-choice net;
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Several liveness theorems for GFC (the generalized free choice) systems in a reductive approach are presented.What is interesting is that the characterization is just based on deadlocks,rather than on both deadlocks and traps as Commoner characterizes the liveness of ordinary free-choice systems.Several proof techniques which may be useful for proving liveness of other types of net systems are also introduced.
引用
收藏
页码:206 / 216
页数:11
相关论文
共 50 条
  • [21] From liveness to promptness
    Kupferman, Orna
    Piterman, Nir
    Vardi, Moshe Y.
    FORMAL METHODS IN SYSTEM DESIGN, 2009, 34 (02) : 83 - 103
  • [22] Declarative Choreographies and Liveness
    Hildebrandt, Thomas T.
    Slaats, Tijs
    Lopez, Hugo A.
    Debois, Soren
    Carbone, Marco
    FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS (FORTE 2019), 2019, 11535 : 129 - 147
  • [23] From liveness to promptness
    Orna Kupferman
    Nir Piterman
    Moshe Y. Vardi
    Formal Methods in System Design, 2009, 34 : 83 - 103
  • [24] Enhancing discovery with liveness
    Bodlaender, M
    Guidi, J
    Heerink, L
    CCNC 2004: 1ST IEEE CONSUMER COMMUNICATIONS AND NETWORKING CONFERENCE, PROCEEDINGS: CONSUMER NETWORKING: CLOSING THE DIGITAL DIVIDE, 2004, : 636 - 638
  • [25] Liveness and boundedness preservations of sharing synthesis of Petri net based representation for embedded systems
    Xia, Chuanliang
    Shen, Bin
    Zhang, Hailin
    Wang, Yigui
    COMPUTER SYSTEMS SCIENCE AND ENGINEERING, 2018, 33 (05): : 345 - 350
  • [26] Liveness-enforcing supervision for resource allocation systems with uncontrollable behavior and forbidden states
    Park, J
    Reveliotis, SA
    IEEE TRANSACTIONS ON ROBOTICS AND AUTOMATION, 2002, 18 (02): : 234 - 240
  • [27] Liveness enforcing supervision for sequential resource allocation systems - State of the art and open issues
    Reveliotis, SA
    SYNTHESIS AND CONTROL OF DISCRETE EVENT SYSTEMS, 2002, : 203 - 212
  • [28] Verifying Liveness for Asynchronous Programs
    Ganty, Pierre
    Majumdar, Rupak
    Rybalchenko, Andrey
    ACM SIGPLAN NOTICES, 2009, 44 (01) : 102 - 113
  • [29] Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols
    Mery, Dominique
    Poppleton, Michael
    SOFTWARE AND SYSTEMS MODELING, 2017, 16 (04) : 1083 - 1115
  • [30] Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols
    Dominique Méry
    Michael Poppleton
    Software & Systems Modeling, 2017, 16 : 1083 - 1115