Navigation

Contact

  • E-Mail: heinxk2w6rich.ody@injtoformacwigxtichk.uni-ouvldiqp4enburg.deqz

Research

My research interests are 

  • Robustness of (temporal/spatial) logics
  • Temporal logics
  • Spatial logics
  • Synthesis of (distributed) reactive systems

Publications

  • [inproceedings] bibtex | Go to document Go to document
    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 | Go to document Go to document
    H. Ody, M. Fränzle, and 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} }
  • [techreport] bibtex | Go to document Go to document
    M. Fränzle, M. R. Hansen, and 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 | Go to document Go to document
    M. Fränzle, M. R. Hansen, and 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 | Go to document Go to document
    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} }
  • [techreport] bibtex | Go to document Go to document
    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} }

Theses

  • [mastersthesis] bibtex | Go to document Go to document
    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} }
Webmavcster (m.s4kwxgiestn+uzekgreving@uolblcl.de) (Changed: 2020-01-23)