Optimal and nearly optimal algorithms for approximating polynomial zeros

We substantially improve the known algorithms for approximating all the complex zeros of an n^th degree polynomial p(x). Our new algorithms save both Boolean and arithmetic sequential time, versus the previous best algorithms of Schönhage [1], Pan [2], and Neff and Reif [3]. In parallel (NC) implementation, we dramatically decrease the number of processors, versus the parallel algorithm of Neff [4], which was the only NC algorithm known for this problem so far. Specifically, under the simple normalization assumption that the variable x has been scaled so as to confine the zeros of p(x) to the unit disc x : |x| ≤ 1, our algorithms (which promise to be practically effective) approximate all the zeros of p(x) within the absolute error bound 2^−b, by using order of n arithmetic operations and order of (b + n)n² Boolean (bitwise) operations (in both cases up to within polylogarithmic factors). The algorithms allow their optimal (work preserving) NC parallelization, so that they can be implemented by using polylogarithmic time and the orders of n arithmetic processors or (b + n)n² Boolean processors. All the cited bounds on the computational complexity are within polylogarithmic factors from the optimum (in terms of n and b) under both arithmetic and Boolean models of computation (in the Boolean case, under the additional (realistic) assumption that n = O(b)).     

Accuracy-enhancing methods for balancing-related frequency-weighted model and controller reduction

We consider the solution of the balancing-related frequency-weighted model and controller reduction problems using accuracy enhanced numerical algorithms. We propose first new stability-enforcing choices of the frequency-weighted grammians which can guarantee the stability of reduced models for two-sided frequency weights. Then we show that for the frequency-weighted controller reduction problems with standard stability and performance-enforcing frequency weights the computation of the frequency-weighted grammians can be done by solving reduced order Lyapunov equations. For both frequency-weighted model and controller reduction problems we indicate how to compute the grammians directly in terms of their Cholesky factors. This allows the extension of the square-root and balancing-free accuracy-enhancing techniques to the frequency-weighted case.     

Partial order reduction for state/event LTL with application to component-interaction automata

Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL (Chaki et al. (2004, 2005) [1] and [2]) incorporates both states and events to express important properties of component-based software systems.The main contribution of this paper is a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.To bring some evidence of the method’s efficiency, we present some of the results obtained by employing the partial order reduction technique within our tool for verification of component-based systems modelled using the formalism of component-interaction automata (Brim et al. (2005) [3]).     

Word level bitwidth reduction for unbounded hardware model checking

In this paper we present a word-level model checking method that attempts to speed up safety property checking of industrial netlists. Our aim is to construct an algorithm that allows us to check both bounded and unbounded properties using standard bit-level model checking methods as back-end decision procedures, while incurring minimum runtime penalties for designs that are unsuited to our analysis. We do this by combining modifications of several previously known techniques into a static abstraction algorithm which is guaranteed to produce bit-level netlists that are as small or smaller than the original bitblasted designs. We evaluate our algorithm on several challenging hardware components.     

Parametric optimisation in a 2-D cellular automata model of fundamental seismic attributes with the use of genetic algorithms

A two-dimensional (2-D) cellular automata (CA) dynamic system constituted of cells-charges has been proposed for the simulation of the earthquake process. In this paper, the study is focused on the optimal parameterisation of the model introducing the use of genetic algorithm (GA). The optimisation of the CA model parameterisation, by applying a standard GA, extends its ability to study various hypotheses concerning the seismicity of the region under consideration. The GA evolves an initially random population of candidate solutions of model parameters, such that in time appropriate solutions to emerge. The quality criterion is realised by taking into account the extent that the simulation results match the Gutenberg-Richter (GR) law derived from recorded data of the area under test. The simulation results presented here regard regions of Greece with different seismic and geophysical characteristics. The results found are in good quantitative and qualitative agreement with the GR scaling relations.     

一种新的进化计算算法模型--种群竞争消亡算法

为克服进化计算自身的早熟收敛缺陷,受自然界和人类社会进化现象的启发,文中研究得到了一种新的进化计算算法模型——种群竞争消亡算法。本文将该模型应用于温室作物生长模型的参数优化,并将试验结果与基本进化计算相比较,结果说明种群竞争消亡算法在稳定性和收敛性上确实比基本进化计算优越。     

Krylov projection framework for Fourier model reduction

This paper analyzes the Fourier model reduction (FMR) method from a rational Krylov projection framework and shows how the FMR reduced model, which has guaranteed stability and a global error bound, can be computed in a numerically efficient and robust manner. By monitoring the rank of the Krylov subspace that underlies the FMR model, the projection framework also provides an improved criterion for determining the number of Fourier coefficients that are needed, and hence the size of the resulting reduced-order model. The advantages of applying FMR in the rational Krylov projection framework are demonstrated on a simple example.     

State space reduction for process algebra specifications

Data-flow analysis to identify “dead” variables and reset them to an “undefined” value is an effective technique for fighting state explosion in the enumerative verification of concurrent systems. Although this technique is well-adapted to imperative languages, it is not directly applicable to value-passing process algebras, in which variables cannot be reset explicitly due to the single-assignment constraints of the functional programming style. This paper addresses this problem by performing data-flow analysis on an intermediate model (Petri nets extended with state variables) into which process algebra specifications can be translated automatically. It also addresses important issues such as avoiding the introduction of useless reset operations and handling shared read-only variables that child processes inherit from their parents.     

Links between probabilistic automata and hidden Markov models: probability distributions, learning models and induction algorithms

This article presents an overview of Probabilistic Automata (PA) and discrete Hidden Markov Models (HMMs), and aims at clarifying the links between them. The first part of this work concentrates on probability distributions generated by these models. Necessary and sufficient conditions for an automaton to define a probabilistic language are detailed. It is proved that probabilistic deterministic automata (PDFA) form a proper subclass of probabilistic non-deterministic automata (PNFA). Two families of equivalent models are described next. On one hand, HMMs and PNFA with no final probabilities generate distributions over complete finite prefix-free sets. On the other hand, HMMs with final probabilities and probabilistic automata generate distributions over strings of finite length. The second part of this article presents several learning models, which formalize the problem of PA induction or, equivalently, the problem of HMM topology induction and parameter estimation. These learning models include the PAC and identification with probability 1 frameworks. Links with Bayesian learning are also discussed. The last part of this article presents an overview of induction algorithms for PA or HMMs using state merging, state splitting, parameter pruning and error-correcting techniques.     

Reverse reachability analysis: A new technique for deadlock detection on communicating finite state machines

The communicating finite state machines can exchange messages over bounded FIFO channels. In this paper, a new technique, called reverse reachability analysis, is proposed to detect deadlocks on the communication between the communicating finite state machines. The technique is based on finding reverse reachable paths starting from possible deadlock states. If a reverse reachable path can reach the initial global state, then deadlock occurs. Otherwise the communication is deadlock-free. The effectiveness of the technique has been verified by some real protocols such as a specification of X.25 call establishment/clear protocol and Bartlet's alternating bit protocol.     

Convergent algorithms for frequency weighted L2 model reduction

This paper is concerned with computing an L₂-optimal reduced-order model for a given stable multivariable linear system in the presence of input and output frequency weightings. By parametrizing a class of reduced-order models in terms of an orthogonal projection and using manifold techniques as tools, both continuous and iterative algorithms are derived and their convergence properties are established. As an application, we show that an L₂ optimal reduced-order filter in the closed-loop sense can be computed using these algorithms.     

Balanced truncation model reduction for systems with inhomogeneous initial conditions

We present a rigorous approach to extend balanced truncation model reduction (BTMR) to systems with inhomogeneous initial conditions, we provide an estimate for the error between the input–output maps of the original and of the reduced initial value system, and we illustrate numerically the superiority of our approach over the naive application of BTMR. When BTMR is applied to linear time invariant systems with inhomogeneous initial conditions, it is crucial that the initial data are well represented by the subspaces generated by BTMR. This requirement is often ignored or it is avoided by making the restrictive assumption that the initial data are zero. To ensure that the initial data are well represented by the BTMR subspaces, we add auxiliary inputs determined by the initial data.     

Application of static analyses for state-space reduction to the microcontroller binary code

This paper describes the application of two abstraction techniques, namely dead variable reduction and path reduction, to the microcontroller binary code in order to tackle the state-explosion problem in model checking. These abstraction techniques are based on static analyses, which have to cope with the peculiarities of the binary code such as hardware dependencies, interrupts, recursion, and globally accessible memory locations. An interprocedural static analysis framework is presented that handles these peculiarities. Based on this framework, extensions of dead variable reduction and path reduction are detailed. A case study using several microcontroller programs is presented in order to demonstrate the efficiency of the described abstraction techniques.     

CSL model checking algorithms for QBDs

We present an in-depth treatment of model checking algorithms for a class of infinite-state continuous-time Markov chains known as quasi-birth death processes. The model class is described in detail, as well as the logic CSL to express properties of interest. Using a new property-independency concept, we provide model checking algorithms for all the CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with representatives. By the use of an application-driven dynamic stopping criterion, the algorithm stops whenever the property to be checked can be certified (or falsified). A comprehensive case study of a connection management system shows the versatility of our new algorithms.     

A two-step approach for model reduction in flexible multibody dynamics

In this work, a two-step approach for model reduction in flexible multibody dynamics is proposed. This technique is a combination of the Krylov-subspace method and a Gramian matrix based reduction approach that is particularly suited if a small reduced-order model of a system charged with many force-inputs has to be generated. The proposed methodology can be implemented efficiently using sparse matrix techniques and is therefore applicable to large-scale systems too. By a numerical example, it is demonstrated that the suggested two-step approach has very good approximation capabilities in the time as well as in the frequency domain and can help to reduce the computation time of a numerical simulation significantly.     

Data reduction and fast routing: A strategy for efficient algorithms for message-passing parallel computers

This paper presents several algorithms for solving problems using massively parallel SIMD hypercube and shuffle-exchange computers. The algorithms solve a wide variety of problems, but they are related because they all use a common strategy. Specifically, all of the algorithms use a divide-and-conquer approach to solve a problem withN inputs using a parallel computer withP processors. The structural properties of the problem are exploited to assure that fewer thanN data items are communicated during the division and combination steps of the divide-and-conquer algorithm. This reduction in the amount of data that must be communicated is central to the efficiency of the algorithm.This paper addresses four problems, namely the multiple-prefix, data-dependent parallel-prefix, image-component-labeling, and closest-pair problems. The algorithms presented for the data-dependent parallel-prefix and closest-pair problems are the fastest known whenN P and the algorithms for the multiple-prefix and image-component-labeling problems are the fastest known whenN is sufficiently large with respect toP.This work was supported in part by our NSF Graduate Fellowship.