---
_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'
article_processing_charge: No
arxiv: 1
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</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</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</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</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. 18(2), 12.
  mla: Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal
    Properties.” <i>ACM Transactions on Computational Logic</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 18 (2017).
corr_author: '1'
date_created: 2018-12-11T11:46:39Z
date_published: 2017-05-01T00:00:00Z
date_updated: 2025-09-22T09:21:16Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/3060139
ec_funded: 1
external_id:
  arxiv:
  - '1504.05739'
  isi:
  - '000405208400005'
fulldoi: https://doi.org/10.1145/3060139
intvolume: '        18'
isi: 1
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: Formal methods for the design and analysis of complex systems
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication: ACM Transactions on Computational Logic
publication_identifier:
  issn:
  - 1529-3785
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 18
year: '2017'
...
---
_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'
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: 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</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</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</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</i>, vol. 18, no. 4. ACM, 2017.
  ista: Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions
    on Computational Logic. 18(4), 31.
  mla: Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>ACM Transactions
    on Computational Logic</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 18 (2017).
corr_author: '1'
das_tickbox: '1'
date_created: 2018-12-11T11:46:38Z
date_published: 2017-12-01T00:00:00Z
date_updated: 2026-07-07T14:01:10Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/3152769
ec_funded: 1
external_id:
  arxiv:
  - '1606.03598'
  isi:
  - '000419237100006'
fulldoi: https://doi.org/10.1145/3152769
intvolume: '        18'
isi: 1
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: Formal methods for the design and analysis of complex systems
- _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
publication_identifier:
  issn:
  - 1529-3785
publication_status: published
publisher: ACM
publist_id: '7354'
quality_controlled: '1'
related_material:
  record:
  - id: '5415'
    relation: earlier_version
    status: public
  - id: '5436'
    relation: earlier_version
    status: public
  - id: '1656'
    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'
...
---
OA_place: repository
OA_type: green
_id: '4454'
abstract:
- lang: eng
  text: We define five increasingly comprehensive classes of infinite-state systems,
    called STS1--STS5, whose state spaces have finitary structure. For four of these
    classes, we provide examples from hybrid systems.STS1 These are the systems with
    finite bisimilarity quotients. They can be analyzed symbolically by iteratively
    applying predecessor and Boolean operations on state sets, starting from a finite
    number of observable state sets. Any such iteration is guaranteed to terminate
    in that only a finite number of state sets can be generated. This enables model
    checking of the μ-calculus.STS2 These are the systems with finite similarity quotients.
    They can be analyzed symbolically by iterating the predecessor and positive Boolean
    operations. This enables model checking of the existential and universal fragments
    of the μ-calculus.STS3 These are the systems with finite trace-equivalence quotients.
    They can be analyzed symbolically by iterating the predecessor operation and a
    restricted form of positive Boolean operations (intersection is restricted to
    intersection with observables). This enables model checking of all ω-regular properties,
    including linear temporal logic.STS4 These are the systems with finite distance-equivalence
    quotients (two states are equivalent if for every distance d, the same observables
    can be reached in d transitions). The systems in this class can be analyzed symbolically
    by iterating the predecessor operation and terminating when no new state sets
    are generated. This enables model checking of the existential conjunction-free
    and universal disjunction-free fragments of the μ-calculus.STS5 These are the
    systems with finite bounded-reachability quotients (two states are equivalent
    if for every distance d, the same observables can be reached in d or fewer transitions).
    The systems in this class can be analyzed symbolically by iterating the predecessor
    operation and terminating when no new states are encountered (this is a weaker
    termination condition than above). This enables model checking of reachability
    properties.
article_processing_charge: No
article_type: original
arxiv: 1
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: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
- first_name: Jean
  full_name: Raskin, Jean
  last_name: Raskin
citation:
  ama: Henzinger TA, Majumdar R, Raskin J. A classification of symbolic transition
    systems. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2005;6(1):1-32.
    doi:<a href="https://doi.org/10.1145/1042038.1042039">10.1145/1042038.1042039</a>
  apa: Henzinger, T. A., Majumdar, R., &#38; Raskin, J. (2005). A classification of
    symbolic transition systems. <i>ACM Transactions on Computational Logic (TOCL)</i>.
    ACM. <a href="https://doi.org/10.1145/1042038.1042039">https://doi.org/10.1145/1042038.1042039</a>
  chicago: Henzinger, Thomas A, Ritankar Majumdar, and Jean Raskin. “A Classification
    of Symbolic Transition Systems.” <i>ACM Transactions on Computational Logic (TOCL)</i>.
    ACM, 2005. <a href="https://doi.org/10.1145/1042038.1042039">https://doi.org/10.1145/1042038.1042039</a>.
  ieee: T. A. Henzinger, R. Majumdar, and J. Raskin, “A classification of symbolic
    transition systems,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol.
    6, no. 1. ACM, pp. 1–32, 2005.
  ista: Henzinger TA, Majumdar R, Raskin J. 2005. A classification of symbolic transition
    systems. ACM Transactions on Computational Logic (TOCL). 6(1), 1–32.
  mla: Henzinger, Thomas A., et al. “A Classification of Symbolic Transition Systems.”
    <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 6, no. 1, ACM, 2005,
    pp. 1–32, doi:<a href="https://doi.org/10.1145/1042038.1042039">10.1145/1042038.1042039</a>.
  short: T.A. Henzinger, R. Majumdar, J. Raskin, ACM Transactions on Computational
    Logic (TOCL) 6 (2005) 1–32.
date_created: 2018-12-11T12:08:56Z
date_published: 2005-01-01T00:00:00Z
date_updated: 2026-10-23T09:08:07Z
day: '01'
doi: 10.1145/1042038.1042039
extern: '1'
external_id:
  arxiv:
  - '0101013'
fulldoi: https://doi.org/10.1145/1042038.1042039
intvolume: '         6'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 1 - 32
publication: ACM Transactions on Computational Logic (TOCL)
publication_identifier:
  eissn:
  - 1557-945X
  issn:
  - 1529-3785
publication_status: published
publisher: ACM
publist_id: '272'
status: public
title: A classification of symbolic transition systems
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 6
year: '2005'
...