4 papers
LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Game
Aditi Kabra, Jonathan Laurent, Ruben Martins +2
Hybrid games model cyber-physical systems (CPS), like cars, trains, and airplanes, where discrete control decisions interact with continuous physical dynamics. We use Large Languag…
Can Large Language Models Autoformalize Kinematics?
Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj +3
Autonomous cyber-physical systems like robots and self-driving cars could greatly benefit from using formal methods to reason reliably about their control decisions. However, befor…
Hybrid Game Control Envelope Synthesis
Aditi Kabra, Jonathan Laurent, Stefan Mitsch +1
Control problems for embedded systems like cars and trains can be modeled by two-player hybrid games. Control envelopes, which are families of safe control solutions, correspond to…
CESAR: Control Envelope Synthesis via Angelic Refinements
Aditi Kabra, Jonathan Laurent, Stefan Mitsch +1
This paper presents an approach for synthesizing provably correct control envelopes for hybrid systems. Control envelopes characterize families of safe controllers and are used to…