---
_id: '3855'
abstract:
- lang: eng
  text: 'We study observation-based strategies for partially-observable Markov decision
    processes (POMDPs) with parity objectives. An observation-based strategy relies
    on partial information about the history of a play, namely, on the past sequence
    of observations. We consider qualitative analysis problems: given a POMDP with
    a parity objective, decide whether there exists an observation-based strategy
    to achieve the objective with probability 1 (almost-sure winning), or with positive
    probability (positive winning). Our main results are twofold. First, we present
    a complete picture of the computational complexity of the qualitative analysis
    problem for POMDPs with parity objectives and its subclasses: safety, reachability,
    Büchi, and coBüchi objectives. We establish several upper and lower bounds that
    were not known in the literature. Second, we give optimal bounds (matching upper
    and lower bounds) for the memory required by pure and randomized observation-based
    strategies for each class of objectives.'
alternative_title:
- LNCS
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- 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: 'Chatterjee K, Doyen L, Henzinger TA. Qualitative analysis of partially-observable
    Markov Decision Processes. In: Vol 6281. Springer; 2010:258-269. doi:<a href="https://doi.org/10.1007/978-3-642-15155-2_24">10.1007/978-3-642-15155-2_24</a>'
  apa: 'Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2010). Qualitative analysis
    of partially-observable Markov Decision Processes (Vol. 6281, pp. 258–269). Presented
    at the MFCS: Mathematical Foundations of Computer Science, Brno, Czech Republic:
    Springer. <a href="https://doi.org/10.1007/978-3-642-15155-2_24">https://doi.org/10.1007/978-3-642-15155-2_24</a>'
  chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Qualitative
    Analysis of Partially-Observable Markov Decision Processes,” 6281:258–69. Springer,
    2010. <a href="https://doi.org/10.1007/978-3-642-15155-2_24">https://doi.org/10.1007/978-3-642-15155-2_24</a>.
  ieee: 'K. Chatterjee, L. Doyen, and T. A. Henzinger, “Qualitative analysis of partially-observable
    Markov Decision Processes,” presented at the MFCS: Mathematical Foundations of
    Computer Science, Brno, Czech Republic, 2010, vol. 6281, pp. 258–269.'
  ista: 'Chatterjee K, Doyen L, Henzinger TA. 2010. Qualitative analysis of partially-observable
    Markov Decision Processes. MFCS: Mathematical Foundations of Computer Science,
    LNCS, vol. 6281, 258–269.'
  mla: Chatterjee, Krishnendu, et al. <i>Qualitative Analysis of Partially-Observable
    Markov Decision Processes</i>. Vol. 6281, Springer, 2010, pp. 258–69, doi:<a href="https://doi.org/10.1007/978-3-642-15155-2_24">10.1007/978-3-642-15155-2_24</a>.
  short: K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2010, pp. 258–269.
conference:
  end_date: 2010-08-27
  location: Brno, Czech Republic
  name: 'MFCS: Mathematical Foundations of Computer Science'
  start_date: 2010-08-23
corr_author: '1'
date_created: 2018-12-11T12:05:32Z
date_published: 2010-08-01T00:00:00Z
date_updated: 2024-10-09T21:08:23Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-15155-2_24
ec_funded: 1
file:
- access_level: open_access
  checksum: b6c82ec82f194e5b0ab7c1c3800e4580
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:13:51Z
  date_updated: 2020-07-14T12:46:17Z
  file_id: '5038'
  file_name: IST-2012-61-v1+1_Qualitative_analysis_of_partially-observable_Markov_Decision_Processes.pdf
  file_size: 173948
  relation: main_file
file_date_updated: 2020-07-14T12:46:17Z
has_accepted_license: '1'
intvolume: '      6281'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 258 - 269
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '215543'
  name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '214373'
  name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '2326'
pubrep_id: '61'
quality_controlled: '1'
related_material:
  record:
  - id: '5395'
    relation: earlier_version
    status: public
scopus_import: 1
status: public
title: Qualitative analysis of partially-observable Markov Decision Processes
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6281
year: '2010'
...
---
_id: '3856'
abstract:
- lang: eng
  text: 'We consider two-player zero-sum games on graphs. These games can be classified
    on the basis of the information of the players and on the mode of interaction
    between them. On the basis of information the classification is as follows: (a)
    partial-observation (both players have partial view of the game); (b) one-sided
    complete-observation (one player has complete observation); and (c) complete-observation
    (both players have complete view of the game). On the basis of mode of interaction
    we have the following classification: (a) concurrent (players interact simultaneously);
    and (b) turn-based (players interact in turn). The two sources of randomness in
    these games are randomness in transition function and randomness in strategies.
    In general, randomized strategies are more powerful than deterministic strategies,
    and randomness in transitions gives more general classes of games. We present
    a complete characterization for the classes of games where randomness is not helpful
    in: (a) the transition function (probabilistic transition can be simulated by
    deterministic transition); and (b) strategies (pure strategies are as powerful
    as randomized strategies). As consequence of our characterization we obtain new
    undecidability results for these games. '
acknowledgement: This research was supported by the European Union project COMBEST
  and the European Network of Excellence ArtistDesign.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Hugo
  full_name: Gimbert, Hugo
  last_name: Gimbert
- 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: 'Chatterjee K, Doyen L, Gimbert H, Henzinger TA. Randomness for free. In: Vol
    6281. Springer; 2010:246-257. doi:<a href="https://doi.org/10.1007/978-3-642-15155-2_23">10.1007/978-3-642-15155-2_23</a>'
  apa: 'Chatterjee, K., Doyen, L., Gimbert, H., &#38; Henzinger, T. A. (2010). Randomness
    for free (Vol. 6281, pp. 246–257). Presented at the MFCS: Mathematical Foundations
    of Computer Science, Brno, Czech Republic: Springer. <a href="https://doi.org/10.1007/978-3-642-15155-2_23">https://doi.org/10.1007/978-3-642-15155-2_23</a>'
  chicago: Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Thomas A Henzinger.
    “Randomness for Free,” 6281:246–57. Springer, 2010. <a href="https://doi.org/10.1007/978-3-642-15155-2_23">https://doi.org/10.1007/978-3-642-15155-2_23</a>.
  ieee: 'K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger, “Randomness for
    free,” presented at the MFCS: Mathematical Foundations of Computer Science, Brno,
    Czech Republic, 2010, vol. 6281, pp. 246–257.'
  ista: 'Chatterjee K, Doyen L, Gimbert H, Henzinger TA. 2010. Randomness for free.
    MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 6281, 246–257.'
  mla: Chatterjee, Krishnendu, et al. <i>Randomness for Free</i>. Vol. 6281, Springer,
    2010, pp. 246–57, doi:<a href="https://doi.org/10.1007/978-3-642-15155-2_23">10.1007/978-3-642-15155-2_23</a>.
  short: K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, in:, Springer, 2010,
    pp. 246–257.
conference:
  end_date: 2010-08-27
  location: Brno, Czech Republic
  name: 'MFCS: Mathematical Foundations of Computer Science'
  start_date: 2010-08-23
corr_author: '1'
date_created: 2018-12-11T12:05:32Z
date_published: 2010-09-06T00:00:00Z
date_updated: 2025-09-23T10:32:00Z
day: '06'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-15155-2_23
ec_funded: 1
external_id:
  arxiv:
  - '1006.0673'
intvolume: '      6281'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1006.0673
month: '09'
oa: 1
oa_version: Preprint
page: 246 - 257
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '215543'
  name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '214373'
  name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '2325'
pubrep_id: '60'
quality_controlled: '1'
related_material:
  record:
  - id: '1731'
    relation: later_version
    status: public
scopus_import: '1'
status: public
title: Randomness for free
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6281
year: '2010'
...
---
_id: '3857'
abstract:
- lang: eng
  text: We consider probabilistic automata on infinite words with acceptance defined
    by safety, reachability, Büchi, coBüchi, and limit-average conditions. We consider
    quantitative and qualitative decision problems. We present extensions and adaptations
    of proofs for probabilistic finite automata and present an almost complete characterization
    of the decidability and undecidability frontier of the quantitative and qualitative
    decision problems for probabilistic automata on infinite words.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- 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: 'Chatterjee K, Henzinger TA. Probabilistic Automata on infinite words: decidability
    and undecidability results. In: Vol 6252. Springer; 2010:1-16. doi:<a href="https://doi.org/10.1007/978-3-642-15643-4_1">10.1007/978-3-642-15643-4_1</a>'
  apa: 'Chatterjee, K., &#38; Henzinger, T. A. (2010). Probabilistic Automata on infinite
    words: decidability and undecidability results (Vol. 6252, pp. 1–16). Presented
    at the ATVA: Automated Technology for Verification and Analysis, Singapore, Singapore:
    Springer. <a href="https://doi.org/10.1007/978-3-642-15643-4_1">https://doi.org/10.1007/978-3-642-15643-4_1</a>'
  chicago: 'Chatterjee, Krishnendu, and Thomas A Henzinger. “Probabilistic Automata
    on Infinite Words: Decidability and Undecidability Results,” 6252:1–16. Springer,
    2010. <a href="https://doi.org/10.1007/978-3-642-15643-4_1">https://doi.org/10.1007/978-3-642-15643-4_1</a>.'
  ieee: 'K. Chatterjee and T. A. Henzinger, “Probabilistic Automata on infinite words:
    decidability and undecidability results,” presented at the ATVA: Automated Technology
    for Verification and Analysis, Singapore, Singapore, 2010, vol. 6252, pp. 1–16.'
  ista: 'Chatterjee K, Henzinger TA. 2010. Probabilistic Automata on infinite words:
    decidability and undecidability results. ATVA: Automated Technology for Verification
    and Analysis, LNCS, vol. 6252, 1–16.'
  mla: 'Chatterjee, Krishnendu, and Thomas A. Henzinger. <i>Probabilistic Automata
    on Infinite Words: Decidability and Undecidability Results</i>. Vol. 6252, Springer,
    2010, pp. 1–16, doi:<a href="https://doi.org/10.1007/978-3-642-15643-4_1">10.1007/978-3-642-15643-4_1</a>.'
  short: K. Chatterjee, T.A. Henzinger, in:, Springer, 2010, pp. 1–16.
conference:
  end_date: 2010-09-24
  location: Singapore, Singapore
  name: 'ATVA: Automated Technology for Verification and Analysis'
  start_date: 2010-09-21
corr_author: '1'
date_created: 2018-12-11T12:05:33Z
date_published: 2010-10-12T00:00:00Z
date_updated: 2024-10-09T21:08:23Z
day: '12'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-15643-4_1
ec_funded: 1
intvolume: '      6252'
language:
- iso: eng
month: '10'
oa_version: None
page: 1 - 16
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '215543'
  name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '214373'
  name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '2324'
pubrep_id: '28'
quality_controlled: '1'
related_material:
  record:
  - id: '5392'
    relation: earlier_version
    status: public
scopus_import: 1
status: public
title: 'Probabilistic Automata on infinite words: decidability and undecidability
  results'
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6252
year: '2010'
...
---
_id: '3859'
abstract:
- lang: eng
  text: This book constitutes the proceedings of the 8th International Conference
    on Formal Modeling and Analysis of Timed Systems, FORMATS 2010, held in Klosterneuburg,
    Austria in September 2010. The 14 papers presented were carefully reviewed and
    selected from 31 submissions. In addition, the volume contains 3 invited talks
    and 2 invited tutorials.The aim of FORMATS is to promote the study of fundamental
    and practical aspects of timed systems, and to bring together researchers from
    different disciplines that share an interest in the modeling and analysis of timed
    systems. Typical topics include foundations and semantics, methods and tools,
    and applications.
alternative_title:
- LNCS
citation:
  ama: Chatterjee K, Henzinger TA, eds. <i>Formal Modeling and Analysis of Timed Systems</i>.
    Vol 6246. Springer; 2010. doi:<a href="https://doi.org/10.1007/978-3-642-15297-9">10.1007/978-3-642-15297-9</a>
  apa: 'Chatterjee, K., &#38; Henzinger, T. A. (Eds.). (2010). <i>Formal modeling
    and analysis of timed systems</i> (Vol. 6246). Presented at the FORMATS: Formal
    Modeling and Analysis of Timed Systems, Klosterneuburg, Austria: Springer. <a
    href="https://doi.org/10.1007/978-3-642-15297-9">https://doi.org/10.1007/978-3-642-15297-9</a>'
  chicago: Chatterjee, Krishnendu, and Thomas A Henzinger, eds. <i>Formal Modeling
    and Analysis of Timed Systems</i>. Vol. 6246. Springer, 2010. <a href="https://doi.org/10.1007/978-3-642-15297-9">https://doi.org/10.1007/978-3-642-15297-9</a>.
  ieee: K. Chatterjee and T. A. Henzinger, Eds., <i>Formal modeling and analysis of
    timed systems</i>, vol. 6246. Springer, 2010.
  ista: Chatterjee K, Henzinger TA eds. 2010. Formal modeling and analysis of timed
    systems, Springer,p.
  mla: Chatterjee, Krishnendu, and Thomas A. Henzinger, editors. <i>Formal Modeling
    and Analysis of Timed Systems</i>. Vol. 6246, Springer, 2010, doi:<a href="https://doi.org/10.1007/978-3-642-15297-9">10.1007/978-3-642-15297-9</a>.
  short: K. Chatterjee, T.A. Henzinger, eds., Formal Modeling and Analysis of Timed
    Systems, Springer, 2010.
conference:
  end_date: 2010-09-10
  location: Klosterneuburg, Austria
  name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
  start_date: 2010-09-08
corr_author: '1'
date_created: 2018-12-11T12:05:33Z
date_published: 2010-09-20T00:00:00Z
date_updated: 2024-10-09T20:54:05Z
day: '20'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-15297-9
editor:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
intvolume: '      6246'
language:
- iso: eng
month: '09'
oa_version: None
publication_status: published
publisher: Springer
publist_id: '2322'
quality_controlled: '1'
related_material:
  link:
  - description: eBook available via IST BookList
    relation: other
    url: https://koha.app.ist.ac.at/cgi-bin/koha/opac-detail.pl?biblionumber=12721
status: public
title: Formal modeling and analysis of timed systems
type: conference_editor
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 6246
year: '2010'
...
---
_id: '3860'
abstract:
- lang: eng
  text: 'In mean-payoff games, the objective of the protagonist is to ensure that
    the limit average of an infinite sequence of numeric weights is nonnegative. In
    energy games, the objective is to ensure that the running sum of weights is always
    nonnegative. Generalized mean-payoff and energy games replace individual weights
    by tuples, and the limit average (resp. running sum) of each coordinate must be
    (resp. remain) nonnegative. These games have applications in the synthesis of
    resource-bounded processes with multiple resources. We prove the finite-memory
    determinacy of generalized energy games and show the inter- reducibility of generalized
    mean-payoff and energy games for finite-memory strategies. We also improve the
    computational complexity for solving both classes of games with finite-memory
    strategies: while the previously best known upper bound was EXPSPACE, and no lower
    bound was known, we give an optimal coNP-complete bound. For memoryless strategies,
    we show that the problem of deciding the existence of a winning strategy for the
    protagonist is NP-complete.'
alternative_title:
- LIPIcs
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- 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: Jean
  full_name: Raskin, Jean
  last_name: Raskin
citation:
  ama: 'Chatterjee K, Doyen L, Henzinger TA, Raskin J. Generalized mean-payoff and
    energy games. In: Vol 8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:505-516.
    doi:<a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505">10.4230/LIPIcs.FSTTCS.2010.505</a>'
  apa: 'Chatterjee, K., Doyen, L., Henzinger, T. A., &#38; Raskin, J. (2010). Generalized
    mean-payoff and energy games (Vol. 8, pp. 505–516). Presented at the FSTTCS: Foundations
    of Software Technology and Theoretical Computer Science, Chennai, India: Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505">https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505</a>'
  chicago: Chatterjee, Krishnendu, Laurent Doyen, Thomas A Henzinger, and Jean Raskin.
    “Generalized Mean-Payoff and Energy Games,” 8:505–16. Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2010. <a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505">https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505</a>.
  ieee: 'K. Chatterjee, L. Doyen, T. A. Henzinger, and J. Raskin, “Generalized mean-payoff
    and energy games,” presented at the FSTTCS: Foundations of Software Technology
    and Theoretical Computer Science, Chennai, India, 2010, vol. 8, pp. 505–516.'
  ista: 'Chatterjee K, Doyen L, Henzinger TA, Raskin J. 2010. Generalized mean-payoff
    and energy games. FSTTCS: Foundations of Software Technology and Theoretical Computer
    Science, LIPIcs, vol. 8, 505–516.'
  mla: Chatterjee, Krishnendu, et al. <i>Generalized Mean-Payoff and Energy Games</i>.
    Vol. 8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 505–16, doi:<a
    href="https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505">10.4230/LIPIcs.FSTTCS.2010.505</a>.
  short: K. Chatterjee, L. Doyen, T.A. Henzinger, J. Raskin, in:, Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik, 2010, pp. 505–516.
conference:
  end_date: 2010-12-18
  location: Chennai, India
  name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
  start_date: 2010-12-15
corr_author: '1'
date_created: 2018-12-11T12:05:34Z
date_published: 2010-12-13T00:00:00Z
date_updated: 2025-09-30T09:33:50Z
day: '13'
ddc:
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.4230/LIPIcs.FSTTCS.2010.505
external_id:
  isi:
  - '000310361000043'
file:
- access_level: open_access
  checksum: 1caabd6319b979927208117a41192637
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:15:27Z
  date_updated: 2020-07-14T12:46:18Z
  file_id: '5147'
  file_name: IST-2012-59-v1+1_Generalized_mean-payoff_and_energy_games.pdf
  file_size: 178278
  relation: main_file
- access_level: open_access
  checksum: 3a59759ceeacdb5b578f3803d5e6769b
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:15:28Z
  date_updated: 2020-07-14T12:46:18Z
  file_id: '5148'
  file_name: IST-2016-59-v2+1_2_1_.pdf
  file_size: 477976
  relation: main_file
file_date_updated: 2020-07-14T12:46:18Z
has_accepted_license: '1'
intvolume: '         8'
isi: 1
language:
- iso: eng
month: '12'
oa: 1
oa_version: Submitted Version
page: 505 - 516
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '2321'
pubrep_id: '59'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Generalized mean-payoff and energy games
tmp:
  image: /images/cc_by_nc_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
  name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
    (CC BY-NC-ND 4.0)
  short: CC BY-NC-ND (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 8
year: '2010'
...
---
_id: '3861'
abstract:
- lang: eng
  text: We introduce strategy logic, a logic that treats strategies in two-player
    games as explicit first-order objects. The explicit treatment of strategies allows
    us to specify properties of nonzero-sum games in a simple and natural way. We
    show that the one-alternation fragment of strategy logic is strong enough to express
    the existence of Nash equilibria and secure equilibria, and subsumes other logics
    that were introduced to reason about games, such as ATL, ATL*, and game logic.
    We show that strategy logic is decidable, by constructing tree automata that recognize
    sets of strategies. While for the general logic, our decision procedure is nonelementary,
    for the simple fragment that is used above we show that the complexity is polynomial
    in the size of the game graph and optimal in the size of the formula (ranging
    from polynomial to 2EXPTIME depending on the form of the formula).
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- 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: Nir
  full_name: Piterman, Nir
  last_name: Piterman
citation:
  ama: Chatterjee K, Henzinger TA, Piterman N. Strategy logic. <i>Information and
    Computation</i>. 2010;208(6):677-693. doi:<a href="https://doi.org/10.1016/j.ic.2009.07.004">10.1016/j.ic.2009.07.004</a>
  apa: Chatterjee, K., Henzinger, T. A., &#38; Piterman, N. (2010). Strategy logic.
    <i>Information and Computation</i>. Elsevier. <a href="https://doi.org/10.1016/j.ic.2009.07.004">https://doi.org/10.1016/j.ic.2009.07.004</a>
  chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Nir Piterman. “Strategy
    Logic.” <i>Information and Computation</i>. Elsevier, 2010. <a href="https://doi.org/10.1016/j.ic.2009.07.004">https://doi.org/10.1016/j.ic.2009.07.004</a>.
  ieee: K. Chatterjee, T. A. Henzinger, and N. Piterman, “Strategy logic,” <i>Information
    and Computation</i>, vol. 208, no. 6. Elsevier, pp. 677–693, 2010.
  ista: Chatterjee K, Henzinger TA, Piterman N. 2010. Strategy logic. Information
    and Computation. 208(6), 677–693.
  mla: Chatterjee, Krishnendu, et al. “Strategy Logic.” <i>Information and Computation</i>,
    vol. 208, no. 6, Elsevier, 2010, pp. 677–93, doi:<a href="https://doi.org/10.1016/j.ic.2009.07.004">10.1016/j.ic.2009.07.004</a>.
  short: K. Chatterjee, T.A. Henzinger, N. Piterman, Information and Computation 208
    (2010) 677–693.
corr_author: '1'
date_created: 2018-12-11T12:05:34Z
date_published: 2010-06-01T00:00:00Z
date_updated: 2025-09-30T09:32:18Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2009.07.004
external_id:
  isi:
  - '000278070100006'
file:
- access_level: open_access
  checksum: 13bff93f3c2a014e2908145a4517f177
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:11:54Z
  date_updated: 2020-07-14T12:46:18Z
  file_id: '4911'
  file_name: IST-2012-56-v1+1_Strategy_logic.pdf
  file_size: 189120
  relation: main_file
file_date_updated: 2020-07-14T12:46:18Z
has_accepted_license: '1'
intvolume: '       208'
isi: 1
issue: '6'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 677 - 693
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '2317'
pubrep_id: '56'
quality_controlled: '1'
related_material:
  record:
  - id: '3884'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Strategy logic
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 208
year: '2010'
...
---
_id: '3863'
abstract:
- lang: eng
  text: 'We consider two-player parity games with imperfect information in which strategies
    rely on observations that provide imperfect information about the history of a
    play. To solve such games, i.e., to determine the winning regions of players and
    corresponding winning strategies, one can use the subset construction to build
    an equivalent perfect-information game. Recently, an algorithm that avoids the
    inefficient subset construction has been proposed. The algorithm performs a fixed-point
    computation in a lattice of antichains, thus maintaining a succinct representation
    of state sets. However, this representation does not allow to recover winning
    strategies. In this paper, we build on the antichain approach to develop an algorithm
    for constructing the winning strategies in parity games of imperfect information.
    One major obstacle in adapting the classical procedure is that the complementation
    of attractor sets would break the invariant of downward-closedness on which the
    antichain representation relies. We overcome this difficulty by decomposing problem
    instances recursively into games with a combination of reachability, safety, and
    simpler parity conditions. We also report on an experimental implementation of
    our algorithm: to our knowledge, this is the first implementation of a procedure
    for solving imperfect-information parity games on graphs.'
article_processing_charge: No
author:
- first_name: Dietmar
  full_name: Berwanger, Dietmar
  last_name: Berwanger
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Martin
  full_name: De Wulf, Martin
  last_name: De Wulf
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- 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: Berwanger D, Chatterjee K, De Wulf M, Doyen L, Henzinger TA. Strategy construction
    for parity games with imperfect information. <i>Information and Computation</i>.
    2010;208(10):1206-1220. doi:<a href="https://doi.org/10.1016/j.ic.2009.09.006">10.1016/j.ic.2009.09.006</a>
  apa: Berwanger, D., Chatterjee, K., De Wulf, M., Doyen, L., &#38; Henzinger, T.
    A. (2010). Strategy construction for parity games with imperfect information.
    <i>Information and Computation</i>. Elsevier. <a href="https://doi.org/10.1016/j.ic.2009.09.006">https://doi.org/10.1016/j.ic.2009.09.006</a>
  chicago: Berwanger, Dietmar, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen,
    and Thomas A Henzinger. “Strategy Construction for Parity Games with Imperfect
    Information.” <i>Information and Computation</i>. Elsevier, 2010. <a href="https://doi.org/10.1016/j.ic.2009.09.006">https://doi.org/10.1016/j.ic.2009.09.006</a>.
  ieee: D. Berwanger, K. Chatterjee, M. De Wulf, L. Doyen, and T. A. Henzinger, “Strategy
    construction for parity games with imperfect information,” <i>Information and
    Computation</i>, vol. 208, no. 10. Elsevier, pp. 1206–1220, 2010.
  ista: Berwanger D, Chatterjee K, De Wulf M, Doyen L, Henzinger TA. 2010. Strategy
    construction for parity games with imperfect information. Information and Computation.
    208(10), 1206–1220.
  mla: Berwanger, Dietmar, et al. “Strategy Construction for Parity Games with Imperfect
    Information.” <i>Information and Computation</i>, vol. 208, no. 10, Elsevier,
    2010, pp. 1206–20, doi:<a href="https://doi.org/10.1016/j.ic.2009.09.006">10.1016/j.ic.2009.09.006</a>.
  short: D. Berwanger, K. Chatterjee, M. De Wulf, L. Doyen, T.A. Henzinger, Information
    and Computation 208 (2010) 1206–1220.
date_created: 2018-12-11T12:05:35Z
date_published: 2010-10-01T00:00:00Z
date_updated: 2026-05-29T09:53:31Z
day: '01'
ddc:
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2009.09.006
ec_funded: 1
external_id:
  isi:
  - '000281830300007'
file:
- access_level: open_access
  checksum: 29d146e4f8049dbb7f80bbf7ea3700ed
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:17:44Z
  date_updated: 2020-07-14T12:46:18Z
  file_id: '5300'
  file_name: IST-2012-58-v1+1_Strategy_construction_for_parity_games_with_imperfect_information.pdf
  file_size: 287496
  relation: main_file
file_date_updated: 2020-07-14T12:46:18Z
has_accepted_license: '1'
intvolume: '       208'
isi: 1
issue: '10'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 1206 - 1220
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '215543'
  name: COMponent-Based Embedded Systems design Techniques
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '2319'
pubrep_id: '58'
quality_controlled: '1'
related_material:
  record:
  - id: '3880'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Strategy construction for parity games with imperfect information
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 208
year: '2010'
...
---
_id: '3864'
abstract:
- lang: eng
  text: 'Often one has a preference order among the different systems that satisfy
    a given specification. Under a probabilistic assumption about the possible inputs,
    such a preference order is naturally expressed by a weighted automaton, which
    assigns to each word a value, such that a system is preferred if it generates
    a higher expected value. We solve the following optimal-synthesis problem: given
    an omega-regular specification, a Markov chain that describes the distribution
    of inputs, and a weighted automaton that measures how well a system satisfies
    the given specification tinder the given input assumption, synthesize a system
    that optimizes the measured value. For safety specifications and measures that
    are defined by mean-payoff automata, the optimal-synthesis problem amounts to
    finding a strategy in a Markov decision process (MDP) that is optimal for a long-run
    average reward objective, which can be done in polynomial time. For general omega-regular
    specifications, the solution rests on a new, polynomial-time algorithm for computing
    optimal strategies in MDPs with mean-payoff parity objectives. We present some
    experimental results showing optimal systems that were automatically generated
    in this way.'
acknowledgement: This research was supported by the European Union project COMBEST
  and the European Network of Excellence ArtistDesign.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- 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: Barbara
  full_name: Jobstmann, Barbara
  last_name: Jobstmann
- first_name: Rohit
  full_name: Singh, Rohit
  last_name: Singh
citation:
  ama: 'Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing
    systems in probabilistic environments. In: Vol 6174. Springer; 2010:380-395. doi:<a
    href="https://doi.org/10.1007/978-3-642-14295-6_34">10.1007/978-3-642-14295-6_34</a>'
  apa: 'Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Singh, R. (2010). Measuring
    and synthesizing systems in probabilistic environments (Vol. 6174, pp. 380–395).
    Presented at the CAV: Computer Aided Verification, Edinburgh, United Kingdom:
    Springer. <a href="https://doi.org/10.1007/978-3-642-14295-6_34">https://doi.org/10.1007/978-3-642-14295-6_34</a>'
  chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit
    Singh. “Measuring and Synthesizing Systems in Probabilistic Environments,” 6174:380–95.
    Springer, 2010. <a href="https://doi.org/10.1007/978-3-642-14295-6_34">https://doi.org/10.1007/978-3-642-14295-6_34</a>.
  ieee: 'K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “Measuring and
    synthesizing systems in probabilistic environments,” presented at the CAV: Computer
    Aided Verification, Edinburgh, United Kingdom, 2010, vol. 6174, pp. 380–395.'
  ista: 'Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2010. Measuring and synthesizing
    systems in probabilistic environments. CAV: Computer Aided Verification, LNCS,
    vol. 6174, 380–395.'
  mla: Chatterjee, Krishnendu, et al. <i>Measuring and Synthesizing Systems in Probabilistic
    Environments</i>. Vol. 6174, Springer, 2010, pp. 380–95, doi:<a href="https://doi.org/10.1007/978-3-642-14295-6_34">10.1007/978-3-642-14295-6_34</a>.
  short: K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, in:, Springer, 2010,
    pp. 380–395.
conference:
  end_date: 2010-07-19
  location: Edinburgh, United Kingdom
  name: 'CAV: Computer Aided Verification'
  start_date: 201-07-15
corr_author: '1'
date_created: 2018-12-11T12:05:35Z
date_published: 2010-07-09T00:00:00Z
date_updated: 2025-09-23T09:33:01Z
day: '09'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-14295-6_34
external_id:
  arxiv:
  - '1004.0739'
intvolume: '      6174'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1004.0739
month: '07'
oa: 1
oa_version: Preprint
page: 380 - 395
publication_status: published
publisher: Springer
publist_id: '2313'
quality_controlled: '1'
related_material:
  record:
  - id: '1856'
    relation: later_version
    status: public
scopus_import: '1'
status: public
title: Measuring and synthesizing systems in probabilistic environments
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6174
year: '2010'
...
---
_id: '3866'
abstract:
- lang: eng
  text: Systems ought to behave reasonably even in circumstances that are not anticipated
    in their specifications. We propose a definition of robustness for liveness specifications
    which prescribes, for any number of environment assumptions that are violated,
    a minimal number of system guarantees that must still be fulfilled. This notion
    of robustness can be formulated and realized using a Generalized Reactivity formula.
    We present an algorithm for synthesizing robust systems from such formulas. For
    the important special case of Generalized Reactivity formulas of rank 1, our algorithm
    improves the complexity of [PPS06] for large specifications with a small number
    of assumptions and guarantees.
alternative_title:
- LNCS
author:
- first_name: Roderick
  full_name: Bloem, Roderick
  last_name: Bloem
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Karin
  full_name: Greimel, Karin
  last_name: Greimel
- 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: Barbara
  full_name: Jobstmann, Barbara
  last_name: Jobstmann
citation:
  ama: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Robustness in
    the presence of liveness. In: Touili T, Cook B, Jackson P, eds. Vol 6174. Springer;
    2010:410-424. doi:<a href="https://doi.org/10.1007/978-3-642-14295-6_36">10.1007/978-3-642-14295-6_36</a>'
  apa: 'Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., &#38; Jobstmann,
    B. (2010). Robustness in the presence of liveness. In T. Touili, B. Cook, &#38;
    P. Jackson (Eds.) (Vol. 6174, pp. 410–424). Presented at the CAV: Computer Aided
    Verification, Edinburgh, UK: Springer. <a href="https://doi.org/10.1007/978-3-642-14295-6_36">https://doi.org/10.1007/978-3-642-14295-6_36</a>'
  chicago: Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger,
    and Barbara Jobstmann. “Robustness in the Presence of Liveness.” edited by Tayssir
    Touili, Byron Cook, and Paul Jackson, 6174:410–24. Springer, 2010. <a href="https://doi.org/10.1007/978-3-642-14295-6_36">https://doi.org/10.1007/978-3-642-14295-6_36</a>.
  ieee: 'R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Robustness
    in the presence of liveness,” presented at the CAV: Computer Aided Verification,
    Edinburgh, UK, 2010, vol. 6174, pp. 410–424.'
  ista: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2010. Robustness
    in the presence of liveness. CAV: Computer Aided Verification, LNCS, vol. 6174,
    410–424.'
  mla: Bloem, Roderick, et al. <i>Robustness in the Presence of Liveness</i>. Edited
    by Tayssir Touili et al., vol. 6174, Springer, 2010, pp. 410–24, doi:<a href="https://doi.org/10.1007/978-3-642-14295-6_36">10.1007/978-3-642-14295-6_36</a>.
  short: R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, T.
    Touili, B. Cook, P. Jackson (Eds.), Springer, 2010, pp. 410–424.
conference:
  end_date: 2010-07-19
  location: Edinburgh, UK
  name: 'CAV: Computer Aided Verification'
  start_date: 2010-07-15
date_created: 2018-12-11T12:05:36Z
date_published: 2010-07-01T00:00:00Z
date_updated: 2021-01-12T07:52:47Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-642-14295-6_36
ec_funded: 1
editor:
- first_name: Tayssir
  full_name: Touili, Tayssir
  last_name: Touili
- first_name: Byron
  full_name: Cook, Byron
  last_name: Cook
- first_name: Paul
  full_name: Jackson, Paul
  last_name: Jackson
file:
- access_level: open_access
  checksum: 9d204611c8d7855bed8134f8708a0010
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:16:52Z
  date_updated: 2020-07-14T12:46:19Z
  file_id: '5243'
  file_name: IST-2012-54-v1+1_Robustness_in_the_presence_of_liveness.pdf
  file_size: 213083
  relation: main_file
file_date_updated: 2020-07-14T12:46:19Z
has_accepted_license: '1'
intvolume: '      6174'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 410 - 424
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '215543'
  name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '214373'
  name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '2310'
pubrep_id: '54'
quality_controlled: '1'
scopus_import: 1
status: public
title: Robustness in the presence of liveness
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6174
year: '2010'
...
---
_id: '3867'
abstract:
- lang: eng
  text: Weighted automata are nondeterministic automata with numerical weights on
    transitions. They can define quantitative languages L that assign to each word
    w a real number L(w). In the case of infinite words, the value of a run is naturally
    computed as the maximum, limsup, liminf, limit-average, or discounted-sum of the
    transition weights. The value of a word w is the supremum of the values of the
    runs over w. We study expressiveness and closure questions about these quantitative
    languages. We first show that the set of words with value greater than a threshold
    can be omega-regular for deterministic limit-average and discounted-sum automata,
    while this set is always omega-regular when the threshold is isolated (i.e., some
    neighborhood around the threshold contains no word). In the latter case, we prove
    that the omega-regular language is robust against small perturbations of the transition
    weights. We next consider automata with transition weights 0 or 1 and show that
    they are as expressive as general weighted automata in the limit-average case,
    but not in the discounted-sum case. Third, for quantitative languages L-1 and
    L-2, we consider the operations max(L-1, L-2), min(L-1, L-2), and 1 - L-1, which
    generalize the boolean operations on languages, as well as the sum L-1 + L-2.
    We establish the closure properties of all classes of quantitative languages with
    respect to these four operations.
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- 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: Chatterjee K, Doyen L, Henzinger TA. Expressiveness and closure properties
    for quantitative languages. <i>Logical Methods in Computer Science</i>. 2010;6(3):1-23.
    doi:<a href="https://doi.org/10.2168/LMCS-6(3:10)2010">10.2168/LMCS-6(3:10)2010</a>
  apa: Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2010). Expressiveness and
    closure properties for quantitative languages. <i>Logical Methods in Computer
    Science</i>. International Federation for Computational Logic. <a href="https://doi.org/10.2168/LMCS-6(3:10)2010">https://doi.org/10.2168/LMCS-6(3:10)2010</a>
  chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Expressiveness
    and Closure Properties for Quantitative Languages.” <i>Logical Methods in Computer
    Science</i>. International Federation for Computational Logic, 2010. <a href="https://doi.org/10.2168/LMCS-6(3:10)2010">https://doi.org/10.2168/LMCS-6(3:10)2010</a>.
  ieee: K. Chatterjee, L. Doyen, and T. A. Henzinger, “Expressiveness and closure
    properties for quantitative languages,” <i>Logical Methods in Computer Science</i>,
    vol. 6, no. 3. International Federation for Computational Logic, pp. 1–23, 2010.
  ista: Chatterjee K, Doyen L, Henzinger TA. 2010. Expressiveness and closure properties
    for quantitative languages. Logical Methods in Computer Science. 6(3), 1–23.
  mla: Chatterjee, Krishnendu, et al. “Expressiveness and Closure Properties for Quantitative
    Languages.” <i>Logical Methods in Computer Science</i>, vol. 6, no. 3, International
    Federation for Computational Logic, 2010, pp. 1–23, doi:<a href="https://doi.org/10.2168/LMCS-6(3:10)2010">10.2168/LMCS-6(3:10)2010</a>.
  short: K. Chatterjee, L. Doyen, T.A. Henzinger, Logical Methods in Computer Science
    6 (2010) 1–23.
corr_author: '1'
das_tickbox: '1'
date_created: 2018-12-11T12:05:36Z
date_published: 2010-08-30T00:00:00Z
date_updated: 2026-07-06T13:24:40Z
day: '30'
ddc:
- '000'
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.2168/LMCS-6(3:10)2010
ec_funded: 1
external_id:
  isi:
  - '000282653500010'
file:
- access_level: open_access
  checksum: 0243da726476817f2ea33b48b78be696
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:17:54Z
  date_updated: 2020-07-14T12:46:19Z
  file_id: '5312'
  file_name: IST-2012-55-v1+1_Expressiveness_Closure_Properties_Quantitative_Languages.pdf
  file_size: 216598
  relation: main_file
- access_level: open_access
  checksum: 5e512b8503a9cb263de26331c4ee9cf2
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:17:55Z
  date_updated: 2020-07-14T12:46:19Z
  file_id: '5313'
  file_name: IST-2016-55-v2+1_1007.4018.pdf
  file_size: 302416
  relation: main_file
file_date_updated: 2020-07-14T12:46:19Z
has_accepted_license: '1'
intvolume: '         6'
isi: 1
issue: '3'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '08'
oa: 1
oa_version: Published Version
page: 1 - 23
project:
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '214373'
  name: Design for Embedded Systems
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '215543'
  name: COMponent-Based Embedded Systems design Techniques
publication: Logical Methods in Computer Science
publication_status: published
publisher: International Federation for Computational Logic
publist_id: '2311'
pubrep_id: '504'
quality_controlled: '1'
related_material:
  record:
  - id: '4540'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Expressiveness and closure properties for quantitative languages
tmp:
  image: /image/cc_by_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
  name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
  short: CC BY-ND (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6
year: '2010'
...
---
_id: '5393'
abstract:
- lang: eng
  text: Gist is a tool that (a) solves the qualitative analysis problem of turn-based
    probabilistic games with ω-regular objectives; and (b) synthesizes reasonable
    environment assumptions for synthesis of unrealizable specifications. Our tool
    provides efficient implementations of several reduction based techniques to solve
    turn-based probabilistic games, and uses the analysis of turn-based probabilistic
    games for synthesizing environment assumptions for unrealizable specifications.
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- 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: Barbara
  full_name: Jobstmann, Barbara
  last_name: Jobstmann
- first_name: Arjun
  full_name: Radhakrishna, Arjun
  id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
  last_name: Radhakrishna
citation:
  ama: 'Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. <i>Gist: A Solver
    for Probabilistic Games</i>. IST Austria; 2009. doi:<a href="https://doi.org/10.15479/AT:IST-2009-0003">10.15479/AT:IST-2009-0003</a>'
  apa: 'Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Radhakrishna, A. (2009).
    <i>Gist: A solver for probabilistic games</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2009-0003">https://doi.org/10.15479/AT:IST-2009-0003</a>'
  chicago: 'Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Arjun
    Radhakrishna. <i>Gist: A Solver for Probabilistic Games</i>. IST Austria, 2009.
    <a href="https://doi.org/10.15479/AT:IST-2009-0003">https://doi.org/10.15479/AT:IST-2009-0003</a>.'
  ieee: 'K. Chatterjee, T. A. Henzinger, B. Jobstmann, and A. Radhakrishna, <i>Gist:
    A solver for probabilistic games</i>. IST Austria, 2009.'
  ista: 'Chatterjee K, Henzinger TA, Jobstmann B, Radhakrishna A. 2009. Gist: A solver
    for probabilistic games, IST Austria, 12p.'
  mla: 'Chatterjee, Krishnendu, et al. <i>Gist: A Solver for Probabilistic Games</i>.
    IST Austria, 2009, doi:<a href="https://doi.org/10.15479/AT:IST-2009-0003">10.15479/AT:IST-2009-0003</a>.'
  short: 'K. Chatterjee, T.A. Henzinger, B. Jobstmann, A. Radhakrishna, Gist: A Solver
    for Probabilistic Games, IST Austria, 2009.'
corr_author: '1'
date_created: 2018-12-12T11:39:05Z
date_published: 2009-10-09T00:00:00Z
date_updated: 2025-04-14T13:37:27Z
day: '09'
ddc:
- '000'
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2009-0003
file:
- access_level: open_access
  checksum: 49551ac552915b17593a14c993845274
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:52:58Z
  date_updated: 2020-07-14T12:46:43Z
  file_id: '5459'
  file_name: IST-2009-0003_IST-2009-0003.pdf
  file_size: 386866
  relation: main_file
file_date_updated: 2020-07-14T12:46:43Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '12'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '29'
related_material:
  record:
  - id: '4388'
    relation: later_version
    status: public
status: public
title: 'Gist: A solver for probabilistic games'
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2009'
...
---
_id: '5394'
abstract:
- lang: eng
  text: We consider two-player games played on graphs with request-response and finitary
    Streett objectives. We show these games are PSPACE-hard, improving the previous
    known NP-hardness. We also improve the lower bounds on memory required by the
    winning strategies for the players.
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- 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: Florian
  full_name: Horn, Florian
  id: 37327ACE-F248-11E8-B48F-1D18A9856A87
  last_name: Horn
citation:
  ama: Chatterjee K, Henzinger TA, Horn F. <i>Improved Lower Bounds for Request-Response
    and Finitary Streett Games</i>. IST Austria; 2009. doi:<a href="https://doi.org/10.15479/AT:IST-2009-0002">10.15479/AT:IST-2009-0002</a>
  apa: Chatterjee, K., Henzinger, T. A., &#38; Horn, F. (2009). <i>Improved lower
    bounds for request-response and finitary Streett games</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2009-0002">https://doi.org/10.15479/AT:IST-2009-0002</a>
  chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Florian Horn. <i>Improved
    Lower Bounds for Request-Response and Finitary Streett Games</i>. IST Austria,
    2009. <a href="https://doi.org/10.15479/AT:IST-2009-0002">https://doi.org/10.15479/AT:IST-2009-0002</a>.
  ieee: K. Chatterjee, T. A. Henzinger, and F. Horn, <i>Improved lower bounds for
    request-response and finitary Streett games</i>. IST Austria, 2009.
  ista: Chatterjee K, Henzinger TA, Horn F. 2009. Improved lower bounds for request-response
    and finitary Streett games, IST Austria, 11p.
  mla: Chatterjee, Krishnendu, et al. <i>Improved Lower Bounds for Request-Response
    and Finitary Streett Games</i>. IST Austria, 2009, doi:<a href="https://doi.org/10.15479/AT:IST-2009-0002">10.15479/AT:IST-2009-0002</a>.
  short: K. Chatterjee, T.A. Henzinger, F. Horn, Improved Lower Bounds for Request-Response
    and Finitary Streett Games, IST Austria, 2009.
corr_author: '1'
date_created: 2018-12-12T11:39:05Z
date_published: 2009-09-09T00:00:00Z
date_updated: 2024-10-09T21:08:23Z
day: '09'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2009-0002
file:
- access_level: open_access
  checksum: 1c50a9723fbae1b2c46d18138968efb3
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:50Z
  date_updated: 2020-07-14T12:46:43Z
  file_id: '5511'
  file_name: IST-2009-0002_IST-2009-0002.pdf
  file_size: 238091
  relation: main_file
file_date_updated: 2020-07-14T12:46:43Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '11'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '30'
status: public
title: Improved lower bounds for request-response and finitary Streett games
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2009'
...
---
_id: '5395'
abstract:
- lang: eng
  text: 'We study observation-based strategies for partially-observable Markov decision
    processes (POMDPs) with omega-regular objectives. An observation-based strategy
    relies on partial information about the history of a play, namely, on the past
    sequence of observa- tions. We consider the qualitative analysis problem: given
    a POMDP with an omega-regular objective, whether there is an observation-based
    strategy to achieve the objective with probability 1 (almost-sure winning), or
    with positive probability (positive winning). Our main results are twofold. First,
    we present a complete picture of the computational complexity of the qualitative
    analysis of POMDPs with parity objectives (a canonical form to express omega-regular
    objectives) and its subclasses. Our contribution consists in establishing several
    upper and lower bounds that were not known in literature. Second, we present optimal
    bounds (matching upper and lower bounds) on the memory required by pure and randomized
    observation-based strategies for the qualitative analysis of POMDPs with parity
    objectives and its subclasses.'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- 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: Chatterjee K, Doyen L, Henzinger TA. <i>Qualitative Analysis of Partially-Observable
    Markov Decision Processes</i>. IST Austria; 2009. doi:<a href="https://doi.org/10.15479/AT:IST-2009-0001">10.15479/AT:IST-2009-0001</a>
  apa: Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2009). <i>Qualitative analysis
    of partially-observable Markov decision processes</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2009-0001">https://doi.org/10.15479/AT:IST-2009-0001</a>
  chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. <i>Qualitative
    Analysis of Partially-Observable Markov Decision Processes</i>. IST Austria, 2009.
    <a href="https://doi.org/10.15479/AT:IST-2009-0001">https://doi.org/10.15479/AT:IST-2009-0001</a>.
  ieee: K. Chatterjee, L. Doyen, and T. A. Henzinger, <i>Qualitative analysis of partially-observable
    Markov decision processes</i>. IST Austria, 2009.
  ista: Chatterjee K, Doyen L, Henzinger TA. 2009. Qualitative analysis of partially-observable
    Markov decision processes, IST Austria, 20p.
  mla: Chatterjee, Krishnendu, et al. <i>Qualitative Analysis of Partially-Observable
    Markov Decision Processes</i>. IST Austria, 2009, doi:<a href="https://doi.org/10.15479/AT:IST-2009-0001">10.15479/AT:IST-2009-0001</a>.
  short: K. Chatterjee, L. Doyen, T.A. Henzinger, Qualitative Analysis of Partially-Observable
    Markov Decision Processes, IST Austria, 2009.
corr_author: '1'
date_created: 2018-12-12T11:39:05Z
date_published: 2009-09-09T00:00:00Z
date_updated: 2025-04-14T13:37:25Z
day: '09'
ddc:
- '005'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:IST-2009-0001
file:
- access_level: open_access
  checksum: 04d9cc065cc19598a4e8631c47f1a562
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:25Z
  date_updated: 2020-07-14T12:46:43Z
  file_id: '5486'
  file_name: IST-2009-0001_IST-2009-0001.pdf
  file_size: 342088
  relation: main_file
file_date_updated: 2020-07-14T12:46:43Z
has_accepted_license: '1'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
page: '20'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '31'
related_material:
  record:
  - id: '3855'
    relation: later_version
    status: public
status: public
title: Qualitative analysis of partially-observable Markov decision processes
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2009'
...
---
_id: '3837'
abstract:
- lang: eng
  text: In this paper we extend the work of Alfaro, Henzinger et al. on interface
    theories for component-based design. Existing interface theories often fail to
    capture functional relations between the inputs and outputs of an interface. For
    example, a simple synchronous interface that takes as input a number n ≥ 0 and
    returns, at the same time, as output n + 1, cannot be expressed in existing theories.
    In this paper we provide a theory of relational interfaces, where such input-output
    relations can be captured. Our theory supports synchronous interfaces, both stateless
    and stateful. It includes explicit notions of environments and pluggability, and
    satisfies fundamental properties such as preservation of refinement by composition,
    and characterization of pluggability by refinement. We achieve these properties
    by making reasonable restrictions on feedback loops in interface compositions.
acknowledgement: 'This work is supported by the Center for Hybrid and Embedded Software
  Systems (CHESS) at UC Berkeley, which receives support from the National Science
  Foundation (NSF awards #0720882 (CSR-EHS: PRET) and #0720841 (CSR-CPS)), the U.S.
  Army Research Office (ARO #W911NF-07-2-0019), the U.S. Air Force Office of Scientific
  Research (MURI #FA9550-06-0312), the Air Force Research Lab (AFRL), the State of
  California Micro Program, and the following companies: Agilent, Bosch, Lockheed-Martin,
  National Instruments, Thales and Toyota. This work is also supported by the COMBEST
  and ArtistDesign projects of the European Union, and the Swiss National Science
  Foundation. '
author:
- first_name: Stavros
  full_name: Tripakis, Stavros
  last_name: Tripakis
- first_name: Ben
  full_name: Lickly, Ben
  last_name: Lickly
- 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: Edward
  full_name: Lee, Edward
  last_name: Lee
citation:
  ama: 'Tripakis S, Lickly B, Henzinger TA, Lee E. On relational interfaces. In: <i>EMSOFT
    ’09 Proceedings of the Seventh ACM International Conference on Embedded Software</i>.
    ACM; 2009:67-76. doi:<a href="https://doi.org/10.1145/1629335.1629346">10.1145/1629335.1629346</a>'
  apa: 'Tripakis, S., Lickly, B., Henzinger, T. A., &#38; Lee, E. (2009). On relational
    interfaces. In <i>EMSOFT ’09 Proceedings of the seventh ACM international conference
    on Embedded software</i> (pp. 67–76). Grenoble, France: ACM. <a href="https://doi.org/10.1145/1629335.1629346">https://doi.org/10.1145/1629335.1629346</a>'
  chicago: Tripakis, Stavros, Ben Lickly, Thomas A Henzinger, and Edward Lee. “On
    Relational Interfaces.” In <i>EMSOFT ’09 Proceedings of the Seventh ACM International
    Conference on Embedded Software</i>, 67–76. ACM, 2009. <a href="https://doi.org/10.1145/1629335.1629346">https://doi.org/10.1145/1629335.1629346</a>.
  ieee: S. Tripakis, B. Lickly, T. A. Henzinger, and E. Lee, “On relational interfaces,”
    in <i>EMSOFT ’09 Proceedings of the seventh ACM international conference on Embedded
    software</i>, Grenoble, France, 2009, pp. 67–76.
  ista: 'Tripakis S, Lickly B, Henzinger TA, Lee E. 2009. On relational interfaces.
    EMSOFT ’09 Proceedings of the seventh ACM international conference on Embedded
    software. EMSOFT: Embedded Software , 67–76.'
  mla: Tripakis, Stavros, et al. “On Relational Interfaces.” <i>EMSOFT ’09 Proceedings
    of the Seventh ACM International Conference on Embedded Software</i>, ACM, 2009,
    pp. 67–76, doi:<a href="https://doi.org/10.1145/1629335.1629346">10.1145/1629335.1629346</a>.
  short: S. Tripakis, B. Lickly, T.A. Henzinger, E. Lee, in:, EMSOFT ’09 Proceedings
    of the Seventh ACM International Conference on Embedded Software, ACM, 2009, pp.
    67–76.
conference:
  end_date: 2009-10-16
  location: Grenoble, France
  name: 'EMSOFT: Embedded Software '
  start_date: 2009-10-12
date_created: 2018-12-11T12:05:26Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2024-10-21T06:03:06Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.1145/1629335.1629346
ec_funded: 1
file:
- access_level: open_access
  checksum: 3a70e21527dfaad2f198549ae5710786
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:13:57Z
  date_updated: 2020-07-14T12:46:16Z
  file_id: '5045'
  file_name: IST-2012-70-v1+1_On_Relational_Interfaces.pdf
  file_size: 310902
  relation: main_file
file_date_updated: 2020-07-14T12:46:16Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 67 - 76
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '215543'
  name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '214373'
  name: Design for Embedded Systems
publication: EMSOFT '09 Proceedings of the seventh ACM international conference on
  Embedded software
publication_status: published
publisher: ACM
publist_id: '2360'
pubrep_id: '70'
quality_controlled: '1'
scopus_import: '1'
status: public
title: On relational interfaces
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2009'
...
---
_id: '3841'
abstract:
- lang: eng
  text: 'We compare several languages for specifying Markovian population models such
    as queuing networks and chemical reaction networks. These languages —matrix descriptions,
    stochastic Petri nets, stoichiometric equations, stochastic process algebras,
    and guarded command models— all describe continuous-time Markov chains, but they
    differ according to important properties, such as compositionality, expressiveness
    and succinctness, executability, ease of use, and the support they provide for
    checking the well-formedness of a model and for analyzing a model. '
acknowledgement: This research was supported in part by the Excellence Cluster on
  Multimodal Computing and Interaction and the Swiss National Science Foundation.
alternative_title:
- LNCS
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: Barbara
  full_name: Jobstmann, Barbara
  last_name: Jobstmann
- first_name: Verena
  full_name: Wolf, Verena
  last_name: Wolf
citation:
  ama: 'Henzinger TA, Jobstmann B, Wolf V. Formalisms for specifying Markovian population
    models. In: Vol 5797. Springer; 2009:3-23. doi:<a href="https://doi.org/10.1007/978-3-642-04420-5_2">10.1007/978-3-642-04420-5_2</a>'
  apa: 'Henzinger, T. A., Jobstmann, B., &#38; Wolf, V. (2009). Formalisms for specifying
    Markovian population models (Vol. 5797, pp. 3–23). Presented at the RP: Reachability
    Problems, Palaiseau, France: Springer. <a href="https://doi.org/10.1007/978-3-642-04420-5_2">https://doi.org/10.1007/978-3-642-04420-5_2</a>'
  chicago: Henzinger, Thomas A, Barbara Jobstmann, and Verena Wolf. “Formalisms for
    Specifying Markovian Population Models,” 5797:3–23. Springer, 2009. <a href="https://doi.org/10.1007/978-3-642-04420-5_2">https://doi.org/10.1007/978-3-642-04420-5_2</a>.
  ieee: 'T. A. Henzinger, B. Jobstmann, and V. Wolf, “Formalisms for specifying Markovian
    population models,” presented at the RP: Reachability Problems, Palaiseau, France,
    2009, vol. 5797, pp. 3–23.'
  ista: 'Henzinger TA, Jobstmann B, Wolf V. 2009. Formalisms for specifying Markovian
    population models. RP: Reachability Problems, LNCS, vol. 5797, 3–23.'
  mla: Henzinger, Thomas A., et al. <i>Formalisms for Specifying Markovian Population
    Models</i>. Vol. 5797, Springer, 2009, pp. 3–23, doi:<a href="https://doi.org/10.1007/978-3-642-04420-5_2">10.1007/978-3-642-04420-5_2</a>.
  short: T.A. Henzinger, B. Jobstmann, V. Wolf, in:, Springer, 2009, pp. 3–23.
conference:
  end_date: 2009-09-25
  location: Palaiseau, France
  name: 'RP: Reachability Problems'
  start_date: 2009-09-23
date_created: 2018-12-11T12:05:28Z
date_published: 2009-09-07T00:00:00Z
date_updated: 2025-09-30T08:49:00Z
day: '07'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-642-04420-5_2
file:
- access_level: open_access
  checksum: df88431872586c773fbcfea37d7b36a2
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:08:41Z
  date_updated: 2020-07-14T12:46:16Z
  file_id: '4702'
  file_name: IST-2012-67-v1+1_Formalisms_for_specifying_Markovian_population_models.pdf
  file_size: 222840
  relation: main_file
file_date_updated: 2020-07-14T12:46:16Z
has_accepted_license: '1'
intvolume: '      5797'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 3 - 23
publication_status: published
publisher: Springer
publist_id: '2352'
pubrep_id: '67'
quality_controlled: '1'
related_material:
  record:
  - id: '3381'
    relation: later_version
    status: public
scopus_import: 1
status: public
title: Formalisms for specifying Markovian population models
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5797
year: '2009'
...
---
_id: '3843'
abstract:
- lang: eng
  text: "Within systems biology there is an increasing interest in the stochastic
    behavior of biochemical reaction networks. An appropriate stochastic description
    is provided by the chemical master equation, which represents a continuous- time
    Markov chain (CTMC).\r\nStandard Uniformization (SU) is an efficient method for
    the transient analysis of CTMCs. For systems with very different time scales,
    such as biochemical reaction networks, SU is computationally expensive. In these
    cases, a variant of SU, called adaptive uniformization (AU), is known to reduce
    the large number of iterations needed by SU. The additional difficulty of AU is
    that it requires the solution of a birth process.\r\nIn this paper we present
    an on-the-fly variant of AU, where we improve the original algorithm for AU at
    the cost of a small approximation error. By means of several examples, we show
    that our approach is particularly well-suited for biochemical reaction networks."
acknowledgement: This research has been partially funded by the Swiss National Science
  Foundation under grant 205321-111840 and by the Cluster of Excellence on Multimodal
  Computing and Interaction at Saarland University.
article_processing_charge: No
author:
- first_name: Frédéric
  full_name: Didier, Frédéric
  last_name: Didier
- 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: Maria
  full_name: Mateescu, Maria
  id: 3B43276C-F248-11E8-B48F-1D18A9856A87
  last_name: Mateescu
- first_name: Verena
  full_name: Wolf, Verena
  last_name: Wolf
citation:
  ama: 'Didier F, Henzinger TA, Mateescu M, Wolf V. Fast adaptive uniformization of
    the chemical master equation. In: Vol 4. IEEE; 2009:118-127. doi:<a href="https://doi.org/10.1109/HiBi.2009.23">10.1109/HiBi.2009.23</a>'
  apa: 'Didier, F., Henzinger, T. A., Mateescu, M., &#38; Wolf, V. (2009). Fast adaptive
    uniformization of the chemical master equation (Vol. 4, pp. 118–127). Presented
    at the HIBI: High-Performance Computational Systems Biology, Trento, Italy: IEEE.
    <a href="https://doi.org/10.1109/HiBi.2009.23">https://doi.org/10.1109/HiBi.2009.23</a>'
  chicago: Didier, Frédéric, Thomas A Henzinger, Maria Mateescu, and Verena Wolf.
    “Fast Adaptive Uniformization of the Chemical Master Equation,” 4:118–27. IEEE,
    2009. <a href="https://doi.org/10.1109/HiBi.2009.23">https://doi.org/10.1109/HiBi.2009.23</a>.
  ieee: 'F. Didier, T. A. Henzinger, M. Mateescu, and V. Wolf, “Fast adaptive uniformization
    of the chemical master equation,” presented at the HIBI: High-Performance Computational
    Systems Biology, Trento, Italy, 2009, vol. 4, no. 6, pp. 118–127.'
  ista: 'Didier F, Henzinger TA, Mateescu M, Wolf V. 2009. Fast adaptive uniformization
    of the chemical master equation. HIBI: High-Performance Computational Systems
    Biology vol. 4, 118–127.'
  mla: Didier, Frédéric, et al. <i>Fast Adaptive Uniformization of the Chemical Master
    Equation</i>. Vol. 4, no. 6, IEEE, 2009, pp. 118–27, doi:<a href="https://doi.org/10.1109/HiBi.2009.23">10.1109/HiBi.2009.23</a>.
  short: F. Didier, T.A. Henzinger, M. Mateescu, V. Wolf, in:, IEEE, 2009, pp. 118–127.
conference:
  end_date: 2009-10-16
  location: Trento, Italy
  name: 'HIBI: High-Performance Computational Systems Biology'
  start_date: 2009-10-14
date_created: 2018-12-11T12:05:28Z
date_published: 2009-10-30T00:00:00Z
date_updated: 2025-09-30T09:54:51Z
day: '30'
ddc:
- '000'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1109/HiBi.2009.23
external_id:
  isi:
  - '000275038300017'
file:
- access_level: open_access
  checksum: 9a3bde48f43203991a0b3c6a277c2f5b
  content_type: application/pdf
  creator: dernst
  date_created: 2020-05-19T16:33:55Z
  date_updated: 2020-07-14T12:46:17Z
  file_id: '7874'
  file_name: 2009_HIBI_Didier.pdf
  file_size: 222890
  relation: main_file
file_date_updated: 2020-07-14T12:46:17Z
has_accepted_license: '1'
intvolume: '         4'
isi: 1
issue: '6'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Submitted Version
page: 118 - 127
publication_status: published
publisher: IEEE
publist_id: '2348'
quality_controlled: '1'
related_material:
  record:
  - id: '3842'
    relation: later_version
    status: public
scopus_import: '1'
status: public
title: Fast adaptive uniformization of the chemical master equation
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 4
year: '2009'
...
---
_id: '3844'
abstract:
- lang: eng
  text: The Hierarchical Timing Language (HTL) is a real-time coordination language
    for distributed control systems. HTL programs must be checked for well-formedness,
    race freedom, transmission safety (schedulability of inter-host communication),
    and time safety (schedulability of host computation). We present a modular abstract
    syntax and semantics for HTL, modular checks of well-formedness, race freedom,
    and transmission safety, and modular code distribution. Our contributions here
    complement previous results on HTL time safety and modular code generation. Modularity
    in HTL can be utilized in easy program composition as well as fast program analysis
    and code generation, but also in so-called runtime patching, where program components
    may be modified at runtime.
acknowledgement: Supported by the EU ArtistDesign Network of Excellence on Embedded
  Systems Design, the EU project COMBEST, the Austrian Science Funds P18913-N15 and
  V00125, and Fundacao para a Ciencia e Tecnologia funds SFRH/BD/29461/2006 and PTDC/EIA/71462/2006
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: Christoph
  full_name: Kirsch, Christoph
  last_name: Kirsch
- first_name: Eduardo
  full_name: Marques, Eduardo
  last_name: Marques
- first_name: Ana
  full_name: Sokolova, Ana
  last_name: Sokolova
citation:
  ama: 'Henzinger TA, Kirsch C, Marques E, Sokolova A. Distributed, modular HTL. In:
    IEEE; 2009:171-180. doi:<a href="https://doi.org/10.1109/RTSS.2009.9">10.1109/RTSS.2009.9</a>'
  apa: 'Henzinger, T. A., Kirsch, C., Marques, E., &#38; Sokolova, A. (2009). Distributed,
    modular HTL (pp. 171–180). Presented at the RTSS: Real-Time Systems Symposium,
    Washington, DC, United States: IEEE. <a href="https://doi.org/10.1109/RTSS.2009.9">https://doi.org/10.1109/RTSS.2009.9</a>'
  chicago: Henzinger, Thomas A, Christoph Kirsch, Eduardo Marques, and Ana Sokolova.
    “Distributed, Modular HTL,” 171–80. IEEE, 2009. <a href="https://doi.org/10.1109/RTSS.2009.9">https://doi.org/10.1109/RTSS.2009.9</a>.
  ieee: 'T. A. Henzinger, C. Kirsch, E. Marques, and A. Sokolova, “Distributed, modular
    HTL,” presented at the RTSS: Real-Time Systems Symposium, Washington, DC, United
    States, 2009, pp. 171–180.'
  ista: 'Henzinger TA, Kirsch C, Marques E, Sokolova A. 2009. Distributed, modular
    HTL. RTSS: Real-Time Systems Symposium, 171–180.'
  mla: Henzinger, Thomas A., et al. <i>Distributed, Modular HTL</i>. IEEE, 2009, pp.
    171–80, doi:<a href="https://doi.org/10.1109/RTSS.2009.9">10.1109/RTSS.2009.9</a>.
  short: T.A. Henzinger, C. Kirsch, E. Marques, A. Sokolova, in:, IEEE, 2009, pp.
    171–180.
conference:
  end_date: 2009-12-04
  location: Washington, DC, United States
  name: 'RTSS: Real-Time Systems Symposium'
  start_date: 2009-12-01
date_created: 2018-12-11T12:05:28Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2025-09-30T09:54:22Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1109/RTSS.2009.9
ec_funded: 1
external_id:
  isi:
  - '000277465500016'
file:
- access_level: open_access
  checksum: b2b15a5ef71eb50d62eaa5aea7efd8c4
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:07:56Z
  date_updated: 2020-07-14T12:46:17Z
  file_id: '4655'
  file_name: IST-2012-65-v1+1_Distributed_modular_Htl.pdf
  file_size: 526458
  relation: main_file
file_date_updated: 2020-07-14T12:46:17Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 171 - 180
project:
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '214373'
  name: Design for Embedded Systems
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '215543'
  name: COMponent-Based Embedded Systems design Techniques
publication_status: published
publisher: IEEE
publist_id: '2346'
pubrep_id: '65'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Distributed, modular HTL
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2009'
...