Optimal Sequential Multiclass Diagnosis

In multiclass classification, one faces greater uncertainty when the data fall near the decision boundary. To reduce the uncertainty, one can wait and collect more data, but this invariably delays the decision. How can one make an accurate classification as quickly as possible? The solution requires a multiclass generalization of Wald’s sequential hypothesis testing, but the standard formulation is intractable because of the curse of dimensionality in dynamic programming. In “Optimal Sequential Multiclass Diagnosis,” Wang shows that, in a broad class of practical problems, the reachable state space is often restricted on, or near, a set of low-dimensional, time-dependent manifolds. After understanding the key drivers of sparsity, the author develops a new solution framework that uses a low-dimensional statistic to reconstruct the high-dimensional state. This framework circumvents the curse of dimensionality, allowing efficient computation of the optimal or near-optimal policies for quickest classification with large numbers of classes.

Fuzzy particle swarm optimization algorithm (NFPSO) for reachability analysis of complex software systems

Nowadays, model checking is applied as an accuratetechnique to verify software systems. The main problem of modelchecking techniques is the state space explosion. This problemoccurs due to the exponential memory usage by the model checker.In this situation, using meta-heuristic and evolutionary algorithmsto search for a state in which a property is satisfied/violated is apromising solution. Recently, different evolutionary algorithmslike GA, PSO, etc. are applied to find deadlock state. Even thoughuseful, most of them are concentrated on finding deadlock. Thispaper proposes a fuzzy algorithm in order to analyze reachabilityproperties in systems specified through GTS with enormous statespace. To do so, we first extend the existing PSO algorithm (forchecking deadlocks) to analyze reachability properties. Then, toincrease the accuracy, we employ a Fuzzy adaptive PSO algorithmto determine which state and path should be explored in each stepto find the corresponding reachable state. These two approachesare implemented in an open-source toolset for designing andmodel checking GTS called GROOVE. Moreover, theexperimental results indicate that the hybrid fuzzy approachimproves speed and accuracy in comparison with other techniquesbased on meta-heuristic algorithms such as GA and the hybrid ofPSO-GSA in analyzing reachability properties.

Invariant Synthesis via Convex Optimization

This chapter focuses on the computation of invariant for a discrete dynamical system collecting semantics. Invariants or collecting semantics properties are properties preserved along all executions of a system and verified in all reachable states. A subset of these invariants are defined as inductive. Inductive invariants are properties, or relationships between variables, that are inductively preserved by one transition of considered systems. Intuitively, it is not required to consider a reachable state and all (or part of) its past while arguing about the validity of the invariant, but only the single state. Applying the induction principle, this chapter obtains that any state satisfying the property is mapped to a next state preserving that same property.

Reachability Analysis of Low-Order Discrete State Reaction Networks Obeying Conservation Laws

In this paper we study the reachability problem of sub- and superconservative discrete state chemical reaction networks (d-CRNs). It is known that a subconservative network has bounded reachable state space, while that of a superconservative one is unbounded. The reachability problem of superconservative reaction networks is traced back to the reachability of subconservative ones. We consider network structures composed of reactions having at most one input and one output species beyond the possible catalyzers. We give a proof that, assuming all the reactions are charged in the initial and target states, the reachability problems of sub- and superconservative reaction networks are equivalent to the existence of nonnegative integer solution of the corresponding d-CRN state equations. Using this result, the reachability problem is reformulated as an Integer Linear Programming (ILP) feasibility problem. Therefore, the number of feasible trajectories satisfying the reachability relation can be counted in polynomial time in the number of species and in the distance of initial and target states, assuming fixed number of reactions in the system.

Robust Controllability and Observability of Boolean Control Networks under Different Disturbances

This paper investigates robust controllability and observability of Boolean control networks under disturbances. Firstly, under unobservable disturbances, some sufficient conditions are obtained for robust controllability of BCNs. Then an algorithm is proposed to construct the least control sequences which drive the trajectory from a state to a given reachable state. If the disturbances are observable, by defining the order-preserving system, an efficient sufficient condition is obtained for robust controllability of BCNs. Finally, the robust observability problem is converted into an equivalent robust controllability via set controllability and is solved by using the results obtained for set controllability. Some numerical examples are presented to illustrate the obtained results.

CARTESIAN PRODUCT PARTITIONING OF MULTI-DIMENSIONAL REACHABLE STATE SPACES

Markov chains (MCs) are widely used to model systems which evolve by visiting the states in their state spaces following the available transitions. When such systems are composed of interacting subsystems, they can be mapped to a multi-dimensional MC in which each subsystem normally corresponds to a different dimension. Usually the reachable state space of the multi-dimensional MC is a proper subset of its product state space, that is, Cartesian product of its subsystem state spaces. Compact storage of the matrix underlying such a MC and efficient implementation of analysis methods using Kronecker operations require the set of reachable states to be represented as a union of Cartesian products of subsets of subsystem state spaces. The problem of partitioning the reachable state space of a three or higher dimensional system with a minimum number of partitions into Cartesian products of subsets of subsystem state spaces is shown to be NP-complete. Two algorithms, one merge based the other refinement based, that yield possibly non-optimal partitionings are presented. Results of experiments on a set of problems from the literature and those that are randomly generated indicate that, although it may be more time and memory consuming, the refinement based algorithm almost always computes partitionings with a smaller number of partitions than the merge-based algorithm. The refinement based algorithm is insensitive to the order in which the states in the reachable state space are processed, and in many cases it computes partitionings that are optimal.

Effective Extraction of State Invariant for Software Verification

In software design of complex systems, more time and effort are spent on verification than on constructions. Model checking for software verification techniques offer a large potential to obtain and early integration of verification in the design process. This paper describes how to easily specify and the software properties and to understand the software generating automatically invariant. In this paper deal with issue that state invariant is a property that holds in every reachable state. Not only can be used in understanding and analysis of complex software systems. In addition, it can be used for system verifications such as checking safety, consistency, and completeness. For these reasons, there are many vital researches for deriving state invariant from finite state machine models. In this research was to be considered to extract state invariant. Thus it is likely to be too complex for the user to understand. This paper let the user focus on some interested parts (called scopes) rather than a whole state space in a model. Computation Tree Logic (CTL) is used to specify scopes in which he/she is interested. Given a scope in CTL, forward reachability analysis is used to find out a set of states inside it. Obviously, a set of states calculated in this way is a subset of every reachable state. Keywords: Software verification, Invariant, Scopes, Model Checking