StarMC: an automata based CTL* model checker.

ABSTRACT: 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 o

SUBMITTER: Amparore EG 

PROVIDER: S-EPMC9044404 | biostudies-literature | 2022

REPOSITORIES: biostudies-literature