---
_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.
date_created: 2018-12-12T11:39:05Z
date_published: 2009-09-09T00:00:00Z
date_updated: 2023-02-23T11:45:39Z
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: 2021-01-12T07:52:33Z
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'
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: 2023-02-23T11:24:49Z
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: 2023-02-23T11:45:05Z
day: '30'
ddc:
- '000'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1109/HiBi.2009.23
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'
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
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
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: 2021-01-12T07:52:36Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1109/RTSS.2009.9
ec_funded: 1
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'
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'
status: public
title: Distributed, modular HTL
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2009'
...