Search Results

Documents authored by Könighofer, Bettina

Document
DOI: 10.4230/DagRep.14.2.95
Safety Assurance for Autonomous Mobility (Dagstuhl Seminar 24071)

Authors: Jyotirmoy Deshmukh, Bettina Könighofer, Dejan Ničković, and Filip Cano

Published in: Dagstuhl Reports, Volume 14, Issue 2 (2024)

Abstract
This report documents the program and the outcomes of the Dagstuhl Seminar "Safety Assurance for Autonomous Mobility" (24071). The seminar brought together an interdisciplinary group of researchers and practitioners from the fields of formal methods, cyber-physical systems, and artificial intelligence, with a common interest in autonomous mobility. Through a series of talks, working groups, and open problem discussions, participants explored the challenges and opportunities associated with ensuring the safety of autonomous systems in various domains, including industrial automation, automotive, railways, and aerospace. Key topics addressed included the need for industrial-grade autonomous products to operate reliably in safety-critical environments, highlighting the lack of standardized procedures for obtaining safety certifications for AI-based systems. Recent advancements in the verification and validation (V&V) of autonomous mobility systems were presented, focusing on requirements verification, testing, certification, and correct-by-design approaches. Overall, the seminar provided a comprehensive overview of the current state and future directions in safe autonomous mobility, emphasizing the need for interdisciplinary collaboration and innovation to address the complex challenges in this rapidly evolving field.
Cite as

Jyotirmoy Deshmukh, Bettina Könighofer, Dejan Ničković, and Filip Cano. Safety Assurance for Autonomous Mobility (Dagstuhl Seminar 24071). In Dagstuhl Reports, Volume 14, Issue 2, pp. 95-119, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{deshmukh_et_al:DagRep.14.2.95,
  author =	{Deshmukh, Jyotirmoy and K\"{o}nighofer, Bettina and Ni\v{c}kovi\'{c}, Dejan and Cano, Filip},
  title =	{{Safety Assurance for Autonomous Mobility (Dagstuhl Seminar 24071)}},
  pages =	{95--119},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{14},
  number =	{2},
  editor =	{Deshmukh, Jyotirmoy and K\"{o}nighofer, Bettina and Ni\v{c}kovi\'{c}, Dejan and Cano, Filip},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.2.95},
  URN =		{urn:nbn:de:0030-drops-205009},
  doi =		{10.4230/DagRep.14.2.95},
  annote =	{Keywords: aerospace, automotive, autonomy, formal methods, railway}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2024.2
Abstraction-Based Decision Making for Statistical Properties (Invited Talk)

Authors: Filip Cano, Thomas A. Henzinger, Bettina Könighofer, Konstantin Kueffner, and Kaushik Mallik

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Sequential decision-making in probabilistic environments is a fundamental problem with many applications in AI and economics. In this paper, we present an algorithm for synthesizing sequential decision-making agents that optimize statistical properties such as maximum and average response times. In the general setting of sequential decision-making, the environment is modeled as a random process that generates inputs. The agent responds to each input, aiming to maximize rewards and minimize costs within a specified time horizon. The corresponding synthesis problem is known to be PSPACE-hard. We consider the special case where the input distribution, reward, and cost depend on input-output statistics specified by counter automata. For such problems, this paper presents the first PTIME synthesis algorithms. We introduce the notion of statistical abstraction, which clusters statistically indistinguishable input-output sequences into equivalence classes. This abstraction allows for a dynamic programming algorithm whose complexity grows polynomially with the considered horizon, making the statistical case exponentially more efficient than the general case. We evaluate our algorithm on three different application scenarios of a client-server protocol, where multiple clients compete via bidding to gain access to the service offered by the server. The synthesized policies optimize profit while guaranteeing that none of the server’s clients is disproportionately starved of the service.
Cite as

Filip Cano, Thomas A. Henzinger, Bettina Könighofer, Konstantin Kueffner, and Kaushik Mallik. Abstraction-Based Decision Making for Statistical Properties (Invited Talk). In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{cano_et_al:LIPIcs.FSCD.2024.2,
  author =	{Cano, Filip and Henzinger, Thomas A. and K\"{o}nighofer, Bettina and Kueffner, Konstantin and Mallik, Kaushik},
  title =	{{Abstraction-Based Decision Making for Statistical Properties}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{2:1--2:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.2},
  URN =		{urn:nbn:de:0030-drops-203310},
  doi =		{10.4230/LIPIcs.FSCD.2024.2},
  annote =	{Keywords: Abstract interpretation, Sequential decision making, Counter machines}
}
Document
DOI: 10.4230/DagRep.13.10.24
Accountable Software Systems (Dagstuhl Seminar 23411)

Authors: Bettina Könighofer, Joshua A. Kroll, Ruzica Piskac, Michael Veale, and Filip Cano Córdoba

Published in: Dagstuhl Reports, Volume 13, Issue 10 (2024)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23411 "Accountable Software Systems". The seminar brought together an interdisciplinary group of researchers from the fields of formal methods, machine learning, philosophy, political science, law, and policy studies to address the critical issue of accountability in the development and deployment of software systems. As these systems increasingly assume roles within safety-critical domains of society, including transportation, healthcare, recruitment, and the judiciary, the seminar aimed to explore the multifaceted concept of accountability, its significance, and its implementation challenges in this context. During the seminar, experts engaged deeply in discussions, presentations, and collaborative sessions, focusing on key themes such as the application of formal tools in socio-technical accountability, the impact of computing infrastructures on software accountability, and the innovation of formal languages and models to improve accountability measures. This interdisciplinary dialogue underscored the complexities involved in defining and operationalizing accountability, especially in light of technological advancements and their societal implications. The participants of the seminar reached a consensus on the pressing need for ongoing research and cross-disciplinary efforts to develop effective accountability mechanisms, highlighting the critical role of integrating socio-technical approaches and formal methodologies to enhance the accountability of autonomous systems and their contributions to society.
Cite as

Bettina Könighofer, Joshua A. Kroll, Ruzica Piskac, Michael Veale, and Filip Cano Córdoba. Accountable Software Systems (Dagstuhl Seminar 23411). In Dagstuhl Reports, Volume 13, Issue 10, pp. 24-49, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{konighofer_et_al:DagRep.13.10.24,
  author =	{K\"{o}nighofer, Bettina and Kroll, Joshua A. and Piskac, Ruzica and Veale, Michael and C\'{o}rdoba, Filip Cano},
  title =	{{Accountable Software Systems (Dagstuhl Seminar 23411)}},
  pages =	{24--49},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{10},
  editor =	{K\"{o}nighofer, Bettina and Kroll, Joshua A. and Piskac, Ruzica and Veale, Michael and C\'{o}rdoba, Filip Cano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.10.24},
  URN =		{urn:nbn:de:0030-drops-198328},
  doi =		{10.4230/DagRep.13.10.24},
  annote =	{Keywords: accountability, Responsible Decision Making, Societal Impact of AI}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2020.3
Safe Reinforcement Learning Using Probabilistic Shields (Invited Paper)

Authors: Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban, and Roderick Bloem

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
This paper concerns the efficient construction of a safety shield for reinforcement learning. We specifically target scenarios that incorporate uncertainty and use Markov decision processes (MDPs) as the underlying model to capture such problems. Reinforcement learning (RL) is a machine learning technique that can determine near-optimal policies in MDPs that may be unknown before exploring the model. However, during exploration, RL is prone to induce behavior that is undesirable or not allowed in safety- or mission-critical contexts. We introduce the concept of a probabilistic shield that enables RL decision-making to adhere to safety constraints with high probability. We employ formal verification to efficiently compute the probabilities of critical decisions within a safety-relevant fragment of the MDP. These results help to realize a shield that, when applied to an RL algorithm, restricts the agent from taking unsafe actions, while optimizing the performance objective. We discuss tradeoffs between sufficient progress in the exploration of the environment and ensuring safety. In our experiments, we demonstrate on the arcade game PAC-MAN and on a case study involving service robots that the learning efficiency increases as the learning needs orders of magnitude fewer episodes.
Cite as

Nils Jansen, Bettina Könighofer, Sebastian Junges, Alex Serban, and Roderick Bloem. Safe Reinforcement Learning Using Probabilistic Shields (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{jansen_et_al:LIPIcs.CONCUR.2020.3,
  author =	{Jansen, Nils and K\"{o}nighofer, Bettina and Junges, Sebastian and Serban, Alex and Bloem, Roderick},
  title =	{{Safe Reinforcement Learning Using Probabilistic Shields}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{3:1--3:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.3},
  URN =		{urn:nbn:de:0030-drops-128155},
  doi =		{10.4230/LIPIcs.CONCUR.2020.3},
  annote =	{Keywords: Safe Reinforcement Learning, Formal Verification, Safe Exploration, Model Checking, Markov Decision Process}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact