Stutter-invariant PPTL And Model Checking

This thesis introduces Stutter-invariant Propositional Projection Temporal Logic (PPTLst) and use the logic to verify unconditional communication protocols. The verifica-tion is based on model checking approach where PPTLst is employed as the specification language.Model checking of finite-state systems with specifications given as formulae of Proposi-tional Projection Temporal Logic (PPTL) was proposed in recent years. Since PPTL has the expressiveness ofω-regular so that it is more powerful than other linear-time propositional temporal logics, and projection together with chop operators in PPTL allows us to define more flexible properties, PPTL becomes a promising formalism for specification and verifi-cation of concurrent systems. However, like other formal verification methods, PPTL model checking suffers from state explosion. To combat state explosion problem, we define the stutter-invariant fragment of PPTL, written as PPTLst, and this fragment proves to capture all stutter-invariant properties expressible in PPTL. Specifications given by PPTLst formulas do not distinguish between the stutter-equivalent behaviors of a system. This allows partial order reduction to reduce state space since the verification is performed using representatives from the equivalent classes of behaviors. Furthermore, we implement a model checker to support verifying PPTLst specifications using partial-order reduction.Moreover, as a specification language, PPTLst can help designers get rid of irrelevant detail in compositional verification of a concurrent system. That is because the projection and chop constructs in PPTLst allows designers to assert properties over points of interest through an execution. In this way, modules can be abstracted based on their local properties by considering only relevant state-changes, importantly, because of stutter-invariance, substi-tution of modules by the abstracted ones will not affect overall properties of the system. Since the verification proceeds a hierarchy of levels of abstraction, the state space is also largely reduced.In addition to techniques for reducing the size of model or optimizing state space search, by our experiences, simple formulas for specifications can also bring low complexity of veri-fication. This encourages us to investigate the complexity of PPTLst and factors affecting the complexity, so we study the upper bound for complexity of PPTLst. To this end, a Complete Normal Graph (CNG) for PPTLst formulas is defined, and an algorithm translating formulas to CNG is formalized. With CNG the upper bound for complexity of PPTLst is proved to be non-elementary. Significantly, from the proof it is found that the complexity is affected only by the number of distinct atomic propositions and the depth of nested negation of chop (or projection) appearing in the formula. Therefore, specifications should be expressed by formu-las which hold small depth of nested negation of chop (or projection) and bounded number of atomic propositions.For developing a practice use of our approach, we investigates Russian Cards problem for the purpose of unconditional secured communication. The original protocol is confined to 3 players and 7 cards. We generalize the problem to tackle n players and n(n-1)+1 cards so that a safe public communication protocol can be established, namely Russian Cards protocol. Also, we give the safe communication condition, and formalize the algorithm for constructing safe communication sequence. Further, we verify the protocol by PPTLst based compositional method, and we check each module using PPTLst based partial-order reduction. The experimental results show integration of the two techniques can combat state explosion problem, and thus can be used for verification of large-scale concurrent system.