Preface

This EPTCS volume contains the papers presented at the Fifth International Workshop on Formal Methods for Autonomous Systems (FMAS 2023), which was held on the 15th and 16th of November 2023. FMAS 2023 was co-located with 18th International Conference on integrated Formal Methods (iFM'23), organised by Leiden Institute of Advanced Computer Science of Leiden University. The workshop itself was held at Scheltema Leiden, a renovated 19th Century blanket factory alongside the canal.

The goal of the FMAS workshop series is to bring together leading researchers who are using formal methods to tackle the unique challenges that autonomous systems present, so that they can publish and discuss their work with a growing community of researchers. Autonomous systems are highly complex and present unique challenges for the application of formal methods. Autonomous systems act without human intervention, and are often embedded in a robotic system, so that they can interact with the real world. As such, they exhibit the properties of safety-critical, cyber-physical, hybrid, and real-time systems. We are interested in work that uses formal methods to specify, model, or verify autonomous and/or robotic systems; in whole or in part. We are also interested in successful industrial applications and potential directions for this emerging application of formal methods.

We continued to hold FMAS as a hybrid event this year. The workshops in 2020 and 2021 have been fully online events because of the restrictions required to deal with the COVID-19 pandemic, and FMAS 2022 continued to facilitate online participation. We feel that a hybrid event, while often challenging to organise, provides accessibility to people not able to travel for the workshop. FMAS 2023 had both presentations and attendees who were remote, and we hope that it was a useful option for those people who made use of it.

FMAS 2023 continued to use the submission categories introduced last year: vision papers and research previews, both of which were types of short paper; and experience reports and regular papers, both of which were types of long paper. In total, FMAS 2023 received 25 submissions. We received 11 regular papers, 3 experience reports, 6 research previews, and 5 vision papers. The researchers who submitted papers to FMAS 2023 were from institutions in: Australia, Canada, Colombia, France, Germany, Ireland, Italy, the Netherlands, Sweden, the United Kingdom, and the United States of America. Increasing our number of submissions for the third year in a row is an encouraging sign that FMAS has established itself as a reputable publication venue for research on the formal modelling and verification of autonomous systems. After each paper was reviewed by three members of our Programme Committee, we accepted a total of 15 papers: 8 long papers and 7 short papers.

FMAS 2023 hosted two invited speakers. Prof. Alice Miller, from the University of Glasgow (UK), gave a talk titled "Formal Methods within the TAS Governance Node"; which focussed on several strands of work using formal methods within the Trustworthy Autonomous Systems Hub's Governance Node. Prof. Erika Ábrahám, from RWTH Aachen University (Germany), gave a talk titled "SMT: Something you Must Try"; which discussed using Satisfiability Modulo Theories (SMT) to solve real-world problems. Prof. Ábrahám's talk was held in a joint session with iFM.

This is the fifth year that we have held an FMAS workshop; five years seems like a number that is round enough to feel significant and warrant some reflection. The idea for FMAS came from conversations between two of the current organisers, Drs Marie Farrell and Matt Luckcuck, and Prof. Michael Fisher during a research project on using robotics and AI in the UK nuclear industry. FMAS 2019 was held as a satellite workshop at FM 2019 in Porto, Portgual. We were unsure if this would be a one-off event or an ongoing series, and there were only five papers presented at that first workshop. After the uncertainty of running workshops during the pandemic, FMAS has rebounded strongly with several years of increasing numbers of submissions. This year, FMAS received five more submissions than last year, giving us our highest-ever number number of submissions. This is a very pleasing pay-off to five years of hard work, and reflects the progress of this burgeoning community in tackling the challenges that autonomous systems pose for formal modelling and verification techniques.

For four years, FMAS has been organised almost entirely by Drs Matt Luckcuck and Marie Farrell in equal partnership, but it was becoming clear that this would be unsustainable as the workshop grows bigger. To help spread the workload, and to inject some fresh perspective, two colleagues joined the FMAS organising committee this year. Matt and Marie were joined by Jun.-Prof. Dr Maike Schwammberger and Dr Mario Gleirscher, who have been supporting FMAS 2023 in preparation for a bigger restructuring from next year's workshop onward. We are already planning for what FMAS will look like for the next five years and we hope that the improvements that are coming will make FMAS an event that is even more useful and enjoyable for our community.

We would like to thank our brilliant Programme Committee and sub-reviewers for their helpful reviews and discussions behind the scenes. Many of the reviewers for FMAS 2023 have been part of our Programme Committee since the first FMAS workshop, we are pleased to have their continuing support. Whether this is their first time or their fifth, we are proud to have a community of reviewers who are so enthusiastic and supportive of our workshop and the work it receives. We thank them for volunteering their time and effort because without them we could not produce our programme of presentations. We also thank our invited speakers, Prof. Alice Miller and Prof. Erika Ábrahám, for their time; the authors who submitted papers; our EPTCS editor, Martin Wirsing, for overseeing the preparation of the proceedings; the organisers of iFM — Marcello M. Bonsangue, Paula Herber, and Anton Wijs — for supporting our workshop; FME for its sponsorship of our student travel grants; and all of the attendees (both virtual and in-person) of FMAS 2023. We hope to see you all at FMAS 2024.

Matt Luckcuck, Marie Farrell, Mario Gleirscher, and Maike Schwammberger

November 2023

Program Committee

Subreviewers

Formal Methods within the TAS Governance Node

The TAS Governance Node part of the £33M Trustworthy Autonomous Systems Programme funded by the UKRI Strategic Priorities Fund. The aim of the node is to explore how to make autonomous systems aware of – and responsive to – changing regulations. Led by the University of Edinburgh, it brings together researchers from the universities of Edinburgh, Glasgow, Nottingham, Heriot-Watt, Sussex, and Kings College London; as well as multiple industrial partners. In this talk I will highlight some of the activities within the node, focussing on those that use Formal Methods. These include:

• an automatic theory repair system for a legal responsibility framework for autonomous vehicles,
• accident anticipation through reasoned simulation,
• robot planning using in-situ model checking; and,
• (formal aspects of) a node-wide automotive case study investigation.

SMT: Something you Must Try

SMT (Satisfiability Modulo Theories) solving is a technology for the fully automated solution of logical formulas. Due to their impressive efficiency, SMT solvers are nowadays frequently used in a wide variety of applications. These tools are general purpose and as off-the-shelf solvers, their usage is truly integrated. A typical application encodes real-world problems as logical formulas, whose solutions can be decoded to solutions of the real-world problem. In this talk we give some insights into the mechanisms of SMT solving, discuss some areas of application, and present a novel application from the domain of simulation.