Theoretical Foundations for Monitorability
Icelandic Research Fund Project nr. 163406-051 (January 2016-August 2020)
Status: Completed

• to explore more stringent conditions for detection than the ones considered in the RV 2015 paper and study whether this has any effect on the monitorable subset of the logic;
• to investigate the monitorability of the logic with respect to instrumentation set-ups other than the one used in the RV 2015 paper;
• to extend our results from the RV 2015 paper to the setting of real-time systems, modelled as timed automata, and to a real-time variant of Hennessy-Milner Logic with recursion;
• to understand how existing notions of monitorability relate to the one formulated in the RV 2015 paper, thereby consolidating disparate concepts of monitorability;
• to investigate extensions to monitorability that incorporate notions of enforceability; and
• to apply the results of the theoretical work in the construction of a prototype software tool for the runtime analysis of systems.

Researchers

Project-related events (in reverse chronological order)

• 16-24 November 2019: Adrian Francalanza and Duncan Paul Attard (University of Malta) visit ICE-TCS. The hosts for their stay are Luca Aceto, Antonis Achilleos and Anna Ingólfsdóttir.
• 15-23 November 2019: Karoliina Lehtinen (University of Liverpool, UK) visits ICE-TCS. The hosts for her stay are Luca Aceto, Antonis Achilleos and Anna Ingólfsdóttir.
• Monday, 16 September 2019: Kim G. Larsen (Aalborg University, Denmark) will deliver a joint ICE-TCS/RUAP seminar entitled Synthesis, Verification and Optimization for Cyber-Physical Systems from 14:00 till 15:00 in room M1.03. Refreshments will be served at 13:30.
• 12-17 September 2019: Kim G. Larsen (Aalborg University, Denmark) visits ICE-TCS. The hosts for his visit are Luca Aceto and Anna Ingólfsdóttir.
• 10 September 2019: Luca Aceto delivers an invited talk at the Colloquium Jacques Morgenstern, INRIA Sophia Antipolis.
• 28 January-29 May 2019: Duncan Paul Attard (University of Malta) will be visiting ICE-TCS. The hosts for his stay are Luca Aceto, Antonis Achilleos and Anna Ingólfsdóttir.
• Friday, 16 November 2018: Antonis Achilleos is an invited speaker at NYCAC 2018, The New York Colloquium on Algorithms and Complexity 2018, The Graduate Center, CUNY, New York City. Antonis Achilleos will present Adventures in monitorability.
• 9 November 2018: Antonis Achilleos will present an overview of the results of the TheoFoMon project at the ICE-TCS/GSSI workshop, which will be held at the Gran Sasso Science Institute, L'Aquila, Italy.
• 17 September-7 December 2018: Ian Cassar (University of Malta and Reykjavik University) will visit ICE-TCS. The hosts for his stay are Luca Aceto, Antonis Achilleos and Anna Ingólfsdóttir.
• 3 September 2018: Adrian Francalanza will deliver an invited talk at the Combined 25th International Workshop on Expressiveness in Concurrency and 15th Workshop on Structural Operational Semantics (EXPRESS/SOS 2018), Beijing, China.
• 19-21 March 2018: Adrian Francalanza will be one of the speakers at the 2nd ARVI COST School on Runtime Verification, sponsored by COST association, Inria, and Persyval-Lab, to be held at Praz sur Arly, France.
• 20-27 January 2018: Karoliina Lehtinen (Christian-Albrechts University of Kiel, Germany) will be visiting ICE-TCS. The hosts for her stay are Luca Aceto and Anna Ingólfsdóttir.
• 19-27 January 2018: Adrian Francalanza (University of Malta) will be visiting ICE-TCS. The hosts for his stay are Luca Aceto and Anna Ingólfsdóttir.
• 15 January-15 March 2018: Duncan Paul Attard and Ian Cassar (both at the University of Malta) will be visiting ICE-TCS. The hosts for their stay are Luca Aceto and Anna Ingólfsdóttir.
• 17 November-8 December 2017: Antonis Achilleos visits the University of Malta.
• 12-15 November 2017: Adrian Francalanza has been invited to attend Dagstuhl Seminar 17462: A Shared Challenge in Behavioural Specification, organized by Klaus Havelund, Martin Leucker, Giles Reger and Volker Stolz.
• Wednesday, 20 September 2017: Luca Aceto will be an invited speaker at the 8th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF'17), Rome, Italy, 20--22 September 2017.
• Tuesday, 19 September 2017: Adrian Francalanza co-organizes the workshop Pre- and post-deployment verification techniques (PrePost), Second International Workshop, co-located with iFM 2017.
• Wednesday, 13 September 2017: Adrian Francalanza delivers an invited tutorial entitled Foundations For Runtime Monitoring at RV 2017.
• 30 June-11 July 2017: Antonis Achilleos visits the University of Malta.
• 5 February-5 March 2017: Antonis Achilleos visits the University of Malta.
• 5-12 February 2017: Guðmundur Stefánsson visits the University of Malta.
• Saturday, 4 June 2016: Luca Aceto, Adrian Francalanza and Anna Ingólfsdóttir organize the workshop Pre- and post-deployment verification techniques (PrePost), co-located with iFM 2016.

Publications

Books and edited volumes

1. Luca Aceto and David de Frutos Escrig. Special Issue: Selected papers from the 26th International Conference on Concurrency Theory (CONCUR 2015), Acta Informatica 54(1):1--125, February 2017.
2. Luca Aceto and David de Frutos Escrig. Special Issue: Selected papers from the 26th International Conference on Concurrency Theory (CONCUR 2015), Acta Informatica 54(2):127-242, March 2017.
3. Luca Aceto and David de Frutos Escrig. Special Issue: Selected papers from the 26th International Conference on Concurrency Theory (CONCUR 2015), Acta Informatica 54(3):243--341, May 2017.
4. Luca Aceto, Adrian Francalanza and Anna Ingólfsdóttir (Eds.). Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques (PrePost 2016). EPTCS Vol. 208, 25 May 2016.
5. Adrian Francalanza and Gordon J. Pace. Proceedings Second Workshop on Pre- and Post-Deployment Verification Techniques (PrePost 2017). EPTCS Vol. 254, July 2017.

Book chapters

1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir and Karoliina Lehtinen. Testing Equivalence vs. Runtime Monitoring. Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday ( Michele Boreale, Flavio Corradini, Michele Loreti, Rosario Pugliese eds.), Lecture Notes in Computer Science 11665, pp. 28-44, Springer 2019. [Official published version]
2. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir and Karoliina Lehtinen. The Cost of Monitoring Alone. From Reactive Systems to Cyber-Physical Systems - Essays Dedicated to Scott A. Smolka on the Occasion of His 65th Birthday (Ezio Bartocci, Rance Cleaveland, Radu Grosu, Oleg Sokolsky, eds.), Lecture Notes in Computer Science 11500, pp. 259-275, Springer 2019. [Official published version]
3. Duncan Paul Attard, Ian Cassar, Adrian Francalanza, Luca Aceto and Anna Ingólfsdóttir. A Runtime Monitoring Tool for Actor-Based Systems. In Behavioural Types: from Theory to Tools (Simon Gay and Antonio Ravara eds.), Chapter 3, pp. 49-76, River Publishers, 2017.

Journal papers

1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir. The Complexity of Identifying Characteristic Formulae. Journal of Logical and Algebraic Methods in Programming 112, Elsevier, April 2020. [Publisher's version]
2. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Sævar Örn Kjartansson. Determinizing Monitors for HML with Recursion. Journal of Logical and Algebraic Methods in Programming 111, Elsevier, 2020. [Publisher's version]
3. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir and Karoliina Lehtinen. Adventures in Monitorability: From Branching to Linear Time and Back Again. Proc. ACM Program. Lang., Vol. 3, No. POPL, Article 52. January 2019. [Official ACM version (open access)]
4. Luca Aceto, Ian Cassar, Adrian Francalanza and Anna Ingólfsdóttir. Comparing Controlled System Synthesis and Suppression Enforcement. International Journal on Software Tools for Technology Transfer (STTT), Springer, 2020. To appear.
5. Adrian Francalanza, Luca Aceto and Anna Ingólfsdóttir. Monitorability for the Hennessy-Milner Logic with Recursion. Formal Methods in System Design, Springer, 2017. The official journal paper is here.

Conference and workshop papers

1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Sævar Örn Kjartansson. On the Complexity of Determinizing Monitors. Proceedings of 22nd International Conference Implementation and Application of Automata (CIAA 2017) (Arnaud Carayol and Cyril Nicaud eds.), Lecture Notes in Computer Science 10329, pp. 1-13, Springer, June 2017. [Official publisher version of the paper]
2. Luca Aceto, Antonis Achilleos, Adrian Francalanza and Anna Ingólfsdóttir. Monitoring for Silent Actions. Proceedings of FSTTCS 2017, the 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs, December 2017. To appear. [Authors' version]
3. Luca Aceto, Antonis Achilleos, Adrian Francalanza and Anna Ingólfsdóttir. A Framework for Parameterized Monitorability. Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018), Lecture Notes in Computer Science 10803, pp. 203-220, Springer, April 2018. [Official publisher version of the paper]
4. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir and Karoliina Lehtinen. An Operational Guide to Monitorability. Proceedings of the 17th International Conference on Software Engineering and Formal Methods (SEFM 2019), LNCS, September 2019.
5. Luca Aceto, Ian Cassar, Adrian Francalanza, Anna Ingólfsdóttir. On Runtime Enforcement via Suppressions. Proceedings of the 29th International Conference on Concurrency Theory, CONCUR 2018, Leibniz International Proceedings in Informatics (LIPIcs) 118, pp. 34:1--34:17, September 2018.
6. Luca Aceto, Ian Cassar, Adrian Francalanza and Anna Ingólfsdóttir. Comparing Controlled System Synthesis and Suppression Enforcement. In: Finkbeiner B., Mariani L. (eds) Runtime Verification. RV 2019. Lecture Notes in Computer Science, vol 11757, pp. 148-164, Springer, October 2019. [Official publisher version]
7. Antonis Achilleos. The Completeness Problem for Modal Logic. Proceedings of Symposium on LOGICAL FOUNDATIONS OF COMPUTER SCIENCE (LFCS'18), Lecture Notes in Computer Science, Springer, December 2017. To appear. [arXiv version].
8. Duncan Paul Attard and Adrian Francalanza. A Monitoring Tool for a Branching-Time Logic. Proceedings of Runtime Verification - 16th International Conference, RV 2016, Volume 10012 of Lecture Notes in Computer Science, pp. 473--481, Springer-Verlag, 2016.
9. Duncan Paul Attard and Adrian Francalanza. Trace Partitioning and Local Monitoring for Asynchronous Components, Proceedings of 15th International Conference on Software Engineering and Formal Methods, SEFM 2017, Lecture Notes in Computer Science, Springer-Verlag, September 2017.
10. Giovanni Bernardi and Adrian Francalanza. Full-Abstraction for Must Testing Preorders (Extended Abstract). In: Jacquet JM., Massink M. (eds) Coordination Models and Languages. COORDINATION 2017. Lecture Notes in Computer Science, vol 10319, pp 237-255. Springer, 2017. [Publisher's version]
11. Ian Cassar and Adrian Francalanza. On Implementing a Monitor-Oriented Programming Framework for Actor Systems. Proceedings of Integrated Formal Methods 2016 (iFM 2016), Volume 9681 of the series Lecture Notes in Computer Science, pp. 176-192, Springer-Verlag, June 2016.
12. Ian Cassar, Adrian Francalanza, Luca Aceto and Anna Ingólfsdóttir. eAOP - An Aspect Oriented Programming Framework for Erlang. Proceedings of the 16th ACM Erlang Workshop 2017, pp. 20-30, ACM Press 2017. [Authors' version]
13. Ian Cassar, Adrian Francalanza, Luca Aceto and Anna Ingólfsdóttir. A Survey of Runtime Monitoring Instrumentation Techniques. Proceedings of PrePost 2017, EPTCS, September 2017.
14. Ian Cassar, Adrian Francalanza, Duncan Paul Attard, Luca Aceto and Anna Ingólfsdóttir. A generic instrumentation tool for Erlang. Proceedings of RV-CuBES 2017 (International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools) (Giles Reger and Klaus Havelund eds.), Kalpa Publications in Computing, vol. 3, pp. 48-54, EasyChair, December 2017.
15. Ian Cassar, Adrian Francalanza, Duncan Paul Attard, Luca Aceto and Anna Ingólfsdóttir. A Suite of Monitoring Tools for Erlang. Proceedings of RV-CuBES 2017 (International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools) (Giles Reger and Klaus Havelund eds.), Kalpa Publications in Computing, vol. 3, pp. 41-47, EasyChair, December 2017.
16. Adrian Francalanza. A Theory of Monitors. Proceedings of Foundations of Software Science and Computation Structures, Volume 9634 of the series Lecture Notes in Computer Science, pp. 145-161, Springer-Verlag, April 2016.
17. Adrian Francalanza. Consistently-Detecting Monitors, Proceedings of the 28th International Conference on Concurrency Theory, CONCUR 2017, LIPIcs, September 2017.
18. Adrian Francalanza, Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Ian Cassar, Dario Della Monica and Anna Ingólfsdóttir. A Foundation for Runtime Monitoring. Proceedings of Runtime Verification 2017, Lecture Notes in Computer Science 10548, pp. 8-29, Springer, September 2017.
19. Vignir Gudmundsson, Mikael Lindvall, Luca Aceto, Johann Bergthorsson and Dharmalingam Ganesan. Model-based Testing of Mobile Systems – An Empirical Study on QuizUp Android App. Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques (PrePost 2016), Reykjavík, Iceland, 4th June 2016, Electronic Proceedings in Theoretical Computer Science 208, pp. 16–30. Published: 25th May 2016. [ArXiv]
20. Annalizz Vella and Adrian Francalanza. Preliminary Results Towards Contract Monitorability. Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques (PrePost 2016), Reykjavík, Iceland, 4th June 2016, Electronic Proceedings in Theoretical Computer Science 208, pp. 54–63. Published: 25th May 2016. [ArXiv]

Other publications

1. Luca Aceto, Antonis Achilleos, Adrian Francalanza and Anna Ingólfsdóttir. The Complexity of Identifying Characteristic Formulas for muHML. Proceedings of PLS11 (11th Panhellenic Logic Symposium), July 2017.
2. Luca Aceto, Antonis Achilleos, Adrian Francalanza and Anna Ingólfsdóttir. The Complexity of Identifying Characteristic Formulae. Proceedings of the 30th Nordic Workshop on Programming Theory, Oslo, Norway.
3. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir. The Complexity of Recursion in Modal Logic: First Steps. Proceeedings of the 12th Panhellenic Logic Symposium, June 2019.
4. Luca Aceto, Elli Anastasiadi and Anna Ingólfsdóttir. An Axiomatization of Verdict Equivalence over Regular Monitors. Proceeedings of the 12th Panhellenic Logic Symposium, June 2019.
5. Luca Aceto and David de Frutos Escrig. Foreword for the special issue of Acta Informatica devoted to selected papers from CONCUR 2015. Acta Informatica, Springer, February 2017. The official published version can be freely viewed here.
6. Dario Della Monica and Adrian Francalanza. Pushing runtime verification to the limit: May process semantics be with us. First Overlay Workshop (held as part of the 18th International Conference of the Italian Association for Artificial Intelligence, AIIA 2019), 19-20 November 2019, Rende, Italy.

Submitted papers

1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir and Karoliina Lehtinen. An Operational Guide to Monitorability (version dated 27 August 2020). Submitted to the journal Software and Systems Modeling, Springer. [Older version dated 28 February 2020].
2. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir and Karoliina Lehtinen. The best a monitor can do. Submitted for conference publication.
3. Luca Aceto, Duncan Paul Attard, Adrian Francalanza, Anna Ingólfsdóttir. On Benchmarking for Concurrent Runtime Monitoring. Submitted for conference publication.
4. Luca Aceto, Duncan Paul Attard, Adrian Francalanza, Anna Ingólfsdóttir. On Monitoring Asynchronous Components, Asynchronously. Submitted for conference publication.
5. Luca Aceto, Ian Cassar, Adrian Francalanza, Anna Ingólfsdóttir. On bidirectional enforcement. Submitted for conference publication. Version dated 24 October 2019.
6. Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Karoliina Lehtinen and Mathis Ruggaard Pedersen. On Probabilistic Monitorability. Submitted for publication.

Pre-prints and Technical Reports

1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Sævar Örn Kjartansson. Determinizing Monitors for HML with Recursion. Version dated 30 November 2016, 53 pages.

Student theses

1. Ian Cassar. Developing Theoretical Foundations for Runtime Enforcement. PhD dissertation.
2. Guðmundur Stefánsson. Work on new event sources for detectEr. MSc thesis, May 2017.
3. Kari Tristan Helgason. Runtime Verification with DetectEr: a case study. Undergraduate research opportunity article at Reykjavik University. May 2015.
4. Sævar Örn Kjartansson. The expressive power of deterministic monitors for muHML. Research-based BSc thesis in the Discrete Mathematics and Computer Science programme at Reykjavik University. December 2015.

Software tools

1. detectEr^LITE
2. detectEr for Java