Colloquium Artificial Intelligence - J. J. Joosten University of Barcelona
| When: | We 18-05-2022 16:00 - 17:00 |
| Where: | Omega at Philosophy Building 11.31 - Oude Boteringestraat 52 |
Title: Model checking and formally verified software for temporal quantitative regulations
Abstract:
In this talk I will first expose the general activities of our research group within the covenant of the University of Barcelona, Formal Vindications S.L. and Guretruck S.L. We will speak on the European Regulation 561 for transport and then generalise the setting to temporal quantitative regulations in general. The challenge here is to find the right balance between expressibility on the one hand and feasible model checking problems on the other hand. In joint work with Moritz Müller we present a particular class of stopwatch automata that in a well-defined sense proposes such a balance. In particular, we expose an automaton for the above mentioned Regulation 561. We will see how work with proof assistants can be combined with model checking to strive for ultimate security in programming certain computable laws. Throughout the talk we shall recurrently dwell on impact of legal software on society.
Some preliminary results can be found on the Formal Vindications website.