A Simplified and Stubborn Approach to CTL Model Checking of Petri Nets
Authors
Johannsen, Mads ; Dyhr, Jakob ; Bønneland, Frederik Meyer
Term
4. term
Education
Publication year
2017
Submitted on
2017-06-02
Pages
60
Abstract
Tilstandsrumsanalyse af distribuerede systemer lider ofte under en eksplosiv vækst i antal tilstande, særligt ved modeltjek af Petri-net ud fra specifikationer i CTL. Denne afhandling præsenterer en samlet, praktisk tilgang, der kombinerer en LTS-baseret fortolkning af stubborn sets (kaldet stædig reduktion), en heltalslineær programmeringsbaseret (ILP) fortolkning af siphon-trap-egenskaben, samt en formelforenklingsteknik for at skære trivielle dele af forespørgsler væk. Stædig reduktion defineres abstrakt på Labelled Transition Systems, anvendes på Petri-net med inhibitorbuer og udvides til at bevare nåbarhed, ildbarhed, kardinalitet og deadlock-egenskaber. Kernen er at udlede en interessant mængde af overgange for en given formel og beregne en lukning med bevis for termination og korrekthed. Siphon-trap-egenskaben karakteriseres som et ILP-problem (med en dybdoparameter), hvilket kan bruges til at konkludere dødlåsfrihed. Formelforenkling bygger på state equations og ILP til at identificere underformler, der er trivielt sande eller falske, og er udvidet med CTL-operatorer; teknikken kan også afsløre uinteressante eller fejlbehæftede specifikationer. Alle metoder er implementeret i den åbne TAPAAL-værktøjskæde og evalueret op mod LoLA. Eksperimenterne viser, at kombinationen af strukturel reduktion og stædig reduktion ofte giver markante forbedringer, men kan konflikte på visse modeller; at ILP-fortolkningen af siphon-trap viser potentiale for at analysere dødlåsfrihed, men i vores implementering er langsommere end LoLAs SAT-baserede tilgang; samt at formelforenkling ofte reducerer forespørgsler til trivielle spørgsmål og forbedrer reduktionernes effekt, om end der opstod problemer for ildbarhedsformler. Samlet set gav TAPAAL flere eksklusive svar og lavere hukommelsesforbrug, mens LoLA generelt var hurtigere og undersøgte færre tilstande; desuden genererer mange realistiske modeller fortsat meget store tilstandsmængder.
State-space analysis of distributed systems often suffers from state explosion, especially when model checking Petri nets against CTL specifications. This thesis proposes a practical, combined approach that integrates an LTS-based interpretation of stubborn sets (called stubborn reduction), an integer linear programming (ILP) interpretation of the siphon-trap property, and a formula simplification technique that removes trivially verifiable parts of queries. Stubborn reduction is defined abstractly on Labelled Transition Systems, applied to Petri nets with inhibitor arcs, and extended to preserve reachability, fireability, cardinality, and deadlock properties. The key idea is to compute an interesting set of transitions for a given formula and then a closure with proven termination and correctness. The siphon-trap property is characterized as an ILP problem (with a depth parameter), enabling conclusions about deadlock freedom. Formula simplification builds on state equations and ILP to detect subformulae that are trivially true or false and is extended with CTL operators; it can also flag uninformative or faulty specifications. All techniques are implemented in the open-source TAPAAL toolchain and benchmarked against LoLA. Experiments indicate that combining structural and stubborn reductions generally yields considerable speed and memory benefits but can conflict on some models; that the ILP-based siphon-trap test shows promise for deadlock analysis yet performs worse than LoLA’s SAT-based implementation; and that simplification often reduces formulas to trivial questions and strengthens reductions, though issues were found for fireability formulas. Overall, TAPAAL produced more exclusive answers with lower memory use, while LoLA was typically faster and explored fewer states; many real-world models still generate very large state spaces.
[This summary has been generated with the help of AI directly from the project (PDF)]
Documents