Approximate Model Checking of Real-Time Systems for Linear Duration Invariants

Real-time systems are usually modelled with timed automata and real-time requirements relating to the state durations of the system are often specifiable using Linear Duration Invariants, which is a decidable subclass of Duration Calculus formulas. Various algorithms have been developed to check timed automata or real-time automata for linear duration invariants, but each needs complicated preprocessing and exponential calculation. To the best of our knowledge, these algorithms have not been implemented. In this paper, we present an approximate model checking technique based on a genetic algorithm to check real-time automata for linear durration invariants in reasonable times. Genetic algorithm is a good optimization method when a problem needs massive computation and it works particularly well in our case because the fitness function which is derived from the linear duration invariant is linear. ACM Computing Classification System (1998): D.2.4, C.3.

LMI-based digital redesign of linear time-invariant systems with state-derivative feedback

A simple method for designing a digital state-derivative feedback gain and a feedforward gain such that the control law is equivalent to a known and adequate state feedback and feedforward control law of a digital redesigned system is presented. It is assumed that the plant is a linear controllable, time-invariant, Single-Input (SI) or Multiple-Input (MI) system. This procedure allows the use of well-known continuous-time state feedback design methods to directly design discrete-time state-derivative feedback control systems. The state-derivative feedback can be useful, for instance, in the vibration control of mechanical systems, where the main sensors are accelerometers. One example considering the digital redesign with state-derivative feedback of a helicopter illustrates the proposed method. © 2009 IEEE.

Applying linear time-varying constraints to econometric models: With an application to demand systems

When linear equality constraints are invariant through time they can be incorporated into estimation by restricted least squares. If, however, the constraints are time-varying, this standard methodology cannot be applied. In this paper we show how to incorporate linear time-varying constraints into the estimation of econometric models. The method involves the augmentation of the observation equation of a state-space model prior to estimation by the Kalman filter. Numerical optimisation routines are used for the estimation. A simple example drawn from demand analysis is used to illustrate the method and its application.

Non-linear time series models

The last three decades have seen quite dramatic changes the way we modeled time dependent data. Linear processes have been in the center stage in modeling time series. As far as the second order properties are concerned, the theory and the methodology are very adequate.However, there are more and more evidences that linear models are not sufficiently flexible and rich enough for modeling purposes and that failure to account for non-linearities can be very misleading and have undesired consequences.

Assembling genes from predicted exons in linear time with dynamic programming

In a number of programs for gene structure prediction in higher eukaryotic genomic sequences, exon prediction is decoupled from gene assembly: a large pool of candidate exons is predicted and scored from features located in the query DNA sequence, and candidate genes are assembled from such a pool as sequences of nonoverlapping frame-compatible exons. Genes are scored as a function of the scores of the assembled exons, and the highest scoring candidate gene is assumed to be the most likely gene encoded by the query DNA sequence. Considering additive gene scoring functions, currently available algorithms to determine such a highest scoring candidate gene run in time proportional to the square of the number of predicted exons. Here, we present an algorithm whose running time grows only linearly with the size of the set of predicted exons. Polynomial algorithms rely on the fact that, while scanning the set of predicted exons, the highest scoring gene ending in a given exon can be obtained by appending the exon to the highest scoring among the highest scoring genes ending at each compatible preceding exon. The algorithm here relies on the simple fact that such highest scoring gene can be stored and updated. This requires scanning the set of predicted exons simultaneously by increasing acceptor and donor position. On the other hand, the algorithm described here does not assume an underlying gene structure model. Indeed, the definition of valid gene structures is externally defined in the so-called Gene Model. The Gene Model specifies simply which gene features are allowed immediately upstream which other gene features in valid gene structures. This allows for great flexibility in formulating the gene identification problem. In particular it allows for multiple-gene two-strand predictions and for considering gene features other than coding exons (such as promoter elements) in valid gene structures.

Duality, observability, and controllability for linear time-varying descriptor systems

A characterization of observability for linear time-varying descriptor systemsE(t)x(t)+F(t)x(t)=B(t)u(t), y(t)=C(t)x(t) was recently developed. NeitherE norC were required to have constant rank. This paper defines a dual system, and a type of controllability so that observability of the original system is equivalent to controllability of the dual system. Criteria for observability and controllability are given in terms of arrays of derivatives of the original coefficients. In addition, the duality results of this paper lead to an improvement on a previous fundamental structure result for solvable systems of the formE(t)x(t)+F(t)x(t)=f(tt).

A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic

The clausal resolution method for propositional linear-time temporal logic is well known and provides the basis for a number of temporal provers. The method is based on an intuitive clausal form, called SNF, comprising three main clause types and a small number of resolution rules. In this paper, we show how the normal form can be radically simplified, and consequently, how a simplified clausal resolutioin method can be defined for this impoprtant variety of logics.

On switched control design of linear time-invariant systems with polytopic uncertainties

This paper proposes a new switched control design method for some classes of linear time-invariant systems with polytopic uncertainties. This method uses a quadratic Lyapunov function to design the feedback controller gains based on linear matrix inequalities (LMIs). The controller gain is chosen by a switching law that returns the smallest value of the time derivative of the Lyapunov function. The proposed methodology offers less conservative alternative than the well-known controller for uncertain systems with only one state feedback gain. The control design of a magnetic levitator illustrates the procedure. © 2013 Wallysonn A. de Souza et al.

Controllability and stabilizability of linear time-varying distributed hereditary control systems

This paper is concerned with the controllability and stabilizability problem for control systems described by a time-varyinglinear abstract differential equation with distributed delay in the state variables. An approximate controllability propertyis established, and for periodic systems, the stabilization problem is studied. Assuming that the semigroup of operatorsassociated with the uncontrolled and non delayed equation is compact, and using the characterization of the asymptoticstability in terms of the spectrum of the monodromy operator of the uncontrolled system, it is shown that the approximatecontrollability property is a sufficient condition for the existence of a periodic feedback control law that stabilizes thesystem. The result is extended to include some systems which are asymptotically periodic. Copyright © 2014 John Wiley &Sons, Ltd.

Fuzzy Connectedness Image Segmentation in Graph Cut Formulation: A Linear-Time Algorithm and a Comparative Analysis

A deep theoretical analysis of the graph cut image segmentation framework presented in this paper simultaneously translates into important contributions in several directions. The most important practical contribution of this work is a full theoretical description, and implementation, of a novel powerful segmentation algorithm, GC(max). The output of GC(max) coincides with a version of a segmentation algorithm known as Iterative Relative Fuzzy Connectedness, IRFC. However, GC(max) is considerably faster than the classic IRFC algorithm, which we prove theoretically and show experimentally. Specifically, we prove that, in the worst case scenario, the GC(max) algorithm runs in linear time with respect to the variable M=|C|+|Z|, where |C| is the image scene size and |Z| is the size of the allowable range, Z, of the associated weight/affinity function. For most implementations, Z is identical to the set of allowable image intensity values, and its size can be treated as small with respect to |C|, meaning that O(M)=O(|C|). In such a situation, GC(max) runs in linear time with respect to the image size |C|. We show that the output of GC(max) constitutes a solution of a graph cut energy minimization problem, in which the energy is defined as the a"" (a) norm ayenF (P) ayen(a) of the map F (P) that associates, with every element e from the boundary of an object P, its weight w(e). This formulation brings IRFC algorithms to the realm of the graph cut energy minimizers, with energy functions ayenF (P) ayen (q) for qa[1,a]. Of these, the best known minimization problem is for the energy ayenF (P) ayen(1), which is solved by the classic min-cut/max-flow algorithm, referred to often as the Graph Cut algorithm. We notice that a minimization problem for ayenF (P) ayen (q) , qa[1,a), is identical to that for ayenF (P) ayen(1), when the original weight function w is replaced by w (q) . Thus, any algorithm GC(sum) solving the ayenF (P) ayen(1) minimization problem, solves also one for ayenF (P) ayen (q) with qa[1,a), so just two algorithms, GC(sum) and GC(max), are enough to solve all ayenF (P) ayen (q) -minimization problems. We also show that, for any fixed weight assignment, the solutions of the ayenF (P) ayen (q) -minimization problems converge to a solution of the ayenF (P) ayen(a)-minimization problem (ayenF (P) ayen(a)=lim (q -> a)ayenF (P) ayen (q) is not enough to deduce that). An experimental comparison of the performance of GC(max) and GC(sum) algorithms is included. This concentrates on comparing the actual (as opposed to provable worst scenario) algorithms' running time, as well as the influence of the choice of the seeds on the output.