The compound interest in relaxing punctuality

T. Ferrere, in:, Springer, 2018, pp. 147–164.

Download
OA 2018_LNCS_Ferrere.pdf 485.58 KB

Conference Paper | Published | English

Scopus indexed
Department
Series Title
LNCS
Abstract
Imprecision in timing can sometimes be beneficial: Metric interval temporal logic (MITL), disabling the expression of punctuality constraints, was shown to translate to timed automata, yielding an elementary decision procedure. We show how this principle extends to other forms of dense-time specification using regular expressions. By providing a clean, automaton-based formal framework for non-punctual languages, we are able to recover and extend several results in timed systems. Metric interval regular expressions (MIRE) are introduced, providing regular expressions with non-singular duration constraints. We obtain that MIRE are expressively complete relative to a class of one-clock timed automata, which can be determinized using additional clocks. Metric interval dynamic logic (MIDL) is then defined using MIRE as temporal modalities. We show that MIDL generalizes known extensions of MITL, while translating to timed automata at comparable cost.
Publishing Year
Date Published
2018-07-12
Volume
10951
Page
147 - 164
Conference
FM: International Symposium on Formal Methods
Conference Location
Oxford, UK
Conference Date
2018-07-15 – 2018-07-17
IST-REx-ID
156

Cite this

Ferrere T. The compound interest in relaxing punctuality. In: Vol 10951. Springer; 2018:147-164. doi:10.1007/978-3-319-95582-7_9
Ferrere, T. (2018). The compound interest in relaxing punctuality (Vol. 10951, pp. 147–164). Presented at the FM: International Symposium on Formal Methods, Oxford, UK: Springer. https://doi.org/10.1007/978-3-319-95582-7_9
Ferrere, Thomas. “The Compound Interest in Relaxing Punctuality,” 10951:147–64. Springer, 2018. https://doi.org/10.1007/978-3-319-95582-7_9.
T. Ferrere, “The compound interest in relaxing punctuality,” presented at the FM: International Symposium on Formal Methods, Oxford, UK, 2018, vol. 10951, pp. 147–164.
Ferrere T. 2018. The compound interest in relaxing punctuality. FM: International Symposium on Formal Methods, LNCS, vol. 10951. 147–164.
Ferrere, Thomas. The Compound Interest in Relaxing Punctuality. Vol. 10951, Springer, 2018, pp. 147–64, doi:10.1007/978-3-319-95582-7_9.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Main File(s)
File Name
Access Level
OA Open Access
Date Uploaded
2020-10-09
MD5 Checksum
a045c213c42c445f1889326f8db82a0a


Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar