---
_id: '467'
abstract:
- lang: eng
  text: Recently there has been a significant effort to handle quantitative properties
    in formal verification and synthesis. While weighted automata over finite and
    infinite words provide a natural and flexible framework to express quantitative
    properties, perhaps surprisingly, some basic system properties such as average
    response time cannot be expressed using weighted automata or in any other known
    decidable formalism. In this work, we introduce nested weighted automata as a
    natural extension of weighted automata, which makes it possible to express important
    quantitative properties such as average response time. In nested weighted automata,
    a master automaton spins off and collects results from weighted slave automata,
    each of which computes a quantity along a finite portion of an infinite word.
    Nested weighted automata can be viewed as the quantitative analogue of monitor
    automata, which are used in runtime verification. We establish an almost-complete
    decidability picture for the basic decision problems about nested weighted automata
    and illustrate their applicability in several domains. In particular, nested weighted
    automata can be used to decide average response time properties.
article_number: '31'
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: Jan
  full_name: Otop, Jan
  id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
  last_name: Otop
citation:
  ama: Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. <i>ACM Transactions
    on Computational Logic (TOCL)</i>. 2017;18(4). doi:<a href="https://doi.org/10.1145/3152769">10.1145/3152769</a>
  apa: Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Nested weighted automata.
    <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href="https://doi.org/10.1145/3152769">https://doi.org/10.1145/3152769</a>
  chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted
    Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a
    href="https://doi.org/10.1145/3152769">https://doi.org/10.1145/3152769</a>.
  ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” <i>ACM
    Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4. ACM, 2017.
  ista: Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions
    on Computational Logic (TOCL). 18(4), 31.
  mla: Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>ACM Transactions
    on Computational Logic (TOCL)</i>, vol. 18, no. 4, 31, ACM, 2017, doi:<a href="https://doi.org/10.1145/3152769">10.1145/3152769</a>.
  short: K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational
    Logic (TOCL) 18 (2017).
date_created: 2018-12-11T11:46:38Z
date_published: 2017-12-01T00:00:00Z
date_updated: 2023-02-23T12:26:19Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/3152769
ec_funded: 1
external_id:
  arxiv:
  - '1606.03598'
intvolume: '        18'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1606.03598
month: '12'
oa: 1
oa_version: Preprint
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: ACM Transactions on Computational Logic (TOCL)
publication_identifier:
  issn:
  - '15293785'
publication_status: published
publisher: ACM
publist_id: '7354'
quality_controlled: '1'
related_material:
  record:
  - id: '1656'
    relation: earlier_version
    status: public
  - id: '5415'
    relation: earlier_version
    status: public
  - id: '5436'
    relation: earlier_version
    status: public
scopus_import: 1
status: public
title: Nested weighted automata
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2017'
...
---
_id: '471'
abstract:
- lang: eng
  text: 'We present a new algorithm for the statistical model checking of Markov chains
    with respect to unbounded temporal properties, including full linear temporal
    logic. The main idea is that we monitor each simulation run on the fly, in order
    to detect quickly if a bottom strongly connected component is entered with high
    probability, in which case the simulation run can be terminated early. As a result,
    our simulation runs are often much shorter than required by termination bounds
    that are computed a priori for a desired level of confidence on a large state
    space. In comparison to previous algorithms for statistical model checking our
    method is not only faster in many cases but also requires less information about
    the system, namely, only the minimum transition probability that occurs in the
    Markov chain. In addition, our method can be generalised to unbounded quantitative
    properties such as mean-payoff bounds. '
article_number: '12'
author:
- first_name: Przemyslaw
  full_name: Daca, Przemyslaw
  id: 49351290-F248-11E8-B48F-1D18A9856A87
  last_name: Daca
- 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: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
- first_name: Tatjana
  full_name: Petrov, Tatjana
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
citation:
  ama: Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking
    for unbounded temporal properties. <i>ACM Transactions on Computational Logic
    (TOCL)</i>. 2017;18(2). doi:<a href="https://doi.org/10.1145/3060139">10.1145/3060139</a>
  apa: Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Petrov, T. (2017). Faster
    statistical model checking for unbounded temporal properties. <i>ACM Transactions
    on Computational Logic (TOCL)</i>. ACM. <a href="https://doi.org/10.1145/3060139">https://doi.org/10.1145/3060139</a>
  chicago: Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov.
    “Faster Statistical Model Checking for Unbounded Temporal Properties.” <i>ACM
    Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a href="https://doi.org/10.1145/3060139">https://doi.org/10.1145/3060139</a>.
  ieee: P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Faster statistical
    model checking for unbounded temporal properties,” <i>ACM Transactions on Computational
    Logic (TOCL)</i>, vol. 18, no. 2. ACM, 2017.
  ista: Daca P, Henzinger TA, Kretinsky J, Petrov T. 2017. Faster statistical model
    checking for unbounded temporal properties. ACM Transactions on Computational
    Logic (TOCL). 18(2), 12.
  mla: Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal
    Properties.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no.
    2, 12, ACM, 2017, doi:<a href="https://doi.org/10.1145/3060139">10.1145/3060139</a>.
  short: P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational
    Logic (TOCL) 18 (2017).
date_created: 2018-12-11T11:46:39Z
date_published: 2017-05-01T00:00:00Z
date_updated: 2023-02-21T16:48:11Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/3060139
ec_funded: 1
intvolume: '        18'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1504.05739
month: '05'
oa: 1
oa_version: Submitted Version
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication: ACM Transactions on Computational Logic (TOCL)
publication_identifier:
  issn:
  - '15293785'
publication_status: published
publisher: ACM
publist_id: '7349'
quality_controlled: '1'
related_material:
  record:
  - id: '1234'
    relation: earlier_version
    status: public
scopus_import: 1
status: public
title: Faster statistical model checking for unbounded temporal properties
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2017'
...