Skip directly to: content | search

ExCAPE: Expeditions in Computer Augmented Program Engineering

Synthesis for Hybrid Systems with Maximal Satisfaction Guarantees

PIs: Kavraki (Rice), Kress-Gazit (Cornell) and Vardi (Rice)

We developed a novel theoretical and computational framework for control synthesis for hybrid systems with general nonlinear continuous dynamics from specifications given as a conjunction of a syntactically co-safe and a syntactically safe linear temporal logic (LTL) formulas. If the specification found unsatisfiable by the hybrid system, the framework computes controls that lead to a user-desired partial satisfaction of the liveness segment of the specification without violating the safety requirements. The approach is based on a synergistic combination of planning layers developed in a prior work. Experiments on a hybrid robotic system with nonlinear dynamics demonstrate that the synthesis framework produces satisfactory behaviors when the LTL specification is not fully achievable.


Synthesis for Nondeterministic Hybrid Systems

Kavraki (Rice) and Vardi (Rice)

We have initiated an effort to examine the problem of synthesis for nondeterministic hybrid systems with complex continuous dynamics and nondeterministic discrete switching between them from a temporal logic specification. Our intention is to employ sampling-based techniques that can deal with nonlinear continuous dynamics and combine it with game-theoretic approaches to handle discrete nondeterminism. The goal of this project is to compute winning strategies for the system to achieve the specification by viewing nondeterminism as an adversary. We will access the framework on a second-order car-like robot in an environment that includes several unknown terrains where moving over each terrain could affect the motion of the robot. In the long run, we are interested in including such systems in synthesis frameworks, a task that is not possible with available machinery [PKV13,LKV14].


Papers:

ExCAPE: Expeditions in Computer Augmented Program Engineering NSF National Science Foundation Award CCF-1138996