Visible to the public Controlled {Markov} Processes with Safety State Constraints


Visible to the public Safe Markov Chains for Density Control of ON/OFF Agents with Observed Transitions


Visible to the public Distributed Averaging with Quantized Communication over Dynamic Graphs


Visible to the public Autonomy Protocols- From Human Behavioral Modeling to Correct-by-Construction, Scalable Control Poster.pdf

Computer systems are increasingly coming to be relied upon to augment or replace human
operators in controlling mechanical devices in contexts such as transportation systems, chemical
plants, and medical devices, where safety and correctness are critical. A central problem is how
to verify that such partially automated or fully autonomous cyber-physical systems (CPS) are
worthy of our trust. One promising approach involves synthesis of the computer implementation