Hyperlogics: Expressiveness, Monitorability and Tools (H.-Lo)  

Hyperlogics: Expressiveness, Monitorability and Tools (H.-Lo)
Funded by the Icelandic Research Fund, 2026-2028
Project no. 2612260-051

Aims of the Project

The overarching aims of the H.-Lo project are
  1. to obtain a complete picture of the expressive power of the main logics that have been proposed to describe hyperproperties, which are important requirements on the behaviour of computing systems (including secure information flow, service-level agreements and mean response time, amongst others) expressed in terms of sets of their executions;
  2. to give correct-by-construction monitor-synthesis procedures that generate communicating decentralised monitors for fragments of an expressive, touchstone specification logic for hyperproperties;
  3. to offer a precise characterisation of the monitoring power of various types of communicating decentralised monitors; and
  4. to build prototype software tools for runtime monitoring based on the aforementioned theoretical advances.

Project Participants

The H.-Lo project sees the involvement of researchers at the Department of Computer Science at Reykjavik University and at the Department of Computer Science at Aalborg University, together with some of their co-workers at institutions in Italy, Malta and the Netherlands. It will be led by Luca Aceto (Reykjavik University and Gran Sasso Science Institute, PI), together with Elli Anastasiadi (Aalborg University, co-PI), Anna Ingólfsdóttir (Reykjavik University, co-PI), Kim G. Larsen (Aalborg University, co-PI) and Martin Zimmermann (Aalborg University, co-PI). Other key contributors to the project at Reykjavik University are Antonis Achilleos (Associate Professor), Aggeliki Chalki (Postdoc) and Nicola Del Giudice (Postdoc). Adrian Francalanza (Malta), Daniele Gorla (Rome "La Sapienza") and Jana Wagemaker (Radboud University Nijmegen), who co-authored one of the articles on which the project work builds, will also take part in research activities related to the project.

Project News

Publications

Submitted Papers

Luca Aceto, Antonis Achilleos, Aggeliki Chalki and Anna Ingólfsdóttir. Deciding characteristic formulae: A journey in the branching-time spectrum. Submitted for journal publication.


Last update: 3 April 2026