Verification of Decision Procedures Modeled in Intelligent Agents
Abstract:
Autonomous Intelligent Systems (AIS) are built on principles defined in cognitive architectures that implement adaptive decision procedures. These procedures can be sets of rules with preconditions which, when satisfied, lead to the execution of conditionalized actions. Further, the rules themselves can be adapted based on episodic and semantic learning methods. These AIS design methods prove beneficial in structuring adaptive systems to respond to dynamic situations but fail to assure correctness of the adapted components. These methods cannot diagnose conflicts in the composition of rules during design time or during runtime after adapting to change. We propose a method of transforming a class of adaptive decision procedures into the formalism of formal methods to assure correctness of resulting composition. This research effort discusses a case study that identifies the challenges in the transformation between the cognitive and formal domains. While the presented method enables analysis of the composition of adaptive decision procedures, there are fundamental differences in the representations and constructs in the two domains that remain to be addressed.
Bios:
Dr. Siddhartha Bhattacharyya is a research scientist in the application of formal analysis to the design, verification and validation of autonomous systems, smart grid and avionics. He got his Masters from Iowa State University in 2003 and PhD from University of Kentucky in 2005 in Electrical Engineering. He led and conducted research efforts with NASA Langley on Certification Considerations of Adaptive Systems, AFRL on formal verification of quasi-synchronous systems, Loyal Wingman, DARPA on System of Systems Integration Testing and Experimentation, as Sr. Research Engineer at Rockwell Collins. This led to advancing research in application of formal methods to complex systems. He conducted research at Applied Research Laboratory at Pennsylvania State University in the summer of 2004. Here he worked on the design, verification, simulation and synthesis of mission control for autonomous underwater vehicles. Additionally, he conducted research as a summer fellow in 2007 at Oak Ridge National Laboratory. Here he worked on developing methods of verification and validation of the smart power grid. Presently, he is working on assurance for complex systems. He has served as principal investigator on projects funded through Kentucky Science and Technology Corporation to develop technologies for fault monitoring and diagnosis with wireless sensor networks. He has led and worked on projects for NASA, AFRL, DARPA and ONR in related areas. He has publications and submissions in refereed conferences and journals. He has chaired sessions and presented at American Control Conferences and other conferences. He has been a reviewer for Journals in the area of automation and control. He had been leading efforts in the area of automation and formal methods as the Interim Chair of the Division of Computer Science at Kentucky State University as a faculty from 2005 to 2012.
Marco M. Carvalho is an Associate Professor at the Florida Institute of Technology, and a Research Scientist at the Institute for Human and Machine Cognition. He graduated in Mechanical Engineering at the University Brasilia (UnB – Brazil), where he also completed his M.Sc. in Mechanical Engineering with specialization in dynamic systems and control theory. Marco Carvalho also holds a M.Sc. in Computer Science from the University of West Florida and a Ph.D. in Computer Science from Tulane University, with specialization in Machine Learning and Data Mining. Dr. Carvalho currently leads a several research efforts in the areas of cyber security, moving target defense, critical infrastructure protection, and tactical communication systems, primarily sponsored by the Department of Defense, the U.S. Army Research Laboratory, the U.S. Air Force Research Laboratory, ONR, the National Science Foundation, DoE and Industry.
Dr. Carvalho’s research interests include resilient distributed systems, multi-agent systems and emergent approaches to systems optimization and security. As the IHMC Principal Investigator for the Biologically Inspired Tactical Security Infrastructure project, sponsored by ARL, and the Adaptive SCADA Technologies for Critical Infrastructure Protection project, sponsored by the DoE, Dr. Carvalho and his team have worked on the development of agent-based frameworks for adaptive defense and mission resilience.
Dr. Jennifer Davis is a Senior Applied Mathematician in the Advanced Technology Center at Rockwell Collins. Dr. Davis has been working in the field of formal methods for several years. She modeled and verified UAV mission behaviors on an internally funded project. She jointly developed a translator from LLVM to ACL2, to enable verification of system properties. She completed the correctness proofs for the DO-333 theorem proving case study with the PVS theorem prover. She made updates to the formal models and proofs of correctness with PVS for NASA-Langley’s Conflict Detection and Resolution tool (a flightplan rerouting tool) called Stratway. Dr. Davis also has experience with cryptography, error-correcting codes, image processing, model-based engineering, and cybersecurity. She earned her Ph.D. in Mathematics at the University of Nebraska at Lincoln in 2007.
Dr. Thomas C. Eskridge is an Associate Professor of Information Assurance and Cybersecurity in the Harris Institute for Assured Information at the Florida Institute of Technology. Dr. Eskridge’s research focuses on amplifying human performance through intelligent assistance and innovative visualizations, both of which require developing a deep understanding of operator goals and mental task models to represent, reason, and visually display. He is currently developing tools that enable software agents and human operators to collaboratively represent and reason about networks, user actions, and cyber security events. Previous projects include developing a hybrid connectionist-symbolic knowledge representation system to model human analogical reasoning, case-based reasoning systems supporting milling-machine operators, formal knowledge representation editors, distributed multi-agent systems, fixed-wing and rotary-wing cockpit displays, visualizations for cyber situation awareness, defense posture, and mission management. Dr Eskridge does not currently hold a DoD clearance.