Narrow Results

Hybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking can be inconclusive, however, in which case the abstraction must be refined. This paper presents a new procedure to perform this refinement operation for abstractions of hybrid systems. Following an approach originally developed for finite-state systems [11, 25], the refinement procedure constructs a new abstraction that eliminates a counterexample generated by the model checker. For hybrid systems, analysis of the counterexample requires the computation of sets of reachable states in the continuous state space. We show how such reachability computations with varying degrees of complexity can be used to refine hybrid system abstractions efficiently. Examples illustrate our counterexample-guided refinement procedure. Experimental results for a prototype implementation indicate significant advantages over existing methods.

Hybrid systems combine continuous and discrete behavior. Hybrid Automata are a powerful formalism for the modeling and verification of such systems. A common problem in hybrid system verification is the good parameters problem, which consists in identifying a set of parameter valuations which guarantee a certain behavior of a system. Recently, a method has been presented for attacking this problem for Timed Automata. In this paper, we show the extension of this methodology for hybrid automata with linear and affine dynamics. The method is demonstrated with a hybrid system benchmark from the literature.

We argue that dynamical systems involving discrete and continuous data can be modelled by Turing machines with oracles that are physical processes. Using the theory introduced in Beggs et al. [2,3], we consider the scope and limits of polynomial time computations by such systems. We propose a general polynomial time Church-Turing Thesis for feasible computations by analogue-digital systems, having the non-uniform complexity class BPP//log* as theoretical upper bound. We show why BPP//log* should be replace P/poly, which was proposed by Siegelmann for neural nets [23,24]. Then we examine whether other sources of hypercomputation can be found in analogue-digital systems besides the oracle itself. We prove that the higher polytime limit P/poly can be attained via non-computable analogue-digital interface protocols.

We consider the experimenter (e.g. the experimental physicist) as a Turing machine — the digital component — and the experiment of measurement — the analog component — as an oracle to the Turing machine. The algorithm running in the machine abstracts the experimental method of measurement (encoding the recursive structure of experimental actions) chosen by the experimenter. In this paper we prove that the central analogue-digital complexity classes $P$, $P/poly$ and $P/poly\cap REC$ can be characterized in terms of protocols to perform measurements controlled by standard Turing machines.

This paper proposes a technique to improve Artificial Neural Network (ANN) prediction accuracy using Particle Swarm Optimization (PSO) combiner. A hybrid system consists of two stages with the first stage containing two ANNs. The first ANN predictor is a multi-layer feed-forward network trained with error back-propagation and the second predictor is a functional link network. These two predictors are combined in the second stage using PSO combiner in a linear and non-linear fashion. The proposed method is applied to problem of predicting daily natural gas consumption. The performance of ANN predictors and combination methods are tested on real data from four different gas utilities. The experimental results show that the proposed particle swarm optimization combiners results in more accurate prediction compared to using single ANN predictor. Prediction accuracy improvement of the proposed PSO combiners have been shown using hypothesis testing.

This paper presents a text categorization system, capable of analyzing HTML/text documents collected from the Web. The system is a component of a more extensive intelligent agent for adaptive information filtering on the Web. It is based on a hybrid case-based architecture, where two multilayer perceptrons are integrated into a case-based reasoner. An empirical evaluation of the system was performed by means of a confidence interval technique. The experimental results obtained are encouraging and support the choice of a hybrid case-based approach to text categorization.

The task discussed in this paper is that of learning to map input sequences to output sequences. In particular, problems of phoneme recognition in continuous speech are considered, but most of the discussed techniques could be applied to other tasks, such as the recognition of sequences of handwritten characters. The systems considered in this paper are based on connectionist models, or artificial neural networks, sometimes combined with statistical techniques for recognition of sequences of patterns, stressing the integration of prior knowledge and learning. Different architectures for sequence and speech recognition are reviewed, including recurrent networks as well as hybrid systems involving hidden Markov models.

Up till recently, state-of-the-art, large vocabulary, continuous speech recognition (CSR) had employed hidden Markov modeling (HMM) to model speech sounds. In an attempt to improve over HMM we developed a hybrid system that integrates HMM technology with neural networks.

We present the concept of a Segmental Neural Net (SNN) for phonetic modeling in CSR. By taking into account all the frames of a phonetic segment simultaneously, the SNN overcomes the well-known conditional-independence limitation of HMMs. We have developed a novel hybrid SNN/HMM system that combines the advantages of SNNs and HMMs using a multiple hypothesis (or N-best) paradigm. In this system, we generate likely phonetic segmentations from the HMM N-best list of word sequences, which are scored by the SNN. The HMM and SNN scores are then combined to optimize performance.

In several speaker-independent, 1000-word CSR tests, the error rate for the hybrid system dropped 20% from that of a state-of-the-art HMM system alone.

This paper presents a methodology for integrating connectionist and symbolic approaches to 2D image recognition. The proposed integration paradigm exploits the synergy of the two approaches for both the training and the recognition phases of an image recognition system. In the training phase, a symbolic module provides an approximate solution to a given image-recognition problem in terms of symbolic models. Such models are hierarchically organized into different abstraction levels, and include contextual descriptions. After mapping such models into a complex neural architecture, a neural training process is carried out to optimize the solution of the recognition problem. The so-obtained neural networks are used during the recognition phase for pattern classification. In this phase, the role of symbolic modules consists of managing complex aspects of information processing: abstraction levels, contextual information, and global recognition hypotheses. A hybrid system implementing the proposed integration paradigm is presented, and its advantages over single approaches are assessed. Results on Magnetic Resonance image recognition are reported, and comparisons with some well-known classifiers are made.

Hand gestures are the natural form of communication among people, yet human-computer interaction is still limited to mice movements. The use of hand gestures in the field of human-computer interaction has attracted renewed interest in the past several years. Special glove-based devices have been developed to analyze finger and hand motion and use them to manipulate and explore virtual worlds. To further enrich the naturalness of the interaction, different computer vision-based techniques have been developed. At the same time the need for more efficient systems has resulted in new gesture recognition approaches. In this paper we present an hybrid intelligent system for hand gesture recognition. The hybrid approach consists of an ensemble of connectionist networks — radial basis functions (RBF) — and inductive decision trees (AQDT). Cross Validation (CV) experimental results yield a false negative rate of 1.7% and a false positive rate of 1% while the evaluation takes place on a data base including 150 images corresponding to 15 gestures of 5 subjects. In order to assess the robustness of the system, the vocabulary of the gestures has been increased from 15 to 25 and the size of the database from 150 to 750 images corresponding now to 15 subjects. Cross Validation (CV) experimental results yield a false negative rate of 3.6% and a false positive rate of 1.8% respectively. The benefits of our hybrid architecture include

(i) robustness via query by consensus as provided by ensembles of networks when facing the inherent variability of the image formation and data acquisition process,

(ii) classifications made using decision trees,

(iii) flexible and adaptive thresholds as opposed to ad hoc and hard thresholds and

(iv) interpretability of the way classification and retrieval is eventually achieved.

In this paper, a new hybrid impulsive and switching control strategy for synchronization of nonlinear systems is developed. Using switched Lyapunov functions, several new criteria for global exponential stability of hybrid impulsive and switching nonlinear systems are established and, particularly, some simple sufficient conditions for driving the synchronization error to zero exponentially are proposed. As an application, Chua's chaotic circuit is investigated.

Switched buffer systems are discretized switched flow systems. They are discrete, but can be handled with the same mathematical framework as hybrid systems. In particular, we show that switched buffer systems form discrete strange billiards. For any initialization, discrete strange billiards lead to a finite periodic attractor. The periods and the buffer switching rates are the most important performance measures for the practical use of switched buffer systems. Both measures depend on the sum of objects in the buffers. For each object sum multiple suboptimal attractors may exist. Onto which attractor the system converges depends on the initial buffer levels. We propose a switched Kanban control algorithm that forces the system onto the attractor with minimum buffer switching rate independently of the initialization of the buffer levels. This algorithm needs to perform only one single additional buffer switching operation. Also Heijunka control of switched buffer systems is considered in the framework of strange billiards. We show that Heijunka forms equilateral triangles in the state space. Heijunka is able to yield low buffer switching rates, but only if the buffer levels are optimally initialized. For suboptimal buffer level initializations very high (bad) buffer switching rates can be achieved. In an illustrative example, our proposed switched Kanban control algorithm outperforms conventional Kanban control by about 29% and Heijunka control by about 5%.

In this paper, we study the chaotic dynamics of a voltage-mode controlled buck converter, which is typically a switched piecewise linear system. For the two-dimensional hybrid system, we consider a properly chosen cross-section and the corresponding Poincaré map, and show that the dynamics of the system is semi-conjugate to a 2-shift map, which implies the chaotic behavior of this system. The essential tool is a topological horseshoe theory and numerical method.

An essential issue for the validation of ciphers is cryptanalysis, that is, the study of attacks in order to reveal possible weaknesses. In this paper, we propose a systematic and unified methodology for cryptanalyzing known chaos-based cryptosystems borrowed from the open literature, namely shift keying, discrete parameter modulation, switched message-embedding, time-varying delay-based schemes. It is shown that all of them have a hybrid feature. Based on this consideration, the cryptanalysis leads to a specific parameter identification. The method is extended in straightforward way for hybrid cryptosystems defined over finite fields, involving in particular Boolean functions. The complexity of the cryptanalysis is derived regardless of the exhibited dynamics and provides a new quantitative measure for security assessment, thus allowing to show, by the way, that most of the chaos-based cryptosystems proposed so far in the literature are weak.

By using the reduction technique to impulsive differential equations [Akhmet & Turan, 2006], we rigorously prove the presence of chaos in dynamic equations on time scales (DETS). The results of the present study are based on the Li–Yorke definition of chaos. This is the first time in the literature that chaos is obtained for DETS. An illustrative example is presented by means of a Duffing equation on a time scale.

An analog electronic implementation by means of operational amplifiers of a class of hybrid dissipative systems in $R^3$ is presented. The switching systems have two unstable hyperbolic focus-saddle equilibria with the same stability index, a positive real eigenvalue and a pair of complex conjugated eigenvalues with negative real part. The analog circuit generates signals that oscillate in an attractor located between the two unstable equilibria, and may present saturation states at the moment of energizing it, i.e. if the initial voltage on the capacitors do not belong to the basin of attraction the circuit will end on a saturation state.

The goal of this paper is to demonstrate the application of the algorithmic analysis of hybrid systems to idle speed control. This problem can be formulated as to design a safety hybrid controller. In principle, such controllers can be derived from the maximal invariant set. It is, however, hard to compute this set for a nonlinear hybrid system with both continuous control and disturbance inputs. We propose to use a class of piecewise constant control functions, which allows to develop an effective synthesis algorithm based on reachability computations. In addition, we show how assume-guarantee reasoning from automatic verification can be used to reduce the computational complexity.

Technical systems that include complex physical dynamics as well as extensive discrete event control, require powerful modeling and simulation techniques. As the most adequate means for modeling hybrid physical systems, we advocate the use of object-oriented modeling languages such as Modelica. However, the discrete event models often require the use of dedicated graphical editors that cannot be defined appropriately using Modelica. The purpose of the DES/M modeling environment [10] is to provide such editors for different discrete event formalisms and to translate discrete event models automatically into Modelica components such that a discrete event controller can be integrated easily into Modelica models and simulated using standard Modelica software tools. This contribution presents the main concepts used for the representation of several discrete event formalisms in the Modelica language and discusses the class of discrete event formalisms that can be supported by the DES/M environment.

This contribution proposes a link between the specification of supervisory controllers by Sequential Function Charts (SFC) and the verification of embedded systems with hybrid dynamics. The SFC are transformed into modular timed automata using a procedure based on graph grammars. The resulting controller model is composed with a hybrid automaton (with possibly nonlinear continuous dynamics) that models the plant behavior. In order to verify safety properties of the composed system algorithmically, a tool implementing the recently proposed approach of counterexample guided model checking is employed. The procedure is illustrated for a processing system example.

In this approach, we investigate the fuzzy γ-models for decision analysis and making. This methodology utilizes fuzzy γ-model as an information aggregation operator. It provides several advantages due to the fact that the input to each model is the evidence supplied by the degree of satisfaction of sub-criteria and the output is the aggregated evidence. We also generalize fuzzy γ-models as a hierarchical network in this work. Thus, the decision making process is to aggregate and propagate the evidence information through such a hierarchical network. This trainable network is able to perceive and interpret complex decisions by using those fuzzy models. The simulation study examines the learning behaviors of the fuzzy γ-models using two numerical examples.