Description: We propose to develop an Action Languages which allows for the representation of time and time dependent processes and which allows for the valid composition of modules. Furthermore, we will develop a provably correct translation from the Action Language into Logic Programs under the Answer Set Semantics. Action Languages have already proven useful for the representation of intelligent agent that can perform planning and diagnosis. Our proposed work would allow for more robust agents as well as the ability to do tasks such as scheduling. We will also develop proof techniques to ensure correctness of the agents. We propose to support control systems developed for such agents in distributed real-time systems with a dynamic, on-line, verification of the system behavior with respect to time-based properties.

Benefits: The potential customers of this technology are mission and distributed real-time system designers and integrators. These customers develop the application solution with their customers, and need to meet high-performance operations requirements with robust performance exceeding those requirements. With humans in the control loop for interactive operations, the requirements are difficult to meet and are best supported with run-time verification to ensure the requirements are upheld now and in the foreseeable future. Outside of aeronautics, space, and other transportation examples, the recent pursuit of Smart Grid applications has these operational attributes. The interactive control is in the exploration of price points meeting expected utility derived from energy distribution for building or microgrid operations. The operating requirements depend on time-valued parameters and online verification ensures safety requirements are satisfied.

We anticipate the implementation of continuous-time action languages with online verification will be especially important to NASA's efforts in developing robotic capabilities to support human exploration. Owing to its reusability to attack different problems, domain models built with Action Languages provide an efficient way to collection knowledge about the system and leverage that knowledge to accomplish operational objectives. The addition herein of continuous time and time-bounded properties adds new capabilities for reasoning about real-time systems in distributed architectures. These capabilities in particular address challenges faced by operational architectures having adjustable levels autonomy in human-computer cooperation. We anticipate that these results then will support a broad range of planning, control, and dynamic verification development activities as well.