Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “logical reasoning”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

At least 91 records · Page 5

Approximate reasoning-based learning and control for proximity operations and docking in space

A recently proposed hybrid-neutral-network and fuzzy-logic-control architecture is applied to a fuzzy logic controller developed for attitude control of the Space Shuttle. A model using reinforcement learning and learning from past experience for fine-tuning its knowledge base is proposed. Two main components of this approximate reasoning-based intelligent control (ARIC) model - an action-state evaluation network and action selection network are described as well as the Space Shuttle attitude controller. An ARIC model for the controller is presented, and it is noted that the input layer in each network includes three nodes representing the angle error, angle error rate, and bias node. Preliminary results indicate that the controller can hold the pitch rate within its desired deadband and starts to use the jets at about 500 sec in the run.

Berenji, Hamid R.↗

Toward a formal verification of a floating-point coprocessor and its composition with a central processing unit

Discussed here is work to formally specify and verify a floating point coprocessor based on the MC68881. The HOL verification system developed at Cambridge University was used. The coprocessor consists of two independent units: the bus interface unit used to communicate with the cpu and the arithmetic processing unit used to perform the actual calculation. Reasoning about the interaction and synchronization among processes using higher order logic is demonstrated.

Pan, Jing↗

High level cognitive information processing in neural networks

Two related research efforts were addressed: (1) high-level connectionist cognitive modeling; and (2) local neural circuit modeling. The goals of the first effort were to develop connectionist models of high-level cognitive processes such as problem solving or natural language understanding, and to understand the computational requirements of such models. The goals of the second effort were to develop biologically-realistic model of local neural circuits, and to understand the computational behavior of such models. In keeping with the nature of NASA's Innovative Research Program, all the work conducted under the grant was highly innovative. For instance, the following ideas, all summarized, are contributions to the study of connectionist/neural networks: (1) the temporal-winner-take-all, relative-position encoding, and pattern-similarity association techniques; (2) the importation of logical combinators into connection; (3) the use of analogy-based reasoning as a bridge across the gap between the traditional symbolic paradigm and the connectionist paradigm; and (4) the application of connectionism to the domain of belief representation/reasoning. The work on local neural circuit modeling also departs significantly from the work of related researchers. In particular, its concentration on low-level neural phenomena that could support high-level cognitive processing is unusual within the area of biological local circuit modeling, and also serves to expand the horizons of the artificial neural net field.

Barnden, John A.↗

Space Research Project Management Can Benefit from Engineering Technology Selection Methods

Many engineering methods have been developed to help management select technology for a system design or further research. The simplest way to compare technologies is to use a checklist containing all the more or less important selection criteria, so that nothing is overlooked. The criteria usually include cost, safety, reliability and maintainability, and potential problems such as noise generation and microgravity sensitivity. The next step typically is to weight and score all the criteria. The process of weighting and scoring is helpful in bringing out different priorities and reaching a shared point of view. Group technology selection methods are designed to highlight initial disagreements and produce a shared consensus. Often a frank discussion led by management rather than decision analysts can be more effective. The final selection depends on management and engineering judgment and may include programmatic and organizational factors that are beyond the engineering checklist. The objective of engineering technology selection methods is to provide engineering information to assist management in making sound decisions. Project management and technology selection are assumed to use rational engineering analytic methods, but they often do not. The reason is that human insight, intuition, and “gut feel,” rather than logic, more frequently determine our decisions. Project selection and management are strongly influenced by nonrational psychological influences, which can produce unjustified confidence and determination. Nevertheless, there is a strong need for space projects to do rational project analysis and selection. Demonstrating a rational spirit is necessary for a scientific and technical organization. Professional ethics at its best requires an open, honest, and fair process, without damaging politics. Rational analysis can help improve good projects and avoid selecting bad ones. A sanity check using rational analysis guided by a checklist can help avoid egregious and damaging errors.

Jones, Harry W.↗

Reasoning by analogy as an aid to heuristic theorem proving.

When heuristic problem-solving programs are faced with large data bases that contain numbers of facts far in excess of those needed to solve any particular problem, their performance rapidly deteriorates. In this paper, the correspondence between a new unsolved problem and a previously solved analogous problem is computed and invoked to tailor large data bases to manageable sizes. This paper outlines the design of an algorithm for generating and exploiting analogies between theorems posed to a resolution-logic system. These algorithms are believed to be the first computationally feasible development of reasoning by analogy to be applied to heuristic theorem proving.

Kling, R. E.↗

ATS displays: A reasoning visualization tool for expert systems

Reasoning visualization is a useful tool that can help users better understand the inherently non-sequential logic of an expert system. While this is desirable in most all expert system applications, it is especially so for such critical systems as those destined for space-based operations. A hierarchical view of the expert system reasoning process and some characteristics of these various levels is presented. Also presented are Abstract Time Slice (ATS) displays, a tool to visualize the plethora of interrelated information available at the host inferencing language level of reasoning. The usefulness of this tool is illustrated with some examples from a prototype potable water expert system for possible use aboard Space Station Freedom.

Selig, William John↗

Fault-tolerance - The survival attribute of digital systems

Fault-tolerance is the architectural attribute of a digital system that keeps the logic machine doing its specified tasks when its host, the physical system, suffers various kinds of failures of its components. A more general concept of fault-tolerance also includes human mistakes committed during software and hardware implementation and during man/machine interaction among the causes of faults that are to be tolerated by the logic machine. This paper discusses the concept of fault-tolerance, the reasons for its inclusion in digital system architecture, and the methods of its implementation. A chronological view of the evolution of fault-tolerant systems and an outline of some goals for its further development conclude the presentation.

Avizienis, A.↗

Formal mechanization of device interactions with a process algebra

The principle emphasis is to develop a methodology to formally verify correct synchronization communication of devices in a composed hardware system. Previous system integration efforts have focused on vertical integration of one layer on top of another. This task examines 'horizontal' integration of peer devices. To formally reason about communication, we mechanize a process algebra in the Higher Order Logic (HOL) theorem proving system. Using this formalization we show how four types of device interactions can be represented and verified to behave as specified. The report also describes the specification of a system consisting of an AVM-1 microprocessor and a memory management unit which were verified in previous work. A proof of correct communication is presented, and the extensions to the system specification to add a direct memory device are discussed.

Schubert, E. Thomas↗

Developing Formal Correctness Properties from Natural Language Requirements

This viewgraph presentation reviews the rationale of the program to transform natural language specifications into formal notation.Specifically, automate generation of Linear Temporal Logic (LTL)correctness properties from natural language temporal specifications. There are several reasons for this approach (1) Model-based techniques becoming more widely accepted, (2) Analytical verification techniques (e.g., model checking, theorem proving) significantly more effective at detecting types of specification design errors (e.g., race conditions, deadlock) than manual inspection, (3) Many requirements still written in natural language, which results in a high learning curve for specification languages, associated tools and increased schedule and budget pressure on projects reduce training opportunities for engineers, and (4) Formulation of correctness properties for system models can be a difficult problem. This has relevance to NASA in that it would simplify development of formal correctness properties, lead to more widespread use of model-based specification, design techniques, assist in earlier identification of defects and reduce residual defect content for space mission software systems. The presentation also discusses: potential applications, accomplishments and/or technological transfer potential and the next steps.

requirements engineering↗

New lunar microcrater evidence against a time varying meteoroid flux

An attempt to measure the relative times of formation of 25 microcraters on lunar rock 60015 is discussed which was carried out as part of a study of the flux of interplanetary dust and possible time variations of that flux over periods of 1000 to 1 million yr. The data obtained could indicate that the formation rate of 100-micron-sized pits was lower in the past as compared with the formation rate of micron-sized pits, that the flux of particles forming 100-micron-sized pits may have varied relative to that of particles forming micron-sized pits, or that 100-micron-sized pits are forming now at a higher rate, relative to the formation rate of accretionary disks, than in the past. The last suggestion is shown to be almost untenable, and the overall results are found to lead to a logical paradox. It is concluded that the attempt probably failed and that the reason for failure raises serious questions regarding the use of lunar rock surfaces as meteoroid detectors.

Hartung, J. B.↗

LOX/Hydrocarbon Combustion Instability Investigation

The LOX/Hydrocarbon Combustion Instability Investigation Program was structured to determine if the use of light hydrocarbon combustion fuels with liquid oxygen (LOX) produces combustion performance and stability behavior similar to the LOX/hydrogen propellant combination. In particular methane was investigated to determine if that fuel can be rated for combustion instability using the same techniques as previously used for LOX/hydrogen. These techniques included fuel temperature ramping and stability bomb tests. The hot fire program probed the combustion behavior of methane from ambient to subambient temperatures. Very interesting results were obtained from this program that have potential importance to future LOX/methane development programs. A very thorough and carefully reasoned documentation of the experimental data obtained is contained. The hot fire test logic and the associated tests are discussed. Subscale performance and stability rating testing was accomplished using 40,000 lb. thrust class hardware. Stability rating tests used both bombs and fuel temperature ramping techniques. The test program was successful in generating data for the evaluation of the methane stability characteristics relative to hydrogen and to anchor stability models. Data correlations, performance analysis, stability analyses, and key stability margin enhancement parameters are discussed.

Jensen, R. J.↗

Envisioning a 21st Century, National, Spacecraft Servicing and Protection Infrastructure and Demand Potential: A Logical Development of the Earth Orbit Economy

The modern world is extremely dependent on thin strings of several hundred civil, military, and commercial spacecraft/satellites currently stationed in space. They provide a steady stream of commerce, defense, and knowledge data. This dependency will in all likelihood increase significantly during this century. A major disruption of any kind in these essential systems and networks could be socially, economically, and politically catastrophic, on a global scale. The development of a space-based, robotic services economy could be useful in mitigating this growing risk, from an efficiency and security standpoint. This paper attempts to suggest what makes sense to invest in next for the logical, economic development of Earth orbit i.e., after ISS completion. It expands on the results of an advanced market research and analysis study that sampled the opinions of several satellite industry executives and presents these results within a broad policy context. The concept of a spacecraft carrier that serves as the nucleus of a national, space-based or on-orbit, robotic services infrastructure is introduced as the next logical step for United States leadership in space. This is viewed as a reasonable and appropriate followon to the development of ELVs and satellites in the 1950s and 1960s, the Space Shuttle/PRLV in the 1970s and 1980s, and the International Space Station (ISS) in the 1980s, 1990s and 2000s. Large-scale experience in LEO-to-GEO spacecraft/satellite servicing and protection by robotic means is assumed to be an indispensable prerequisite or stepping-stone toward the development and preservation of the large scientific exploration facilities that are envisioned by NASA for operation beyond GEO. A balanced, return on national investment (RONI) strategy for space, focused on the provision of enhanced national/homeland security for increased protection, national economic/industrial expansion for increased revenue, and national scientific exploration for increased knowledge is recommended as the next strong, irrepressible goal toward realizing and achieving the official NASA vision and mission.

Horsham, Gary A.↗

R2U2 in Space: System and Software Health Management for Small Satellites

In order for small but complex systems like rovers, SmallSats, or Unmanned Aircraft (UAS) to operate autonomously, they must have a real-time solution for assessing their own system health. System and Software Health Management (SHM) enables better detection of faulty sensors and software problems, and enables better fault management including mitigation of unpredicted fault scenarios in the absence of a human on-board. In recent work, we have developed a Responsive, Realizable, Unobtrusive Unit (R2U2) for on-board SHM of autonomous UAS and demonstrated its ability to detect faults during flight time. These faults, from sensor failures, to software problems, to malicious security attacks, can present as transient temporal faults that even humans are challenged to find. An R2U2 congfiuration is a modular combination of multiple types of temporal logic runtime observers with fault-specic Bayesian Nets and sensor filters. R2U2 reasons about both on-board hardware and software components; R2U2 itself can be instantiated as an independent FPGA (Field-Programmable Gate Array)-based conguration or as a software component running independently from other software on-board. Small satellites, such as CubeSats, also require on-board SHM and failure mitigation, as limited telemetry bandwidth does not allow the transmission of the entire system state for ground-based health management. However, the autonomous operation of satellites brings a set of challenges different from UAS, including the effects of radiation on non-rad-hard, low-cost components, and the harsher environment of space. We surmise that a new extension of R2U2 could be adapted to help better detect, for example, radiation errors in cheaper COTS (Commercial Off the Shelf) (not rad-hard) components often used in small space systems. Since small satellites often operate in coordination, we will also examine new ways of distributed monitoring of their communication and cooperation and real-time detection of off-nominal situations utilizing multiple satellites. This talk will discuss preliminary work and ideas for building on terrestrial success of system and software health management for the harsher, and differently challenging, environment of space.

Runtime Verification & Validation↗

An experiment-based comparative study of fuzzy logic control

An approach is presented to the control of a dynamic physical system through the use of approximate reasoning. The approach has been implemented in a program named POLE, and the authors have successfully built a prototype hardware system to solve the cartpole balancing problem in real-time. The approach provides a complementary alternative to the conventional analytical control methodology and is of substantial use when a precise mathematical model of the process being controlled is not available. A set of criteria for comparing controllers based on approximate reasoning and those based on conventional control schemes is furnished.

Berenji, Hamid R.↗

The Moon as a way station for planetary exploration

The Moon can be on the pathway to the exploration of other planets in the solar system in three distinct ways: science, systems and technology experience, and as a fuel depot. The most important of these from the point of view of near term potential is to provide systems and technology development that increases capability and reduces the cost and risk of Mars exploration. The development of capability for a lunar program, if planned properly, can significantly influence strategies for sending humans to Mars. In conclusion, the exploration of the Moon should come before the exploration of Mars. This is a statement of developmental and operational logic that is almost self evident. Technological advancement could, however, make a different strategy reasonable. Principally, the development of a propulsion capability that could substantially reduce round trip mission times to Mars (to say 6 to 12 months) could eliminate much of the argument that the Moon is an essential stepping stone. This would reduce the problem to one of similitude with current space station program concepts. However, for any reasonably near term program, such technology does not appear likely to be available. Thus, the answer remains that lunar exploration should come first, and the expectation that it will make Mars exploration much more affordable and safe. The use of lunar propellant in an Earth-Mars transportation system is not practical with current propulsion systems; however, the discovery of caches of water ice at a lunar pole could change considerably the strategy for utilization of lunar resources in planetary exploration.

Duke, M. B.↗

DRS: Derivational Reasoning System

The high reliability requirements for airborne systems requires fault-tolerant architectures to address failures in the presence of physical faults, and the elimination of design flaws during the specification and validation phase of the design cycle. Although much progress has been made in developing methods to address physical faults, design flaws remain a serious problem. Formal methods provides a mathematical basis for removing design flaws from digital systems. DRS (Derivational Reasoning System) is a formal design tool based on advanced research in mathematical modeling and formal synthesis. The system implements a basic design algebra for synthesizing digital circuit descriptions from high level functional specifications. DRS incorporates an executable specification language, a set of correctness preserving transformations, verification interface, and a logic synthesis interface, making it a powerful tool for realizing hardware from abstract specifications. DRS integrates recent advances in transformational reasoning, automated theorem proving and high-level CAD synthesis systems in order to provide enhanced reliability in designs with reduced time and cost.

Bose, Bhaskar↗

A Constraint-based Attribute and Interval Planning

In this paper we introduce Constraint-based Attribute and Interval Planning (CAIP), a new paradigm for representing and reasoning about plans. The paradigm enables the description of planning domains with time, resources, concurrent activities, mutual exclusions among sets of activities, disjunctive preconditions and conditional effects. We provide a theoretical foundation for the paradigm using a mapping to first order logic. We also show that CAIP plans are naturally expressed by networks of constraints, and that planning maps directly to dynamic constraint reasoning. In addition, we show how constraint templates are used to provide a compact mechanism for describing planning domains.

Frank, Jeremy↗

Intelligent machines in the twenty-first century: foundations of inference and inquiry

The last century saw the application of Boolean algebra to the construction of computing machines, which work by applying logical transformations to information contained in their memory. The development of information theory and the generalization of Boolean algebra to Bayesian inference have enabled these computing machines, in the last quarter of the twentieth century, to be endowed with the ability to learn by making inferences from data. This revolution is just beginning as new computational techniques continue to make difficult problems more accessible. Recent advances in our understanding of the foundations of probability theory have revealed implications for areas other than logic. Of relevance to intelligent machines, we recently identified the algebra of questions as the free distributive algebra, which will now allow us to work with questions in a way analogous to that which Boolean algebra enables us to work with logical statements. In this paper, we examine the foundations of inference and inquiry. We begin with a history of inferential reasoning, highlighting key concepts that have led to the automation of inference in modern machine-learning systems. We then discuss the foundations of inference in more detail using a modern viewpoint that relies on the mathematics of partially ordered sets and the scaffolding of lattice theory. This new viewpoint allows us to develop the logic of inquiry and introduce a measure describing the relevance of a proposed question to an unresolved issue. Last, we will demonstrate the automation of inference, and discuss how this new logic of inquiry will enable intelligent machines to ask questions. Automation of both inference and inquiry promises to allow robots to perform science in the far reaches of our solar system and in other star systems by enabling them not only to make inferences from data, but also to decide which question to ask, which experiment to perform, or which measurement to take given what they have learned and what they are designed to understand.

Review↗