---
_id: '4632'
abstract:
- lang: eng
  text: We present a compositional trace-based model for probabilistic systems. The
    behavior of a system with probabilistic choice is a stochastic process, namely,
    a probability distribution on traces, or “bundle.” Consequently, the semantics
    of a system with both nondeterministic and probabilistic choice is a set of bundles.
    The bundles of a composite system can be obtained by combining the bundles of
    the components in a simple mathematical way. Refinement between systems is bundle
    containment. We achieve assume-guarantee compositionality for bundle semantics
    by introducing two scoping mechanisms. The first mechanism, which is standard
    in compositional modeling, distinguishes inputs from outputs and hidden state.
    The second mechanism, which arises in probabilistic systems, partitions the state
    into probabilistically independent regions.
acknowledgement: This research was supported in part by the SRC contract 99-TJ-683.003,
  the AFOSR MURI grant F49620-00-1-0327, the MARCO GSRC grant 98-DT-660, the NSF Theory
  grant CCR-9988172, and the DARPA SEC grant F33615-C-98-3614.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: Ranjit
  full_name: Jhala, Ranjit
  last_name: Jhala
citation:
  ama: 'De Alfaro L, Henzinger TA, Jhala R. Compositional methods for probabilistic
    systems. In: <i>Proceedings of the 12th International Conference on on Concurrency
    Theory</i>. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:351-365.
    doi:<a href="https://doi.org/10.1007/3-540-44685-0_24">10.1007/3-540-44685-0_24</a>'
  apa: 'De Alfaro, L., Henzinger, T. A., &#38; Jhala, R. (2001). Compositional methods
    for probabilistic systems. In <i>Proceedings of the 12th International Conference
    on on Concurrency Theory</i> (Vol. 2154, pp. 351–365). Aalborg, Denmark: Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.1007/3-540-44685-0_24">https://doi.org/10.1007/3-540-44685-0_24</a>'
  chicago: De Alfaro, Luca, Thomas A Henzinger, and Ranjit Jhala. “Compositional Methods
    for Probabilistic Systems.” In <i>Proceedings of the 12th International Conference
    on on Concurrency Theory</i>, 2154:351–65. Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2001. <a href="https://doi.org/10.1007/3-540-44685-0_24">https://doi.org/10.1007/3-540-44685-0_24</a>.
  ieee: L. De Alfaro, T. A. Henzinger, and R. Jhala, “Compositional methods for probabilistic
    systems,” in <i>Proceedings of the 12th International Conference on on Concurrency
    Theory</i>, Aalborg, Denmark, 2001, vol. 2154, pp. 351–365.
  ista: 'De Alfaro L, Henzinger TA, Jhala R. 2001. Compositional methods for probabilistic
    systems. Proceedings of the 12th International Conference on on Concurrency Theory.
    CONCUR: Concurrency Theory, LNCS, vol. 2154, 351–365.'
  mla: De Alfaro, Luca, et al. “Compositional Methods for Probabilistic Systems.”
    <i>Proceedings of the 12th International Conference on on Concurrency Theory</i>,
    vol. 2154, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 351–65,
    doi:<a href="https://doi.org/10.1007/3-540-44685-0_24">10.1007/3-540-44685-0_24</a>.
  short: L. De Alfaro, T.A. Henzinger, R. Jhala, in:, Proceedings of the 12th International
    Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2001, pp. 351–365.
conference:
  end_date: 2001-08-25
  location: Aalborg, Denmark
  name: 'CONCUR: Concurrency Theory'
  start_date: 2001-08-20
date_created: 2018-12-11T12:09:51Z
date_published: 2001-08-13T00:00:00Z
date_updated: 2023-05-08T10:24:59Z
day: '13'
doi: 10.1007/3-540-44685-0_24
extern: '1'
intvolume: '      2154'
language:
- iso: eng
month: '08'
oa_version: None
page: 351 - 365
publication: Proceedings of the 12th International Conference on on Concurrency Theory
publication_identifier:
  isbn:
  - '9783540424970'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '75'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Compositional methods for probabilistic systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2154
year: '2001'
...
---
_id: '4633'
abstract:
- lang: eng
  text: "A procedure for the analysis of state spaces is called symbolic if it manipulates
    not individual states, but sets of states that are represented by constraints.
    Such a procedure can be used for the analysis of infinite state spaces, provided
    termination is guaranteed. We present symbolic procedures, and corresponding termination
    criteria, for the solution of infinite-state games, which occur in the control
    and modular verification of infinite-state systems. To characterize the termination
    of symbolic procedures for solving infinite-state games, we classify these game
    structures into four increasingly restrictive categories:\r\n1  \tClass 1 consists
    of infinite-state structures for which all safety and reachability games can be
    solved.\r\n2  \tClass 2 consists of infinite-state structures for which all ω-regular
    games can be solved.\r\n3  \tClass 3 consists of infinite-state structures for
    which all nested positive boolean combinations of ω-regular games can be solved.\r\n4
    \ \tClass 4 consists of infinite-state structures for which all nested boolean
    combinations of ω-regular games can be solved.\r\nWe give a structural characterization
    for each class, using equivalence relations on the state spaces of games which
    range from game versions of trace equivalence to a game version of bisimilarity.
    We provide infinite-state examples for all four classes of games from control
    problems for hybrid systems. We conclude by presenting symbolic algorithms for
    the synthesis of winning strategies (“controller synthesis”) for infinitestate
    games with arbitrary ω-regular objectives, and prove termination over all class-2
    structures. This settles, in particular, the symbolic controller synthesis problem
    for rectangular hybrid systems."
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327,
  the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the NSF Theory
  grant CCR-9988172, and the NSF ITR grant CCR-0085949.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
citation:
  ama: 'De Alfaro L, Henzinger TA, Majumdar R. Symbolic algorithms for infinite-state
    games. In: <i>Proceedings of the 12th International Conference on on Concurrency
    Theory</i>. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:536-550.
    doi:<a href="https://doi.org/10.1007/3-540-44685-0_36">10.1007/3-540-44685-0_36</a>'
  apa: 'De Alfaro, L., Henzinger, T. A., &#38; Majumdar, R. (2001). Symbolic algorithms
    for infinite-state games. In <i>Proceedings of the 12th International Conference
    on on Concurrency Theory</i> (Vol. 2154, pp. 536–550). Aalborg, Denmark: Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.1007/3-540-44685-0_36">https://doi.org/10.1007/3-540-44685-0_36</a>'
  chicago: De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “Symbolic Algorithms
    for Infinite-State Games.” In <i>Proceedings of the 12th International Conference
    on on Concurrency Theory</i>, 2154:536–50. Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2001. <a href="https://doi.org/10.1007/3-540-44685-0_36">https://doi.org/10.1007/3-540-44685-0_36</a>.
  ieee: L. De Alfaro, T. A. Henzinger, and R. Majumdar, “Symbolic algorithms for infinite-state
    games,” in <i>Proceedings of the 12th International Conference on on Concurrency
    Theory</i>, Aalborg, Denmark, 2001, vol. 2154, pp. 536–550.
  ista: 'De Alfaro L, Henzinger TA, Majumdar R. 2001. Symbolic algorithms for infinite-state
    games. Proceedings of the 12th International Conference on on Concurrency Theory.
    CONCUR: Concurrency Theory, LNCS, vol. 2154, 536–550.'
  mla: De Alfaro, Luca, et al. “Symbolic Algorithms for Infinite-State Games.” <i>Proceedings
    of the 12th International Conference on on Concurrency Theory</i>, vol. 2154,
    Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 536–50, doi:<a href="https://doi.org/10.1007/3-540-44685-0_36">10.1007/3-540-44685-0_36</a>.
  short: L. De Alfaro, T.A. Henzinger, R. Majumdar, in:, Proceedings of the 12th International
    Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2001, pp. 536–550.
conference:
  end_date: 2001-08-25
  location: Aalborg, Denmark
  name: 'CONCUR: Concurrency Theory'
  start_date: 2001-08-20
date_created: 2018-12-11T12:09:52Z
date_published: 2001-08-13T00:00:00Z
date_updated: 2023-05-08T09:57:31Z
day: '13'
doi: 10.1007/3-540-44685-0_36
extern: '1'
intvolume: '      2154'
language:
- iso: eng
month: '08'
oa_version: None
page: 536 - 550
publication: Proceedings of the 12th International Conference on on Concurrency Theory
publication_identifier:
  isbn:
  - '9783540424970'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '73'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic algorithms for infinite-state games
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2154
year: '2001'
...
---
_id: '4634'
abstract:
- lang: eng
  text: "A controller is an environment for a system that achieves a particular control
    objective by providing inputs to the system without constraining the choices of
    the system. For synchronous systems, where system and controller make simultaneous
    and interdependent choices, the notion that a controller must not constrain the
    choices of the system can be formalized by type systems for composability. In
    a previous paper, we solved the control problem for static and dynamic types:
    a static type is a dependency relation between inputs and outputs, and composition
    is well-typed if it does not introduce cyclic dependencies; a dynamic type is
    a set of static types, one for each state. Static and dynamic types, however,
    cannot capture many important digital circuits, such as gated clocks, bidirectional
    buses, and random-access memory. We therefore introduce more general type systems,
    so-called dependent and bidirectional types, for modeling these situations, and
    we solve the corresponding control problems.\r\nIn a system with a dependent type,
    the dependencies between inputs and outputs are determined gradually through a
    game of the system against the controller. In a system with a bidirectional type,
    also the distinction between inputs and outputs is resolved dynamically by such
    a game. The game proceeds in several rounds. In each round the system and the
    controller choose to update some variables dependent on variables that have already
    been updated. The solution of the control problem for dependent and bidirectional
    types is based on algorithms for solving these games."
acknowledgement: This research was supported in part by the SRC contract 99-TJ-683.003,
  the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the AFOSR
  MURI grant F49620-00-1-0327, and the NSF Theory grant CCR-9988172.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: 'De Alfaro L, Henzinger TA, Mang F. The control of synchronous systems, Part
    II. In: <i>Proceedings of the 12th International Conference on on Concurrency
    Theory</i>. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:566-581.
    doi:<a href="https://doi.org/10.1007/3-540-44685-0_38">10.1007/3-540-44685-0_38</a>'
  apa: 'De Alfaro, L., Henzinger, T. A., &#38; Mang, F. (2001). The control of synchronous
    systems, Part II. In <i>Proceedings of the 12th International Conference on on
    Concurrency Theory</i> (Vol. 2154, pp. 566–581). Aalborg, Denmark: Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.1007/3-540-44685-0_38">https://doi.org/10.1007/3-540-44685-0_38</a>'
  chicago: De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “The Control of Synchronous
    Systems, Part II.” In <i>Proceedings of the 12th International Conference on on
    Concurrency Theory</i>, 2154:566–81. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2001. <a href="https://doi.org/10.1007/3-540-44685-0_38">https://doi.org/10.1007/3-540-44685-0_38</a>.
  ieee: L. De Alfaro, T. A. Henzinger, and F. Mang, “The control of synchronous systems,
    Part II,” in <i>Proceedings of the 12th International Conference on on Concurrency
    Theory</i>, Aalborg, Denmark, 2001, vol. 2154, pp. 566–581.
  ista: 'De Alfaro L, Henzinger TA, Mang F. 2001. The control of synchronous systems,
    Part II. Proceedings of the 12th International Conference on on Concurrency Theory.
    CONCUR: Concurrency Theory, LNCS, vol. 2154, 566–581.'
  mla: De Alfaro, Luca, et al. “The Control of Synchronous Systems, Part II.” <i>Proceedings
    of the 12th International Conference on on Concurrency Theory</i>, vol. 2154,
    Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 566–81, doi:<a href="https://doi.org/10.1007/3-540-44685-0_38">10.1007/3-540-44685-0_38</a>.
  short: L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 12th International
    Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2001, pp. 566–581.
conference:
  end_date: 2001-08-25
  location: Aalborg, Denmark
  name: 'CONCUR: Concurrency Theory'
  start_date: 2001-08-20
date_created: 2018-12-11T12:09:52Z
date_published: 2001-08-13T00:00:00Z
date_updated: 2023-05-08T10:20:19Z
day: '13'
doi: 10.1007/3-540-44685-0_38
extern: '1'
intvolume: '      2154'
language:
- iso: eng
month: '08'
oa_version: None
page: 566 - 581
publication: Proceedings of the 12th International Conference on on Concurrency Theory
publication_identifier:
  isbn:
  - '9783540424970'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '74'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The control of synchronous systems, Part II
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2154
year: '2001'
...