IC Colloquium: Shields: Runtime Enforcement for Reactive Systems
Event details
| Date | 12.12.2019 |
| Hour | 16:15 › 17:15 |
| Location | |
| Category | Conferences - Seminars |
By: Roderick Bloem - Graz University of Technology
Video of his talk
Abstract:
We often have high confidence in the correctness of a system without being able to prove its correctness. Machine learning in particular can be used to learn systems that have excellent behavior but no guarantees. We discuss an approach to learn optimal policies while enforcing properties expressed in temporal logic. To this end, given a temporal logic specification, we synthesize a reactive system called a shield. The shield monitors the actions from the learner and corrects them only if the chosen action causes a violation of the specification.
Bio:
Roderick Bloem received his M.Sc. degree in Computer Science from Leiden University, the Netherlands in 1996, and his Ph.D. degree in Computer Science from the University of Colorado at Boulder, in 2001. From 2002 until 2008, he was an Assistant at Graz University of Technology, Graz, Austria. From 2008, he has been a full professor of Computer Science at the same university. He has published over 100 peer reviewed papers in formal verification, reactive synthesis and security. He leads the Austrian National Research Network on Rigorous Systems Engineering and has organized events including the Computer Aided Verification conference and Formal Methods in Computer Aided Design.
More information
Video of his talk
Abstract:
We often have high confidence in the correctness of a system without being able to prove its correctness. Machine learning in particular can be used to learn systems that have excellent behavior but no guarantees. We discuss an approach to learn optimal policies while enforcing properties expressed in temporal logic. To this end, given a temporal logic specification, we synthesize a reactive system called a shield. The shield monitors the actions from the learner and corrects them only if the chosen action causes a violation of the specification.
Bio:
Roderick Bloem received his M.Sc. degree in Computer Science from Leiden University, the Netherlands in 1996, and his Ph.D. degree in Computer Science from the University of Colorado at Boulder, in 2001. From 2002 until 2008, he was an Assistant at Graz University of Technology, Graz, Austria. From 2008, he has been a full professor of Computer Science at the same university. He has published over 100 peer reviewed papers in formal verification, reactive synthesis and security. He leads the Austrian National Research Network on Rigorous Systems Engineering and has organized events including the Computer Aided Verification conference and Formal Methods in Computer Aided Design.
More information
Practical information
- General public
- Free
- This event is internal
Contact
- Host: Giovanni De Micheli