Timed logics play a pivotal role in modelling and verifying systems with temporal constraints, whichare pervasive in real-world applications ranging from embedded systems to cyber-physical systems.However, formal verification and synthesis of systems based on timed logic specifications facessignificant challenges due to the combinatorial explosion of state spaces and inherent difficultiesin implementation. 

The primary objective of this research is to develop novel machine learning methodologies tailoredto address the verification and synthesis problems for timed logics. Specifically, we aim to:  

• Investigate the applicability of machine learning algorithms in generating models and abstractions;  
• Explore techniques to improve the scalability and efficiency of verification procedures for timed  logics. 
• Develop methodologies for automated synthesis of counterexamples and explanations. 

Our proposed methodology comprises the following key steps: 

Data Representation: Develop appropriate representations of timed logic specifications and models tofacilitate learning-based approaches. 

Feature Engineering: Extract relevant features from systemmodels and temporal specifications to enable effective learning. 

Algorithm Selection: Evaluate andadapt machine learning algorithms suited to the characteristics of timed logics verification. 

Training Data Generation: Generate synthetic and gather real-world datasets for training and validating machine learning models, ensuring representativeness and diversity. 

Model Training: Train machine learning models to predict temporal properties, verify system behaviours, identify counterexamples, and provide explanations. 

Integration with Verification Tools: Integrate trainedmodels into existing verification frameworks to enhance their capabilities and performance. 

The proposed research is expected to make several contributions to the field of formal methods andmachine learning, including: 

The proposed research will be conducted over a three-year period, with the following milestones: 

Year 1: Literature review, data collection, and initial experimentation. 

Year 2: Methodology development, training, and integration with existing verification tools. 

Year 3: Evaluation and dissemination of results through publications and presentations. 

This scholarship is available to UK, EU and overseas applicants. 

Eligible candidates will have an upper second-class (2:1) undergraduate honours degree (or equivalent qualification) in a related field. 

The University of Sussex believes that the diversity of its staff and student community is fundamental to creative thinking, pedagogic innovation, intellectual challenge, and the interdisciplinary approach to research and learning. We celebrate and promote diversity, equality and inclusion amongst our staff and students. As such, we welcome applicants from all backgrounds.

Please clearly state on your application that you are applying for the Leveraging Machine Learning for Verification Problems in Timed Logics under the supervision of Dr Hsi-Ming Ho. 

Please ensure you application includes each of the following: 

• A research proposal. For guidance on preparing your proposal, please see here. 
• Your CV.
• Degree certificates and transcripts. 
• 2 references, including a minimum of 1 from any institution studied at within the last 5 years.
• If your first language is not English you will need to demonstrate that you meet the University’s English language requirements, see here for details of our accepted documentation.