1

OFTEN-DeepRL: On-the-Fly Teaching of Ethical Norms to Deep Reinforcement Learning Agents
AI agents trained with reinforcement learning (RL) usually focus on completing their intended tasks without detours, as doing so …
Ignacio D. Lopez-Miguel, Sebastian Adam, Ezio Bartocci, Thomas Eiter, Martin Tappler
OFTEN-DeepRL: On-the-Fly Teaching of Ethical Norms to Deep Reinforcement Learning Agents
Rule-Guided Reinforcement Learning Policy Evaluation and Improvement
We consider the challenging problem of using domain knowledge to improve deep reinforcement learning policies. To this end, we propose …
Martin Tappler, Ignacio D. Lopez-Miguel, Sebastian Tschiatschek, Ezio Bartocci
DOI
Rule-Guided Reinforcement Learning Policy Evaluation and Improvement
Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study
The increased technological complexity and demand for software reliability require organizations to formally design and verify their …
Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Matias Salinas, Christine Betz
DOI
Student Research Abstract: Enhancing Safety in Cyber-Physical Systems Through Runtime Enforcement
The verification and safety assurance of cyber-physical systems pose significant challenges, necessitating innovative solutions for …
Ignacio D. Lopez-Miguel
Student Research Abstract: Enhancing Safety in Cyber-Physical Systems Through Runtime Enforcement
Working Together for Safer Systems: A Collaboration Model for Verification of PLC Code
Formal verification techniques are widely used in critical industries to minimize software flaws. However, despite the benefits and …
Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Enrique Blanco Viñuela, Matias Salinas, Christine Betz
DOI
Working Together for Safer Systems: A Collaboration Model for Verification of PLC Code
Progression for Monitoring in Temporal ASP
In recent years, there has been growing interest in the application of temporal reasoning approaches and non-monotonic logics from …
Davide Soldà, Ignacio D. Lopez-Miguel, Ezio Bartocci, Thomas Eiter
DOI
Progression for Monitoring in Temporal ASP
From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif
PLCverif is an actively developed project at CERN, enabling the formal verification of Programmable Logic Controller (PLC) programs in …
Zsófi Ádám, Ignacio D. Lopez-Miguel, Anastasia Mavridou, Thomas Pressburger, Marcin Bęś, Enrique Blanco Viñuela, Andreas Katis, Jean-Charles Tournier, Khanh V. Trinh, Borja Fernández Adiego
DOI
From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif
Verification of Neural Networks Meets PLC Code: An LHC Cooling Tower Control System at CERN
In the last few years, control engineers have started to use artificial neural networks (NNs) embedded in advanced feedback control …
Ignacio D. Lopez-Miguel
DOI
Verification of Neural Networks Meets PLC Code: An LHC Cooling Tower Control System at CERN
Stop at red? Engineering meets ethics
Over the past few years, artificial intelligence has fueled a revolution in several scientific fields. Intelligent agents can now give …
Ignacio D. Lopez-Miguel
DOI
Simplification of numeric variables for PLC model checking
Software model checking has recently started to be applied in the verification of programmable logic controller (PLC) programs. It …
Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Jean-Charles Tournier, Enrique Blanco Viñuela, Juan A. Rodriguez-Aguilar
DOI
Simplification of numeric variables for PLC model checking