Planning with increasingly complex executive models

We are developing autonomous control systems for mission-critical domains that require hard real-time performance guarantees. To automatically build reactive plans that meet these requirements, we use formal verification (model checking) techniques to assess the quality of plans as they are built. The verification process uses precise timed automaton models of the executive that will run the resulting reactive plan. This reflexive modeling allows our system to formally verify not just that its plans are correct, but that they will be executed correctly.

Authors

• David J. Musliner
• Robert P. Goldman
• Michael J. S. Pelican

Keywords

• Automatic control
• Control systems
• Mission critical systems
• Process planning
• Predictive models
• Intelligent control
• Certification
• Automatic generation control
• Timing
• Delay effects
• Model Execution
• Verification Process
• Model Checking
• Formal Verification
• Active Control
• System State
• Time Constraints
• Control Problem
• Planning Process
• Time Information
• Goal State
• Control Synthesis
• Temporal Modulation
• Failure Conditions
• Reactive Control
• Execution Plan
• Entire Planning
• Final Verification
• Reachable States