key: cord-0046604-kwlz1nw5 authors: Amparore, Elvio Gilberto; Donatelli, Susanna; Gallà, Francesco title: A CTL* Model Checker for Petri Nets date: 2020-06-02 journal: Application and Theory of Petri Nets and Concurrency DOI: 10.1007/978-3-030-51831-8_21 sha: 798c9d8c623e3dd33c7ac97edd26d39786ec3f59 doc_id: 46604 cord_uid: kwlz1nw5 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üchi 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 [Formula: see text]-calculus model checker of LTSmin for proper CTL* formulae (using a translator from CTL* to [Formula: see text]-calculus available in LTSmin). As far as we know, RGMEDD* is the only available Büchi-based CTL* model checker. In recent years, the model checking of CTL [10] and LTL [22] temporal logics for (colored) Petri nets (PN) has seen a boost in interest, and several tools and methods have been developed. Efficiency has been a main driving force behind this effort, also motivated by the lively Model Checking Competition (MCC) [19] . MCC models, formulae, and their evaluations are publicly available, making MCC data a very valuable benchmark for (Petri net) tools. The MCC includes LTL and CTL properties, but does not consider CTL* [15] ones. CTL* is a temporal logic strictly more expressive than CTL and LTL. Although various theoretical aspects of CTL* model checking have been extensively studied in the past, very few CTL* model checkers exist, despite the fact that CTL* properties are of practical interests, for example for modelling fairness constraints for CTL properties. It is well known that various forms of fairness constraints are directly expressible in LTL, while this is not the case for CTL. Algorithms for CTL* model checking can either be based on Büchi automata, as illustrated in [6] (page 429), or they can rely on the translation from CTL* into μ-calculus [20] , as done in the work of Dam [11, 12] , using the standard fixed point iteration of μ-calculus to compute the sat-set. RGMEDD*, the CTL* model checker described in this paper, computes the sat-sets using a Büchi-based model checking algorithm. Given a CTL* formula, the algorithm identifies the LTL sub-formulae of maximal length and uses Spot [14] to translate each of them into a Büchi automaton. States are encoded as Decision Diagrams (DD), using the Meddly [5] library. RGMEDD* can be run as a stand-alone tool or as part of the GreatSPN [2] tool suite, called from a "check property" window of the GreatSPN graphical interface [1] . We could only find another Petri net tool that can deal directly with CTL*: LTSmin [18] . This tool translates CTL* into μ-calculus, using the procedures defined in [11, 12] ). Note that μ-calculus for Petri nets is available also in TINA [7] , but no translator from CTL* to μ-calculus is provided. We could not find any CTL* tool based on Büchi automata. the set of available tools does not change even when looking to model checkers with input languages other than Petri Nets. There are papers on CTL* for Spin [17, 25] , but we could not find any implementation available. There is an implementation of μ-calculus for nuXmv [8] , which could lead to a CTL* model checker but, for the time being, only CTL* formulae that are either LTL or CTL are actually processed. Validation of RGMEDD* has been achieved taking advantage of the MCC2018 models, LTL and CTL formulae, and associated truth values for the models' initial state. Computations of the sat-sets of CTL* formulae have been checked in two ways: sat-sets of formulae that are plain CTL have been compared with the sat-set computed by RGMEDD3, the existing CTL model checker of GreatSPN, and LTSmin, while for CTL*-only formulae the comparison has been conducted against LTSmin, using its CTL* module. We undertook the construction of a CTL* model checker to use it: 1) to test the efficiency of a DD-based implementation of LTL and CTL*; 2) to explore whether a Büchi automata approach can favour the formulation of counterexamples and witnesses; 3) to investigate the efficacy for CTL* of the variable ordering techniques developed in [3] ; and 4) to support teaching: following the effort in [4] the users of GreatSPN to experiment (within the same window of the GUI) formulae of multiple logics: LTL, (fair )CTL and CTL*. The paper is organized as follows: Sect. 2 introduces basic definitions, Sect. 3 reviews the algorithm for CTL* model checking, the symbolic data structures used to implement it, the tool architecture and the integration into the Great-SPN graphical interface. Section 4 describes the testing performed, while Sect. 5 concludes the paper. where Q is a finite set of locations, Σ is a set of atomic proposition labels, δ : Q × Σ → 2 Q is a total transition function, q 0 ⊆ Q is the set of initial locations, and F is a subset of 2 Q and each element of F is called an acceptance set. Every LTL formula φ can be translated into an equivalent GBA [23] . The details of this translation are outside the scope of this paper. Figure 1 (B) shows a GBA with 3 locations and a single atomic proposition #P 2=1, corresponding to a boolean formula on M . Location 1 is q 0 , and F = {0} . CTL*. The language of CTL* formulae of RGMEDD* is inductively defined by: ≤} is a comparison operator, and • ∈ {+, −, * , /} is an arithmetic operator. The rules Ψ , φ and Θ are the rules for the state, path and integer formulae, respectively. The state formula dead is a special label for all RS states that do not enable any transition; en(τ ) is satisfied in all RS states enabling at least one transition t ∈ τ ; #p evaluates to the cardinality of place p in the current marking; bounds(π) is the maximum sum of token counts of all places in π in every reachable marking. A CTL* formula with no quantifiers but the initial one is an LTL formula. Product RS ⊗ A. Model checking of properties expressed using Büchi automata follows the schema of [24] . A Transition System (TS) is generated from the cross product RS ⊗ A between a path-formula GBA A and the RS of M . States of this TS are pairs m, q , with m a Petri net marking and q a GBA location. Decision Diagrams (DD) are a data structure used to encode large sets of structured data. GreatSPN uses the DD library Meddly [5] , which Algorithm 1. Sat-set generation of a maximal proper state subformula φ. case StrongBüchi: 7: case TerminalBüchi: 11: return Sat(φ) 14: end procedure supports, among others, binary (BDD) and multivalued (MDD) DDs. We shall use MDD to encode both the RS of the Petri net, and the TS of the product RS ⊗ A. MDDs encoding a relation function are called MxD, and are used by the tool to represent transitions and their union as a transition relation. An MxD has twice the levels of an MDD, and in each pair of levels it encodes the before/after relations of a variable (i.e. a place or a location). Figure 1 (C) and (D) shows the RS and the transition relation of M encoded as a MDD and as a MxD, respectively. A reachable state corresponds to a path in the MDD of (C): so, taking the rightmost path, we have that (1, 0, 0) is a reachable state. The MDD are fully-reduce, so the leftmost path encodes both (0, 0, 0) and (0, 0, 1). Given a Petri net model M and a CTL* formula ψ, the solver first descends recursively through the syntax tree of ψ to extract each maximal proper state subformula [6, pp. 427 ], and then model checks each maximal proper state subformula ψ independently, in a bottom up process. Let ψ be a maximal proper state subformula where all inner maximal proper state subformulae have been replaced with atomic propositions. For example if a and b are atomic propositions, then ∃XX(∀ aUFb) has two maximal subformulas: ∀ aUFb and ∃XXc, where c is the atomic proposition that stands for the sat-set of ∀ aUFb. If ψ only contain logical operations, it is trivially checked by applying the corresponding logical functions. Therefore, it remains to treat only the quantified cases ψ = ∃φ and ψ = ∀φ. For the first case the model checker implements a single function to compute the set of states of M satisfying φ, denoted Sat∃LTL(M, φ). The method Sat∃LTL(M, φ) identifies the set of all markings m that have at least one path starting in m satisfying φ, which gives the semantics for the CTL* expression ∃φ. The CTL* expression ∀φ, corresponding to the more usual LTL semantics, is obtained from ∀φ = ¬(∃¬φ), which is computed as Sat(∀φ) = RS \ Sat∃LTL(M, ¬φ). A pseudo-code of the Sat∃LTL(M, φ) function is given in Algorithm 1. The function first translates the path formula φ into a GBA A using Spot (line 2). It then encodes (line 3) the transition system RS ⊗ A: each TS state m, q , is encoded in a MDD with |P | + 1 levels. The set of reachable states in RS ⊗ A is generated using saturation [9] (line 4). An infinite path meets the state-based acceptance condition of a GBA if it visits infinitely often at least one state in each acceptance set F ∈ F. The work in [16] shows that the set of states originating accepting paths can be computed by the fair CTL formula E fair G(true, F) on the TS. For some subclasses of GBAs (weak and terminal), a simplified procedure (lines 5-11) can be used [26] . The final set Sat(φ) is obtained by taking all the fair states (i.e. those that satisfy the acceptance condition of the GBA) that are also initial states of the RS (line 12). Most of the complexity resides in the generation of RS ⊗ A with Decision Diagrams, summarized in Algorithm 2. Its generation requires both the MDD of the RS and the MxD of the transition relation, referred to as the Next-State-Function [9] (NSF ) of the Petri net model. Each edge q s − → q of A is encoded as a new MxD (line 5), by modifying the transition relation of the Petri net to reach only Sat(s) markings, and at the same time by moving the GBA location from q to q . To ensure that the generated transition system is a proper Kripke structure, all deadlock states of the Petri net model must be closed by a selfloop, which is built separately for each edge (lines 6-7). The transition relation NSF T S of the TS is created from the union of all the edge's MxD (line 8). The function relabel(d, q) takes a MDD d and sets the location level to q, while the loc change(x, q, q ) takes a MxD x and replaces for the location level the relation Algorithm 2. Encoding of the RS ⊗ A transition system. b ← Sat(s) ∩ deadlock Self loops 7: if q ∈ Q0 then 10: Tool. The CTL* model checker is available both as a command line tool and inside the integrated GUI. Figure 2 shows the interface. For each model, a list of queries can be inserted, following the grammar given in Sect. 2. Queries are declared as either CTL or CTL*, which changes the model checking algorithm used. The algorithm described in Sect. 3 is used for CTL* queries only. We have tested different aspects of RGMEDD*: the correctness of the results and the performance of the tool. MCC2018 models and relative model instances and formulae were used. We have considered only instances for which GreatSPN is able to build the RS, since the RS is required for sat-set computation. The reported tests are the final ones, but the MCC instances have been extensively used also during the debugging phase allowing to discover both technical errors (in the implementation of the algorithm) and semantics ones (different behaviour for systems with deadlocks). Indeed Petri net models with deadlocks do not feature only infinite paths, as per the semantics of LTL and CTL. A standard way to turn around this problem is to "stutter" deadlock states by adding a self-loop. MCC assumes that deadlock states are stuttered only for LTL model checking, since this is required by the Büchi-based construction. RGMEDD* assumes deadlocks are stuttered, which may cause discrepancies when comparing RGMEDD* on CTL formulae. Therefore the MCC instances considered have been split in two sets: deadlock-free models (DFM), with 408 instances, and non deadlock-free models (DM), with 539 instances. This test is based on the MCC2018 results for four categories of queries: CTL-Cardinality, CTLFireability, LTLCardinality and LTLFireability. Each category has 16 queries. A pair model instance, category is called an examination. For each examination an expected result is provided, that was used to check the correctness of RGMEDD*. To limit resource consumption we set a time limit of 300s and a memory limit of 2GB. With these limitations we could complete 360 examinations, that is to say 5760 (=360 * 16) queries. For LTL categories we have used instances of both DFM and DF models, while for CTL only DFM ones have been used. Over all the 5760 tests performed we have got a single mismatch, but this is query for which there is a mismatch also among the three tools that were able to evaluate the query in MCC2018. GreatSPN has a CTL model checker called RGMEDD3 that recursively computes the sat-set of CTL formulae. With a timeout of 60 seconds and 2GB of memory, RGMEDD3 completes 3544 queries from 168 different model instances from the DF set. RGMEDD* timeout-out on 10.05% of the queries. RGMEDD3 was faster than RGMEDD* in 92.65% of all queries completed by both tools. Figure 3 (A) shows the execution times of the two tools, each query being a dot. In all completed tests the tools produce sat-sets of equal cardinality. Here we report the assessment of RGMEDD* against LTSmin, run using the pins2lts-sym interface with the -ctlstar option which first converts CTL* into μcalculus (which may incur an exponential cost). Also LTSmin is based on decision diagrams (of the Sylvan [13] library) and to make a more realistic comparison we have enforced the use of the same variable order by the two tools. Before checking CTL* formulae we have tested their behaviours on known results. We computed the sat-sets generated by RGMEDD* and pnml2lts-sym when provided with the same queries from the MCC examination of LTLCardinality and CTLCardinality (DF only models) set for which the RS can be built. With the same resource limits as before, of the 1248 formulae considered (covering instances from 32 different models), RGMEDD* completed 1162 and LTSmin 702. Among these 702 formulae successfully completed by both model checkers, there were 7, from different models, over which the two tools did not agree: For these formulae MCC states that they are true in the initial marking, RGMEDD* returns sat-sets that include the initial marking, while LTSmin returns empty sat-sets, which seems a wrong answer. 2. Relative performances of the two tools. We checked the time performance of the two tools on the same instances as above, excluding the time for RS computation. Figure 3 (B) shows the comparison. RGMEDD* performs better in average and a closer look at LTSmin times reveals that a significant amount of time is spent converting CTL* formulae to μ-calculus. 3. Correctness and performance on CTL* formulae. Since there is no available set of CTL* formulae for the MCC models (and for any other models we could find) we have generated formulae algorithmically by parsing CTLCardinality queries from MCC2018 and deleting each path quantifiers with a probability of 70%. The first quantifier is always kept, in order to preserve consistency with the CTL* grammar. For these tests, which are mainly aimed at checking correctness, we considered only 39 models whose RS are rather quick to generate. This gives a total of 624 queries, and on 218 both tools complete with the given resources. RGMEDD* timed out in 5.44% of the queries while LTSmin timed out in 65.06% of the queries. RGMEDD* was faster than LTSmin in 85.78% of all queries completed by both tools. More importantly the cardinality of the sat-sets coincides for both tools. RGMEDD* is the new CTL* model checker of GreatSPN. It leverages two libraries: Spot for the translation from CTL* to Büchi automata and Meddly for decision diagram manipulation. RGMEDD* allows GreatSPN users to compute the set of reachable states that satify CTL* and LTL properties. The approach is fully integrated into the GreatSPN GUI, that already included the possibility of computing the sat-set of CTL formulae. RGMEDD* itself can be used to check also CTL properties, although our testing has confirmed that, as expected, the standard CTL model checking algorithm has superior performances. Testing of RGMEDD* had to face a number of difficulties, due to the availability of a single CTL* tool, LTSmin. To be able to use LTSmin for our benchmark it was first necessary to fix a few syntactic problems in the LTSmin parsing of CTL* formulae: nevertheless it was an easy to use tool and we observed very limited discrepancies in the results. Although both tools are based on decision diagrams, RGMEDD* seems to perform significantly better than LTSmin, that suffers for the expensive translation from CTL* into μ-calculus. Based on the experience gained in building RGMEDD* we plan to develop a model checker for the fair variant of CTL (reusing the available implementation of the Emerson-Lei algorithm for E fair Gφ). We also plan to work on the generation of counterexamples and witnesses: these two topics are of paramount importance for the verification of distributed algorithms. Finally, we shall work on improving memory and time performance by avoiding, as much as possible, the construction of a single monolithic decision diagram for the next state function of the Petri Net and of the RS ⊗ A transition system. A virtual machine with the tool pre-installed can be downloaded from http://www.di.unito.it/ ∼ greatspn/VBox/RGMEDDstar-vm.ova. The source code of GreatSPN is available from https://github.com/greatspn/SOURCES. A new GreatSPN GUI for GSPN editing and CSL TA model checking Principles of Performance and Reliability Modeling and Evaluation. SSRE Rank : a variable order metric for DEDS subject to linear invariants GreatTeach: a tool for teaching (stochastic) petri nets Meddly: multi-terminal and edge-valued decision diagram library Principles of Model Checking The tool TINA -construction of abstract state spaces for Petri nets and time Petri nets The nuXmv symbolic model checker Saturation: an efficient iteration strategy for symbolic state-space generation Design and synthesis of synchronization skeletons using branching time temporal logic Translating CTL* into the modal μ-calculus CTL* and ECTL* as fragments of the modal μ-calculus Sylvan: multi-core framework for decision diagrams Spot 2.0-a framework for LTL and ω-automata manipulation Sometimes" and "not never" revisited: on branching versus linear time temporal logic Efficient model checking in fragments of the propositional mu-calculus The Spin Model Checker: Primer and Reference Manual LTSmin: high-performance language-independent model checking Presentation of the 9th edition of the model checking contest Results on the propositional μ-calculus Petri nets: properties, analysis and applications The temporal logic of programs An automata-theoretic approach to linear temporal logic Reasoning about infinite computations CTL* model checking for spin Abstraction Refinement for Large Scale Model Checking We would like to thank Jaco van de Pol for the various insights given on LTSmin, and Yann Thierry Mieg for the discussion on finite paths and model checking.