---
_id: '4602'
abstract:
- lang: eng
  text: 'Modular techniques for automatic verification attempt to overcome the state-explosion
    problem by exploiting the modular structure naturally present in many system designs.
    Unlike other tasks in the verification of finite-state systems, current modular
    techniques rely heavily on user guidance. In particular, the user is typically
    required to construct module abstractions that are neither too detailed as to
    render insufficient benefits in state exploration, nor too coarse as to invalidate
    the desired systemproperties. In this paper, we construct abstractmodules automatically,
    using reachability and controllability information about the concrete modules.
    This allows us to leverage automatic verification techniques by applying them
    in layers: first we compute on the state spaces of system components, then we
    use the results for constructing abstractions, and finally we compute on the abstract
    state space of the system. Our experimental results indicate that if reachability
    and controllability information is used in the construction of abstractions, the
    resulting abstract modules are often significantly smaller than the concrete modules
    and can drastically reduce the space and time requirements for verification.'
acknowledgement: This research was supported in part by the NSF CAREER award CCR-9734115,
  by the NSF CAREER award CCR-9501708, by the DARPA (NASA Ames) grant NAG2-1214, by
  the DARPA (Wright-Patterson AFB) grant F33615-98-C-3614, by the ARO MURI grant DAAH-
  04-96-1-0341, and by the Gigascale Silicon Research Center.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Luca
  full_name: De Alfaro, Luca
  last_name: De Alfaro
- 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: Freddy
  full_name: Mang, Freddy
  last_name: Mang
citation:
  ama: 'Alur R, De Alfaro L, Henzinger TA, Mang F. Automating modular verification.
    In: <i>Proceedings of the 10th International Conference on Concurrency Theory</i>.
    Vol 1664. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1999:82-97. doi:<a
    href="https://doi.org/10.1007/3-540-48320-9_8">10.1007/3-540-48320-9_8</a>'
  apa: 'Alur, R., De Alfaro, L., Henzinger, T. A., &#38; Mang, F. (1999). Automating
    modular verification. In <i>Proceedings of the 10th International Conference on
    Concurrency Theory</i> (Vol. 1664, pp. 82–97). Eindhoven, The Netherlands: Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.1007/3-540-48320-9_8">https://doi.org/10.1007/3-540-48320-9_8</a>'
  chicago: Alur, Rajeev, Luca De Alfaro, Thomas A Henzinger, and Freddy Mang. “Automating
    Modular Verification.” In <i>Proceedings of the 10th International Conference
    on Concurrency Theory</i>, 1664:82–97. Schloss Dagstuhl - Leibniz-Zentrum für
    Informatik, 1999. <a href="https://doi.org/10.1007/3-540-48320-9_8">https://doi.org/10.1007/3-540-48320-9_8</a>.
  ieee: R. Alur, L. De Alfaro, T. A. Henzinger, and F. Mang, “Automating modular verification,”
    in <i>Proceedings of the 10th International Conference on Concurrency Theory</i>,
    Eindhoven, The Netherlands, 1999, vol. 1664, pp. 82–97.
  ista: 'Alur R, De Alfaro L, Henzinger TA, Mang F. 1999. Automating modular verification.
    Proceedings of the 10th International Conference on Concurrency Theory. CONCUR:
    Concurrency Theory, LNCS, vol. 1664, 82–97.'
  mla: Alur, Rajeev, et al. “Automating Modular Verification.” <i>Proceedings of the
    10th International Conference on Concurrency Theory</i>, vol. 1664, Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik, 1999, pp. 82–97, doi:<a href="https://doi.org/10.1007/3-540-48320-9_8">10.1007/3-540-48320-9_8</a>.
  short: R. Alur, L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 10th
    International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 1999, pp. 82–97.
conference:
  end_date: 1999-08-27
  location: Eindhoven, The Netherlands
  name: 'CONCUR: Concurrency Theory'
  start_date: 1999-08-24
date_created: 2018-12-11T12:09:42Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-01T14:15:35Z
day: '01'
doi: 10.1007/3-540-48320-9_8
extern: '1'
intvolume: '      1664'
language:
- iso: eng
month: '01'
oa_version: None
page: 82 - 97
publication: Proceedings of the 10th International Conference on Concurrency Theory
publication_identifier:
  isbn:
  - '9783540664253'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '105'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Automating modular verification
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1664
year: '1999'
...
---
_id: '4485'
abstract:
- lang: eng
  text: 'In order to study control problems for hybrid systems, we generalize hybrid
    automata to hybrid games —say, controller vs. plant. If we specify the continuous
    dynamics by constant lower and upper bounds, we obtain rectangular games. We show
    that for rectangular games with objectives expressed in Ltl (linear temporal logic),
    the winning states for each player can be computed, and winning strategies can
    be synthesized. Our result is sharp, as already reachability is undecidable for
    generalizations of rectangular systems, and optimal —singly exponential in the
    size of the game structure and doubly exponential in the size of the Ltl objective.
    Our proof systematically generalizes the theory of hybrid systems from automata
    (single-player structures) [9] to games (multi-player structures): we show that
    the successively more general infinite-state classes of timed, 2D rectangular,
    and rectangular games induce successively weaker, but still finite, quotient structures
    called game bisimilarity, game similarity, and game trace equivalence. These quotients
    can be used, in particular, to solve the Ltl control problem.'
acknowledgement: This research was supported in part by the NSF CAREER award CCR-9501708,
  by the NSF grant CCR-9504469, by the DARPA (NASA Ames) grant NAG2-1214, by the DARPA
  (Wright-Patterson AFB) grant F33615-98-C-3614, and by the ARO MURI grant DAAH-04-96-1-0341.
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: Benjamin
  full_name: Horowitz, Benjamin
  last_name: Horowitz
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
citation:
  ama: 'Henzinger TA, Horowitz B, Majumdar R. Rectangular hybrid games. In: <i>Proceedings
    of the 10th International Conference on Concurrency Theory</i>. Vol 1664. Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik; 1999:320-335. doi:<a href="https://doi.org/10.1007/3-540-48320-9_23">10.1007/3-540-48320-9_23</a>'
  apa: 'Henzinger, T. A., Horowitz, B., &#38; Majumdar, R. (1999). Rectangular hybrid
    games. In <i>Proceedings of the 10th International Conference on Concurrency Theory</i>
    (Vol. 1664, pp. 320–335). Eindhoven, The Netherlands: Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik. <a href="https://doi.org/10.1007/3-540-48320-9_23">https://doi.org/10.1007/3-540-48320-9_23</a>'
  chicago: Henzinger, Thomas A, Benjamin Horowitz, and Ritankar Majumdar. “Rectangular
    Hybrid Games.” In <i>Proceedings of the 10th International Conference on Concurrency
    Theory</i>, 1664:320–35. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999.
    <a href="https://doi.org/10.1007/3-540-48320-9_23">https://doi.org/10.1007/3-540-48320-9_23</a>.
  ieee: T. A. Henzinger, B. Horowitz, and R. Majumdar, “Rectangular hybrid games,”
    in <i>Proceedings of the 10th International Conference on Concurrency Theory</i>,
    Eindhoven, The Netherlands, 1999, vol. 1664, pp. 320–335.
  ista: 'Henzinger TA, Horowitz B, Majumdar R. 1999. Rectangular hybrid games. Proceedings
    of the 10th International Conference on Concurrency Theory. CONCUR: Concurrency
    Theory, LNCS, vol. 1664, 320–335.'
  mla: Henzinger, Thomas A., et al. “Rectangular Hybrid Games.” <i>Proceedings of
    the 10th International Conference on Concurrency Theory</i>, vol. 1664, Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik, 1999, pp. 320–35, doi:<a href="https://doi.org/10.1007/3-540-48320-9_23">10.1007/3-540-48320-9_23</a>.
  short: T.A. Henzinger, B. Horowitz, R. Majumdar, in:, Proceedings of the 10th International
    Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    1999, pp. 320–335.
conference:
  location: Eindhoven, The Netherlands
  name: 'CONCUR: Concurrency Theory'
date_created: 2018-12-11T12:09:05Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-02T10:54:12Z
day: '01'
doi: 10.1007/3-540-48320-9_23
extern: '1'
intvolume: '      1664'
language:
- iso: eng
month: '01'
oa_version: None
page: 320 - 335
publication: Proceedings of the 10th International Conference on Concurrency Theory
publication_identifier:
  isbn:
  - '9783540664253'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '245'
quality_controlled: '1'
status: public
title: Rectangular hybrid games
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1664
year: '1999'
...