---
_id: '1594'
abstract:
- lang: eng
  text: Quantitative extensions of temporal logics have recently attracted significant
    attention. In this work, we study frequency LTL (fLTL), an extension of LTL which
    allows to speak about frequencies of events along an execution. Such an extension
    is particularly useful for probabilistic systems that often cannot fulfil strict
    qualitative guarantees on the behaviour. It has been recently shown that controller
    synthesis for Markov decision processes and fLTL is decidable when all the bounds
    on frequencies are 1. As a step towards a complete quantitative solution, we show
    that the problem is decidable for the fragment fLTL\GU, where U does not occur
    in the scope of G (but still F can). Our solution is based on a novel translation
    of such quantitative formulae into equivalent deterministic automata.
acknowledgement: "This work is partly supported by the German Research Council (DFG)
  as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by
  the Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework
  Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the
  CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative
  Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie
  Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013)
  REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE),
  and by the ERC Start Grant (279307: Graph Games).\r\n"
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Vojtěch
  full_name: Forejt, Vojtěch
  last_name: Forejt
- first_name: Jan
  full_name: Krčál, Jan
  last_name: Krčál
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
citation:
  ama: 'Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency
    LTL\GU. In: Vol 9450. Springer; 2015:162-177. doi:<a href="https://doi.org/10.1007/978-3-662-48899-7_12">10.1007/978-3-662-48899-7_12</a>'
  apa: 'Forejt, V., Krčál, J., &#38; Kretinsky, J. (2015). Controller synthesis for
    MDPs and frequency LTL\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic
    for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer.
    <a href="https://doi.org/10.1007/978-3-662-48899-7_12">https://doi.org/10.1007/978-3-662-48899-7_12</a>'
  chicago: Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for
    MDPs and Frequency LTL\GU,” 9450:162–77. Springer, 2015. <a href="https://doi.org/10.1007/978-3-662-48899-7_12">https://doi.org/10.1007/978-3-662-48899-7_12</a>.
  ieee: 'V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and
    frequency LTL\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence,
    and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177.'
  ista: 'Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency
    LTL\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS,
    vol. 9450, 162–177.'
  mla: Forejt, Vojtěch, et al. <i>Controller Synthesis for MDPs and Frequency LTL\GU</i>.
    Vol. 9450, Springer, 2015, pp. 162–77, doi:<a href="https://doi.org/10.1007/978-3-662-48899-7_12">10.1007/978-3-662-48899-7_12</a>.
  short: V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.
conference:
  end_date: 2015-11-28
  location: Suva, Fiji
  name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
  start_date: 2015-11-24
date_created: 2018-12-11T11:52:55Z
date_published: 2015-11-22T00:00:00Z
date_updated: 2025-09-23T08:21:59Z
day: '22'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-662-48899-7_12
ec_funded: 1
external_id:
  isi:
  - '000375574900012'
intvolume: '      9450'
isi: 1
language:
- iso: eng
month: '11'
oa_version: None
page: 162 - 177
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication_status: published
publisher: Springer
publist_id: '5577'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Controller synthesis for MDPs and frequency LTL\GU
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9450
year: '2015'
...