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

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;
to give correct-by-construction monitor-synthesis procedures that generate communicating decentralised monitors for fragments of an expressive, touchstone specification logic for hyperproperties;
to offer a precise characterisation of the monitoring power of various types of communicating decentralised monitors; and
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

7-12 March 2027: Elli Anastasiadi and Martin Zimmermann will take part in, and contribute to, Dagstuhl Seminar 27101, Towards a Unified Theory and Application of Hyperproperties.
1 October 2026: Aggeliki Chalki joins H.-Lo as a postdoctoral researcher.
15-17 September 2026: Elli Anastasiadi co-organises GandALF 2026.
14 September 2026: Project meeting at the Department of Computer Science at Aalborg University. Details will be posted in due course.
1 September 2026-28 February 2027: Pietro Bernabei, PhD student at IMT Lucca, visits the project at Reykjavik University hosted by Luca Aceto.
6-10 July 2026: Elli Anastasiadi and Martin Zimmermann delivered invited talks at a Special Session on Logics for Formal Verification at the 15th Panhellenic Logic Symposium, which was held in Athens, Greece. Elli's talk was entitled "Equational logic for formal verification" and Martin spoke about "Game-based model-checking of hyperproperties". See here for more details.
8-22 June 2026: Luca Aceto visits the Department of Computer Science at Aalborg University.
15 April 2026: Nicola Del Giudice joins H.-Lo as a postdoctoral researcher from the University of Camerino.

Publications

Conference and Workshop Papers

Antonis Achilleos and Vasiliki Kyriakou. A Topological Framework for Finite Behavioural Observations and Verification. Proceedings of the Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2026, 15-17 September 2026, Aalborg, Denmark, EPTCS 454, 2026, pp. 13-30.
Elli Anastasiadi, Aske Leth Raaen Thomsen, Christian Steen Nielsen, Nina Hansen Blegmand and Simon Stjernholm. Dynamic Device Environments in Runtime Verification: Monitoring Power Consumption in Smart Homes. Proceedings of STARS 2026, 1st workshop on STAtic + Runtime verification Synergies, 23 November 2026 – Satellite event of SEFM 2026, Malta. To appear. [Entry in the workshop programme]
Gaetan Regaud and Martin Zimmermann. The Complexity of Asynchronous HyperLTL. Proceedings of the Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2026, 15-17 September 2026, Aalborg, Denmark, EPTCS 454, 2026, pp. 183-199.
Sarah Winter and Martin Zimmermann. Logics for Context-free Hyperproperties. Proceedings of the 51st conference on Mathematical Foundations of Computer Science, MFCS 2026, 24-28 August 2026, Paris, France, LIPIcs 386, pp. 54:1-54:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2026. [arXiv version]

Submitted Papers

Luca Aceto, Antonis Achilleos, Aggeliki Chalki and Anna Ingólfsdóttir. Deciding characteristic formulae: A journey in the branching-time spectrum.
Elli Anastasiadi, Kim Guldstrand Larsen and Martin Zimmermann. Model Checking HyperRecHML is Decidable.

Last update: 19 October 2026