Publications



2017
[Ehl17] Rüdiger Ehlers. Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks. Accepted at the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017).
The preprint of the paper is available on ArXiV/CoRR.
[DERBK17] Jonathan A. DeCastro, Rüdiger Ehlers, Matthias Rungger, Ayca Balkan, Hadas Kress-Gazit. Automated generation of dynamics-based runtime certificates for high-level control. Discrete Event Dynamic Systems 27(2): 371-405, 2017, Springer Verlag.
[ELTV17] Rüdiger Ehlers, Stéphane Lafortune, Stavros Tripakis, and Moshe Y. Vardi. Supervisory Control and Reactive Synthesis: A Comparative Introduction. Discrete Event Dynamic Systems 27(2): 209-260, 2017, Springer Verlag.
[REG17] Heinz Riener, Rüdiger Ehlers, and Görschwin Fey. CEGAR-based EF Synthesis of Boolean Functions with an Application to Circuit Rectification. 23rd Asia and South Pacific Design Automation Conference (ASP-DAC 2017).
The authors' version of the work is posted here for your personal use. Not for redistribution.
2016
[ER16] Rüdiger Ehlers, Salar Moarref, and Ufuk Topcu. Risk-Averse Control of Markov Decision Processes with Omega-regular Objectives. 55th IEEE Conference on Decision and Control (CDC 2016).
[ER16] Rüdiger Ehlers and Vasumathi Raman. Slugs: Extensible GR(1) Synthesis. 28th International Conference on Computer Aided Verification (CAV 2016).
The original publication is available at www.springerlink.com
2015
[ERB15] Rüdiger Ehlers, Robert Könighofer, and Roderick Bloem. Cooperative Reactive Synthesis. 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015)
The original publication is available at www.springerlink.com
[REG15] Heinz Riener, Rüdiger Ehlers, and Görschwin Fey. Path-Based Program Repair. 12th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA 2015).
[WET15] Min Wen, Rüdiger Ehlers, and Ufuk Topcu. Correct-by-synthesis Reinforcement Learning with Temporal Logic Constraints. 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2015).
[ET15] Rüdiger Ehlers, Robert Könighofer, and Roderick Bloem. Synthesizing Cooperative Reactive Mission Plans. 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2015).
This is the authors' version of the work. It is posted here for your personal use. Not for redistribution.
[ET15] Rüdiger Ehlers and Ufuk Topcu. Estimator-Based Reactive Synthesis under Incomplete Information. 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015).
This is the authors' version of the work. It is posted here for your personal use. Not for redistribution.
2014
[WEG14] Kai Weng Wong, Rüdiger Ehlers, and Hadas Kress-Gazit. Correct High-level Robot Behavior in Environments with Unexpected Events. Robotics: Science and Systems X (RSS 2014)
[EL14] Rüdiger Ehlers and Martin Lange. A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic. 7th International Joint Conference on Automated Reasoning (IJCAR 2014)
[ET14] Rüdiger Ehlers and Ufuk Topcu. Resilience to Intermittent Assumption Violations in Reactive Synthesis. 17th International Conference on Hybrid Systems: Computation and Control (HSCC 2014)
[ESK14] Rüdiger Ehlers, Sanjit A. Seshia, and Hadas Kress-Gazit. Synthesis with Identifiers. 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014).
The original publication is available at www.springerlink.com
2013
[JEK13] Gangyuan Jing, Rüdiger Ehlers, and Hadas Kress-Gazit. Shortcut Through an Evil Door: Optimality of Correct-by-Construction Controllers in Adversarial Environments. IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2013)
[ELTV13] Rüdiger Ehlers, Stephane Lafortune, Stavros Tripakis, and Moshe Vardi. Reactive Synthesis vs. Supervisory Control: Bridging the Gap, 2013. UC Berkeley Technical Report No. UCB/EECS-2013-162
[Ehl13] Rüdiger Ehlers. Symmetric and Efficient Synthesis, Dissertation, Saarland University
2012
[EKH12] Rüdiger Ehlers, Robert Könighofer, and Georg Hofferek. Symbolically Synthesizing Small Circuits. 12th Conference on Formal Methods in Computer-Aided Design (FMCAD 2012)
[BELM12] Bernd Becker, Rüdiger Ehlers, Matthew Lewis, and Paolo Marin. ALLQBF Solving by Computational Learning. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA 2012)
The original publication is available at www.springerlink.com
[Ehl12b] Rüdiger Ehlers. ACTL ∩ LTL Synthesis. 24th International Conference on Computer Aided Verification (CAV 2012).
The original publication is available at www.springerlink.com
[EM12] Rüdiger Ehlers and Daniela Moldovan. Sparse Positional Strategies for Safety Games. 1st Workshop on Synthesis (SYNT 2012).
[GEFP12] Michael Gerke, Rüdiger Ehlers, Bernd Finkbeiner, and Hans-Jörg Peter. FlexRay for Avionics: Automatic Verification with Parametric Physical Layers. Infotech@Aerospace 2012
[Ehl12a] Rüdiger Ehlers. Symbolic Bounded Synthesis. Formal Methods in System Design, Volume 40, Number 2, 2012. Extended journal version of [Ehl10c].
The original publication is available at www.springerlink.com
2011
[EF11b] Rüdiger Ehlers and Bernd Finkbeiner. Monitoring Realizability. 2nd International Conference on Runtime Verification (RV 2011)
The original publication is available at www.springerlink.com
[Ehl11d] Rüdiger Ehlers. Small witnesses, accepting lassos and winning strategies in omega-automata and games, 2011. AVACS Technical Report No. 80, SFB/TR 14 AVACS, also appeared as arXiv/CoRR: 1108.0315
[EF11] Rüdiger Ehlers and Bernd Finkbeiner. Reactive Safety. Second International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2011) (Errata)
[Ehl11c] Rüdiger Ehlers. Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis.
Third NASA Formal Methods Symposium (NFM 2011). Peer-reviewed conference version of the discussion paper [Ehl10a]. (Erratum)
The original publication is available at www.springerlink.com
[Ehl11b] Rüdiger Ehlers. Unbeast: Symbolic Bounded Synthesis.
Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011). Tool paper.
The original publication is available at www.springerlink.com
[Ehl11a] Rüdiger Ehlers. Experimental Aspects of Synthesis.
International Workshop on Interactions, Games and Protocols 2011 (iWIGP 2011)
2010
[EFGP10] Rüdiger Ehlers, Daniel Fass, Michael Gerke and Hans-Jörg Peter. Fully Symbolic Timed Model Checking using Constraint Matrix Diagrams. Thirty-first IEEE Real-Time Systems Symposium (RTSS 2010). (Errata)
[EGP10] Rüdiger Ehlers, Michael Gerke and Hans-Jörg Peter. Making the Right Cut in Model Checking Data-Intensive Timed Systems. Twelfth International Conference on Formal Engineering Methods (ICFEM 2010).
[GEFP10] Michael Gerke, Rüdiger Ehlers, Bernd Finkbeiner and Hans-Jörg Peter. Model Checking the FlexRay Physical Layer Protocol. Formal Methods for Industrial Critical Systems (FMICS 2010).
[EF10] Rüdiger Ehlers and Bernd Finkbeiner. On the Virtue of Patience: Minimizing Büchi Automata. 17th International SPIN Workshop on Model Checking of Software (SPIN 2010).
The original publication is available at www.springerlink.com
[EMP10] Rüdiger Ehlers, Robert Mattmüller and Hans-Jörg Peter. Combining Symbolic Representations for Solving Timed Games. Eighth International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2010).
[Ehl10d] Rüdiger Ehlers. Minimising Deterministic Büchi Automata Precisely using SAT Solving. Thirteenth International Conference on Theory and Applications of Satisfiability Testing (SAT 2010). (Slides)
The original publication is available at www.springerlink.com
[Ehl10c] Rüdiger Ehlers. Symbolic Bounded Synthesis. 22nd International Conference on Computer Aided Verification (CAV 2010). (Author’s notes)
The original publication is available at www.springerlink.com
[Ehl10b] Rüdiger Ehlers. Short Witnesses and Accepting Lassos in omega-automata. 4th International Conference on Language and Automata Theory and Applications (LATA 2010). (Author’s notes & erratum)
The original publication is available at www.springerlink.com
[Ehl10a] Rüdiger Ehlers. Generalized Rabin(1) synthesis, 2010. arXiv/CoRR: 1003.1684 — This is a discussion paper. Please feel free to send me comments, notes, corrections, suggestions, etc. (Slides from my talk at the GASICS 2010 workshop)