---
_id: '4450'
abstract:
- lang: eng
  text: "Hybrid systems model discrete programs that are embedded in continuous environments.
    Model-checking tools are available for the analysis of linear hybrid systems,
    whose continuous variables are bounded by piecewise-linear trajectories. Most
    embedded programs, however, operate in nonlinear environments. We present, analyze,
    and apply two algorithms for translating nonlinear hybrid systems into linear
    hybrid systems.\r\nThe clock translation replaces nonlinear variables by clock
    variables; the rate translation approximates nonlinear variables by piecewise-linear
    envelopes. Both translations are sound for reachability; that is, if we establish
    a safety property of the translated linear system, we may conclude that the original
    nonlinear system satisfies the property. The clock translation is also complete
    for reachability; that is, the original system and the translated system satisfy
    the same safety properties. The two translations apply to incomparable classes
    of nonlinear hybrid systems. From the clock translation we obtain a new decidability
    result for hybrid systems.\r\nWith the help of Hytech, a symbolic model checker
    for linear hybrid systems, we automatically verify a nonlinear railroad gate control
    program using the clock translation, and a nonlinear temperature control program
    using the rate translation."
acknowledgement: This research was supported in part by the NSF grant CCR-9200794,
  by the AFOSR contract F49620-93-1-0056, and by the DARPA grant NAG2-892.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: Pei
  full_name: Ho, Pei
  last_name: Ho
citation:
  ama: 'Henzinger TA, Ho P. Algorithmic analysis of nonlinear hybrid systems. In:
    <i>7th International Conference on Computer Aided Verification</i>. Vol 939. Springer;
    1995:225-238. doi:<a href="https://doi.org/10.1007/3-540-60045-0_53">10.1007/3-540-60045-0_53</a>'
  apa: 'Henzinger, T. A., &#38; Ho, P. (1995). Algorithmic analysis of nonlinear hybrid
    systems. In <i>7th International Conference on Computer Aided Verification</i>
    (Vol. 939, pp. 225–238). Liege, Belgium: Springer. <a href="https://doi.org/10.1007/3-540-60045-0_53">https://doi.org/10.1007/3-540-60045-0_53</a>'
  chicago: Henzinger, Thomas A, and Pei Ho. “Algorithmic Analysis of Nonlinear Hybrid
    Systems.” In <i>7th International Conference on Computer Aided Verification</i>,
    939:225–38. Springer, 1995. <a href="https://doi.org/10.1007/3-540-60045-0_53">https://doi.org/10.1007/3-540-60045-0_53</a>.
  ieee: T. A. Henzinger and P. Ho, “Algorithmic analysis of nonlinear hybrid systems,”
    in <i>7th International Conference on Computer Aided Verification</i>, Liege,
    Belgium, 1995, vol. 939, pp. 225–238.
  ista: 'Henzinger TA, Ho P. 1995. Algorithmic analysis of nonlinear hybrid systems.
    7th International Conference on Computer Aided Verification. CAV: Computer Aided
    Verification, LNCS, vol. 939, 225–238.'
  mla: Henzinger, Thomas A., and Pei Ho. “Algorithmic Analysis of Nonlinear Hybrid
    Systems.” <i>7th International Conference on Computer Aided Verification</i>,
    vol. 939, Springer, 1995, pp. 225–38, doi:<a href="https://doi.org/10.1007/3-540-60045-0_53">10.1007/3-540-60045-0_53</a>.
  short: T.A. Henzinger, P. Ho, in:, 7th International Conference on Computer Aided
    Verification, Springer, 1995, pp. 225–238.
conference:
  end_date: 1995-07-05
  location: Liege, Belgium
  name: 'CAV: Computer Aided Verification'
  start_date: 1995-07-03
date_created: 2018-12-11T12:08:55Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-10T09:48:52Z
day: '01'
doi: 10.1007/3-540-60045-0_53
extern: '1'
intvolume: '       939'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-60045-0_53
month: '01'
oa_version: None
page: 225 - 238
publication: 7th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540494133'
publication_status: published
publisher: Springer
publist_id: '280'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Algorithmic analysis of nonlinear hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 939
year: '1995'
...