---
_id: '12170'
abstract:
- lang: eng
  text: 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.
acknowledgement: We thank Pranav Ashok and Maximilian Weininger for their contributions
  to spiritual predecessors of PET as well as motivating the initial development of
  this tool.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Tobias
  full_name: Meggendorfer, Tobias
  id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
  last_name: Meggendorfer
  orcid: 0000-0002-1712-2165
citation:
  ama: 'Meggendorfer T. PET – A partial exploration tool for probabilistic verification.
    In: <i>20th International Symposium on Automated Technology for Verification and
    Analysis</i>. Vol 13505. Springer Nature; 2022:320-326. doi:<a href="https://doi.org/10.1007/978-3-031-19992-9_20">10.1007/978-3-031-19992-9_20</a>'
  apa: 'Meggendorfer, T. (2022). PET – A partial exploration tool for probabilistic
    verification. In <i>20th International Symposium on Automated Technology for Verification
    and Analysis</i> (Vol. 13505, pp. 320–326). Virtual: Springer Nature. <a href="https://doi.org/10.1007/978-3-031-19992-9_20">https://doi.org/10.1007/978-3-031-19992-9_20</a>'
  chicago: Meggendorfer, Tobias. “PET – A Partial Exploration Tool for Probabilistic
    Verification.” In <i>20th International Symposium on Automated Technology for
    Verification and Analysis</i>, 13505:320–26. Springer Nature, 2022. <a href="https://doi.org/10.1007/978-3-031-19992-9_20">https://doi.org/10.1007/978-3-031-19992-9_20</a>.
  ieee: T. Meggendorfer, “PET – A partial exploration tool for probabilistic verification,”
    in <i>20th International Symposium on Automated Technology for Verification and
    Analysis</i>, Virtual, 2022, vol. 13505, pp. 320–326.
  ista: 'Meggendorfer T. 2022. PET – A partial exploration tool for probabilistic
    verification. 20th International Symposium on Automated Technology for Verification
    and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS,
    vol. 13505, 320–326.'
  mla: Meggendorfer, Tobias. “PET – A Partial Exploration Tool for Probabilistic Verification.”
    <i>20th International Symposium on Automated Technology for Verification and Analysis</i>,
    vol. 13505, Springer Nature, 2022, pp. 320–26, doi:<a href="https://doi.org/10.1007/978-3-031-19992-9_20">10.1007/978-3-031-19992-9_20</a>.
  short: T. Meggendorfer, in:, 20th International Symposium on Automated Technology
    for Verification and Analysis, Springer Nature, 2022, pp. 320–326.
conference:
  end_date: 2022-10-28
  location: Virtual
  name: 'ATVA: Automated Technology for Verification and Analysis'
  start_date: 2022-10-25
date_created: 2023-01-12T12:11:07Z
date_published: 2022-10-21T00:00:00Z
date_updated: 2023-09-05T15:11:51Z
day: '21'
department:
- _id: KrCh
doi: 10.1007/978-3-031-19992-9_20
intvolume: '     13505'
language:
- iso: eng
month: '10'
oa_version: None
page: 320-326
publication: 20th International Symposium on Automated Technology for Verification
  and Analysis
publication_identifier:
  eisbn:
  - '9783031199929'
  eissn:
  - 1611-3349
  isbn:
  - '9783031199912'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: PET – A partial exploration tool for probabilistic verification
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 13505
year: '2022'
...
---
_id: '12171'
abstract:
- lang: eng
  text: '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.'
acknowledgement: This work was supported in part by the European Union’s Horizon 2020
  research and innovation programme under the Marie Skłodowska-Curie grant agreement
  no. 847635, by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark,
  and by the Villum Investigator Grant S4OS.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Miriam
  full_name: Garcia Soto, Miriam
  id: 4B3207F6-F248-11E8-B48F-1D18A9856A87
  last_name: Garcia Soto
  orcid: 0000-0003-2936-5719
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
- first_name: Christian
  full_name: Schilling, Christian
  id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
  last_name: Schilling
  orcid: 0000-0003-3658-1065
citation:
  ama: 'Garcia Soto M, Henzinger TA, Schilling C. Synthesis of parametric hybrid automata
    from time series. In: <i>20th International Symposium on Automated Technology
    for Verification and Analysis</i>. Vol 13505. Springer Nature; 2022:337-353. doi:<a
    href="https://doi.org/10.1007/978-3-031-19992-9_22">10.1007/978-3-031-19992-9_22</a>'
  apa: 'Garcia Soto, M., Henzinger, T. A., &#38; Schilling, C. (2022). Synthesis of parametric
    hybrid automata from time series. In <i>20th International Symposium on Automated
    Technology for Verification and Analysis</i> (Vol. 13505, pp. 337–353). Virtual:
    Springer Nature. <a href="https://doi.org/10.1007/978-3-031-19992-9_22">https://doi.org/10.1007/978-3-031-19992-9_22</a>'
  chicago: Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis
    of Parametric Hybrid Automata from Time Series.” In <i>20th International Symposium
    on Automated Technology for Verification and Analysis</i>, 13505:337–53. Springer
    Nature, 2022. <a href="https://doi.org/10.1007/978-3-031-19992-9_22">https://doi.org/10.1007/978-3-031-19992-9_22</a>.
  ieee: M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of parametric
    hybrid automata from time series,” in <i>20th International Symposium on Automated
    Technology for Verification and Analysis</i>, Virtual, 2022, vol. 13505, pp. 337–353.
  ista: 'Garcia Soto M, Henzinger TA, Schilling C. 2022. Synthesis of parametric hybrid
    automata from time series. 20th International Symposium on Automated Technology
    for Verification and Analysis. ATVA: Automated Technology for Verification and
    Analysis, LNCS, vol. 13505, 337–353.'
  mla: Garcia Soto, Miriam, et al. “Synthesis of Parametric Hybrid Automata from Time
    Series.” <i>20th International Symposium on Automated Technology for Verification
    and Analysis</i>, vol. 13505, Springer Nature, 2022, pp. 337–53, doi:<a href="https://doi.org/10.1007/978-3-031-19992-9_22">10.1007/978-3-031-19992-9_22</a>.
  short: M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, 20th International Symposium
    on Automated Technology for Verification and Analysis, Springer Nature, 2022,
    pp. 337–353.
conference:
  end_date: 2022-10-28
  location: Virtual
  name: 'ATVA: Automated Technology for Verification and Analysis'
  start_date: 2022-10-25
date_created: 2023-01-12T12:11:16Z
date_published: 2022-10-21T00:00:00Z
date_updated: 2023-02-13T09:27:55Z
day: '21'
department:
- _id: ToHe
doi: 10.1007/978-3-031-19992-9_22
ec_funded: 1
external_id:
  arxiv:
  - '2208.06383'
intvolume: '     13505'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.48550/arXiv.2208.06383
month: '10'
oa: 1
oa_version: Preprint
page: 337-353
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 20th International Symposium on Automated Technology for Verification
  and Analysis
publication_identifier:
  eisbn:
  - '9783031199929'
  eissn:
  - 1611-3349
  isbn:
  - '9783031199912'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesis of parametric hybrid automata from time series
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13505
year: '2022'
...