Technische Universität München Robotics and Embedded Systems

Albert Rizaldi M.Sc


Research Assistant

Room MI 03.07.039
Phone +
Fax +
Address Institut für Informatik VI
Technische Universität München
Boltzmannstraße 3
85748 Garching bei München

Curriculum Vitæ

I am PhD student under Prof. Dr.-Ing. Matthias Althoff since 2014. I completed my master degree in Erasmus Mundus programme Dependable Software Engineering (DESEM) in 2014. I spent my first and second year in Universite de Lorraine (UdL), France and University of St Andrews (StA), Scotland respectively. In UdL, I researched the problem of how we can model an insulin pump formally in Event-B specification system. In StA, I studied the foundation of action-based stochastic logic for Markov Automata. From 2011 to 2012, I was working as software engineer in Gemalto, Singapore. I also completed my bachelor degree in Electrical Engineering from Institut Teknologi Bandung, Indonesia in 2011.

Research Interests

I am doing my PhD under PUMA and my topic is mainly about formal verification of autonomous sytems in Isabelle theorem prover.

From a top-bottom perspective (Artificial Intelligence), I am currently researching about eliciting and formally specifying traffic rules, e.g. from the Vienna Convention, as a specification for self-driving cars. We believe that if a self-driving car always obeys traffic rules, it should not be held liable even during an accident. At the moment, I am inclined to use BDI logic for specifying the traffic rules. With this set of formalised traffic rules, we could design a planner in agent-oriented language to achieve a rational --- and formally verified --- agent.

From a bottom-up perspective (Cyber-Physical Systems), I am currently researching about a formally verified and executable temporal logic-based motion planner in Isabelle theorem prover. This research combines three different interpretations of `formal verification' i.e. reachability analysis, model checking, and theorem proving. A plan from this motion planner will not only be the sequence of discrete actions to perform, but also a physical controller in control theory sense --- both are formally verified.

In overall, I really like to do cross-disciplinary research (control theory, theorem proving, model checking, functional programming, multi-agent systems) so that we can have a full stack, formally verified implementation of autonomous systems.



[1] Albert Rizaldi, Jonas Keinholz, Monika Huber, Jochen Feldle, Fabian Immler, Matthias Althoff, and Eric Hilgendorf andTobias Nipkow. Formalising and monitoring traffic rules for autonomous vehicles in isabelle/hol. In integrated Formal Methods (iFM 2017), 2017. [ .bib | .pdf ]
[2] Albert Rizaldi, Fabian Immler, and Matthias Althoff. A formally verified checker of the safe distance traffic rules for autonomous vehicles. In NASA Formal Methods - 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings, pages 175-190, 2016. [ DOI | .bib | .pdf ]
[3] D. Han, A. Rizaldi, A. El-Guindy, and M. Althoff. On enlarging backward reachable sets via zonotopic set membership. In Proceedings of the IEEE International Symposium on Intelligent Control, 2016. [ .bib | .pdf ]
[4] A. Rizaldi, S. Söntges, and M. Althoff. On time-memory trade-off for collision detection. In Proc. of the IEEE Intelligent Vehicles Symposium, 2015. [ .bib | .pdf ]
[5] A. Rizaldi and M. Althoff. Formalising traffic rules for accountability of autonomous vehicles. In Proc. of the 18th IEEE International Conference on Intelligent Transportation Systems, 2015. [ .bib | .pdf ]