---
_id: '1692'
abstract:
- lang: eng
  text: Computing an approximation of the reachable states of a hybrid system is a
    challenge, mainly because overapproximating the solutions of ODEs with a finite
    number of sets does not scale well. Using template polyhedra can greatly reduce
    the computational complexity, since it replaces complex operations on sets with
    a small number of optimization problems. However, the use of templates may make
    the over-approximation too conservative. Spurious transitions, which are falsely
    considered reachable, are particularly detrimental to performance and accuracy,
    and may exacerbate the state explosion problem. In this paper, we examine how
    spurious transitions can be avoided with minimal computational effort. To this
    end, detecting spurious transitions is reduced to the well-known problem of showing
    that two convex sets are disjoint by finding a hyperplane that separates them.
    We generalize this to owpipes by considering hyperplanes that evolve with time
    in correspondence to the dynamics of the system. The approach is implemented in
    the model checker SpaceEx and demonstrated on examples.
author:
- first_name: Goran
  full_name: Frehse, Goran
  last_name: Frehse
- first_name: Sergiy
  full_name: Bogomolov, Sergiy
  id: 369D9A44-F248-11E8-B48F-1D18A9856A87
  last_name: Bogomolov
  orcid: 0000-0002-0686-0365
- first_name: Marius
  full_name: Greitschus, Marius
  last_name: Greitschus
- first_name: Thomas
  full_name: Strump, Thomas
  last_name: Strump
- first_name: Andreas
  full_name: Podelski, Andreas
  last_name: Podelski
citation:
  ama: 'Frehse G, Bogomolov S, Greitschus M, Strump T, Podelski A. Eliminating spurious
    transitions in reachability with support functions. In: <i>Proceedings of the
    18th International Conference on Hybrid Systems: Computation and Control</i>.
    ACM; 2015:149-158. doi:<a href="https://doi.org/10.1145/2728606.2728622">10.1145/2728606.2728622</a>'
  apa: 'Frehse, G., Bogomolov, S., Greitschus, M., Strump, T., &#38; Podelski, A.
    (2015). Eliminating spurious transitions in reachability with support functions.
    In <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation
    and Control</i> (pp. 149–158). Seattle, WA, United States: ACM. <a href="https://doi.org/10.1145/2728606.2728622">https://doi.org/10.1145/2728606.2728622</a>'
  chicago: 'Frehse, Goran, Sergiy Bogomolov, Marius Greitschus, Thomas Strump, and
    Andreas Podelski. “Eliminating Spurious Transitions in Reachability with Support
    Functions.” In <i>Proceedings of the 18th International Conference on Hybrid Systems:
    Computation and Control</i>, 149–58. ACM, 2015. <a href="https://doi.org/10.1145/2728606.2728622">https://doi.org/10.1145/2728606.2728622</a>.'
  ieee: 'G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, and A. Podelski, “Eliminating
    spurious transitions in reachability with support functions,” in <i>Proceedings
    of the 18th International Conference on Hybrid Systems: Computation and Control</i>,
    Seattle, WA, United States, 2015, pp. 149–158.'
  ista: 'Frehse G, Bogomolov S, Greitschus M, Strump T, Podelski A. 2015. Eliminating
    spurious transitions in reachability with support functions. Proceedings of the
    18th International Conference on Hybrid Systems: Computation and Control. HSCC:
    Hybrid Systems - Computation and Control, 149–158.'
  mla: 'Frehse, Goran, et al. “Eliminating Spurious Transitions in Reachability with
    Support Functions.” <i>Proceedings of the 18th International Conference on Hybrid
    Systems: Computation and Control</i>, ACM, 2015, pp. 149–58, doi:<a href="https://doi.org/10.1145/2728606.2728622">10.1145/2728606.2728622</a>.'
  short: 'G. Frehse, S. Bogomolov, M. Greitschus, T. Strump, A. Podelski, in:, Proceedings
    of the 18th International Conference on Hybrid Systems: Computation and Control,
    ACM, 2015, pp. 149–158.'
conference:
  end_date: 2015-04-16
  location: Seattle, WA, United States
  name: 'HSCC: Hybrid Systems - Computation and Control'
  start_date: 2015-04-14
date_created: 2018-12-11T11:53:30Z
date_published: 2015-04-14T00:00:00Z
date_updated: 2021-01-12T06:52:33Z
day: '14'
department:
- _id: ToHe
doi: 10.1145/2728606.2728622
ec_funded: 1
language:
- iso: eng
month: '04'
oa_version: None
page: 149 - 158
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: 'Proceedings of the 18th International Conference on Hybrid Systems:
  Computation and Control'
publication_identifier:
  isbn:
  - 978-1-4503-3433-4
publication_status: published
publisher: ACM
publist_id: '5452'
quality_controlled: '1'
scopus_import: 1
status: public
title: Eliminating spurious transitions in reachability with support functions
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...