Correct-by-Construction Runtime Enforcement in AI – A Survey

Bettina Könighofer*, Roderick Bloem, Rüdiger Ehlers, Christian Pek

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

Abstract

Runtime enforcement refers to the theories, techniques, and tools for enforcing correct behavior with respect to a formal specification of systems at runtime. In this paper, we are interested in techniques for constructing runtime enforcers for the concrete application domain of enforcing safety in AI. We discuss how safety is traditionally handled in the field of AI and how more formal guarantees on the safety of a self-learning agent can be given by integrating a runtime enforcer. We survey a selection of work on such enforcers, where we distinguish between approaches for discrete and continuous action spaces. The purpose of this paper is to foster a better understanding of advantages and limitations of different enforcement techniques, focusing on the specific challenges that arise due to their application in AI. Finally, we present some open challenges and avenues for future work.

Original languageEnglish
Title of host publicationPrinciples of Systems Design
Subtitle of host publicationEssays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday
EditorsJF Raskin, R. Bloem, R. Ehlers, C. Pek
Place of PublicationCham
PublisherSpringer Science and Business Media Deutschland GmbH
Pages650-663
Number of pages14
ISBN (Electronic)978-3-031-22337-2
ISBN (Print)978-3-031-22336-5
DOIs
Publication statusPublished - 2022

Publication series

NameLecture Notes in Computer Science
Volume13660
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • Formal methods
  • Reinforcement learning
  • Runtime enforcement
  • Safety in AI
  • Shielding

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Correct-by-Construction Runtime Enforcement in AI – A Survey'. Together they form a unique fingerprint.

Cite this