Symmetry And Action Refinement

For computer software and hardware systems containing many identical andisomorphic components, the models of such systems correspondingly exhibit agreat deal of symmetry in which the identical and isomorphic components havethe same and similar properties. For simplifying these systems, one develops sym-metry reduction algorithms to reduce their models. In particular, the symmetryreduction has been one of the e?ective techniques for combating state explosionproblem in formal veri?cation. However, most of work mainly exploits symmetryin labelled transition systems for model checking, almost no investigations no-tice symmetry in process algebra languages and other models. In this thesis, weinvestigate symmetry in process algebra languages and event structures in orderto construct a structural reduction system which is similar to from ?ne to coarsebehavioral equivalences for developing complex systems. On the other hand, themethodology of top-down stepwise re?nement is widely used to develop hardwareand software systems, and action re?nement is the core of this methodology. Thetheory of action re?nement has been investigated in process algebras and in eventstructure models. On the basis of these investigations, we investigate how thesymmetry reduction to a?ect action re?nement and discuss the preservation ofinterleaving and step equivalences under action re?nement.A process is de?ned as an algebraic structure. Having symmetry in a processstructure implies the existence of nontrivial permutation groups that preserveboth the identical or isomorphic process terms and all relations of sequentialcomposition and parallel composition that exist between process terms. Suchpermutation groups can be used to de?ne an equivalence relation on the set ofprocess terms of this process structure. The quotient process structure inducedby this equivalence relation is showed to be interleaving trace equivalent andinterleaving bisimulation equivalent to the original process structure. Then wedevelop the symmetry reduction algorithm for process algebra.A notion of symmetry for event structures is de?ned, which is based onpermutation groups. Given an event structure and a permutation group over it,we give the quotient model of the event structure and show that the quotientmodel is interleaving trace, interleaving bisimulation and pomset equivalent tothe original event structure. And we prove that interleaving trace, interleavingbisimulation and pomset trace equivalences between the quotient model and theoriginal event structure are preserved under action re?nement. Moreover, we de-velop the symmetry reduction algorithm for event structures. After investigatingthe symmetry, we compare the symmetry reduction with the autobisimualtionreduction.Interleaving equivalences, namely interleaving trace equivalence and inter-leaving bisimulation equivalence, and step equivalences, namely step trace equiv-alence and step bisimulation equivalence, are not preserved under action re?ne-ment. Generally, one investigates how to restrict the concept of action re?nementsuch that these equivalences are preserved under the restricted re?nement. Here,a class of systems with certain properties are found, which satisfy that theseestablished equivalences on them are preserved under no restricted re?nement.That is, the two interleaving equivalences and two step equivalences are showedthat they are preserved under re?nement in this kind of systems in which there arenot causal independence relations or all the transitions are bundle action transi-tions in a certain setting with concurrency. In order to facilitate the preservationquestion, we propose a new kind of transitions which are called bundle actiontransitions which is used to improve the partial order reduction.State space explosion problem is a fundamental obstacle in model checkingfor formal veri?cation of designs. The method of partial order reduction hasbeen e?ciently developed to alleviate this problem. The main notion is that thetechnique based on trace semantics exploits this redundancy and visits only asubset of the global reachable states through selective search method using actionindependence and path stuttering equivalence relations in order to reduce statespace explosion problems. The partial order reduction is based on actions, whichis limited to reduce state space for smaller action granular. We present bundle-actions based partial order reduction, which reduces much better state spaceand combat its explosion problem than action based partial order reduction. Anbundle of actions, which is bigger action granular, is a set of concurrent executiveactions and is performed in a bundle action transition way.