Co-Evolution of Symbolic AI with Data and Specification

Trusted autonomous systems (TAS) rely on AI components that perform critical tasks for stakeholders that have to rely on the services provided by the system, e.g., self-driving cars or intelligent robotic systems. Two techniques that help the designers automatically construct symbolic AI systems for trusted autonomous systems from data and specification are model learning and reactive synthesis. Model learning relies on data and observations to derive a model of the AI component for transparency, analysis, and quality assurance tasks. Reactive synthesis takes as input a formal specification of what a system is expected to do and automatically produces an implementation of the AI component, if one exits.

This work considers the evolution of symbolic AI components and how novel software engineering methods may support trust in evolving symbolic AI for TAS by evolving their design and explaining the evolution in the face of continuous evolution of data and specifications. Despite the fundamental differences of model learning and reactive synthesis the methods present common challenges: the constructed symbolic models should evolve in both techniques and the evolution should pinpoint the confine the scope of evolution in data and specification. We need to develop similar adaptive techniques in both cases that can provide an explanation about the nature of evolution and act upon it. This PhD project will address the challenge of developing adaptive model-learning and synthesis techniques that can explain the nature of evolution in underlying data and specification.

Methodology: First, the successful candidate will build familiarity with model learning and reactive synthesis on existing TAS case studies. Next, methods for detecting, justifying, and explaining differences will be developed first independently for model learning and reactive synthesis and then lifted and generalized to a framework based on identified commonalities of the approach.

We will use different sources of data to drive and evaluate the research: for initial studies, we will use open data sets regarding the evolution of systems in time (e.g., fixing rules and protocols, such as the changes in the SSL and SSH protocol implementations, available at: https://automata.cs.ru.nl/Overview) and in space (e.g., features of automotive systems, such as the Body Comfort System developed for Volkswagen Golf available at: https://www.isf.cs.tu-bs.de/cms/team/lity/bcs_tubs_tech_rep_V1_4.pdf). For further empirical studies, we will use the data from our firefighting drone case study at the Trustworthy Autonomous Systems Hub.

  • S. Maoz, J. O. Ringert. Spectra: a specification language for reactive systems. SoSym. Springer 2021  Available at: https://link.springer.com/content/pdf/10.1007/s10270-021-00868-z.pdf 
  • C.D. Damasceno, M.R. Mousavi, and A. Simao. Learning by Sampling: Learning Behavioral Family Models from Software Product Lines. Empirical Software Engineering, 26(1): 4, 2021. Available at: https://nms.kcl.ac.uk/mohammad.mousavi/pub/mousavi-emse-2020.pdf  
  • C.D. Nascimento Damasceno, M.R. Mousavi and A. Simao. Learning to Reuse: Adaptive Model Learning for Evolving Systems. Proceedings of the 15th International Conference on integrated Formal Methods (iFM 2019). Springer, 2019. Available at: https://nms.kcl.ac.uk/mohammad.mousavi/pub/mousavi-ifm-2019.pdf 
  • S. Maoz, J. O. Ringert: A Framework for Relating Syntactic and Semantic Model Differences. SoSym 2018. Available at: https://drive.google.com/file/d/1CQ-ncGyweg_SUzQimlwDYR-4B0iySxT3/view?usp=sharing 

Project ID

STAI-CDT-2022-KCL-6

Supervisor

Jan Oliver Ringerthttps://ringert.blogspot.com/

Mohammad Mousavi

Category

Verification