---
_id: '4616'
abstract:
- lang: eng
  text: We present a model checking procedure and its implementation for the automatic
    verification of embedded systems. Systems are represented by hybrid automata -
    machines with finite control and real-valued variables modeling continuous environment
    parameters such as time, pressure, and temperature. System properties are specified
    in a real-time temporal logic and verified by symbolic computation. The verification
    procedure, implemented in Mathematica, is used to prove digital controllers and
    distributed algorithms correct. The verifier checks safety, liveness, time-bounded,
    and duration properties of hybrid automata
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- 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: 'Alur R, Henzinger TA, Ho P. Automatic symbolic verification of embedded systems.
    In: <i>1993 Proceedings Real-Time Systems Symposium</i>. IEEE; 1993:2-11. doi:<a
    href="https://doi.org/10.1109/REAL.1993.393520 ">10.1109/REAL.1993.393520 </a>'
  apa: 'Alur, R., Henzinger, T. A., &#38; Ho, P. (1993). Automatic symbolic verification
    of embedded systems. In <i>1993 Proceedings Real-Time Systems Symposium</i> (pp.
    2–11). Raleigh, NC, United States of America: IEEE. <a href="https://doi.org/10.1109/REAL.1993.393520
    ">https://doi.org/10.1109/REAL.1993.393520 </a>'
  chicago: Alur, Rajeev, Thomas A Henzinger, and Pei Ho. “Automatic Symbolic Verification
    of Embedded Systems.” In <i>1993 Proceedings Real-Time Systems Symposium</i>,
    2–11. IEEE, 1993. <a href="https://doi.org/10.1109/REAL.1993.393520 ">https://doi.org/10.1109/REAL.1993.393520
    </a>.
  ieee: R. Alur, T. A. Henzinger, and P. Ho, “Automatic symbolic verification of embedded
    systems,” in <i>1993 Proceedings Real-Time Systems Symposium</i>, Raleigh, NC,
    United States of America, 1993, pp. 2–11.
  ista: 'Alur R, Henzinger TA, Ho P. 1993. Automatic symbolic verification of embedded
    systems. 1993 Proceedings Real-Time Systems Symposium. RTSS: Real-Time Systems
    Symposium, 2–11.'
  mla: Alur, Rajeev, et al. “Automatic Symbolic Verification of Embedded Systems.”
    <i>1993 Proceedings Real-Time Systems Symposium</i>, IEEE, 1993, pp. 2–11, doi:<a
    href="https://doi.org/10.1109/REAL.1993.393520 ">10.1109/REAL.1993.393520 </a>.
  short: R. Alur, T.A. Henzinger, P. Ho, in:, 1993 Proceedings Real-Time Systems Symposium,
    IEEE, 1993, pp. 2–11.
conference:
  end_date: 1993-12-03
  location: Raleigh, NC, United States of America
  name: 'RTSS: Real-Time Systems Symposium'
  start_date: 1993-12-01
date_created: 2018-12-11T12:09:46Z
date_published: 1993-01-01T00:00:00Z
date_updated: 2022-03-23T13:01:41Z
day: '01'
doi: '10.1109/REAL.1993.393520 '
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://ieeexplore.ieee.org/document/393520
month: '01'
oa_version: None
page: 2 - 11
publication: 1993 Proceedings Real-Time Systems Symposium
publication_identifier:
  isbn:
  - 0-8186-4480-X
publication_status: published
publisher: IEEE
publist_id: '90'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Automatic symbolic verification of embedded systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1993'
...
---
_id: '4618'
abstract:
- lang: eng
  text: We introduce the framework of hybrid automata as a model and specification
    language for hybrid systems. Hybrid automata can be viewed as a generalization
    of timed automata, in which the behavior of variables is governed in each state
    by a set of differential equations. We show that many of the examples considered
    in the workshop can be defined by hybrid automata. While the reachability problem
    is undecidable even for very restricted classes of hybrid automata, we present
    two semidecision procedures for verifying safety properties of piecewiselinear
    hybrid automata, in which all variables change at constant rates. The two procedures
    are based, respectively, on minimizing and computing fixpoints on generally infinite
    state spaces. We show that if the procedures terminate, then they give correct
    answers. We then demonstrate that for many of the typical workshop examples, the
    procedures do terminate and thus provide an automatic way for verifying their
    properties.
acknowledgement: BRA ESPRIT project REACT, National Science Foundation under grant
  CCR-9200794 , United States Air Force Office of Scientific Research contract F49620-93-1-0056.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Costas
  full_name: Courcoubetis, Costas
  last_name: Courcoubetis
- 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: 'Alur R, Courcoubetis C, Henzinger TA, Ho P. Hybrid automata: An algorithmic
    approach to the specification and verification of hybrid systems. In: Grossman
    R, Nerode A, Ravn A, Rischel H, eds. <i>Hybrid Systems</i>. Vol 736. Springer;
    1993:209-229. doi:<a href="https://doi.org/10.1007/3-540-57318-6_30">10.1007/3-540-57318-6_30</a>'
  apa: 'Alur, R., Courcoubetis, C., Henzinger, T. A., &#38; Ho, P. (1993). Hybrid
    automata: An algorithmic approach to the specification and verification of hybrid
    systems. In R. Grossman, A. Nerode, A. Ravn, &#38; H. Rischel (Eds.), <i>Hybrid
    Systems</i> (Vol. 736, pp. 209–229). Springer. <a href="https://doi.org/10.1007/3-540-57318-6_30">https://doi.org/10.1007/3-540-57318-6_30</a>'
  chicago: 'Alur, Rajeev, Costas Courcoubetis, Thomas A Henzinger, and Pei Ho. “Hybrid
    Automata: An Algorithmic Approach to the Specification and Verification of Hybrid
    Systems.” In <i>Hybrid Systems</i>, edited by Robert Grossman, Anil Nerode, Anders
    Ravn, and Hans Rischel, 736:209–29. Springer, 1993. <a href="https://doi.org/10.1007/3-540-57318-6_30">https://doi.org/10.1007/3-540-57318-6_30</a>.'
  ieee: 'R. Alur, C. Courcoubetis, T. A. Henzinger, and P. Ho, “Hybrid automata: An
    algorithmic approach to the specification and verification of hybrid systems,”
    in <i>Hybrid Systems</i>, 1993, vol. 736, pp. 209–229.'
  ista: 'Alur R, Courcoubetis C, Henzinger TA, Ho P. 1993. Hybrid automata: An algorithmic
    approach to the specification and verification of hybrid systems. Hybrid Systems.
    , LNCS, vol. 736, 209–229.'
  mla: 'Alur, Rajeev, et al. “Hybrid Automata: An Algorithmic Approach to the Specification
    and Verification of Hybrid Systems.” <i>Hybrid Systems</i>, edited by Robert Grossman
    et al., vol. 736, Springer, 1993, pp. 209–29, doi:<a href="https://doi.org/10.1007/3-540-57318-6_30">10.1007/3-540-57318-6_30</a>.'
  short: R. Alur, C. Courcoubetis, T.A. Henzinger, P. Ho, in:, R. Grossman, A. Nerode,
    A. Ravn, H. Rischel (Eds.), Hybrid Systems, Springer, 1993, pp. 209–229.
date_created: 2018-12-11T12:09:47Z
date_published: 1993-01-01T00:00:00Z
date_updated: 2022-03-21T11:04:54Z
day: '01'
doi: 10.1007/3-540-57318-6_30
editor:
- first_name: Robert
  full_name: Grossman, Robert
  last_name: Grossman
- first_name: Anil
  full_name: Nerode, Anil
  last_name: Nerode
- first_name: Anders
  full_name: Ravn, Anders
  last_name: Ravn
- first_name: Hans
  full_name: Rischel, Hans
  last_name: Rischel
extern: '1'
intvolume: '       736'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-57318-6_30
month: '01'
oa_version: None
page: 209 - 229
publication: Hybrid Systems
publication_status: published
publisher: Springer
publist_id: '87'
quality_controlled: '1'
status: public
title: 'Hybrid automata: An algorithmic approach to the specification and verification
  of hybrid systems'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 736
year: '1993'
...
---
_id: '4619'
abstract:
- lang: eng
  text: Traditional approaches to the algorithmic verification of real-time systems
    are limited to checking program correctness with respect to concrete timing properties
    (e.g., &quot;message delivery within 10 milliseconds&quot;). We address the more
    realistic and more ambitious problem of deriving symbolic constraints on the timing
    properties required of real-time systems (e.g., &quot;message delivery within
    the time it takes to execute two assignment statements&quot;). To model this problem,
    we introduce parametric timed automata -- finite-state machines whose transitions
    are constrained with parametric timing requirements. The emptiness question for
    parametric timed automata is central to the verification problem. On the negative
    side, we show that in general this question is undecidable. On the positive side,
    we provide algorithms for checking the emptiness of restricted classes of parametric
    timed automata. The practical relevance of these classes is illustrated with several
    verification examples. There remains a gap between the automata classes for which
    we know that emptiness is decidable and undecidable, respectively, and this gap
    is related to various hard and open problems of logic and automata theory.
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- 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: Moshe
  full_name: Vardi, Moshe
  last_name: Vardi
citation:
  ama: 'Alur R, Henzinger TA, Vardi M. Parametric real-time reasoning. In: <i>Proceedings
    of the 25th Annual ACM Symposium on Theory of Computing</i>. ACM; 1993:592-601.
    doi:<a href="https://doi.org/10.1145/167088.167242">10.1145/167088.167242</a>'
  apa: 'Alur, R., Henzinger, T. A., &#38; Vardi, M. (1993). Parametric real-time reasoning.
    In <i>Proceedings of the 25th annual ACM symposium on Theory of Computing</i>
    (pp. 592–601). San Diego, CA, United States of America: ACM. <a href="https://doi.org/10.1145/167088.167242">https://doi.org/10.1145/167088.167242</a>'
  chicago: Alur, Rajeev, Thomas A Henzinger, and Moshe Vardi. “Parametric Real-Time
    Reasoning.” In <i>Proceedings of the 25th Annual ACM Symposium on Theory of Computing</i>,
    592–601. ACM, 1993. <a href="https://doi.org/10.1145/167088.167242">https://doi.org/10.1145/167088.167242</a>.
  ieee: R. Alur, T. A. Henzinger, and M. Vardi, “Parametric real-time reasoning,”
    in <i>Proceedings of the 25th annual ACM symposium on Theory of Computing</i>,
    San Diego, CA, United States of America, 1993, pp. 592–601.
  ista: 'Alur R, Henzinger TA, Vardi M. 1993. Parametric real-time reasoning. Proceedings
    of the 25th annual ACM symposium on Theory of Computing. STOC: Symposium on the
    Theory of Computing, 592–601.'
  mla: Alur, Rajeev, et al. “Parametric Real-Time Reasoning.” <i>Proceedings of the
    25th Annual ACM Symposium on Theory of Computing</i>, ACM, 1993, pp. 592–601,
    doi:<a href="https://doi.org/10.1145/167088.167242">10.1145/167088.167242</a>.
  short: R. Alur, T.A. Henzinger, M. Vardi, in:, Proceedings of the 25th Annual ACM
    Symposium on Theory of Computing, ACM, 1993, pp. 592–601.
conference:
  end_date: 1993-05-18
  location: San Diego, CA, United States of America
  name: 'STOC: Symposium on the Theory of Computing'
  start_date: 1993-05-16
date_created: 2018-12-11T12:09:47Z
date_published: 1993-06-01T00:00:00Z
date_updated: 2022-03-21T11:11:37Z
day: '01'
doi: 10.1145/167088.167242
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://dl.acm.org/doi/10.1145/167088.167242
month: '06'
oa_version: None
page: 592 - 601
publication: Proceedings of the 25th annual ACM symposium on Theory of Computing
publication_status: published
publisher: ACM
publist_id: '88'
quality_controlled: '1'
status: public
title: Parametric real-time reasoning
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1993'
...
---
_id: '4620'
abstract:
- lang: eng
  text: We present a verification algorithm for duration properties of finite-state
    real-time systems. While simple real-time properties constrain the total elapsed
    time between events, duration properties constrain the accumulated time during
    which certain state predicates hold. We formalize the concept of durations by
    introducing duration measures for (dense-time) timed automata. Given a timed automaton
    with a duration measure, a start and a target state, and a duration constraint,
    the duration-bounded reachability problem asks if there is a run of the automaton
    from the start state to the target state such that the accumulated duration along
    the run satisfies the constraint. Our main result is a novel decision procedure
    for solving the duration-bounded reachability problem. We also prove that the
    problem is PSPACE-complete and demonstrate how the solution can be used to verify
    interesting duration properties of real-time systems.
acknowledgement: BRA ESPRIT project REACT, National Science Foundation grant CCR-9200794
  United States Air Force Office of Scientific Research contract F49620-93-1-0056
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Costas
  full_name: Courcoubetis, Costas
  last_name: Courcoubetis
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: 'Alur R, Courcoubetis C, Henzinger TA. Computing accumulated delays in real-time
    systems. In: <i>5th International Conference on Computer Aided Verification</i>.
    Vol 697. Springer; 1993:181-193. doi:<a href="https://doi.org/10.1007/3-540-56922-7_16">10.1007/3-540-56922-7_16</a>'
  apa: 'Alur, R., Courcoubetis, C., &#38; Henzinger, T. A. (1993). Computing accumulated
    delays in real-time systems. In <i>5th International Conference on Computer Aided
    Verification</i> (Vol. 697, pp. 181–193). Elounda, Greece: Springer. <a href="https://doi.org/10.1007/3-540-56922-7_16">https://doi.org/10.1007/3-540-56922-7_16</a>'
  chicago: Alur, Rajeev, Costas Courcoubetis, and Thomas A Henzinger. “Computing Accumulated
    Delays in Real-Time Systems.” In <i>5th International Conference on Computer Aided
    Verification</i>, 697:181–93. Springer, 1993. <a href="https://doi.org/10.1007/3-540-56922-7_16">https://doi.org/10.1007/3-540-56922-7_16</a>.
  ieee: R. Alur, C. Courcoubetis, and T. A. Henzinger, “Computing accumulated delays
    in real-time systems,” in <i>5th International Conference on Computer Aided Verification</i>,
    Elounda, Greece, 1993, vol. 697, pp. 181–193.
  ista: 'Alur R, Courcoubetis C, Henzinger TA. 1993. Computing accumulated delays
    in real-time systems. 5th International Conference on Computer Aided Verification.
    CAV: Computer Aided Verification, LNCS, vol. 697, 181–193.'
  mla: Alur, Rajeev, et al. “Computing Accumulated Delays in Real-Time Systems.” <i>5th
    International Conference on Computer Aided Verification</i>, vol. 697, Springer,
    1993, pp. 181–93, doi:<a href="https://doi.org/10.1007/3-540-56922-7_16">10.1007/3-540-56922-7_16</a>.
  short: R. Alur, C. Courcoubetis, T.A. Henzinger, in:, 5th International Conference
    on Computer Aided Verification, Springer, 1993, pp. 181–193.
conference:
  end_date: 1993-07-01
  location: Elounda, Greece
  name: 'CAV: Computer Aided Verification'
  start_date: 1993-06-28
date_created: 2018-12-11T12:09:47Z
date_published: 1993-01-01T00:00:00Z
date_updated: 2022-03-21T13:55:53Z
day: '01'
doi: 10.1007/3-540-56922-7_16
extern: '1'
intvolume: '       697'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-56922-7_16
month: '01'
oa_version: None
page: 181 - 193
publication: 5th International Conference on Computer Aided Verification
publication_status: published
publisher: Springer
publist_id: '89'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Computing accumulated delays in real-time systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 697
year: '1993'
...