About the project
In this project, you will develop new foundations for quantitative verification grounded in the mathematical theory of coalgebras. By studying quantitative logics, their expressiveness and their associated model checking problems, you will lay the groundwork for verification tools that are more widely applicable and more expressive than existing ones.
The nature of software systems being developed nowadays is shifting the focus in formal approaches to software development from correctness guarantees to optimality ones. For example, when developing autonomous agents whose actions are resource-dependent, optimality w.r.t. resource usage is a key concern. While existing verification and synthesis techniques can be adapted to accommodate this, their applicability is limited and the process cumbersome. There is thus a real need for quantitative verification tools that can seamlessly accommodate optimality requirements.
The mathematical theory of coalgebras, developed over the last three decades, has proved extremely fruitful in modelling and reasoning about general dynamical systems. The emphasis in coalgebraic approaches is on the observable system behaviour and on logics which are (i) invariant under observational equivalence and (ii) sufficiently expressive to distinguish between non-equivalent systems.
The existing theory covers automata models, transition system models and even multi-player games. While notions of observational equivalence and associated (two-valued) logics are by now extremely well understood, these are often too strong for systems which exhibit quantitative (e.g. resource-aware) behaviour and where quantitative guarantees are much more desirable than qualitative ones. This project will take a systematic approach to generalising notions of behaviour, logics and associated verification procedures from a qualitative to a quantitative setting, with resource-aware systems a key instance.
