Computer Engineering Commons^™

Interval Methods: An Introduction, Luke Achenie, Vladik Kreinovich, Kaj Madsen

Departmental Technical Reports (CS)

The ongoing development of ever more advanced computers provides the potential for solving increasingly difficult computational problems. However, given the complexity of modern computer architectures, the task of realizing this potential needs careful attention. A main concern of High Performance Computing is the development of software that optimizes the performance of a given computer.

An important characteristic of the computer performance in scientific computing is the accuracy of the computation results. Often, we can estimate this accuracy by using traditional statistical techniques. However, in many practical situations, we do not know the probability distributions of different measurement, estimation, and/or roundoff …

Supporting Documentation For The Sps-Prospec Case Study, Salamah I. Salamah, Ann Q. Gates

Departmental Technical Reports (CS)

In this work, we report on the results of a case study comparing the correctness of Linear Temporal Logic (LTL)formulas generated by the Property Specification Tool Prospec and the Specification Pattern System (SPS). The report includes all the components used in the case study. In addition, this report provides a description of the use of the SPIN model checker to verify correctness of LTL specifications. Particularly, the report provides screenshots of XSPIN (SPIN�s graphical interface) and how properties (i.e., LTL formulas) can be specified and verified.

How To Reconstruct The Original Shape Of A Radar Signal?, Matthew G. Averill, Gang Xiang, Vladik Kreinovich, George R. Keller, Scott A. Starks, Patrick S. Debroux, James Boehm

Departmental Technical Reports (CS)

The shape of the radar signal can provide us with the additional information about the reflecting surface. However, to decrease the noise, radars use filtering, and filtering changes the shapes of the radar signal. It is therefore necessary to reconstruct the original shape of the radar signal.

Towards An Optimal Approach To Soft Constraint Problems, Martine Ceberio, Vladik Kreinovich

Departmental Technical Reports (CS)

In traditional constraint satisfaction, constraints are ``hard'' in the sense that we need to satisfy them all. In many practical situations, however, constraints are "soft" in the sense that if we are unable to satisfy some of them, the corresponding solution is still practically useful. In such situations, it is desirable to satisfy as many high-priority constraints as possible. In this paper, we describe an optimal algorithm for solving the corresponding soft constraint problem.

Nsf Advance: Institutional Transformation For Faculty Diversity - Faculty Worklife Survey Results, Manuela Romero, Ann Q. Gates

Departmental Technical Reports (CS)

The The University of Texas at El Paso (UTEP) received an NSF ADVANCE grant in October 2003 to create an initiative for institutional change with the goal of serving as a model for other institutions that desire to increase the representation and advancement of women, including underrepresented minorities, in academic science and engineering careers. In the first year of the grant, co-PI's Ann Gates and Patricia Witherspoon worked with the ADVANCE Program Evaluator, Manuela Romero, to create an instrument to survey faculty work life at UTEP. The instrument is based on the "Study of Faculty Work Life" survey instrument that …

Supporting Documentation For The 2003 Sps-Prospec Experiment, Oscar Mondragon, Salamah Salamah

Departmental Technical Reports (CS)

In spring of 2003 an empirical study was conducted to compare the effectiveness of the Prospec tool with the Specification Pattern System (SPS). The objective of the experiment was to determine the effect that Prospec and SPS have over the completeness and correctness of the generated software property specifications. The purpose of this document is to present the material that was used during the experiment, and to document how the classification of the patterns and scopes of each trial was validated.

A Contextual Interpretation Of Undefinedness For Runtime Assertion Checking, Yoonsik Cheon, Gary T. Leavens

Departmental Technical Reports (CS)

Runtime assertion checkers and static checking and verification tools must all cope with the well-known undefinedness problem of logic. This problem is particularly severe for runtime assertion checkers, since, in addition to the possibility of exceptions and errors, runtime assertion checkers must cope with non-executable expressions (such as certain quantified expressions). This paper describes how the runtime assertion checker of the Java Modeling Language (JML) copes with undefinedness. JML is interesting because it attempts to satisfy the needs of a wide range of tools; besides runtime assertion checking, these include static checking tools (like ESC/Java) and static verification tools. These …

Fast Algorithm For Computing The Upper Endpoint Of Sample Variance For Interval Data: Case Of Sufficiently Accurate Measurements, Gang Xiang

Departmental Technical Reports (CS)

When we have n results x1,...,xn of repeated measurement of the same quantity, the traditional statistical approach usually starts with computing their sample average E and their sample variance V. Often, due to the inevitable measurement uncertainty, we do not know the exact values of the quantities, we only know the intervals [xi] of possible values of xi. In such situations, for different possible values xi from [xi], we get different values of the variance. We must therefore find the range [V] of possible values of V. It is known that in general, this problem is NP-hard. For the case …

Specifying And Checking Method Call Sequences In Jml, Yoonsik Cheon, Ashaveena Perumandla

Departmental Technical Reports (CS)

In a pre- and post-conditions style specification, it is difficult to specify allowed sequences of method calls, often called protocols. However, the protocols are essential properties of reusable object-oriented classes and application frameworks, and the approaches based on the pre- and post-conditions, such as design by contracts (DBC) and formal behavioral interface specification languages (BISL), are being accepted as a practical and effective way of describing precise interfaces of (reusable) program modules. We propose a simple extension to JML, a BISL for Java, to specify protocol properties in an intuitive and concise manner. We also define a formal semantics of …

A Complete Automation Of Unit Testing For Java Programs, Yoonsik Cheon, Myoung Yee Kim, Ashaveena Perumandla

Departmental Technical Reports (CS)

Program testing is expensive and labor-intensive, often consuming more than half of the total development costs, and yet it is frequently not done well and the results are not always satisfactory. However, testing is the primary method to ensure that programs comply with requirements. We describe our on-going project that attempts to completely automate unit testing of object-oriented programs. Our project investigates the use of an evolutionary approach, called genetic algorithms, for the test data generation and the use of program specifications, written in JML, for the test result determination. A proof-of-concept tool has been implemented and shows that a …

On Inverse Halftoning: Computational Complexity And Interval Computations, Sergio D. Cabrera, K. Iyer, Gang Xiang, Vladik Kreinovich

Departmental Technical Reports (CS)

We analyze the problem of inverse half-toning. This problem is a particular case of a class of difficult-to-solve problems: inverse problems for reconstructing piece-wise smooth images. We show that this general problem is NP-hard. We also propose a new idea for solving problems of this type, including the inverse halftoning problem.

Exact Bounds For Interval And Fuzzy Functions Under Monotonicity Constraints, With Potential Applications To Biostratigraphy, Emil Platon, Kavitha Tupelly, Vladik Kreinovich, Scott A. Starks, Karen Villaverde

Departmental Technical Reports (CS)

The age of fossil species in samples recovered from a well that penetrates an undisturbed sequence of sedimentary rocks increases with depth. The results of biostratigraphic analysis of such a sequence consist of several age-depth values -- both known with interval (or fuzzy) uncertainty -- and we would like to find, for each possible depth, the interval of the possible values of the corresponding age. A similar problem of bounding an intervally (fuzzily) defined function under monotonicity constraint occurs in many other application areas. In this paper, we provide an efficient algorithm for solving this problem.

To Properly Reflect Physicists' Reasoning About Randomness, We Also Need A Maxitive (Possibility) Measure, Andrei M. Finkelstein, Olga Kosheleva, Vladik Kreinovich, Scott A. Starks, Hung T. Nguyen

Departmental Technical Reports (CS)

According to the traditional probability theory, events with a positive but very small probability can occur (although very rarely). For example, from the purely mathematical viewpoint, it is possible that the thermal motion of all the molecules in a coffee cup goes in the same direction, so this cup will start lifting up.

In contrast, physicists believe that events with extremely small probability cannot occur. In this paper, we show that to get a consistent formalization of this belief, we need, in addition to the original probability measure, to also consider a maxitive (possibility) measure.

A Universal Sensor Model, Valery Mazin, Vladik Kreinovich

Departmental Technical Reports (CS)

No abstract provided.

Towards Applying Computational Complexity To Foundations Of Physics, Vladik Kreinovich, Andrei Finkelstein

Departmental Technical Reports (CS)

In one of his early papers, D. Grigoriev analyzed the decidability and computational complexity of different physical theories. This analysis was motivated by the hope that this analysis would help physicists. In this paper, we survey several similar ideas that may be of help to physicists. We hope that further research may lead to useful physical applications.

The Multi-Layered Interval Categorizer Tesselation-Based Model, Marilton S. De Aguiar, Gracaliz P. Dimuro, Antonio C. Da Rocha Costa, Rafael K.S. Silva, Fabia A. Da Costa, Vladik Kreinovich

Departmental Technical Reports (CS)

No abstract provided.

Monte-Carlo-Type Techniques For Processing Interval Uncertainty, And Their Geophysical And Engineering Applications, Matthew G. Averill, Kate C. Miller, George R. Keller, Vladik Kreinovich, Jan Beck, Roberto Araiza, Roberto Torres, Scott A. Starks

Departmental Technical Reports (CS)

To determine the geophysical structure of a region, we measure seismic travel times and reconstruct velocities at different depths from this data. There are several algorithms for solving this inverse problem, but these algorithms do not tell us how accurate these reconstructions are.

Traditional approach to accuracy estimation assumes that the measurement errors are independently normally distributed. Problem: the resulting accuracies are not in line with geophysical intuition. Reason: a typical error is when we miss the first arrival of the seismic wave; it is not normal (bounded by the wave period T) and not independent.

Typically, all we know …

Advanced Relation Model For Genome Sequence Visualization (Arm 4 Gsv): Exploratory Visualization Examples, Brian J. D'Auriol, Kavitha Tupelly

Departmental Technical Reports (CS)

The Advanced Relation Model for Genome Sequence Visualization (ARM 4 GSV) is proposed in this paper. This model is adapted from an earlier visualization model which has been applied to the visualization of computer programs. A review of the fundamental model components of the earlier visualization model is given. Enhancements so as to make it applicable in genome visualization are discussed. As part of these enhancements, a relational characterization of genome sequences in terms of bases, codons, and patterns such as close inversions is developed and described. An adapted form of the Conceptual Crown Visualization (CCV) model, a part of …

Checking If There Exists A Monotonic Function That Is Consistent With The Measurements: An Efficient Algorithm, Kavitha Tupelly, Vladik Kreinovich, Karen Villaverde

Departmental Technical Reports (CS)

In many problems in science and engineering ranging from astrophysics to geosciences to financial analysis, we know that a physical quantity y depends on the physical quantity x, i.e., y=f(x) for some function f(x), and we want to check whether this dependence is monotonic. Specifically, finitely many measurements of xi and yi=f(xi) have been made, and we want to check whether the results of these measurements are consistent with the monotonicity of f. An efficient parallelizable algorithm is known for solving this problem when the values xi are known precisely, while the values yi are known with interval uncertainty. In …

Probabilistic Approach To Trust: Ideas, Algorithms, And Simulations, Pattama Jaksurat, Eric A. Freudenthal, Martine Ceberio, Vladik Kreinovich

Departmental Technical Reports (CS)

In traditional security systems, for each task, we either trust an agent or we don't. If we trust an agent, we allow this agent full access to this particular task. This agent can usually allow his trusted sub-agents the same access, etc. If a trust management system only uses "trust" and "no trust" options, then a person should trust everyone in this potentially long chain. The problem is that trust is rarely a complete trust, there is a certain probability of distrust. So, when the chain becomes long, the probability of a security leak increases. It is desirable to keep …

Computing The Cube Of An Interval Matrix Is Np-Hard, Olga Kosheleva, Vladik Kreinovich, Guenter Mayer, Hung T. Nguyen

Departmental Technical Reports (CS)

In many practical applications, we are interested in computing the product of given matrices and/or a power of a given matrix. In some cases, the initial matrices are only known with interval uncertainty. It turns out that under this uncertainty, there is a principal difference between the product of two matrices and the product of three (or more) matrices:

on the one hand, it is more or less known that the problems of computing the exact range for the product of two matrices -- and for the square of a matrix -- are computationally feasible;

on the other hand, we …

Foundations Of Statistical Processing Of Set-Valued Data: Towards Efficient Algorithms, Hung T. Nguyen, Vladik Kreinovich, Gang Xiang

Departmental Technical Reports (CS)

Due to measurement uncertainty, often, instead of the actual values xi of the measured quantities, we only know the intervals [Xi]=[Xi-Di,Xi+Di], where Xi is the measured value and Di is the upper bound on the measurement error (provided, e.g., by the manufacturer of the measuring instrument). These intervals can be viewed as random intervals, i.e., as samples from the interval-valued random variable. In such situations, instead of the exact value of a sample statistic such as covariance C(x,y), we can only have an interval [C](x,y) of possible values of this statistic.

In this paper, we extend the foundations of traditional …

Convergence Properties Of An Interval Probabilistic Approach To System Reliability Estimation, Cliff Joslyn, Vladik Kreinovich

Departmental Technical Reports (CS)

Based on a black box model of a complex system, and on intervals and probabilities describing the known information about the inputs, we want to estimate the system's reliability. Using the results of tests performed on the system's computer model, we can estimate the lower and upper bounds of the probability that the system is in a desirable state. In this paper, we prove that these estimates are correct in the sense that under reasonable assumptions, these estimates converge to the actual probability bounds.

A Model Of Computer Science Graduate Admissions Decisions, Nigel Ward

Departmental Technical Reports (CS)

Potential applicants to graduate school find it difficult to predict, even approximately, which schools will accept them. We have created a predictive model of admissions decision-making, packaged in the form of a web page that allows students to enter their information and see a list of schools where they are likely to be accepted. This paper discusses the design of the model and the way its parameters were estimated. Interesting points include the way that weights are assigned dynamically to various factors based on the informativeness of each factor and on the applicant's relative strengths on each factor.

Exact Bounds On Finite Populations Of Interval Data, Scott Ferson, Lev Ginzburg, Vladik Kreinovich, Luc Longpre, Monica Aviles

Departmental Technical Reports (CS)

In this paper, we start research into using intervals to bound the impact of bounded measurement errors on the computation of bounds on finite population parameters ("descriptive statistics"). Specifically, we provide a feasible (quadratic time) algorithm for computing the lower bound on the finite population variance function of interval data. We prove that the problem of computing the upper bound on the finite population variance function of interval data is, in general, NP-hard. We provide a feasible algorithm that computes this upper bound under reasonable easily verifiable conditions, and provide preliminary results on computing other functions of finite populations.

Generating Properties For Runtime Monitoring From Software Specification Patterns, Oscar Mondragon, Ann Q. Gates, Oleg Sokolsky

Departmental Technical Reports (CS)

The paper presents an approach to support run-time verification of software systems that combines two existing tools, Prospec and Java-MaC, into a single framework. Prospec can be used to clarify natural language specifications for sequential, concurrent, and nondeterministic behavior. In addition, the tool assists the user in reading, writing, and understanding formal specifications through the use of property patterns and visual abstractions. Currently, Prospec automatically generates a specification written in Future Interval Logic (FIL). The goal is to automate the generation of MEDL formulas that can be used by the Java-MaC tool to check run-time compliance of system execution to …

Non-Lexical Conversational Sounds In American English, Nigel Ward

Departmental Technical Reports (CS)

This article analyzes the non-lexical conversational sounds (conversational grunts) of English, including such items as uh-huh, un-hn, um, mm, and oh, based primarily on examination of a few hundred occurrences in a corpus of conversations. The data includes extensive phonetic variation, suggesting that these items are best explained, not as fixed words, but as dynamic creations. In particular, the vast majority of these items can be generated by a simple model consisting of 10 component sounds and 2 combining rules. Moreover, each of these component sounds seems to bear some meaning or function which is fairly constant across grunts and …

Beyond Convex? Global Optimization Is Feasible Only For Convex Objective Functions: A Theorem, R. Baker Kearfott, Vladik Kreinovich

Departmental Technical Reports (CS)

It is known that there are feasible algorithms for minimizing convex functions, and that for general functions, global minimization is a difficult (NP-hard) problem. It is reasonable to ask whether there exists a class of functions that is larger than the class of all convex functions for which we can still solve the corresponding minimization problems feasibly. In this paper, we prove, in essence, that no such more general class exists. In other words, we prove that global optimization is always feasible only for convex objective functions.

Optimal Finite Characterization Of Linear Problems With Inexact Data, Vladik Kreinovich

Departmental Technical Reports (CS)

For many linear problems, in order to check whether a certain property is true for all matrices A from an interval matrix [A], it is sufficient to check this property for finitely many "vertex" matrices. J. Rohn has discovered that we do not need to use all 2^(n^2) vertex matrices, it is sufficient to only check these properties for 2^(2n-1)<<2^(n^2) vertex matrices of a special type A_{yz}. In this paper, we show that a further reduction is impossible: without checking all 2^(2n-1) matrices A_{yz}, we cannot guarantee that the desired property holds for all A from [A]. Thus, these special vertex matrices provide an optimal finite characterization of linear problems with inexact data.

Outlier Detection Under Interval Uncertainty: Algorithmic Solvability And Computational Complexity, Vladik Kreinovich, Luc Longpre, Praveen Patangay, Scott Ferson, Lev Ginzburg

Departmental Technical Reports (CS)

In many application areas, it is important to detect outliers. Traditional engineering approach to outlier detection is that we start with some "normal" values x1,...,xn, compute the sample average E, the sample standard variation sigma, and then mark a value x as an outlier if x is outside the k0-sigma interval [E-k0*sigma,E+k0*sigma] (for some pre-selected parameter k0). In real life, we often have only interval ranges [xi] for the normal values x1,...,xn. In this case, we only have intervals of possible values for the bounds E-k0*sigma and E+k0*sigma. We can therefore identify outliers as values that are outside all k0-sigma …