On the constructive orbit problem

Symmetry reduction techniques aim to combat the state-space explosion problem for model checking by restricting search to representative states from equivalence classes with respect to a group of symmetries. The standard approach to representative computation involves converting a state to its minimal image under a permutation group G, before storing the state. This is known as the constructive orbit problem (COP), and is NP{\mathit{NP}} hard. It may be possible to solve the COP efficiently if G is known to have certain structural properties: in particular if G is isomorphic to a full symmetry group, or G is a disjoint/wreath product of subgroups. We extend existing results on solving the COP efficiently for fully symmetric groups, and investigate the problem of automatically classifying an arbitrary permutation group as a disjoint/wreath product of subgroups. We also present an approximate COP strategy based on local search, and some computational group-theoretic optimisations to improve the basic approach of solving the COP by symmetry group enumeration. Experimental results using the TopSPIN symmetry reduction package, which interfaces with the computational group-theoretic system GAP, illustrate the effectiveness of our techniques.     

A template-based approach for the generation of abstractable and reducible models of featured networks

We investigate the relationship between symmetry reduction and inductive reasoning when applied to model checking networks of featured components. Popular reduction techniques for combatting state space explosion in model checking, like abstraction and symmetry reduction, can only be applied effectively when the natural symmetry of a system is not destroyed during specification. We introduce a property which ensures this is preserved, open symmetry. We describe a template-based approach for the construction of open symmetric Promela specifications of featured systems. For certain systems (safely featured parameterised systems) our generated specifications are suitable for conversion to abstract specifications representing any size of network. This enables feature interaction analysis to be carried out, via model checking and induction, for systems of any number of featured components. In addition, we show how, for any balanced network of components, by using a graphical representation of the features and the process communication structure, a group of permutations of the underlying state space of the generated specification can be determined easily. Due to the open symmetry of our Promela specifications, this group of permutations can be used directly for symmetry reduced model checking.The main contributions of this paper are an automatic method for developing open symmetric specifications which can be used for generic feature interaction analysis, and the novel application of symmetry detection and reduction in the context of model checking featured networks.We apply our techniques to a well known example of a featured network – an email system.     

Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more

The size of formal models is steadily increasing and there is a demand from industrial users to be able to use expressive temporal query languages for validating and exploring high-level formal specifications. We present an extension of LTL, which is well adapted for validating B, Z and CSP specifications. We present a generic, flexible LTL model checker, implemented inside the PROB tool, that can be applied to a multitude of formalisms such as B, Z, CSP, B||CSP, as well as Object Petri nets, compensating CSP, and dSL. Our algorithm can deal with deadlock states, partially explored state spaces, past operators, and can be combined with existing symmetry reduction techniques of PROB. We establish correctness of our algorithm in general, as well as combined with symmetry reduction. Finally, we present various applications and empirical results of our tool, showing that it can be applied successfully in practice.     

Symmetry and partial order reduction techniques in model checking Rebeca

Rebeca is an actor-based language with formal semantics which is suitable for modeling concurrent and distributed systems and protocols. Due to its object model, partial order and symmetry detection and reduction techniques can be efficiently applied to dynamic Rebeca models. We present two approaches for detecting symmetry in Rebeca models: One that detects symmetry in the topology of inter-connections among objects and another one which exploits specific data structures to reflect internal symmetry in the internal structure of an object. The former approach is novel in that it does not require any input from the modeler and can deal with the dynamic changes of topology. This approach is potentially applicable to a wide range of modeling languages for distributed and reactive systems. We have also developed a model checking tool that implements all of the above-mentioned techniques. The evaluation results show significant improvements in model size and model-checking time.     

Generation of an arbitrary four-photon polarization-entangled decoherence-free state with cross-Kerr nonlinearity

We present a new scheme to provide an arbitrary four-photon polarization-entangled state, which enables the encoding of single logical qubit information into a four-qubit decoherence-free subspace robustly against collective decoherence. With the assistance of the cross-Kerr nonlinearities, a spatial entanglement gate and a polarization entanglement gate are inserted into the circuit, where the X-quadrature homodyne measurement is properly performed. According to the outcomes of homodyne measurement in the spatial entanglement process, some swap gates are inserted into the corresponding paths of the photons to swap their spatial modes. Apart from Kerr media, some basic linear optical elements are necessary, which make it feasible with current experimental techniques.     

Exploiting symmetry in temporal logic model checking

In practice, finite state concurrent systems often exhibit considerable symmetry. We investigate techniques for reducing the complexity of temporal logic model checking in the presence of symmetry. In particular, we show that symmetry can frequently be used to reduce the size of the state space that must be explored during model checking. In the past, symmetry has been exploited in computing the set of reachable states of a system when the transition relation is represented explicitly [14, 11, 19]. However, this research did not consider arbitrary temporal properties or the complications that arise when BDDs are used in such procedures.We have formalized what it means for a finite state system to be symmetric and described techniques for reducing such systems when the transition relation is given explicitly in terms of states or symbolically as a BDD. Moreover, we have identified an important class of temporal logic formulas that are preserved under this reduction. Our paper also investigates the complexity of various critical steps, like the computation of the orbit relation, which arise when symmetry is used in this type of verification. Finally, we have tested our ideas on a simple cache-coherency protocol based on the IEEE Futurebus + standard.This research was sponsored in part by the Avionics Laboratory, Wright Research and Development Center, Aeronautical Systems Division (AFSC), U.S. Air Force, Wright-Patterson AFB, Ohio 45433-6543 under Contract F33615-90-C-1465, ARPA Order No. 7597 and in part by the National Science Foundation under Grant No. CCR-8722633 and in part by the Semiconductor Research Corporation under Contract 92-DJ-294.The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. government.     

Symmetry reductions for model checking of concurrent dynamic software

Symmetry reduction techniques exploit symmetries that occur during the execution of a system in order to minimize its state space for efficient verification of temporal logic properties. This paper presents a framework for concisely defining and evaluating symmetry reductions currently used in software model checking, involving heap objects and processes. An on-the-fly state space exploration algorithm combining both techniques will also be presented. Second, the relation between symmetry and partial-order reductions is investigated, showing how ones strengths can be used to compensate for the others weaknesses. The symmetry reductions presented here were implemented in the dSPIN model-checking tool. We also performed a number of experiments that show significant progress in reducing the cost of finite-state software verification.     

Automated generation of a progress measure for the sweep-line method

In the context of Petri nets, we propose an automated construction of a progress measure which is an important pre-requisite for a state space reduction technique called the sweep-line method. Our construction is based on linear-algebraic techniques concerning the transition vectors of the Petri net under consideration. We further discuss the possible combination of the sweep-line method with other state space reduction techniques (partial order reduction, the symmetry method).     

Partial-order reduction for general state exploring algorithms

Partial-order reduction is one of the main techniques used to tackle the combinatorial state explosion problem occurring in explicit-state model checking of concurrent systems. The reduction is performed by exploiting the independence of concurrently executed events, which allows portions of the state space to be pruned. An important condition for the soundness of partial-order-based reduction algorithms is a condition that prevents indefinite ignoring of actions when pruning the state space. This condition is commonly known as the cycle proviso. In this paper, we present a new version of this proviso, which is applicable to a general search algorithm skeleton that we refer to as the general state exploring algorithm (GSEA). GSEA maintains a set of open states from which states are iteratively selected for expansion and moved to a closed set of states. Depending on the data structure used to represent the open set, GSEA can be instantiated as a depth-first, a breadth-first, or a directed search algorithm such as Best-First Search or A*. The proviso is characterized by reference to the open and closed set of states of the search algorithm. As a result, it can be computed in an efficient manner during the search based on local information. We implemented partial-order reduction for GSEA based on our proposed proviso in the tool HSF-SPIN, an extension of the explicit-state model checker SPIN for directed model checking. We evaluate the state space reduction achieved by partial-order reduction using the proposed proviso by comparing it on a set of benchmark problems to the use of other provisos. We also compare the use of breadth-first search (BFS) and A*, two algorithms ensuring that counterexamples of minimal length will be found, together with the proviso that we propose.     

A new verification technique for large processes based on identification of relevant tasks

Verification recently has become a challenging topic for business process languages. Verification techniques like model checking allow to ensure that a process complies with domain-specific requirements, prior to the execution. To execute full-state verification techniques like model checking, the state space of the process needs to be constructed. This tends to increase exponentially with the size of the process schema, or it can even be infinite. We address this issue by means of requirements-specific reduction techniques, i.e., reducing the size of the state space without changing the result of the verification. We present an approach that, for a given requirement the system must fulfill, identifies the tasks relevant for the verification. Our approach then uses these relevant tasks for a reduction that confines the process to regions of interest for the verification. To evaluate our new technique, we use real-world industrial processes and requirements. Mainly because these processes make heavy use of parallelization, full-state-search verification algorithms are not able to verify them. With our reduction in turn, even complex processes with many parallel branches can be verified in less than 10 s.     

Novel hybrid SVM-TLBO forecasting model incorporating dimensionality reduction techniques

In this paper, we present a highly accurate forecasting method that supports improved investment decisions. The proposed method extends the novel hybrid SVM-TLBO model consisting of a support vector machine (SVM) and a teaching-learning-based optimization (TLBO) method that determines the optimal SVM parameters, by combining it with dimensional reduction techniques (DR-SVM-TLBO). The dimension reduction techniques (feature extraction approach) extract critical, non-collinear, relevant, and de-noised information from the input variables (features), and reduce the time complexity. We investigated three different feature extraction techniques: principal component analysis, kernel principal component analysis, and independent component analysis. The feasibility and effectiveness of this proposed ensemble model were examined using a case study, predicting the daily closing prices of the COMDEX commodity futures index traded in the Multi Commodity Exchange of India Limited. In this study, we assessed the performance of the new ensemble model with the three feature extraction techniques, using different performance metrics and statistical measures. We compared our results with results from a standard SVM model and an SVM-TLBO hybrid model. Our experimental results show that the new ensemble model is viable and effective, and provides better predictions. This proposed model can provide technical support for better financial investment decisions and can be used as an alternative model for forecasting tasks that require more accurate predictions.     

A probabilistic dynamic technique for the distributed generation of very large state spaces

Conventional methods for state space exploration are limited to the analysis of small systems because they suffer from excessive memory and computational requirements. We have developed a new dynamic probabilistic state exploration algorithm which addresses this problem for general, structurally unrestricted state spaces.

Our method has a low state omission probability and low memory usage that is independent of the length of the state vector. In addition, the algorithm can be easily parallelised. This combination of probability and parallelism enables us to rapidly explore state spaces that are an order of magnitude larger than those obtainable using conventional exhaustive techniques.

We derive a performance model of this new algorithm in order to quantify its benefits in terms of distributed run-time, speedup and efficiency. We implement our technique on a distributed-memory parallel computer and demonstrate results which compare favourably with the performance model. Finally, we discuss suitable choices for the three hash functions upon which our algorithm is based.     

Disappearance of entanglement: a topological point of view

We give a topological classification of the evolution of entanglement, particularly the different ways the entanglement can disappear as a function of time. Four categories exhaust all possibilities given the initial quantum state is entangled and the final one is not. Exponential decay of entanglement, entanglement sudden death and sudden birth can all be understood and visualized in the associated geometrical picture - the polarization vector representation. The entanglement evolution categories of any model are determined by the topology of the state space and the dynamical subspace, the limiting state and the memory effect of the environment. Transitions between these types of behaviors as a function of physical parameters are also possible. These transitions are thus of topological nature. The symmetry of the system is also important, since it determines the dimension of the dynamical subspace. We illustrate the general concepts with a visualizable model for two qubits, and give results for extensions to N-qubit GHZ states and W states.     

A Partial Order Approach to Branching Time Logic Model Checking

Partial order techniques enable reducing the size of the state space used for model checking, thus alleviating the “state space explosion” problem. These reductions are based on selecting a subset of the enabled operations from each program state. So far, these methods have been studied, implemented, and demonstrated for assertional languages that model the executions of a program as computation sequences, in particular the linear temporal logic. The present paper shows, for the first time, how this approach can be applied to languages that model the behavior of a program as a tree. We study here partial order reductions for branching temporal logics, e.g., the logics CTL and CTL* (with the next time operator removed) and process algebra logics such as Hennesy–Milner logic (withτactions). Conditions on the selection of subset of successors from each state during the state-space construction, which guarantee reduction that preserves CTL* properties, are given. The experimental results provided show that the reduction is substantial.     

Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs

Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of system states explored (and thus the time and memory required) for verification. As model checking techniques are scaled up to software systems, it is important to develop and assess partial-order reduction strategies that are effective for addressing the complex structures found in software and for reducing the tremendous cost of model checking software systems. In this paper, we consider a number of reduction strategies for model checking concurrent object-oriented software. We investigate a range of techniques that have been proposed in the literature, improve on those in several ways, and develop five novel reduction techniques that advance the state of the art in partial-order reduction for concurrent object-oriented systems. These reduction strategies are based on (a) detecting heap objects that are thread-local (i.e., can be accessed by a single thread) and (b) exploiting information about patterns of lock-acquisition and release in a program (building on previous work). We present empirical results that demonstrate upwards of a hundred fold reduction in both space and time over existing approaches to model checking concurrent Java programs. In addition to validating their effectiveness, we prove that the reductions preserve LTL_?X properties and describe an implementation architecture that allows them to be easily incorporated into existing explicit-state software model checkers.     

Partial-Order Reduction in Symbolic State-Space Exploration

State-space explosion is a fundamental obstacle in the formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reduction and symbolic state-space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.     

Faster power estimation of CMOS designs using vector compaction - a fractal approach

Low power digital complementary metal oxide semiconductor (CMOS) circuit design requires accurate power estimation. In this paper, we present a compaction algorithm for generating compact vector sets to estimate power efficiently. Power can be estimated using dynamic (simulation) or static (statistical/probabilistic) techniques. Dynamic power estimation techniques simulate the design using a large input vector set for accurate estimation. However, the simulation time is prohibitively long for bigger designs with larger vector sets. The statistical methods, on the other hand, use analytical tools that make them faster but less accurate. To achieve the accuracy of dynamic power estimation and the speed of statistical methods, one approach is to generate a compact, representative vector set that has the same switching transition behavior as the original larger vector set. The compaction algorithm presented in this paper uses fractal concepts to generate such a compact vector set. The fractal technique quantifies correlation by a fractal parameter which can be determined faster than calculating correlation explicitly. Experimental results on circuits from the ISCAS85 and ISCAS89 benchmark suites, with correlated input vector sets, resulted in a maximum compaction ratio of 65.57X (average 38.14X) and maximum power estimation error of 2.4% (average 2.06%). Since the size of the compact vector set used for simulation is smaller, the simulation time will be shorter and will significantly speed up the design cycle.     

A realization approach to stochastic model reduction

The problem of discrete-time stochastic model reduction (approximation) is considered. Using the canonical correlation analysis approach of Akaike (1975), a new order-reduction algorithm is developed. Furthermore, it is shown that the inverse of the reduced-order realization is asymptotically stable. Next, an explicit relationship between canonical variables and the linear least-squares estimate of the state vector is established. Using this, a more direct approach for order reduction is presented, and also a new design for reduced-order Kalman filters is developed. Finally, the uniqueness and symmetry properties for the new realization—the balanced stochastic realization—along with a simulation result, are presented.     

循环对称化简及在三值模型上的扩展

为了将对称化简扩展到更多的非对称系统上,扩展了传统的基于自同构的对称性,提出了一种称为循环对称的新的对称性.证明了采用循环对称置换群或者由一组循环对称置换所生成的置换群仍可得到与原模型互模拟的对称商结构,从而达到化简系统规模的目的.进一步地,研究如何将对称化简应用于多值模型.多值模型可以有效地表示系统中的不确定信息,正越来越多地用于软件系统的建模与分析中.针对一种具体的多值模型——三值模型,定义传统的对称化简和循环对称化简在其上面的扩展.最后,分析三值模型的商结构与由约简得到的二值模型商结构之间的关系,证明了两种途径的等价性.