English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Metric Temporal Logic $\mathsf{MTL}[\until_I,\since_I]$ is one of the moststudied real time logics. It exhibits considerable diversity in expressivenessand decidability properties based on the permitted set of modalities and thenature of time interval constraints $I$. Henzinger et al., in their seminalpaper showed that the non-punctual fragment of $\mathsf{MTL}$ called$\mathsf{MITL}$ is decidable. In this paper, we sharpen this decidabilityresult by showing that the partially punctual fragment of $\mathsf{MTL}$(denoted $\mathsf{PMTL}$) is decidable over strictly monotonic finite pointwise time. In this fragment, we allow either punctual future modalities, orpunctual past modalities, but never both together. We give two satisfiabilitypreserving reductions from $\mathsf{PMTL}$ to the decidable logic$\mathsf{MTL}[\until_I]$. The first reduction uses simple projections, whilethe second reduction uses a novel technique of temporal projections withoversampling. We study the trade-off between the two reductions: while thesecond reduction allows the introduction of extra action points in theunderlying model, the equisatisfiable $\mathsf{MTL}[\until_I]$ formula obtainedis exponentially succinct than the one obtained via the first reduction, whereno oversampling of the underlying model is needed. We also show that$\mathsf{PMTL}$ is strictly more expressive than the fragments$\mathsf{MTL}[\until_I,\since]$ and $\mathsf{MTL}[\until,\since_I]$.

Partially Punctual Metric Temporal Logic is Decidable