Controller Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints

Controller Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints. Hofmann, T. & Lakemeyer, G. 2021.

Paper abstract bibtex 1 download

Executing a Golog program on an actual robot typically requires additional steps to account for hardware or software details of the robot platform, which can be formulated as constraints on the program. Such constraints are often temporal, refer to metric time, and require modifications to the abstract Golog program. We describe how to formulate such constraints based on a modal variant of the Situation Calculus. These constraints connect the abstract program with the platform models, which we describe using timed automata. We show that for programs over finite domains and with fully known initial state, the problem of synthesizing a controller that satisfies the constraints while preserving the effects of the original program can be reduced to MTL synthesis. We do this by constructing a timed automaton from the abstract program and synthesizing an MTL controller from this automaton, the platform models, and the constraints. We prove that the synthesized controller results in execution traces which are the same as those of the original program, possibly interleaved with platform-dependent actions, that they satisfy all constraints, and that they have the same effects as the traces of the original program. By doing so, we obtain a decidable procedure to synthesize a controller that satisfies the specification while preserving the original program.

@misc{hofmannMTLSynthesis2021,
    title={Controller Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints},
    author={Till Hofmann and Gerhard Lakemeyer},
    year={2021},
    eprint={2102.09837},
    archivePrefix={arXiv},
    primaryClass={cs.AI},
    url = {https://arxiv.org/abs/2102.09837},
    abstract = {
      Executing a Golog program on an actual robot typically requires
      additional steps to account for hardware or software details of the
      robot platform, which can be formulated as constraints on the program.
      Such constraints are often temporal, refer to metric time, and require
      modifications to the abstract Golog program.  We describe how to
      formulate such constraints based on a modal variant of the Situation
      Calculus. These constraints connect the abstract program with the
      platform models, which we describe using timed automata.  We show that
      for programs over finite domains and with fully known initial state, the
      problem of synthesizing a controller that satisfies the constraints
      while preserving the effects of the original program can be reduced to
      MTL synthesis.  We do this by constructing a timed automaton from the
      abstract program and synthesizing an MTL controller from this automaton,
      the platform models, and the constraints. We prove that the synthesized
      controller results in execution traces which are the same as those of
      the original program, possibly interleaved with platform-dependent
      actions, that they satisfy all constraints, and that they have the same
      effects as the traces of the original program. By doing so, we obtain a
      decidable procedure to synthesize a controller that satisfies the
      specification while preserving the original program.
    }
}

Downloads: 1

{"_id":"LazKmFJcYhPssaMCQ","bibbaseid":"hofmann-lakemeyer-controllersynthesisforgologprogramsoverfinitedomainswithmetrictemporalconstraints-2021","author_short":["Hofmann, T.","Lakemeyer, G."],"bibdata":{"bibtype":"misc","type":"misc","title":"Controller Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints","author":[{"firstnames":["Till"],"propositions":[],"lastnames":["Hofmann"],"suffixes":[]},{"firstnames":["Gerhard"],"propositions":[],"lastnames":["Lakemeyer"],"suffixes":[]}],"year":"2021","eprint":"2102.09837","archiveprefix":"arXiv","primaryclass":"cs.AI","url":"https://arxiv.org/abs/2102.09837","abstract":"Executing a Golog program on an actual robot typically requires additional steps to account for hardware or software details of the robot platform, which can be formulated as constraints on the program. Such constraints are often temporal, refer to metric time, and require modifications to the abstract Golog program. We describe how to formulate such constraints based on a modal variant of the Situation Calculus. These constraints connect the abstract program with the platform models, which we describe using timed automata. We show that for programs over finite domains and with fully known initial state, the problem of synthesizing a controller that satisfies the constraints while preserving the effects of the original program can be reduced to MTL synthesis. We do this by constructing a timed automaton from the abstract program and synthesizing an MTL controller from this automaton, the platform models, and the constraints. We prove that the synthesized controller results in execution traces which are the same as those of the original program, possibly interleaved with platform-dependent actions, that they satisfy all constraints, and that they have the same effects as the traces of the original program. By doing so, we obtain a decidable procedure to synthesize a controller that satisfies the specification while preserving the original program. ","bibtex":"@misc{hofmannMTLSynthesis2021,\n title={Controller Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints},\n author={Till Hofmann and Gerhard Lakemeyer},\n year={2021},\n eprint={2102.09837},\n archivePrefix={arXiv},\n primaryClass={cs.AI},\n url = {https://arxiv.org/abs/2102.09837},\n abstract = {\n Executing a Golog program on an actual robot typically requires\n additional steps to account for hardware or software details of the\n robot platform, which can be formulated as constraints on the program.\n Such constraints are often temporal, refer to metric time, and require\n modifications to the abstract Golog program. We describe how to\n formulate such constraints based on a modal variant of the Situation\n Calculus. These constraints connect the abstract program with the\n platform models, which we describe using timed automata. We show that\n for programs over finite domains and with fully known initial state, the\n problem of synthesizing a controller that satisfies the constraints\n while preserving the effects of the original program can be reduced to\n MTL synthesis. We do this by constructing a timed automaton from the\n abstract program and synthesizing an MTL controller from this automaton,\n the platform models, and the constraints. We prove that the synthesized\n controller results in execution traces which are the same as those of\n the original program, possibly interleaved with platform-dependent\n actions, that they satisfy all constraints, and that they have the same\n effects as the traces of the original program. By doing so, we obtain a\n decidable procedure to synthesize a controller that satisfies the\n specification while preserving the original program.\n }\n}\n\n","author_short":["Hofmann, T.","Lakemeyer, G."],"key":"hofmannMTLSynthesis2021","id":"hofmannMTLSynthesis2021","bibbaseid":"hofmann-lakemeyer-controllersynthesisforgologprogramsoverfinitedomainswithmetrictemporalconstraints-2021","role":"author","urls":{"Paper":"https://arxiv.org/abs/2102.09837"},"metadata":{"authorlinks":{}},"downloads":1},"bibtype":"misc","biburl":"https://kbsg.rwth-aachen.de/files/kbsgweb.bib","dataSources":["dqRQPSg6Hy3ZXQg7z"],"keywords":[],"search_terms":["controller","synthesis","golog","programs","over","finite","domains","metric","temporal","constraints","hofmann","lakemeyer"],"title":"Controller Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints","year":2021,"downloads":1}