Automatic verification of distributed logic specifications

Formal specification is vital to the development of distributed real-time systems as these systems are inherently complex and safety-critical. It is widely acknowledged that formal specification and automatic analysis of specifications can significantly increase system reliability. Although a number of specification techniques for real-time systems have been reported in the literature, most of these formalisms do not adequately address to the constraints that the aspects of 'distribution' and 'real-time' impose on specifications. Further, an automatic verification tool is necessary to reduce human errors in the reasoning process. In this regard, this paper is an attempt towards the development of a novel executable specification language for distributed real-time systems. First, we give a precise characterization of the syntax and semantics of DL. Subsequently, we discuss the problems of model checking, automatic verification of satisfiability of DL specifications, and testing conformance of event traces with DL specifications. Effective solutions to these problems are presented as extensions to the classical first-order tableau algorithm. The use of the proposed framework is illustrated by specifying a sample problem.

Robust/Optimal Temperature Profile Control of a High-Speed Aerospace Vehicle Using Neural Networks

An approximate dynamic programming (ADP)-based suboptimal neurocontroller to obtain desired temperature for a high-speed aerospace vehicle is synthesized in this paper. A I-D distributed parameter model of a fin is developed from basic thermal physics principles. "Snapshot" solutions of the dynamics are generated with a simple dynamic inversion-based feedback controller. Empirical basis functions are designed using the "proper orthogonal decomposition" (POD) technique and the snapshot solutions. A low-order nonlinear lumped parameter system to characterize the infinite dimensional system is obtained by carrying out a Galerkin projection. An ADP-based neurocontroller with a dual heuristic programming (DHP) formulation is obtained with a single-network-adaptive-critic (SNAC) controller for this approximate nonlinear model. Actual control in the original domain is calculated with the same POD basis functions through a reverse mapping. Further contribution of this paper includes development of an online robust neurocontroller to account for unmodeled dynamics and parametric uncertainties inherent in such a complex dynamic system. A neural network (NN) weight update rule that guarantees boundedness of the weights and relaxes the need for persistence of excitation (PE) condition is presented. Simulation studies show that in a fairly extensive but compact domain, any desired temperature profile can be achieved starting from any initial temperature profile. Therefore, the ADP and NN-based controllers appear to have the potential to become controller synthesis tools for nonlinear distributed parameter systems.

A Flat Concurrent Prolog compiler for PARAM

We describe a compiler for the Flat Concurrent Prolog language on a message passing multiprocessor architecture. This compiler permits symbolic and declarative programming in the syntax of Guarded Horn Rules, The implementation has been verified and tested on the 64-node PARAM parallel computer developed by C-DAC (Centre for the Development of Advanced Computing, India), Flat Concurrent Prolog (FCP) is a logic programming language designed for concurrent programming and parallel execution, It is a process oriented language, which embodies dataflow synchronization and guarded-command as its basic control mechanisms. An identical algorithm is executed on every processor in the network, We assume regular network topologies like mesh, ring, etc, Each node has a local memory, The algorithm comprises of two important parts: reduction and communication, The most difficult task is to integrate the solutions of problems that arise in the implementation in a coherent and efficient manner. We have tested the efficacy of the compiler on various benchmark problems of the ICOT project that have been reported in the recent book by Evan Tick, These problems include Quicksort, 8-queens, and Prime Number Generation, The results of the preliminary tests are favourable, We are currently examining issues like indexing and load balancing to further optimize our compiler.

Optimal management of beaver population using a reduced-order distributed parameter model and single network adaptive critics

Beavers are often found to be in conflict with human interests by creating nuisances like building dams on flowing water (leading to flooding), blocking irrigation canals, cutting down timbers, etc. At the same time they contribute to raising water tables, increased vegetation, etc. Consequently, maintaining an optimal beaver population is beneficial. Because of their diffusion externality (due to migratory nature), strategies based on lumped parameter models are often ineffective. Using a distributed parameter model for beaver population that accounts for their spatial and temporal behavior, an optimal control (trapping) strategy is presented in this paper that leads to a desired distribution of the animal density in a region in the long run. The optimal control solution presented, imbeds the solution for a large number of initial conditions (i.e., it has a feedback form), which is otherwise nontrivial to obtain. The solution obtained can be used in real-time by a nonexpert in control theory since it involves only using the neural networks trained offline. Proper orthogonal decomposition-based basis function design followed by their use in a Galerkin projection has been incorporated in the solution process as a model reduction technique. Optimal solutions are obtained through a "single network adaptive critic" (SNAC) neural-network architecture.

An optimal dynamic inversion approach for controlling a class of one-dimensional nonlinear distributed parameter systems

Combining the principles of dynamic inversion and optimization theory, a new approach is presented for stable control of a class of one-dimensional nonlinear distributed parameter systems, assuming the availability a continuous actuator in the spatial domain. Unlike the existing approximate-then-design and design-then-approximate techniques, here there is no need of any approximation either of the system dynamics or of the resulting controller. Rather, the control synthesis approach is fairly straight-forward and simple. The controller formulation has more elegance because we can prove the convergence of the controller to its steady state value. To demonstrate the potential of the proposed technique, a real-life temperature control problem for a heat transfer application is solved. It has been demonstrated that a desired temperature profile can be achieved starting from any arbitrary initial temperature profile.

Optimal control of arrivals to queues with delayed queue length information

We consider discrete-time versions of two classical problems in the optimal control of admission to a queueing system: i) optimal routing of arrivals to two parallel queues and ii) optimal acceptance/rejection of arrivals to a single queue. We extend the formulation of these problems to permit a k step delay in the observation of the queue lengths by the controller. For geometric inter-arrival times and geometric service times the problems are formulated as controlled Markov chains with expected total discounted cost as the minimization objective. For problem i) we show that when k = 1, the optimal policy is to allocate an arrival to the queue with the smaller expected queue length (JSEQ: Join the Shortest Expected Queue). We also show that for this problem, for k greater than or equal to 2, JSEQ is not optimal. For problem ii) we show that when k = 1, the optimal policy is a threshold policy. There are, however, two thresholds m(0) greater than or equal to m(1) > 0, such that mo is used when the previous action was to reject, and mi is used when the previous action was to accept.

Moving boundaries due to distributed sources in a slab

Analytical and numerical solutions have been obtained for some moving boundary problems associated with Joule heating and distributed absorption of oxygen in tissues. Several questions have been examined which are concerned with the solutions of classical formulation of sharp melting front model and the classical enthalpy formulation in which solid, liquid and mushy regions are present. Thermal properties and heat sources in the solid and liquid regions have been taken as unequal. The short-time analytical solutions presented here provide useful information. An effective numerical scheme has been proposed which is accurate and simple.

Modeling and control of unified power flow controller for transient stability

FACTS controllers are emerging as viable and economic solutions to the problems of large interconnected ne networks, which can endanger the system security. These devices are characterized by their fast response, absence of inertia, and minimum maintenance requirements. Thyristor controlled equipment like Thyristor Controlled Series Capacitor (TCSC), Static Var Compensator (SVC), Thyristor Controlled Phase angle Regulator (TCPR) etc. which involve passive elements result in devices of large sizes with substantial cost and significant labour for installation. An all solid-state device using GTOs leads to reduction in equipment size and has improved performance. The Unified Power Flow Controller (UPFC) is a versatile controller which can be used to control the active and reactive power in the Line independently. The concept of UPFC makes it possible to handle practically all power flow control and transmission line compensation problems, using solid-state controllers, which provide functional flexibility, generally not attainable by conventional thyristor controlled systems. In this paper, we present the development of a control scheme for the series injected voltage of the UPFC to damp the power oscillations and improve transient stability in a power system. (C) 1998 Elsevier Science Ltd. All rights reserved.

Throughput performance of distributed applications in switched networks in presence of end-system bottlenecks

The steady state throughput performance of distributed applications deployed in switched networks in presence of end-system bottlenecks is studied in this paper. The effect of various limitations at an end-system is modelled as an equivalent transmission capacity limitation. A class of distributed applications is characterised by a static traffic distribution matrix that determines the communication between various components of the application. It is found that uniqueness of steady state throughputs depends only on the traffic distribution matrix and that some applications (e.g., broadcast applications) can yield non-unique values for the steady state component throughputs. For a given switch capacity, with traffic distribution that yield fair unique throughputs, the trade-off between the end-system capacity and the number of application components is brought out. With a proposed distributed rate control, it has been illustrated that it is possible to have unique solution for certain traffic distributions which is otherwise impossible. Also, by proper selection of rate control parameters, various throughput performance objectives can be realised.

On the achievable rates of sources having a group alphabet in a distributed source coding setting

We consider the problem of compression via homomorphic encoding of a source having a group alphabet. This is motivated by the problem of distributed function computation, where it is known that if one is only interested in computing a function of several sources, then one can at times improve upon the compression rate required by the Slepian-Wolf bound. The functions of interest are those which could be represented by the binary operation in the group. We first consider the case when the source alphabet is the cyclic Abelian group, Zpr. In this scenario, we show that the set of achievable rates provided by Krithivasan and Pradhan [1], is indeed the best possible. In addition to that, we provide a simpler proof of their achievability result. In the case of a general Abelian group, an improved achievable rate region is presented than what was obtained by Krithivasan and Pradhan. We then consider the case when the source alphabet is a non-Abelian group. We show that if all the source symbols have non-zero probability and the center of the group is trivial, then it is impossible to compress such a source if one employs a homomorphic encoder. Finally, we present certain non-homomorphic encoders, which also are suitable in the context of function computation over non-Abelian group sources and provide rate regions achieved by these encoders.

Doubly spectral stochastic finite element method (DSSFEM) for random field problems

Uncertainties in complex dynamic systems play an important role in the prediction of a dynamic response in the mid- and high-frequency ranges. For distributed parameter systems, parametric uncertainties can be represented by random fields leading to stochastic partial differential equations. Over the past two decades, the spectral stochastic finite-element method has been developed to discretize the random fields and solve such problems. On the other hand, for deterministic distributed parameter linear dynamic systems, the spectral finite-element method has been developed to efficiently solve the problem in the frequency domain. In spite of the fact that both approaches use spectral decomposition (one for the random fields and the other for the dynamic displacement fields), very little overlap between them has been reported in literature. In this paper, these two spectral techniques are unified with the aim that the unified approach would outperform any of the spectral methods considered on their own. An exponential autocorrelation function for the random fields, a frequency-dependent stochastic element stiffness, and mass matrices are derived for the axial and bending vibration of rods. Closed-form exact expressions are derived by using the Karhunen-Loève expansion. Numerical examples are given to illustrate the unified spectral approach.

Viscoelastic phenomenology based structure assignment for closed-loop vibration control of a beam with sensors and actuators

In this paper we incorporate a novel approach to synthesize a class of closed-loop feedback control, based on the variational structure assignment. Properties of a viscoelastic system are used to design an active feedback controller for an undamped structural system with distributed sensor, actuator and controller. Wave dispersion properties of onedimensional beam system have been studied. Efficiency of the chosen viscoelastic model in enhancing damping and stability properties of one-dimensional viscoelastic bar have been analyzed. The variational structure is projected on a solution space of a closed-loop system involving a weakly damped structure with distributed sensor and actuator with controller. These assign the phenomenology based internal strain rate damping parameter of a viscoelastic system to the usual elastic structure but with active control. In the formulation a model of cantilever beam with non-collocated actuator and sensor has been considered. The formulation leads to the matrix identification problem of two dynamic stiffness matrices. The method has been simplified to obtain control system gains for the free vibration control of a cantilever beam system with collocated actuator-sensor, using quadratic optimal control and pole-placement methods.

Robustness Study of a Dynamic Inversion Control Law for a High Performance Aircraft

In the design of °ight control system modeling uncertainties in the form of param-eter variations is one of the major problems. It is even more critical for high performance aircrafts,since such aircrafts are purposefully designed unstable to enhance their performance (especially ma-neuverability). Hence the °ight control system needs to be quite e®ective in both assuring accurate tracking of pilot commands, while simultaneously assuring overall stability of the aircraft. In addi-tion, the control system must also be su±ciently robust to cater for possible parameter variations and inaccuracies . The primary aim of this paper is to carry out a robustness study of a dynamic inversion based nonlinear control design for a high performance aircraft, which has been developed recently [1].

Distributed Source Coding for Sensor Data Model and Estimation of Cluster Head Errors Using Bayesian and K-Near Neighborhood Classifiers in Deployment of Dense Wireless Sensor Networks

The lifetime calculation of large dense sensor networks with fixed energy resources and the remaining residual energy have shown that for a constant energy resource in a sensor network the fault rate at the cluster head is network size invariant when using the network layer with no MAC losses.Even after increasing the battery capacities in the nodes the total lifetime does not increase after a max limit of 8 times. As this is a serious limitation lots of research has been done at the MAC layer which allows to adapt to the specific connectivity, traffic and channel polling needs for sensor networks. There have been lots of MAC protocols which allow to control the channel polling of new radios which are available to sensor nodes to communicate. This further reduces the communication overhead by idling and sleep scheduling thus extending the lifetime of the monitoring application. We address the two issues which effects the distributed characteristics and performance of connected MAC nodes. (1) To determine the theoretical minimum rate based on joint coding for a correlated data source at the singlehop, (2a) to estimate cluster head errors using Bayesian rule for routing using persistence clustering when node densities are the same and stored using prior probability at the network layer, (2b) to estimate the upper bound of routing errors when using passive clustering were the node densities at the multi-hop MACS are unknown and not stored at the multi-hop nodes a priori. In this paper we evaluate many MAC based sensor network protocols and study the effects on sensor network lifetime. A renewable energy MAC routing protocol is designed when the probabilities of active nodes are not known a priori. From theoretical derivations we show that for a Bayesian rule with known class densities of omega1, omega2 with expected error P* is bounded by max error rate of P=2P* for single-hop. We study the effects of energy losses using cross-layer simulation of - large sensor network MACS setup, the error rate which effect finding sufficient node densities to have reliable multi-hop communications due to unknown node densities. The simulation results show that even though the lifetime is comparable the expected Bayesian posterior probability error bound is close or higher than Pges2P*.

Distributed load adaptive scheduling for throughput and delay guarantees in fading wireless LANs

We consider a problem of providing mean delay and average throughput guarantees in random access fading wireless channels using CSMA/CA algorithm. This problem becomes much more challenging when the scheduling is distributed as is the case in a typical local area wireless network. We model the CSMA network using a novel queueing network based approach. The optimal throughput per device and throughput optimal policy in an M device network is obtained. We provide a simple contention control algorithm that adapts the attempt probability based on the network load and obtain bounds for the packet transmission delay. The information we make use of is the number of devices in the network and the queue length (delayed) at each device. The proposed algorithms stay within the requirements of the IEEE 802.11 standard.