Selected Publications


  1. 1
    Switching Controller Synthesis for Delay Hybrid Systems under Perturbations
    Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue and Naijun Zhan.

    To appear in Proceedings of the 24th ACM International Conference on Hybrid Systems: Computation and Control(HSCC 2021)

    PDF
    Robots need models of human behavior for both inferring human goals and preferences, and predicting what people will do. A common model is the Boltzmann noisily-rational decision model, which assumes people approximately optimize a reward function and choose trajectories in proportion to their exponentiated reward. While this model has been successful in a variety of robotics domains, its roots lie in econometrics, and in modeling decisions among different discrete options, each with its own utility or reward. In contrast, human trajectories lie in a continuous space, with continuous-valued features that influence the reward function. We propose that it is time to rethink the Boltzmann model, and design it from the ground up to operate over such trajectory spaces. We introduce a model that explicitly accounts for distances between trajectories, rather than only their rewards. Rather than each trajectory affecting the decision independently, similar trajectories now affect the decision together. We start by showing that our model better explains human behavior in a user study. We then analyze the implications this has for robot inference, first in toy environments where we have ground truth and find more accurate inference, and finally for a 7DOF robot arm learning from user demonstrations.
  2. 2
    Nonlinear Craig Interpolant Generation
    Ting Gan, Bican Xia, Bai Xue, Naijun Zhan and Liyun Dai.

    CAV 2020: 415--438, 2020.

    PDF
  3. 3
    PAC Learning of Deterministic One-Clock Timed Automata
    Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue and Naijun Zhan.

    ICFEM 2020: 129--146, 2020.

    PDF
  4. 4
    Linearization based Safety Verification of a Glucose Control Protocol
    Ankita Samaddar, Zahra Rahiminasab, Arvind Easwaran, Ansuman Banerjee and Bai Xue.

    ISORC 2019: 221--228, 2019.

    PDF
  5. 5
    Model Checking Delay Differential Equations Against Metric Interval Temporal Logic
    Peter Nazier Mosaad, Martin Fränzle and Bai Xue.

    Sci. Ann. Comp. Sci., 27: 77--109, 2017.

    PDF
Formal Analysis on Deep Neural Networks
1
Improving Neural Network Verification through Spurious Region Guided Refinement
Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue and Lijun Zhang.

To appear in Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems(TACAS 2021), 2021.

PDF
2
PRODEEP: a platform for robustness verification of deep neural networks
Renjue Li, Jianlin Li, Cheng Huang, Pengfei Yang, Xiaowei Huang, Lijun Zhang, Bai Xue and Holger Hermanns.

ESEC/FSE 2020: 1630--1634, 2020.

PDF
Unbounded Verification Based on Bounded Verification
1
Unbounded-Time Safety Verification of Stochastic Differential Dynamics
Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan and Naijun Zhan.

CAV 2020: 327--348, 2020

PDF
2
Taming delays in dynamical systems: Unbounded verification of delay differential equations
Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle, and Bai Xue.

CAV 2019: 650--669, 2019.

PDF
PAC Learning Based Reachability Analysis
1
PAC Model Checking of Black-Box Continuous-Time Dynamical Systems
Bai Xue, Miaomiao Zhang, Arvind Easwaran and Qin Li.

IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (IEEE TCAD), 39(11): 3944--3955, 2020. (Special issue of EMSOFT 2020)

PDF
2
Safe Inputs Approximation for Black-Box Systems
Bai Xue, Yang Liu, Lei Ma, Xiyue Zhang, Meng Sun and Xiaofei Xie.

ICECCS 2019: 180--189, 2019.

PDF
3
Probably Approximate Safety Verification of Hybrid Dynamical Systems
Bai Xue, Martin Fränzle, Hengjun Zhao, Naijun Zhan and Arvind Easwaran.

ICFEM 2019: 236--252, 2019.

PDF
4
Probably Approximately Correct Interpolants Generation
Bai Xue and Naijun Zhan.

SETTA 2020: 143--159, 2020

PDF
Convex Programming Based (Under/Inner Approximated) Reachability Analysis
1
Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems
Bai Xue, Qiuye Wang, Naijun Zhan, Shijie Wang and Zhikun She.

To appear in SIAM Journal on Control and Optimization (SICON), 2020.

PDF
2
Reach-avoid Analysis for Stochastic Discrete-time Systems
Bai Xue, Renjue Li, Naijun Zhan and Martin Fränzle.

To appear in Proceedings of of the 2021 American Control Conference (ACC 2021), 2021.

PDF
3
Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems
Bai Xue, Naijun Zhan and Martin Fränzle.

CDC 2020: 867--873, 2020.

PDF
4
Safety Verification for Random Ordinary Differential Equations
Bai Xue, Martin Fränzle, Naijun Zhan, Sergiy Bogomolov and Bican Xia.

IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (IEEE TCAD), 39(11): 4090-4101, 2020. (Special issue of EMSOFT 2020)

PDF
5
Robust Regions of Attraction Generation for State-Constrained Perturbed Discrete-Time Polynomial Systems
Bai Xue, Naijun Zhan and Yangjia Li.

IFAC 2020: 6405--6411, 2020.

PDF
6
A Characterization of Robust Regions of Attraction for Discrete-Time Systems Based on Bellman Equations
Bai Xue, Naijun Zhan and Yangjia Li.

IFAC 2020: 6468--6475, 2020.

PDF
7
Inner-Approximating Reachable Sets for Polynomial Systems with Time-Varying Uncertainties
Bai Xue, Martin Fränzle and Naijun Zhan.

IEEE Transactions on Automatic Control (IEEE TAC), 65(4): 1468-1483, 2020.

PDF
8
Robust invariant sets generation for state-constrained perturbed polynomial systems
Bai Xue, Qiuye Wang, Naijun Zhan and Martin Fränzle.

HSCC 2019: 128--137, 2019.

PDF
9
Under-Approximating Reach Sets for Polynomial Continuous Systems
Bai Xue, Martin Fräzle and Naijun Zhan.

HSCC 2018: 51--60, 2018.

PDF
10
Robust Invariant Sets Computation for Switched Discrete-Time Polynomial Systems
Bai Xue and Naijun Zhan.

Arxiv

PDF
11
Reach-Avoid Differential Games Based on Invariant Generation
Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle and Shenghua Feng.

Arxiv

PDF
12
Safe Over- and Under-Approximation of Reachable Sets for Autonomous Dynamical Systems
Meilun Li, Peter Nazier Mosaad, Martin Fränzle, Zhikun She and Bai Xue.

FORMATS 2018: 252-270, 2018.

PDF
13
Robust Non-termination Analysis of Numerical Software
Bai Xue, Naijun Zhan, Yangjia Li and Qiuye Wang.

SETTA 2018: 69--88, 2018. (Best paper awards)

PDF
Set-Boundary Reachability Analysis
1
Over- and Under-Approximating Reach Sets for Perturbed Delay Differential Equations
Bai Xue, Qiuye Wang, Shenghua Feng and Naijun Zhan.

. IEEE Transactions on Automatic Control (IEEE TAC), 66(1): 283--290, 2021.

PDF
2
Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations
Bai Xue, Peter Nazier Mosaad, Martin Fränzle, Mingshuai Chen, Yangjia Li and Naijun Zhan.

FORMATS 2017: 281--299, 2017.

PDF(Revised Version)
3
Reach-Avoid Verification for Nonlinear Systems Based on Boundary Analysis
Bai Xue, Arvind Easwaran, Nam-Joon Cho and Martin Fränzle.

IEEE Transactions on Automatic Control (IEEE TAC), vol. 62: 3518--3523, 2017.

PDF
4
Under-Approximating Backward Reachable Sets by Polytopes
Bai Xue, Zhikun She and Arvind Easwaran.

CAV 2016: 457--476, 2016.

PDF
5
Just scratching the surface: Partial exploration of initial values in reach-set computation
Bai Xue, Martin Fränzle and Peter Nazier Mosaad.

CDC 2017: 1769--1775, 2017.

PDF
6
Underapproximating Backward Reachable Sets by Semialgebraic Sets
Bai Xue, Zhikun She and Arvind Easwaran.

IEEE Transactions on Automatic Control (IEEE TAC), 62: 5185--5197, 2017.

PDF