Un implementazione basata su automi di un model checker CTL* simbolico

This dissertation presents the implementation of a symbolic CTL* model checking algorithm based on multi-valued decision diagrams (MDDs). Model checkers are programs whose task is to determine whether a given finite-state model satisfies a set of specifications which describe its behavior. This is often referred to as the verification problem. The models we are considering are all classes of Petri nets supported by the GreatSPN editor. Specifications are provided using temporal logics: modal logics which are able to represent propositions qualified in terms of time. Many temporal logics exist, most of which give an interpretation of time which is different from the others. Possibly the most successful temporal logic in terms of adoption is Linear Temporal Logic (LTL), which describes time as a linear infinite path through program states with only one possible future. Conversely, Computational Tree Logic (CTL) describes time as a branching tree of program states, in which various possible futures are considered. CTL and LTL are not comparable in term of expressiveness. This means that not every proposition which can be expressed in LTL can be expressed in CTL and vice-versa. This difference is rooted in their semantics: CTL semantics is defined over sets of states, while LTL semantics is defined over infinite paths through states. Nevertheless, both logics are fragments of the branching temporal logic CTL*, which describes time as a tree of linear paths through program states. In terms of time complexity, CTL* model checking can be polynomially reduced to LTL model checking. Indeed the CTL* model checking algorithm applies LTL model checking over every branch of the tree of executions. Given these premises, we chose to explore the efficiency and usefulness of a CTL* model checker. At its core lies a LTL model checker based on automata over infinite words. Given a Petri net model and a CTL* proposition, our algorithm of identifying LTL subformulas, translate them to Büchi automata and compute the synchronous product of each LTL formula with the model. MDDs are used to encode the Petri net and such composition. With respect to explicit model checking tecniques, MDDs lower both system memory and time required to manipulate the graph of reachable system states. The sets of satisfying states for each LTL subformula are then combined according to the temporal quantifiers preceding them. Thus the algorithm is capable of producing the boolean satisfaction result of the CTL* formula. Timed test runs executed againts a large set of models and specifications of LTL, CTL and CTL* temporal logics show competitive performance results with respect to other tools which process CTL* by translating each formula to mu-calculus. This algorithm has been implemented as one of the free and open source programs composing the GreatSPN framework for formal verification of systems.