License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2021.45
URN: urn:nbn:de:0030-drops-155562
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15556/
Holla, Raveendra ;
Deka, Nabarun ;
D'Souza, Deepak
On the Expressive Equivalence of TPTL in the Pointwise and Continuous Semantics
Abstract
We consider a first-order logic with linear constraints interpreted in a pointwise and continuous manner over timed words. We show that the two interpretations of this logic coincide in terms of expressiveness, via an effective transformation of sentences from one logic to the other. As a consequence it follows that the pointwise and continuous semantics of the logic TPTL with the since operator also coincide. Along the way we exhibit a useful normal form for sentences in these logics.
BibTeX - Entry
@InProceedings{holla_et_al:LIPIcs.FSTTCS.2021.45,
author = {Holla, Raveendra and Deka, Nabarun and D'Souza, Deepak},
title = {{On the Expressive Equivalence of TPTL in the Pointwise and Continuous Semantics}},
booktitle = {41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
pages = {45:1--45:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-215-0},
ISSN = {1868-8969},
year = {2021},
volume = {213},
editor = {Boja\'{n}czy, Miko{\l}aj and Chekuri, Chandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/15556},
URN = {urn:nbn:de:0030-drops-155562},
doi = {10.4230/LIPIcs.FSTTCS.2021.45},
annote = {Keywords: Real-Time Logics, First-Order Logics}
}
|
Keywords: |
|
Real-Time Logics, First-Order Logics |
|
Collection: |
|
41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021) |
|
Issue Date: |
|
2021 |
|
Date of publication: |
|
29.11.2021 |
