Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “symbolic”

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 109 records · Page 6

Use of symbolic computation in robotics education

An application of symbolic computation in robotics education is described. A software package is presented which combines generality, user interaction, and user-friendliness with the systematic usage of symbolic computation and artificial intelligence techniques. The software utilizes MACSYMA, a LISP-based symbolic algebra language, to automatically generate closed-form expressions representing forward and inverse kinematics solutions, the Jacobian transformation matrices, robot pose error-compensation models equations, and Lagrange dynamics formulation for N degree-of-freedom, open chain robotic manipulators. The goal of such a package is to aid faculty and students in the robotics course by removing burdensome tasks of mathematical manipulations. The software package has been successfully tested for its accuracy using commercially available robots.

Vira, Naren↗

Slew Timer For Symbol Display Generator

Slew-length timer generates delay and, at end of delay, signal indicating end of one of slews of electron beam in cathode-ray-tube display driven by symbol generator. End-of-slew signal constitutes "permission" for symbol generator to begin drawing next symbol segment.

Fisher, Paul A.↗

Symbolic discrete event system specification

Extending discrete event modeling formalisms to facilitate greater symbol manipulation capabilities is important to further their use in intelligent control and design of high autonomy systems. An extension to the DEVS formalism that facilitates symbolic expression of event times by extending the time base from the real numbers to the field of linear polynomials over the reals is defined. A simulation algorithm is developed to generate the branching trajectories resulting from the underlying nondeterminism. To efficiently manage symbolic constraints, a consistency checking algorithm for linear polynomial constraints based on feasibility checking algorithms borrowed from linear programming has been developed. The extended formalism offers a convenient means to conduct multiple, simultaneous explorations of model behaviors. Examples of application are given with concentration on fault model analysis.

Zeigler, Bernard P.↗

Multiple-Symbol, Partially Coherent Detection of MPSK

Proposed method of reception of multiple-phase-shift-keyed (MPSK) radio signals involves multiple-symbol, partially coherent detection. Instead of attempting to determine phase of transmitted signal during each symbol period as in coherent detection, receiver acquires signal data during multiple-symbol observation interval, then produces maximum-likelihood-sequence estimate of phases transmitted during interval. Combination of coherent-reception and incoherent-reception decision rules are used.

Simon, Marvin K.↗

Symbolic Computational Approach to the Marangoni Convection Problem With Soret Diffusion

A recently reported solution for stationary stability of a thermosolutal system with Soret diffusion is re-derived and examined using a symbolic computational package. Symbolic computational languages are well suited for such an analysis and facilitate a pragmatic approach that is adaptable to similar problems. Linearization of the equations, normal mode analysis, and extraction of the final solution are performed in a Mathematica notebook format. An exact solution is obtained for stationary stability in the limit of zero gravity. A closed form expression is also obtained for the location of asymptotes in relevant parameter, (Sm(sub c), Mac(sub c)), space. The stationary stability behavior is conveniently examined within the symbolic language environment. An abbreviated version of the Mathematica notebook is given in the Appendix.

Skarda, J. Raymond↗

Combining Automated Theorem Provers with Symbolic Algebraic Systems: Position Paper

In contrast to pure mathematical applications where automated theorem provers (ATPs) are quite capable, proof tasks arising form real-world applications from the area of Software Engineering show quite different characteristics: they usually do not only contain much arithmetic (albeit often quite simple one), but they also often contain reasoning about specific structures (e.g. graphics, sets). Thus, an ATP must be capable of performing reasoning together with a fair amount of simplification, calculation and solving. Therefore, powerful simplifiers and other (symbolic and semi-symbolic) algorithms seem to be ideally suited to augment ATPs. In the following we shortly describe two major points of interest in combining SASs (symbolic algebraic systems) with top-down automated theorem provers (here: SETHEO [Let92, GLMS94]).

Schumann, Johann↗

Practical Formal Verification of Diagnosability of Large Models via Symbolic Model Checking

This document reports on the activities carried out during a four-week visit of Roberto Cavada at the NASA Ames Research Center. The main goal was to test the practical applicability of the framework proposed, where a diagnosability problem is reduced to a Symbolic Model Checking problem. Section 2 contains a brief explanation of major techniques currently used in Symbolic Model Checking, and how these techniques can be tuned in order to obtain good performances when using Model Checking tools. Diagnosability is performed on large and structured models of real plants. Section 3 describes how these plants are modeled, and how models can be simplified to improve the performance of Symbolic Model Checkers. Section 4 reports scalability results. Three test cases are briefly presented, and several parameters and techniques have been applied on those test cases in order to produce comparison tables. Furthermore, comparison between several Model Checkers is reported. Section 5 summarizes the application of diagnosability verification to a real application. Several properties have been tested, and results have been highlighted. Finally, section 6 draws some conclusions, and outlines future lines of research.

Cavada, Roberto↗

Multiple Layer Identification Label Using Stacked Identification Symbols

An automatic identification system and method are provided which employ a machine readable multiple layer label. The label has a plurality of machine readable marking layers stacked one upon another. Each of the marking layers encodes an identification symbol detectable using one or more sensing technologies. The various marking layers may comprise the same marking material or each marking layer may comprise a different medium having characteristics detectable by a different sensing technology. These sensing technologies include x-ray, radar, capacitance, thermal, magnetic and ultrasonic. A complete symbol may be encoded within each marking layer or a symbol may be segmented into fragments which are then divided within a single marking layer or encoded across multiple marking layers.

Harry F Schramm↗

Multiple layer identification label using stacked identification symbols

An automatic identification system and method are provided which employ a machine readable multiple layer label. The label has a plurality of machine readable marking layers stacked one upon another. Each of the marking layers encodes an identification symbol detectable using one or more sensing technologies. The various marking layers may comprise the same marking material or each marking layer may comprise a different medium having characteristics detectable by a different sensing technology. These sensing technologies include x-ray, radar, capacitance, thermal, magnetic and ultrasonic. A complete symbol may be encoded within each marking layer or a symbol may be segmented into fragments which are then divided within a single marking layer or encoded across multiple marking layers.

Schramm, Harry F.↗

Using LDPC Code Constraints to Aid Recovery of Symbol Timing

A method of utilizing information available in the constraints imposed by a low-density parity-check (LDPC) code has been proposed as a means of aiding the recovery of symbol timing in the reception of a binary-phase-shift-keying (BPSK) signal representing such a code in the presence of noise, timing error, and/or Doppler shift between the transmitter and the receiver. This method and the receiver architecture in which it would be implemented belong to a class of timing-recovery methods and corresponding receiver architectures characterized as pilotless in that they do not require transmission and reception of pilot signals. Acquisition and tracking of a signal of the type described above have traditionally been performed upstream of, and independently of, decoding and have typically involved utilization of a phase-locked loop (PLL). However, the LDPC decoding process, which is iterative, provides information that can be fed back to the timing-recovery receiver circuits to improve performance significantly over that attainable in the absence of such feedback. Prior methods of coupling LDPC decoding with timing recovery had focused on the use of output code words produced as the iterations progress. In contrast, in the present method, one exploits the information available from the metrics computed for the constraint nodes of an LDPC code during the decoding process. In addition, the method involves the use of a waveform model that captures, better than do the waveform models of the prior methods, distortions introduced by receiver timing errors and transmitter/ receiver motions. An LDPC code is commonly represented by use of a bipartite graph containing two sets of nodes. In the graph corresponding to an (n,k) code, the n variable nodes correspond to the code word symbols and the n-k constraint nodes represent the constraints that the code places on the variable nodes in order for them to form a valid code word. The decoding procedure involves iterative computation of values associated with these nodes. A constraint node represents a parity-check equation using a set of variable nodes as inputs. A valid decoded code word is obtained if all parity-check equations are satisfied. After each iteration, the metrics associated with each constraint node can be evaluated to determine the status of the associated parity check. Heretofore, normally, these metrics would be utilized only within the LDPC decoding process to assess whether or not variable nodes had converged to a codeword. In the present method, it is recognized that these metrics can be used to determine accuracy of the timing estimates used in acquiring the sampled data that constitute the input to the LDPC decoder. In fact, the number of constraints that are satisfied exhibits a peak near the optimal timing estimate. Coarse timing estimation (or first-stage estimation as described below) is found via a parametric search for this peak. The present method calls for a two-stage receiver architecture illustrated in the figure. The first stage would correct large time delays and frequency offsets; the second stage would track random walks and correct residual time and frequency offsets. In the first stage, constraint-node feedback from the LDPC decoder would be employed in a search algorithm in which the searches would be performed in successively narrower windows to find the correct time delay and/or frequency offset. The second stage would include a conventional first-order PLL with a decision-aided timing-error detector that would utilize, as its decision aid, decoded symbols from the LDPC decoder. The method has been tested by means of computational simulations in cases involving various timing and frequency errors. The results of the simulations ined in the ideal case of perfect timing in the receiver.

Jones, Christopher↗

Inter-Symbol Guard Time for Synchronizing Optical PPM

An inter-symbol guard time has been proposed as a means of synchronizing the symbol and slot clocks of an optical pulse-position modulation (PPM) receiver with the symbol and slot periods of an incoming optical PPM signal.The proposal is applicable to the low-flux case in which the receiver photodetector operates in a photon-counting mode and the count can include contributions from incidental light sources and dark current.

Far, William↗

Fusing Symbolic and Numerical Diagnostic Computations

X-2000 Anomaly Detection Language denotes a developmental computing language, and the software that establishes and utilizes the language, for fusing two diagnostic computer programs, one implementing a numerical analysis method, the other implementing a symbolic analysis method into a unified event-based decision analysis software system for realtime detection of events (e.g., failures) in a spacecraft, aircraft, or other complex engineering system. The numerical analysis method is performed by beacon-based exception analysis for multi-missions (BEAMs), which has been discussed in several previous NASA Tech Briefs articles. The symbolic analysis method is, more specifically, an artificial-intelligence method of the knowledge-based, inference engine type, and its implementation is exemplified by the Spacecraft Health Inference Engine (SHINE) software. The goal in developing the capability to fuse numerical and symbolic diagnostic components is to increase the depth of analysis beyond that previously attainable, thereby increasing the degree of confidence in the computed results. In practical terms, the sought improvement is to enable detection of all or most events, with no or few false alarms.

James, Mark↗

A Comparative Study of Randomized Constraint Solvers for Random-Symbolic Testing

The complexity of constraints is a major obstacle for constraint-based software verification. Automatic constraint solvers are fundamentally incomplete: input constraints often build on some undecidable theory or some theory the solver does not support. This paper proposes and evaluates several randomized solvers to address this issue. We compare the effectiveness of a symbolic solver (CVC3), a random solver, three hybrid solvers (i.e., mix of random and symbolic), and two heuristic search solvers. We evaluate the solvers on two benchmarks: one consisting of manually generated constraints and another generated with a concolic execution of 8 subjects. In addition to fully decidable constraints, the benchmarks include constraints with non-linear integer arithmetic, integer modulo and division, bitwise arithmetic, and floating-point arithmetic. As expected symbolic solving (in particular, CVC3) subsumes the other solvers for the concolic execution of subjects that only generate decidable constraints. For the remaining subjects the solvers are complementary.

Takaki, Mitsuo↗

Maximum Likelihood Synchronization for Pulse Position Modulation with Inter-Symbol Guard Times

Deep space optical communications promises orders-of-magnitude growth in communication capacity, supporting high data rate applications such as video streaming and high-bandwidth science instruments. Pulse position modulation is the modulation format of choice for deep space applications, and by inserting inter-symbol guard times between the symbols, the signal carries the timing information needed by the demodulator. Accurately extracting this timing information is crucial to demodulating and decoding this signal. In this paper we propose a low complexity maximum likelihood timing estimator for pulse position modulation with inter-symbol guard times which significantly outperforms the prior art in this domain. We show that this estimator can achieve the same performance as prior estimators with an order-of-magnitude less signal flux, or multiple orders-of-magnitude less flux-accumulation time. Further we show that this estimator achieves the Cramer-Rao bound, making it asymptotically efficient. This method does not require an explicit synchronization sequence, freeing up channel resources for data transmission.

Rogalin, Ryan↗

Hybrid Symbolic-Numerical Modeling and Parametric Stability Analysis of DC–AC Power Systems

Hybrid DC-AC power systems integrating diverse inverter-based resources (IBRs) and multi-terminal high-voltage direct current (MTDC) networks represent a promising architecture for future power grids, while introducing challenges for modeling, stability analysis, and control design. This paper develops a hybrid symbolic-numerical modeling framework and tool to characterize the parametric small-signal stability of DC-AC coupled power systems. The proposed approach constructs parametric state-space models to enable efficient representation of system dynamics under varying control parameters and network configurations, with target parameters retained as symbolic variables and the remainder treated numerically. The stability analysis framework covers eigenvalue, sensitivity, and stability boundary and region characterization. Enhanced linear matrix inequality (LMI) techniques are proposed to directly certify small-signal stability over regions of parameter space while also reducing the conservativeness and computational burden. The resulting tools and frameworks enable rapid parametric model construction across diverse grid conditions, thereby facilitating stability-informed control and operation in complex DC–AC power systems.

DC–AC power systems↗

MINLP for regularized symbolic regression with applications to data-driven modeling of critical minerals processes

The poster summarizes recent advances in symbolic regression developed as part of the PrOMMiS project over the past year. In particular, it describes the comparison of surrogates for critical minerals (CM) & rare earth element (REE) recovery flowsheets obtained via symbolic regression and ALAMO. It also compares the predictive ability and solvability of optimization models that incorporate these surrogates.

36 MATERIALS SCIENCE↗

Multibody for Everybody (M4E): A Symbolic Dynamics Modeling Tool with Applications in Simulation, Control, and Optimization

Developing the analytical model of a multibody system is often the initial step in control and optimization. The analytical model (equations of motion) describes a system’s time evolution under specified forcing conditions. Although developing these equations is easy for simple systems, this process becomes more complex for systems composed of multiple bodies. Deriving equations of motion for complex multibody systems requires specialized expertise in multibody dynamics, is time-consuming, and is susceptible to error. To address this issue, this paper presents an open-source, easy-to-use, systematic framework to derive symbolic equations of motion in both Python and MATLAB using the joint coordinate formulation. This formulation results in a set of ordinary differential equations that use the minimum set of coordinates needed to model a system. The symbolic representation provides better insight into the influence of design parameters on system performance, facilitates sensitivity analysis and parameter studies, and supports direct implementation of control and optimization routines. The tool enables numerical simulation for specified parameter sets, is modular for straightforward integration with other tools and libraries, and allows incorporation of hydrodynamics, mooring, and other external forces. The result is a reproducible, extensible pipeline for modeling, simulation, and design of complex multibody systems. The proposed tool is versatile and can be applied to domains such as robotics, control, and design. In addition, we integrated external libraries that provide capabilities for modeling offshore systems such as underwater robots and marine energy converters.

16 TIDAL AND WAVE POWER↗

Bingo: A Customizable Framework for Symbolic Regression with Genetic Programming

In this paper, we introduce Bingo, a flexible and customizable yet performant Python framework for symbolic regression with genetic programming. Bingo maintains a modular code structure for simple abstraction and easily swappable components. Fitness functions, selection methods, and constant optimization methods allow for easy problem-specific customization. Bingo also maintains several features for increased efficiency such as parallelism, equation simplification, and a C++ backend. We compare Bingo’s performance to other genetic programming for symbolic regression (GPSR) methods to show that it is both competitive and flexible.

machine learning↗