starMC: an automata based CTL* model checker

被引：0
作者：
Amparore E.G. [1 ]
Donatelli S. [1 ]
Gallà F. [1 ]
机构：
[1] Dipartimento di Informatica, Università degli Studi di Torino, Torino
来源：
PeerJ Computer Science | 2022年 / 8卷
关键词：
Buchi automata; Ctl; logic; Model-checking; Petri nets; System verification; Tools;
D O I：
10.7717/PEERJ-CS.823
中图分类号：
学科分类号：
摘要：
Model-checking of temporal logic formulae is a widely used technique for the verification of systems. CTL* is a temporal logic that allows to consider an intermix of both branching behaviours (like in CTL) and linear behaviours (LTL), overcoming the limitations of LTL (that cannot express “possibility”) and CTL (cannot fully express fairness). Nevertheless CTL* model-checkers are uncommon. This paper presents (1) the algorithms for a fully symbolic automata-based approach for CTL*, and (2) their implementation in the open-source tool starMC, a CTL* model checker for systems specified as Petri nets. Testing has been conducted on thousands of formulas over almost a hundred models. The experiments show that the fully symbolic automata-based approach of starMC can compute the set of states that satisfy a CTL* formula for very large models (non trivial formulas for state spaces larger than 10480 states are evaluated in less than a minute) © Copyright 2022 Amparore et al
引用
收藏
相关论文
共 59 条
  • [1] Aalst W., The application ofPetri nets to workflow management, Journal ofCircuits, Systems, and Computers, 8, pp. 21-66, (1998)
  • [2] Amparore E, Donatelli S., Efficient model checking of the stochastic logic CSLTA, Performance Evaluation, 123-124, pp. 1-34, (2018)
  • [3] Amparore EG., A new GreatSPN GUI for GSPN editing and CSLTA model checking, Proceeding ofthe 11th QEST Conference, 8657, pp. 170-173, (2014)
  • [4] Amparore EG, Balbo G, Beccuti M, Donatelli S, Franceschinis G., 30 Years of GreatSPN, Principles ofPerformance and Reliability Modeling and Evaluation: Essays in Honor ofKishor Trivedi, pp. 227-254, (2016)
  • [5] Amparore EG, Beccuti M, Donatelli S., (Stochastic) model checking in GreatSPN, 35th International Conference on Application and Theory ofPetri Nets and Concurrency, pp. 354-363, (2014)
  • [6] Amparore EG, Ciardo G, Donatelli S, Miner AS., i-Rank: a variable order metric for DEDS subject to linear invariants, 25th International Conference, TACAS 2019, pp. 285-302, (2019)
  • [7] Amparore EG, Donatelli S., GreatTeach: a tool for teaching (Stochastic) Petri Nets, 39th ATPN International Conference, pp. 416-425, (2018)
  • [8] Amparore EG, Donatelli S, Ciardo G., Variable order metrics for decision diagrams in system verification, International Journal on Software Toolsfor Technology Transfer, 22, 5, pp. 541-562, (2020)
  • [9] Amparore EG, Donatelli S, Galla F., A CTL* model checker for Petri nets, 41st International Conference on Application and Theory ofPetri Nets, PN2020, volume 12152 ofLecture Notes in Computer Science, pp. 403-413, (2020)
  • [10] Babar J, Miner A., Meddly: multi-terminal and edge-valued decision diagram library, Proceedings ofQEST Conference, pp. 195-196, (2010)
123456