Entwicklung korrekter Systeme

Forschung

Meine Forschungsinteressen sind:

  • Robustheit von spatio-temporalen Logiken
  • Temporale Logik
  • Räumliche Logik
  • Synthese von (verteilten) Reaktiven Systemen

Publikationen

  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    H. Ody, "Monitoring of Traffic Manoeuvres with Imprecise Information," in Proc. Proceedings First Workshop on Formal Verification of Autonomous Vehicles, Turin, Italy, 19th September 2017, 2017, pp. 43-58.
    @inproceedings{Ody17,
      author = {Ody, Heinrich},
      year = {2017},
      title = {Monitoring of Traffic Manoeuvres with Imprecise Information},
      editor = {Bulwahn, Lukas and Kamali, Maryam and Linker, Sven},
      booktitle = {{Proceedings First Workshop on} Formal Verification of Autonomous Vehicles, {Turin, Italy, 19th September 2017}},
      series = {Electronic Proceedings in Theoretical Computer Science},
      volume = {257},
      publisher = {Open Publishing Association},
      pages = {43-58},
      doi = {10.4204/EPTCS.257.6},
      url = {https://arxiv.org/abs/1709.02558v1} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    H. Ody, M. Fränzle, und M. R. Hansen, "Discounted Duration Calculus," in Proc. FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, 2016, pp. 577-592.
    @inproceedings{OFH16,
      author = {Heinrich Ody and Martin Fr{\"{a}}nzle and Michael R. Hansen},
      editor = {John S. Fitzgerald and Constance L. Heitmeyer and Stefania Gnesi and Anna Philippou},
      title = {Discounted Duration Calculus},
      booktitle = {{FM} 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings},
      series = {Lecture Notes in Computer Science},
      volume = {9995},
      pages = {577--592},
      year = {2016},
      url = {http://theoretica.informatik.uni-oldenburg.de/~sefie/files/discounted-duration-calculus.pdf},
      doi = {10.1007/978-3-319-48989-6_35},
      timestamp = {Mon, 22 May 2017 17:11:19 +0200},
      biburl = {http://dblp.uni-trier.de/rec/bib/conf/fm/OdyFH16},
      bibsource = {dblp computer science bibliography, http://dblp.org} }
  • M. Fränzle, M. R. Hansen, und H. Ody, "Discounted Duration Calculus," School of Computer Science, Reykjavik University, RUTR-SCS16001, 2015.
    @techreport{FHO15b, title = {Discounted Duration Calculus},
      author = {Fr{\"a}nzle, Martin and Hansen, Michael R. and Ody, Heinrich},
      year = {2015},
      booktitle = {Nordic Workshop on Programming Theory - NWPT},
      editor = {Luca Aceto, Ignacio Fabregas, Alvaro Garcia-Perez and Anna Ingolfsdottir},
      institution = {School of Computer Science, Reykjavik University},
      number = {RUTR-SCS16001},
      url = {http://icetcs.ru.is/nwpt2015/NWPT15Proceedings.pdf} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    M. Fränzle, M. R. Hansen, und H. Ody, "No Need Knowing Numerous Neighbours - Towards a Realizable Interpretation of MLSL," in Proc. Correct System Design, 2015, pp. 152-171.
    @inproceedings{FHO15a,
      author = {Martin Fr{\"{a}}nzle and Michael R. Hansen and Heinrich Ody},
      title = {No Need Knowing Numerous Neighbours - Towards a Realizable Interpretation of {MLSL}},
      editor = {Roland Meyer and Andr{\'{e}} Platzer and Heike Wehrheim},
      booktitle = {Correct System Design},
      pages = {152--171},
      year = {2015},
      series = {Lecture Notes in Computer Science},
      volume = {9360},
      publisher = {Springer},
      url = {http://theoretica.informatik.uni-oldenburg.de/~sefie/files/neighbours-csd15.pdf},
      doi = {10.1007/978-3-319-23506-6_11},
      biburl = {http://dblp.uni-trier.de/rec/bib/conf/birthday/FranzleHO15},
      bibsource = {dblp computer science bibliography, http://dblp.org} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    H. Ody, "Undecidability Results for Multi-Lane Spatial Logic," in Proc. Theoretical Aspects of Computing - ICTAC, 2015, pp. 404-421.
    @inproceedings{Ody15b,
      author = {Heinrich Ody},
      title = {Undecidability Results for Multi-Lane Spatial Logic},
      booktitle = {Theoretical Aspects of Computing - {ICTAC}},
      pages = {404--421},
      year = {2015},
      editor = {Martin Leucker and Camilo Rueda and Frank D. Valencia},
      volume = {9399},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      url = {http://theoretica.informatik.uni-oldenburg.de/~sefie/files/mlsl-undec-ictac15.pdf},
      doi = {10.1007/978-3-319-25150-9_24},
      biburl = {http://dblp.uni-trier.de/rec/bib/conf/ictac/Ody15},
      bibsource = {dblp computer science bibliography, http://dblp.org} }
  • H. Ody, "Undecidability Results for Multi-Lane Spatial Logic," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 112, 2015.
    @techreport{Ody15a, title = {Undecidability Results for Multi-Lane Spatial Logic},
      author = {Heinrich Ody},
      institution = {SFB/TR 14 AVACS},
      year = {2015},
      month = {September},
      note = {http://www.avacs.org},
      number = {112},
      type = {Reports of SFB/TR 14 AVACS},
      abstract = {We consider (un)decidability of Multi-Lane Spatial Logic (MLSL), a multi-dimensional modal logic introduced for reasoning about traffic manoeuvres. MLSL with length measurement has been shown to be undecidable. However, the proof relies on exact values. This raises the question whether the logic remains undecidable when we consider robust satisfiability, i.e. when values are known only approximately. Our main result is that robust satisfiability of MLSL is undecidable. Furthermore, we prove that even MLSL without length measurement is undecidable. In both cases we reduce the intersection emptiness of two context-free languages to the respective satisfiability problem. This is the full version of a paper with the same title published at the ICTAC 2015.},
      access = {open},
      bibtex = {atr112.bib},
      editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski},
      pdf = {avacs_technical_report_112.pdf},
      url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs\_technical\_report\_112.pdf},
      series = {ATR},
      subproject = {H3,R1} }

Abschlussarbeiten

  • [mastersthesis] bibtex | Dokument aufrufen Dokument aufrufen
    H. Ody, "Synthesis of Distributed Reactive Programs," Master's Dissertation , 2013.
    @mastersthesis{ody13, title = {Synthesis of Distributed Reactive Programs},
      author = {Heinrich Ody},
      type = {Master Thesis},
      url = {http://theoretica.informatik.uni-oldenburg.de/~sefie/files/master-thesis.pdf},
      school = {Saarland University},
      year = {2013} }