A CTL* Model Checker for Petri Nets

被引：4
作者：
Amparore, Elvio Gilberto
Donatelli, Susanna
Galla, Francesco
机构：
来源：
APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY (PETRI NETS 2020) | 2020年 / 12152卷
关键词：
D O I：
10.1007/978-3-030-51831-8_21
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This tool paper describes RGMEDD*, a CTL* model checker that computes the set of states (sat-sets) of a Petri net that satisfy a CTL* formula. The tool can be used as a stand-alone program or from the GreatSPN graphical interface. The tool is based on the decision diagram library Meddly, it uses Spot to translate (sub)formulae into B <spacing diaeresis>uchi automata and a variation of the Emerson-Lei algorithm to compute the sat-sets. Correctness has been assessed based on the Model Checking Context 2018 results (for LTL and CTL queries), the sat-set computation of GreatSPN (for CTL) and LTSmin (for LTL), and the mu-calculus model checker of LTSmin for proper CTL* formulae (using a translator from CTL* to mu-calculus available in LTSmin). As far as we know, RGMEDD* is the only available Buchi-based CTL* model checker.
引用
收藏
页码：403 / 413
页数：11
相关论文
共 26 条
  • [1] Amparore Elvio Gilberto, 2018, Application and Theory of Petri Nets and Concurrency. 39th International Conference, PETRI NETS 2018. Proceedings: LNCS 10877, P416, DOI 10.1007/978-3-319-91268-4_24
  • [2] Presentation of the 9th Edition of the Model Checking Contest
    Amparore, Elvio
    Berthomieu, Bernard
    Ciardo, Gianfranco
    Dal Zilio, Silvano
    Galla, Francesco
    Hillah, Lom Messan
    Hulin-Hubard, Francis
    Jensen, Peter Gjol
    Jezequel, Loig
    Kordon, Fabrice
    Le Botlan, Didier
    Liebke, Torsten
    Meijer, Jeroen
    Miner, Andrew
    Paviot-Adet, Emmanuel
    Srba, Jiri
    Thierry-Mieg, Yann
    van Dijk, Tom
    Wolf, Karsten
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, 2019, 11429 : 50 - 68
  • [3] iRank: A Variable Order Metric for DEDS Subject to Linear Invariants
    Amparore, Elvio Gilberto
    Ciardo, Gianfranco
    Donatelli, Susanna
    Miner, Andrew
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, 2019, 11428 : 285 - 302
  • [4] Amparore EG, 2016, SPRINGER SER RELIAB, P227, DOI 10.1007/978-3-319-30599-8_9
  • [5] Amparore EG, 2014, LECT NOTES COMPUT SC, V8657, P170, DOI 10.1007/978-3-319-10696-0_13
  • [6] Babar Junaid, 2010, Proceedings of the 2010 Seventh International Conference on the Quantitative Evaluation of Systems (QEST 2010), P195, DOI 10.1109/QEST.2010.34
  • [7] Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1
  • [8] Berthomieu B, 2004, INT J PROD RES, V42, P2741, DOI 10.1080/00207540410001705257
  • [9] Cavada R, 2014, LECT NOTES COMPUT SC, V8559, P334, DOI 10.1007/978-3-319-08867-9_22
  • [10] Ciardo G., 2001, Tools and Algorithms for the Construction and Analysis of Systems. 7th International Conference, TACAS 2001. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001. Proceedings (Lecture Notes in Computer Science Vol.2031), P328
123