@inproceedings{7231,
  abstract     = {Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation for nonlinear systems with polynomial dynamics, which leverages a combination of barrier certificates. PBT has advantages over traditional time-step based methods in dealing with those nonlinear dynamical systems in which there is a large difference in speed between trajectories, producing an overapproximation that is time independent. However, the existing approach for PBT is not efficient due to the application of interval methods for enclosure-box computation, and it can only deal with continuous dynamical systems without uncertainty. In this paper, we extend the approach with the ability to handle both continuous and hybrid dynamical systems with uncertainty that can reside in parameters and/or noise. We also improve the efficiency of the method significantly, by avoiding the use of interval-based methods for the enclosure-box computation without loosing soundness. We have developed a C++ prototype implementing the proposed approach and we evaluate it on several benchmarks. The experiments show that our approach is more efficient and precise than other methods in the literature.},
  author       = {Kong, Hui and Bartocci, Ezio and Jiang, Yu and Henzinger, Thomas A},
  booktitle    = {17th International Conference on Formal Modeling and Analysis of Timed Systems},
  isbn         = {978-3-0302-9661-2},
  issn         = {1611-3349},
  location     = {Amsterdam, The Netherlands},
  pages        = {123--141},
  publisher    = {Springer Nature},
  title        = {{Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty}},
  doi          = {10.1007/978-3-030-29662-9_8},
  volume       = {11750},
  year         = {2019},
}

@inproceedings{7232,
  abstract     = {We present Mixed-time Signal Temporal Logic (STL−MX), a specification formalism which extends STL by capturing the discrete/ continuous time duality found in many cyber-physical systems (CPS), as well as mixed-signal electronic designs. In STL−MX, properties of components with continuous dynamics are expressed in STL, while specifications of components with discrete dynamics are written in LTL. To combine the two layers, we evaluate formulas on two traces, discrete- and continuous-time, and introduce two interface operators that map signals, properties and their satisfaction signals across the two time domains. We show that STL-mx has the expressive power of STL supplemented with an implicit T-periodic clock signal. We develop and implement an algorithm for monitoring STL-mx formulas and illustrate the approach using a mixed-signal example. },
  author       = {Ferrere, Thomas and Maler, Oded and Nickovic, Dejan},
  booktitle    = {17th International Conference on Formal Modeling and Analysis of Timed Systems},
  isbn         = {978-3-0302-9661-2},
  issn         = {1611-3349},
  location     = {Amsterdam, The Netherlands},
  pages        = {59--75},
  publisher    = {Springer Nature},
  title        = {{Mixed-time signal temporal logic}},
  doi          = {10.1007/978-3-030-29662-9_4},
  volume       = {11750},
  year         = {2019},
}