Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “timed automata”

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 19 records
All sourcesNASA NTRSDOE OSTI
NASA NTRS2004

Towards Time Automata and Multi-Agent Systems

The design of reactive systems must comply with logical correctness (the system does what it is supposed to do) and timeliness (the system has to satisfy a set of temporal constraints) criteria. In this paper, we propose a global approach for the design of adaptive reactive systems, i.e., systems that dynamically adapt their architecture depending on the context. We use the timed automata formalism for the design of the agents' behavior. This allows evaluating beforehand the properties of the system (regarding logical correctness and timeliness), thanks to model-checking and simulation techniques. This model is enhanced with tools that we developed for the automatic generation of code, allowing to produce very quickly a running multi-agent prototype satisfying the properties of the model.

Hutzler, G.↗
DOE OSTI2022

Designing Secure and Resilient Cyber-Physical Systems Using Formal Models

This work-in-progress paper proposes a design methodology that addresses the complexity and heterogeneity of cyber-physical systems (CPS) while simultaneously proving resilient control logic and security properties. The design methodology involves a formal methods-based approach by translating the complex control logic and security properties of a water flow CPS into timed automata. Timed automata are a formal model that describes system behaviors and properties using mathematics-based logic languages with precision. Due to the semantics that are used in developing the formal models, verification techniques, such as theorem proving and model checking, are used to mathematically prove the specifications and security properties of the CPS. This work-in-progress paper aims to highlight the need for formalizing plant models by creating a timed automata of the physical portions of the water flow CPS. Extending the time automata with control logic, network security, and privacy control processes is investigated. The final model will be formally verified to prove the design specifications of the water flow CPS to ensure efficacy and security.

42 ENGINEERING↗
NASA NTRS2010

Using Integer Clocks to Verify the Timing-Sync Sensor Network Protocol

We use the UPPAAL model checker for Timed Automata to verify the Timing-Sync time-synchronization protocol for sensor networks (TPSN). The TPSN protocol seeks to provide network-wide synchronization of the distributed clocks in a sensor network. Clock-synchronization algorithms for sensor networks such as TPSN must be able to perform arithmetic on clock values to calculate clock drift and network propagation delays. They must be able to read the value of a local clock and assign it to another local clock. Such operations are not directly supported by the theory of Timed Automata. To overcome this formal-modeling obstacle, we augment the UPPAAL specification language with the integer clock derived type. Integer clocks, which are essentially integer variables that are periodically incremented by a global pulse generator, greatly facilitate the encoding of the operations required to synchronize clocks as in the TPSN protocol. With this integer-clock-based model of TPSN in hand, we use UPPAAL to verify that the protocol achieves network-wide time synchronization and is devoid of deadlock. We also use the UPPAAL Tracer tool to illustrate how integer clocks can be used to capture clock drift and resynchronization during protocol execution

Huang, Xiaowan↗
NASA NTRS1994

Efficient massively parallel simulation of dynamic channel assignment schemes for wireless cellular communications

Fast, efficient parallel algorithms are presented for discrete event simulations of dynamic channel assignment schemes for wireless cellular communication networks. The driving events are call arrivals and departures, in continuous time, to cells geographically distributed across the service area. A dynamic channel assignment scheme decides which call arrivals to accept, and which channels to allocate to the accepted calls, attempting to minimize call blocking while ensuring co-channel interference is tolerably low. Specifically, the scheme ensures that the same channel is used concurrently at different cells only if the pairwise distances between those cells are sufficiently large. Much of the complexity of the system comes from ensuring this separation. The network is modeled as a system of interacting continuous time automata, each corresponding to a cell. To simulate the model, conservative methods are used; i.e., methods in which no errors occur in the course of the simulation and so no rollback or relaxation is needed. Implemented on a 16K processor MasPar MP-1, an elegant and simple technique provides speedups of about 15 times over an optimized serial simulation running on a high speed workstation. A drawback of this technique, typical of conservative methods, is that processor utilization is rather low. To overcome this, new methods were developed that exploit slackness in event dependencies over short intervals of time, thereby raising the utilization to above 50 percent and the speedup over the optimized serial code to about 120 times.

Greenberg, Albert G.↗
NASA NTRS2013

Rewriting Modulo SMT

Combining symbolic techniques such as: (i) SMT solving, (ii) rewriting modulo theories, and (iii) model checking can enable the analysis of infinite-state systems outside the scope of each such technique. This paper proposes rewriting modulo SMT as a new technique combining the powers of (i)-(iii) and ideally suited to model and analyze infinite-state open systems; that is, systems that interact with a non-deterministic environment. Such systems exhibit both internal non-determinism due to the system, and external non-determinism due to the environment. They are not amenable to finite-state model checking analysis because they typically are infinite-state. By being reducible to standard rewriting using reflective techniques, rewriting modulo SMT can both naturally model and analyze open systems without requiring any changes to rewriting-based reachability analysis techniques for closed systems. This is illustrated by the analysis of a real-time system beyond the scope of timed automata methods.

Rocha, Camilo↗
NASA NTRS2014

Rewriting Modulo SMT and Open System Analysis

This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze infinite-state open systems, i.e., systems that interact with a non-deterministic environment. Such systems exhibit both internal non-determinism, which is proper to the system, and external non-determinism, which is due to the environment. In a reflective formalism, such as rewriting logic, rewriting modulo SMT can be reduced to standard rewriting. Hence, rewriting modulo SMT naturally extends rewriting-based reachability analysis techniques, which are available for closed systems, to open systems. The proposed technique is illustrated with the formal analysis of: (i) a real-time system that is beyond the scope of timed-automata methods and (ii) automatic detection of reachability violations in a synchronous language developed to support autonomous spacecraft operations.

Rocha, Camilo↗
NASA NTRS2021

Assuring Intelligent Systems: Contingency Management for UAS

Unmanned aircraft systems (UAS) collaborate with humans to operate in diverse, safety-critical applications. However, assurance technologies need to be integrated into the design process in order to guarantee safe behavior, thereby enabling UAS operations in the National Airspace System (NAS). In this paper, formal methods are integrated with learning-enabled systems representations. The generation and representation of knowledge are captured via monadic second-order logic rules in the cognitive architecture Soar. These rules are translated into timed automata, and a proof of correctness for the translation is provided so that safety and liveness properties can be checked in the formal verification environment Uppaal. This approach is agnostic to the learning mechanism used to generate the learned rules (e.g., chunking, etc.). An example of a fault-tolerant, learning-enabled UAS deciding which of four contingency procedures to execute under a lost link scenario while overflying an urban area is used to illustrate the approach.

Intelligent Systems↗
DOE OSTI2019

Action principles for quantum automata and Lorentz invariance of discrete time quantum walks

A discrete action principle for general quantum automata is proposed. This action principle is particularized to Discrete Time Quantum Walks (DTQWs) and then extended into an energy and momentum preserving, manifestly covariant formulation. Space–time coordinates are introduced as new variables of the action and their equations of motion enforce energy and momentum conservation. This guarantees that the proposed action can be used to build future, DTQW-based self-consistent models of spinors interacting with gauge fields. A discrete stress–energy tensor for the DTQW is also obtained. The manifest covariance of the formulation highlights the special role played by the grid reference frame in the DTQW dynamics. The main discussion is complemented by three appendices.

71 CLASSICAL AND QUANTUM MECHANICS, GENERAL PHYSIC↗
NASA NTRS1991

Reasoning about real-time systems with temporal interval logic constraints on multi-state automata

Models of real-time systems using a single paradigm often turn out to be inadequate, whether the paradigm is based on states, rules, event sequences, or logic. A model-based approach to reasoning about real-time systems is presented in which a temporal interval logic called TIL is employed to define constraints on a new type of high level automata. The combination, called hierarchical multi-state (HMS) machines, can be used to model formally a real-time system, a dynamic set of requirements, the environment, heuristic knowledge about planning-related problem solving, and the computational states of the reasoning mechanism. In this framework, mathematical techniques were developed for: (1) proving the correctness of a representation; (2) planning of concurrent tasks to achieve goals; and (3) scheduling of plans to satisfy complex temporal constraints. HMS machines allow reasoning about a real-time system from a model of how truth arises instead of merely depending of what is true in a system.

Gabrielian, Armen↗
DOE OSTI2014

A Runtime Verification Framework for Control System Simulation

n a standard workflow for the validation of a control system, the control system is implemented as an extension to a simulator. Such simulators are complex software systems, and engineers may unknowingly violate constraints a simulator places on extensions. As such, errors may be introduced in the implementation of either the control system or the simulator leading to invalid simulation results. This paper presents a novel runtime verification approach for verifying control system implementations within simulators. The major contribution of the approach is the two-tier specification process. In the first tier, engineers model constraints using a domain-specific language tailored to modeling a controller’s response to changes in its input. The language is high-level and effectively hides the implementation details of the simulator, allowing engineers to specify design-level constraints independent of low-level simulator interfaces. In the second tier, simulator developers provide mapping rules for mapping design-level constraints to the implementation of the simulator. Using the rules, an automated tool transforms the design-level specifications into simulator-specific runtime verification specifications and generates monitoring code which is injected into the implementation of the simulator. During simulation, these monitors observe the input and output variables of the control system and report changes to the verifier. The verifier checks whether these changes follow the constraints of the control system. We describe application of this approach to the verification of the constraints of an HVAC control system implemented with the power grid simulator GridLAB-D.

control system↗
DOE OSTI2026

A scalable framework for efficient coupling of thermal and microstructural simulations in additive manufacturing

Predicting microstructure evolution in metal additive manufacturing (AM) is important for process optimization, but spatiotemporal scale disparities between thermal transport and microstructure evolution create significant challenges for efficient data transfer between simulation codes. To address this, we present Stork, a scalable framework for coupling thermal and microstructural simulations. Stork uses a sparse data representation to identify and store active solidification sub-volumes, enabling highly parallel quad-linear interpolation from coarse thermal grids to fine microstructure grids without large intermediate storage. We demonstrate the framework by coupling the semi-analytic heat transfer code 3DThesis with the time-parallel cellular automata code Toucan. This approach achieves over two orders of magnitude reduction in data generation time and file size compared to prior workflows. Numerical studies show that quad-linear interpolation preserves grain morphology and crystallographic texture in laser powder bed fusion (LPBF) simulations for coarsening ratios up to 16. Overall, Stork provides a scalable pathway for high-throughput, component-scale AM simulations on modern high-performance computing systems.

36 MATERIALS SCIENCE↗
NASA NTRS1994

Design of Flight Vehicle Management Systems

As the operation of large systems becomes ever more dependent on extensive automation, the need for an effective solution to the problem of design and validation of the underlying software becomes more critical. Large systems possess much detailed structure, typically hierarchical, and they are hybrid. Information processing at the top of the hierarchy is by means of formal logic and sentences; on the bottom it is by means of simple scalar differential equations and functions of time; and in the middle it is by an interacting mix of nonlinear multi-axis differential equations and automata, and functions of time and discrete events. The lecture will address the overall problem as it relates to flight vehicle management, describe the middle level, and offer a design approach that is based on Differential Geometry and Discrete Event Dynamic Systems Theory.

Meyer, George↗
NASA NTRS1995

Nonlinear Control and Discrete Event Systems

As the operation of large systems becomes ever more dependent on extensive automation, the need for an effective solution to the problem of design and validation of the underlying software becomes more critical. Large systems possesses much detailed structure, typically hierarchical, and they are hybrid. Information processing at the top of the hierarchy is by means of formal logic and sentences; on the bottom it is by means of simple scalar differential equations and functions of time; and in the middle it is by an interacting mix of nonlinear multi-axis differential equations and automata, and functions of time and discrete events. The lecture will address the overall problem as it relates to flight vehicle management, describe the middle level, and offer a design approach that is based on Differential Geometry and Discrete Event Dynamic Systems Theory.

Meyer, George↗
DOE OSTI2023

Absolutely Stable Time Crystals at Finite Temperature

Here, we show that locally interacting, periodically driven (Floquet) Hamiltonian dynamics coupled to a Langevin bath support finite-temperature discrete time crystals (DTCs) with an infinite autocorrelation time. By contrast to both prethermal and many-body localized DTCs, the time crystalline order we uncover is stable to arbitrary perturbations, including those that break the time translation symmetry of the underlying drive. Our approach utilizes a general mapping from probabilistic cellular automata to open classical Floquet systems undergoing continuous-time Langevin dynamics. Applying this mapping to a variant of the Toom cellular automaton, which we dub the "π-Toom time crystal," leads to a 2D Floquet Hamiltonian with a finite-temperature DTC phase transition. We provide numerical evidence for the existence of this transition, and analyze the statistics of the finite temperature fluctuations. Finally, we discuss how general results from the field of probabilistic cellular automata imply the existence of discrete time crystals (with an infinite autocorrelation time) in all dimensions, d ≥ 1.

72 PHYSICS OF ELEMENTARY PARTICLES AND FIELDS↗
DOE OSTI2020

Classical discrete time crystals

The spontaneous breaking of time-translation symmetry in periodically driven quantum systems leads to a new phase of matter: the discrete time crystal (DTC). This phase exhibits collective subharmonic oscillations that depend upon an interplay of non-equilibrium driving, many-body interactions and the breakdown of ergodicity. However, subharmonic responses are also a well-known feature of classical dynamical systems ranging from predator–prey models to Faraday waves and a.c.-driven charge density waves. This raises the question of whether these classical phenomena display the same rigidity characteristic of a quantum DTC. In this work, we explore this question in the context of periodically driven Hamiltonian dynamics coupled to a finite-temperature bath, which provides both friction and, crucially, noise. Focusing on one-dimensional chains, where in equilibrium any transition would be forbidden at finite temperature, we provide evidence that the combination of noise and interactions drives a sharp, first-order dynamical phase transition between a discrete time-translation invariant phase and an activated classical discrete time crystal (CDTC) in which time-translation symmetry is broken out to exponentially long timescales. Power-law correlations are present along a first-order line, which terminates at a critical point. We analyse the transition by mapping it to the locked-to-sliding transition of a d.c.-driven charge density wave. To conclude, building upon results from the field of probabilistic cellular automata, we conjecture the existence of classical time crystals with true long-range order, where time-translation symmetry is broken out to infinite times.

71 CLASSICAL AND QUANTUM MECHANICS, GENERAL PHYSIC↗