On-demand strategy annotations revisited: An improved on-demand evaluation strategy

In functional languages such as OBJ*, CafeOBJ, and Maude, symbols are given strategy annotations that specify (the order in) which subterms are evaluated. Syntactically, strategy annotations are given either as lists of natural numbers or as lists of integers associated to function symbols whose (absolute) values refer to the arguments of the corresponding symbol. A positive index prescribes the evaluation of an argument whereas a negative index means “evaluation on-demand”. These on-demand indices have been proposed to support laziness in OBJ-like languages. While strategy annotations containing only natural numbers have been implemented and investigated to some extent (regarding, for example, termination, confluence, and completeness), fully general annotations (including positive and negative indices) have been disappointingly under-explored to date.In this paper, we first point out a number of problems of current proposals for handling on-demand strategy annotations. Then, we propose a solution to these problems by keeping an accurate track of annotations along the evaluation sequences. We formalize this solution as a suitable extension of the evaluation strategy of OBJ-like languages (which only consider annotations given as natural numbers) to on-demand strategy annotations. Our on-demand evaluation strategy (ODE) overcomes the drawbacks of previous proposals and also has better computational properties. For instance, we show how to use this strategy for computing (head-)normal forms. We also introduce a transformation which allows us to prove the termination of the new evaluation strategy by using standard rewriting techniques. Finally, we present two interpreters of the new strategy together with some encouraging experiments which demonstrate the usefulness of our approach.     

ML-KNN: A lazy learning approach to multi-label learning

Multi-label learning originated from the investigation of text categorization problem, where each document may belong to several predefined topics simultaneously. In multi-label learning, the training set is composed of instances each associated with a set of labels, and the task is to predict the label sets of unseen instances through analyzing training instances with known label sets. In this paper, a multi-label lazy learning approach named ML-KNN is presented, which is derived from the traditional K-nearest neighbor (KNN) algorithm. In detail, for each unseen instance, its K nearest neighbors in the training set are firstly identified. After that, based on statistical information gained from the label sets of these neighboring instances, i.e. the number of neighboring instances belonging to each possible class, maximum a posteriori (MAP) principle is utilized to determine the label set for the unseen instance. Experiments on three different real-world multi-label learning problems, i.e. Yeast gene functional analysis, natural scene classification and automatic web page categorization, show that ML-KNN achieves superior performance to some well-established multi-label learning algorithms.     

Deadlock and starvation free reentrant readers-writers: A case study combining model checking with theorem proving

The classic readers-writers problem has been extensively studied. This holds to a lesser degree for the reentrant version, where it is allowed to nest locking actions. Such nesting is useful when a library is created with various procedures each starting and ending with a lock operation. Allowing nesting makes it possible for these procedures to call each other.We considered an existing widely used industrial implementation of the reentrant readers-writers problem. Staying close to the original code, we modelled and analyzed it using a model checker resulting in the detection of a serious error: a possible deadlock situation. The model was improved and checked satisfactorily for a fixed number of processes. To achieve a correctness result for an arbitrary number of processes the model was converted to a specification that was proven with a theorem prover. Furthermore, we studied starvation. Using model checking we found a starvation problem. We have fixed the problem and checked the solution. Combining model checking with theorem proving appeared to be very effective in reducing the time of the verification process.     

ADF95: Tool for automatic differentiation of a FORTRAN code designed for large numbers of independent variables

ADF95 is a tool to automatically calculate numerical first derivatives for any mathematical expression as a function of user defined independent variables. Accuracy of derivatives is achieved within machine precision. ADF95 may be applied to any FORTRAN 77/90/95 conforming code and requires minimal changes by the user. It provides a new derived data type that holds the value and derivatives and applies forward differencing by overloading all FORTRAN operators and intrinsic functions. An efficient indexing technique leads to a reduced memory usage and a substantially increased performance gain over other available tools with operator overloading. This gain is especially pronounced for sparse systems with large number of independent variables. A wide class of numerical simulations, e.g., those employing implicit solvers, can profit from ADF95.

Program summary

Title of program:ADF95Catalogue identifier: ADVIProgram summary URL:http://cpc.cs.qub.ac.uk/summaries/ADVIProgram obtainable from: CPC Program Library, Queen's University of Belfast, N. IrelandComputer for which the program is designed: all platforms with a FORTRAN 95 compilerProgramming language used:FORTRAN 95No. of lines in distributed program, including test data, etc.: 3103No. of bytes in distributed program, including test data, etc.: 9862Distribution format: tar.gzNature of problem: In many areas in the computational sciences first order partial derivatives for large and complex sets of equations are needed with machine precision accuracy. For example, any implicit or semi-implicit solver requires the computation of the Jacobian matrix, which contains the first derivatives with respect to the independent variables. ADF95 is a software module to facilitate the automatic computation of the first partial derivatives of any arbitrarily complex mathematical FORTRAN expression. The program exploits the sparsity inherited by many set of equations thereby enabling faster computations compared to alternate differentiation toolsSolution method: A class is constructed which applies the chain rule of differentiation to any FORTRAN expression, to compute the first derivatives by forward differencing. An efficient indexing technique leads to a reduced memory usage and a substantially increased performance gain when sparsity can be exploited. From a users point of view, only minimal changes to his/her original code are needed in order to compute the first derivatives of any expression in the codeRestrictions: Processor and memory hardware may restrict both the possible number of independent variables and the computation timeUnusual features:ADF95 can operate on user code that makes use of the array features introduced in FORTRAN 90. A convenient extraction subroutine for the Jacobian matrix is also providedRunning time: In many realistic cases, the evaluation of the first order derivatives of a mathematical expression is only six times slower compared to the evaluation of analytically derived and hard-coded expressions. The actual factor depends on the underlying set of equations for which derivatives are to be calculated, the number of independent variables, the sparsity and on the FORTRAN 95 compiler     

A tracking problem for mechanical systems with delay in control

A problem of tracking for mechanical systems described by nonstationary nonlinear equations is studied at relay control with delay is studied. An approach that makes it possible to solve problems of tracking for mechanical systems whose parameters may continuously vary with time is developed. This approach is based on the transformation of the system and construction of a Lyapunov vector-function with components of the form of vector norm.     

A perspective on service orchestration

Service-oriented computing is an emerging paradigm with increasing impact on the way modern software systems are designed and developed. Services are autonomous, loosely coupled and heterogeneous computational entities able to cooperate to achieve common goals. This paper introduces a model for service orchestration, which combines a exogenous coordination model, with services’ interfaces annotated with behavioural patterns specified in a process algebra which is parametric on the interaction discipline. The coordination model is a variant of Reo for which a new semantic model is proposed.     

A stochastic estimation problem at aeromagnetometer deviation compensation

A formulation of the problem of magnitometer deviation compensation occurring at aeromagnetic survey is considered in the form of a standard stochastic estimation problem. A specific feature of this approach is the introduction of the model of a geomagnetic field anomaly. The parameters of the stochastic model are selected basing on spectral and variance analysis of the aeromagnetic survey data. Normalization of the problem parameters is made; this makes it possible to estimate the accuracy of compensation and conduct a necessary decomposition. The posed stochastic estimation problem is solved by the method of Kalman filtering.     

Nonlinear parity relations: A logic-dynamic approach

Consideration was given to construction of the parity relations for systems described by the nonlinear dynamic models. To solve this problem, a logic-dynamic approach was proposed, and the realizability conditions providing insensitivity to the perturbing actions were given for it.     

Invariance for impulsive control systems

The conventional concepts of invariance are extended in this article to include impulsive control systems represented by measure driven differential inclusions. Invariance conditions and some of their main features are derived. The solution concept plays a critical role in the extension of the conditions for conventional problems to the impulsive control context.     

Two strong equilibria for game problems

The paper presents two new definitions of equilibrium for arbitrary game problems. The new definitions allow finding a unique solution for a significantly wider class of problems.     

Algorithm of multithreshold decoding for Gaussian channels

Major principles of the method of the linear codes multithreshhold decoding as search for the global functional extremum for a great number of variables are considered. It was demonstrated that the multithreshold decoding efficiency is close to the results ensured by the optimum exhaustive search methods. Decoding complexity under software and hardware realizations is evaluated.     

Conditional variational problems of control for distributed-parameter systems

Solved was a number of the classical variational problems of control of the distributed-parameter dynamic systems constrained also by nondifferential and differential equations. The corresponding rules of the Lagrange multipliers were formulated and proved. For the generalized diffusion and generalized wave processes, the results obtained were applied to the conditional variational problems of distributed optimal control. Derivation of the Euler-Poisson and Euler equations as applied to the designed control system was substantiated for these problems.     

Design of robust stable controls for nonlinear objects

We consider a problem of discrete control for a class of nonlinear time-varying objects. Only set estimations for object parameters are available. The aim is to design controls that ensure robust stability of closed-loop systems in a given domain of state space. Since the considered class of objects is large enough not to have a stabilizing control, the proposed design method has to verify at the last step if the obtained conditions of robust stability are satisfied for a nonlinear system “in a given domain.”     

Optimal multilevel organizations for the power cost functions

The problem of maximizing the profit of an economic organization with simultaneous selection of its composition and structure was formulated. Consideration was given to a class of the power cost functions whose parameters reflect the organization environmental characteristics. The optimal organization was analytically established for this case, and the regularities of its variation vs. the environmental conditions were investigated.     

Pontryagin principle of maximum for the quantum problem of speed

The Pontryagin principle of maximum as originally formulated for the classical dynamic systems, was extended to the quantum systems with a finite number of states of the discrete spectrum. The principle was derived on the basis of equivalence of the matrix representation of the Schrödinger equation to the system of ordinary differential equations. An example of the problem of speed for generation of the given-structure wave package was considered.     

Boolean models and planning methods for parallel abstract programs

For the parallel computer systems, a new formulation of the problem of constructing parallel asynchronous abstract programs of the desired length was proposed. The conditions for the problem of planning were represented as a system of Boolean equations (constraints) whose solutions define the feasible plans for activation of the program modules specified in the planner’s knowledge base. The constraints on the number of processors and time delays arising at execution of the program modules were taken into consideration.     

Topological method for analysis of periodic canards

Singularly perturbed systems of ordinary differential equations are studied. A method for analysis of canard-type trajectories in such systems based on the topological degree theory is suggested. The method does not require smoothness of the right-hand side of the system. A result on the existence of periodic canards in systems with non-smooth perturbations is obtained. The trajectories located in this way are not necessarily Lyapunov stable, and appropriate control algorithms are required to stabilize them, e.g., feedback control.