Discounted Duration Calculus

Heinrich  Ody; Martin Fränzle; Michael Reichhardt Hansen

doi:10.1007/978-3-319-48989-6_35

Discounted Duration Calculus

Heinrich Ody, Martin Fränzle, Michael Reichhardt Hansen

University of Oldenburg

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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 language	English
Title of host publication	Proceedings of the 21st International Symposium on Formal Methods (FM 2016)
Publisher	Springer
Publication date	2016
Pages	577-592
ISBN (Print)	978-3-319-48988-9
ISBN (Electronic)	978-3-319-48989-6
DOIs	https://doi.org/10.1007/978-3-319-48989-6_35
Publication status	Published - 2016
Event	21st International Symposium on Formal Methods (FM 2016) - Limassol, Cyprus Duration: 7 Nov 2016 → 11 Nov 2016 Conference number: 21 http://fm2016.cs.ucy.ac.cy/

Conference

Conference	21st International Symposium on Formal Methods (FM 2016)
Number	21
Country/Territory	Cyprus
City	Limassol
Period	07/11/2016 → 11/11/2016
Internet address	http://fm2016.cs.ucy.ac.cy/

Series	Lecture Notes in Computer Science
Volume	9995
ISSN	0302-9743

Keywords

Duration calculus
Temporal logic
Model checking
Timed automata
Discounting

Access to Document

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

OpenUrl availability

Full text

Cite this

@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{\"a}nzle and Hansen, {Michael Reichhardt}",

year = "2016",

doi = "10.1007/978-3-319-48989-6_35",

language = "English",

isbn = "978-3-319-48988-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "577--592",

booktitle = "Proceedings of the 21st International Symposium on Formal Methods (FM 2016)",

note = "21st International Symposium on Formal Methods (FM 2016), FM 2016 ; Conference date: 07-11-2016 Through 11-11-2016",

url = "http://fm2016.cs.ucy.ac.cy/",

}

TY - GEN

T1 - Discounted Duration Calculus

AU - Ody, Heinrich

AU - Fränzle, Martin

AU - Hansen, Michael Reichhardt

N1 - Conference code: 21

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

T3 - Lecture Notes in Computer Science

SP - 577

EP - 592

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

PB - Springer

T2 - 21st International Symposium on Formal Methods (FM 2016)

Y2 - 7 November 2016 through 11 November 2016

ER -

Discounted Duration Calculus

Abstract

Conference

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this