Discounted Duration Calculus

Heinrich Ody, Martin Fränzle, Michael Reichhardt Hansen

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

To formally reason about the temporal quality of systems discounting was introduced to CTL and LTL. However, these logic are discrete and they cannot express duration properties. In this work we introduce discounting for a variant of Duration Calculus. We prove decidability of model checking for a useful fragment of discounted Duration Calculus formulas on timed automata under mild assumptions. Further, we provide an extensive example to show the usefulness of the fragment.
Original languageEnglish
Title of host publicationProceedings of the 21st International Symposium on Formal Methods (FM 2016)
PublisherSpringer
Publication date2016
Pages577-592
ISBN (Print)978-3-319-48988-9
ISBN (Electronic)978-3-319-48989-6
DOIs
Publication statusPublished - 2016
Event21st International Symposium on Formal Methods (FM 2016) - Limassol, Cyprus
Duration: 7 Nov 201611 Nov 2016
Conference number: 21
http://fm2016.cs.ucy.ac.cy/

Conference

Conference21st International Symposium on Formal Methods (FM 2016)
Number21
CountryCyprus
CityLimassol
Period07/11/201611/11/2016
Internet address
SeriesLecture Notes in Computer Science
Volume9995
ISSN0302-9743

Keywords

  • Duration calculus
  • Temporal logic
  • Model checking
  • Timed automata
  • Discounting

Cite this

Ody, H., Fränzle, M., & Hansen, M. R. (2016). Discounted Duration Calculus. In Proceedings of the 21st International Symposium on Formal Methods (FM 2016) (pp. 577-592). Springer. Lecture Notes in Computer Science, Vol.. 9995 https://doi.org/10.1007/978-3-319-48989-6_35
Ody, Heinrich ; Fränzle, Martin ; Hansen, Michael Reichhardt. / Discounted Duration Calculus. Proceedings of the 21st International Symposium on Formal Methods (FM 2016). Springer, 2016. pp. 577-592 (Lecture Notes in Computer Science, Vol. 9995).
@inproceedings{46aba99caab044ae877b0c755610e2db,
title = "Discounted Duration Calculus",
abstract = "To formally reason about the temporal quality of systems discounting was introduced to CTL and LTL. However, these logic are discrete and they cannot express duration properties. In this work we introduce discounting for a variant of Duration Calculus. We prove decidability of model checking for a useful fragment of discounted Duration Calculus formulas on timed automata under mild assumptions. Further, we provide an extensive example to show the usefulness of the fragment.",
keywords = "Duration calculus, Temporal logic, Model checking, Timed automata, Discounting",
author = "Heinrich Ody and Martin Fränzle and Hansen, {Michael Reichhardt}",
year = "2016",
doi = "10.1007/978-3-319-48989-6_35",
language = "English",
isbn = "978-3-319-48988-9",
pages = "577--592",
booktitle = "Proceedings of the 21st International Symposium on Formal Methods (FM 2016)",
publisher = "Springer",

}

Ody, H, Fränzle, M & Hansen, MR 2016, Discounted Duration Calculus. in Proceedings of the 21st International Symposium on Formal Methods (FM 2016). Springer, Lecture Notes in Computer Science, vol. 9995, pp. 577-592, 21st International Symposium on Formal Methods (FM 2016), Limassol, Cyprus, 07/11/2016. https://doi.org/10.1007/978-3-319-48989-6_35

Discounted Duration Calculus. / Ody, Heinrich ; Fränzle, Martin; Hansen, Michael Reichhardt.

Proceedings of the 21st International Symposium on Formal Methods (FM 2016). Springer, 2016. p. 577-592 (Lecture Notes in Computer Science, Vol. 9995).

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

TY - GEN

T1 - Discounted Duration Calculus

AU - Ody, Heinrich

AU - Fränzle, Martin

AU - Hansen, Michael Reichhardt

PY - 2016

Y1 - 2016

N2 - To formally reason about the temporal quality of systems discounting was introduced to CTL and LTL. However, these logic are discrete and they cannot express duration properties. In this work we introduce discounting for a variant of Duration Calculus. We prove decidability of model checking for a useful fragment of discounted Duration Calculus formulas on timed automata under mild assumptions. Further, we provide an extensive example to show the usefulness of the fragment.

AB - To formally reason about the temporal quality of systems discounting was introduced to CTL and LTL. However, these logic are discrete and they cannot express duration properties. In this work we introduce discounting for a variant of Duration Calculus. We prove decidability of model checking for a useful fragment of discounted Duration Calculus formulas on timed automata under mild assumptions. Further, we provide an extensive example to show the usefulness of the fragment.

KW - Duration calculus

KW - Temporal logic

KW - Model checking

KW - Timed automata

KW - Discounting

U2 - 10.1007/978-3-319-48989-6_35

DO - 10.1007/978-3-319-48989-6_35

M3 - Article in proceedings

SN - 978-3-319-48988-9

SP - 577

EP - 592

BT - Proceedings of the 21st International Symposium on Formal Methods (FM 2016)

PB - Springer

ER -

Ody H, Fränzle M, Hansen MR. Discounted Duration Calculus. In Proceedings of the 21st International Symposium on Formal Methods (FM 2016). Springer. 2016. p. 577-592. (Lecture Notes in Computer Science, Vol. 9995). https://doi.org/10.1007/978-3-319-48989-6_35