@inproceedings{12170,
  abstract     = {We present PET, a specialized and highly optimized framework for partial exploration on probabilistic systems. Over the last decade, several significant advances in the analysis of Markov decision processes employed partial exploration. In a nutshell, this idea allows to focus computation on specific parts of the system, guided by heuristics, while maintaining correctness. In particular, only relevant parts of the system are constructed on demand, which in turn potentially allows to omit constructing large parts of the system. Depending on the model, this leads to dramatic speed-ups, in extreme cases even up to an arbitrary factor. PET unifies several previous implementations and provides a flexible framework to easily implement partial exploration for many further problems. Our experimental evaluation shows significant improvements compared to the previous implementations while vastly reducing the overhead required to add support for additional properties.},
  author       = {Meggendorfer, Tobias},
  booktitle    = {20th International Symposium on Automated Technology for Verification and Analysis},
  isbn         = {9783031199912},
  issn         = {1611-3349},
  location     = {Virtual},
  pages        = {320--326},
  publisher    = {Springer Nature},
  title        = {{PET – A partial exploration tool for probabilistic verification}},
  doi          = {10.1007/978-3-031-19992-9_20},
  volume       = {13505},
  year         = {2022},
}

@inproceedings{12171,
  abstract     = {We propose an algorithmic approach for synthesizing linear hybrid automata from time-series data. Unlike existing approaches, our approach provides a whole family of models with the same discrete structure but different dynamics. Each model in the family is guaranteed to capture the input data up to a precision error ε, in the following sense: For each time series, the model contains an execution that is ε-close to the data points. Our construction allows to effectively choose a model from this family with minimal precision error ε. We demonstrate the algorithm’s efficiency and its ability to find precise models in two case studies.},
  author       = {Garcia Soto, Miriam and Henzinger, Thomas A and Schilling, Christian},
  booktitle    = {20th International Symposium on Automated Technology for Verification and Analysis},
  isbn         = {9783031199912},
  issn         = {1611-3349},
  location     = {Virtual},
  pages        = {337--353},
  publisher    = {Springer Nature},
  title        = {{Synthesis of parametric hybrid automata from time series}},
  doi          = {10.1007/978-3-031-19992-9_22},
  volume       = {13505},
  year         = {2022},
}