Dynamics-Based Reactive Synthesis and Automated Revisions for High-Level Robot Control

Ayca Balkan; Hadas Kress-Gazit; Jonathan A. DeCastro; Matthias Rungger; Paulo Tabuada; Ruediger Ehlers

Dynamics-Based Reactive Synthesis and Automated Revisions for High-Level Robot Control

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1410.6375 v2 pith:WMEVGVMJ submitted 2014-10-23 cs.RO

Jonathan A. DeCastro , Ruediger Ehlers , Matthias Rungger , Ayca Balkan , Paulo Tabuada , Hadas Kress-Gazit This is my paper

classification cs.RO

keywords robotenvironmentspecificationssystembehaviorsdynamicsframeworkreactive

verification ladder T0 review T1 audit T2 compute T3 formal

0 comments

read the original abstract

The aim of this work is to address issues where formal specifications cannot be realized on a given dynamical system subjected to a changing environment. Such failures occur whenever the dynamics of the system restrict the robot in such a way that the environment may prevent the robot from progressing safely to its goals. We provide a framework that automatically synthesizes revisions to such specifications that restrict the assumed behaviors of the environment and the behaviors of the system. We provide a means for explaining such modifications to the user in a concise, easy-to-understand manner. Integral to the framework is a new algorithm for synthesizing controllers for reactive specifications that include a discrete representation of the robot's dynamics. The new approach is demonstrated with a complex task implemented using a unicycle model.

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Physically-Feasible Reactive Synthesis for Terrain-Adaptive Locomotion
cs.RO 2025-09 conditional novelty 5.0 of 10

A quadruped locomotion planner combines reactive synthesis with mixed-integer convex optimization to generate and repair terrain-adaptive gaits, with hardware demonstrations on stepping stones and rebar.

Pith tools