---
_id: '81'
abstract:
- lang: eng
  text: We solve the offline monitoring problem for timed propositional temporal logic
    (TPTL), interpreted over dense-time Boolean signals. The variant of TPTL we consider
    extends linear temporal logic (LTL) with clock variables and reset quantifiers,
    providing a mechanism to specify real-time constraints. We first describe a general
    monitoring algorithm based on an exhaustive computation of the set of satisfying
    clock assignments as a finite union of zones. We then propose a specialized monitoring
    algorithm for the one-variable case using a partition of the time domain based
    on the notion of region equivalence, whose complexity is linear in the length
    of the signal, thereby generalizing a known result regarding the monitoring of
    metric temporal logic (MTL). The region and zone representations of time constraints
    are known from timed automata verification and can also be used in the discrete-time
    case. Our prototype implementation appears to outperform previous discrete-time
    implementations of TPTL monitoring,
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Adrian
  full_name: Elgyütt, Adrian
  id: 4A2E9DBA-F248-11E8-B48F-1D18A9856A87
  last_name: Elgyütt
- first_name: Thomas
  full_name: Ferrere, Thomas
  id: 40960E6E-F248-11E8-B48F-1D18A9856A87
  last_name: Ferrere
  orcid: 0000-0001-5199-3143
- 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: 'Elgyütt A, Ferrere T, Henzinger TA. Monitoring temporal logic with clock variables.
    In: Vol 11022. Springer; 2018:53-70. doi:<a href="https://doi.org/10.1007/978-3-030-00151-3_4">10.1007/978-3-030-00151-3_4</a>'
  apa: 'Elgyütt, A., Ferrere, T., &#38; Henzinger, T. A. (2018). Monitoring temporal
    logic with clock variables (Vol. 11022, pp. 53–70). Presented at the FORMATS:
    Formal Modeling and Analysis of Timed Systems, Beijing, China: Springer. <a href="https://doi.org/10.1007/978-3-030-00151-3_4">https://doi.org/10.1007/978-3-030-00151-3_4</a>'
  chicago: Elgyütt, Adrian, Thomas Ferrere, and Thomas A Henzinger. “Monitoring Temporal
    Logic with Clock Variables,” 11022:53–70. Springer, 2018. <a href="https://doi.org/10.1007/978-3-030-00151-3_4">https://doi.org/10.1007/978-3-030-00151-3_4</a>.
  ieee: 'A. Elgyütt, T. Ferrere, and T. A. Henzinger, “Monitoring temporal logic with
    clock variables,” presented at the FORMATS: Formal Modeling and Analysis of Timed
    Systems, Beijing, China, 2018, vol. 11022, pp. 53–70.'
  ista: 'Elgyütt A, Ferrere T, Henzinger TA. 2018. Monitoring temporal logic with
    clock variables. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS,
    vol. 11022, 53–70.'
  mla: Elgyütt, Adrian, et al. <i>Monitoring Temporal Logic with Clock Variables</i>.
    Vol. 11022, Springer, 2018, pp. 53–70, doi:<a href="https://doi.org/10.1007/978-3-030-00151-3_4">10.1007/978-3-030-00151-3_4</a>.
  short: A. Elgyütt, T. Ferrere, T.A. Henzinger, in:, Springer, 2018, pp. 53–70.
conference:
  end_date: 2018-09-06
  location: Beijing, China
  name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
  start_date: 2018-09-04
date_created: 2018-12-11T11:44:31Z
date_published: 2018-08-26T00:00:00Z
date_updated: 2023-09-13T08:58:34Z
day: '26'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-00151-3_4
external_id:
  isi:
  - '000884993200004'
file:
- access_level: open_access
  checksum: e5d81c9b50a6bd9d8a2c16953aad7e23
  content_type: application/pdf
  creator: dernst
  date_created: 2020-10-09T06:24:21Z
  date_updated: 2020-10-09T06:24:21Z
  file_id: '8638'
  file_name: 2018_LNCS_Elgyuett.pdf
  file_size: 537219
  relation: main_file
  success: 1
file_date_updated: 2020-10-09T06:24:21Z
has_accepted_license: '1'
intvolume: '     11022'
isi: 1
language:
- iso: eng
month: '08'
oa: 1
oa_version: Submitted Version
page: 53 - 70
project:
- _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
publication_status: published
publisher: Springer
publist_id: '7973'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Monitoring temporal logic with clock variables
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11022
year: '2018'
...
---
_id: '24'
abstract:
- lang: eng
  text: Partially-observable Markov decision processes (POMDPs) with discounted-sum
    payoff are a standard framework to model a wide range of problems related to decision
    making under uncertainty. Traditionally, the goal has been to obtain policies
    that optimize the expectation of the discounted-sum payoff. A key drawback of
    the expectation measure is that even low probability events with extreme payoff
    can significantly affect the expectation, and thus the obtained policies are not
    necessarily risk-averse. An alternate approach is to optimize the probability
    that the payoff is above a certain threshold, which allows obtaining risk-averse
    policies, but ignores optimization of the expectation. We consider the expectation
    optimization with probabilistic guarantee (EOPG) problem, where the goal is to
    optimize the expectation ensuring that the payoff is above a given threshold with
    at least a specified probability. We present several results on the EOPG problem,
    including the first algorithm to solve it.
acknowledgement: "This research was supported by the Vienna Science and Technology
  Fund (WWTF) grant ICT15-003; Austrian Science Fund (FWF): S11407-N23(RiSE/SHiNE);and
  an ERC Start Grant (279307:Graph Games).\r\n"
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: Adrian
  full_name: Elgyütt, Adrian
  id: 4A2E9DBA-F248-11E8-B48F-1D18A9856A87
  last_name: Elgyütt
- first_name: Petr
  full_name: Novotny, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotny
- first_name: Owen
  full_name: Rouillé, Owen
  last_name: Rouillé
citation:
  ama: 'Chatterjee K, Elgyütt A, Novotný P, Rouillé O. Expectation optimization with
    probabilistic guarantees in POMDPs with discounted-sum objectives. In: Vol 2018.
    IJCAI; 2018:4692-4699. doi:<a href="https://doi.org/10.24963/ijcai.2018/652">10.24963/ijcai.2018/652</a>'
  apa: 'Chatterjee, K., Elgyütt, A., Novotný, P., &#38; Rouillé, O. (2018). Expectation
    optimization with probabilistic guarantees in POMDPs with discounted-sum objectives
    (Vol. 2018, pp. 4692–4699). Presented at the IJCAI: International Joint Conference
    on Artificial Intelligence, Stockholm, Sweden: IJCAI. <a href="https://doi.org/10.24963/ijcai.2018/652">https://doi.org/10.24963/ijcai.2018/652</a>'
  chicago: Chatterjee, Krishnendu, Adrian Elgyütt, Petr Novotný, and Owen Rouillé.
    “Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum
    Objectives,” 2018:4692–99. IJCAI, 2018. <a href="https://doi.org/10.24963/ijcai.2018/652">https://doi.org/10.24963/ijcai.2018/652</a>.
  ieee: 'K. Chatterjee, A. Elgyütt, P. Novotný, and O. Rouillé, “Expectation optimization
    with probabilistic guarantees in POMDPs with discounted-sum objectives,” presented
    at the IJCAI: International Joint Conference on Artificial Intelligence, Stockholm,
    Sweden, 2018, vol. 2018, pp. 4692–4699.'
  ista: 'Chatterjee K, Elgyütt A, Novotný P, Rouillé O. 2018. Expectation optimization
    with probabilistic guarantees in POMDPs with discounted-sum objectives. IJCAI:
    International Joint Conference on Artificial Intelligence vol. 2018, 4692–4699.'
  mla: Chatterjee, Krishnendu, et al. <i>Expectation Optimization with Probabilistic
    Guarantees in POMDPs with Discounted-Sum Objectives</i>. Vol. 2018, IJCAI, 2018,
    pp. 4692–99, doi:<a href="https://doi.org/10.24963/ijcai.2018/652">10.24963/ijcai.2018/652</a>.
  short: K. Chatterjee, A. Elgyütt, P. Novotný, O. Rouillé, in:, IJCAI, 2018, pp.
    4692–4699.
conference:
  end_date: 2018-07-19
  location: Stockholm, Sweden
  name: 'IJCAI: International Joint Conference on Artificial Intelligence'
  start_date: 2018-07-13
date_created: 2018-12-11T11:44:13Z
date_published: 2018-07-01T00:00:00Z
date_updated: 2025-06-02T08:53:48Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.24963/ijcai.2018/652
ec_funded: 1
external_id:
  arxiv:
  - '1804.10601'
  isi:
  - '000764175404117'
intvolume: '      2018'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1804.10601
month: '07'
oa: 1
oa_version: Preprint
page: 4692 - 4699
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
- _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: IJCAI
publist_id: '8031'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum
  objectives
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 2018
year: '2018'
...