The compound interest in relaxing punctuality Conference Paper

Author(s): Ferrère, Thomas
Editor(s): Havelund K; Peleska J; Roscoe B; de Vink E
Title: The compound interest in relaxing punctuality
Title Series: LNCS
Affiliation IST Austria
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.
Keywords: Formal methods; Temporal logic; Automata theory; Pattern matching; Timed automata; Decision procedure; Time sharing systems; Timed systems; Formal framework; Computer circuits; Clocks; Dynamic logic; Interval temporal logic; Regular expressions; Temporal modalities
Conference Title: FM: International Symposium on Formal Methods
Volume: 10951 LNCS
Conference Dates: July 15 -17, 2018
Conference Location: Oxford, UK
ISBN: 03029743 (ISSN); 9783319955810 (ISBN)
Publisher: Springer  
Date Published: 2018-07-12
Start Page: 147
End Page: 164
Sponsor: S11402-N23 Austrian Science Fund FWF, Z211-N23 Austrian Science Fund FWF
DOI: 10.1007/978-3-319-95582-7_9
Open access: no
IST Austria Authors
Related IST Austria Work