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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

In the plethora of fragments of Halpern and Shoham's modal logic of timeintervals (HS), the logic AB of Allen's relations Meets and Started-by is at acentral position. Statements that may be true at certain intervals, but at nosub-interval of them, such as accomplishments, as well as metric constraintsabout the length of intervals, that force, for instance, an interval to be atleast (resp., at most, exactly) k points long, can be expressed in AB.Moreover, over the linear order of the natural numbers N, it subsumes the(point-based) logic LTL, as it can easily encode the next and until modalities.Finally, it is expressive enough to capture the {\omega}-regular languages,that is, for each {\omega}-regular expression R there exists an AB formula{\phi} such that the language defined by R coincides with the set of models of{\phi} over N. It has been shown that the satisfiability problem for AB over Nis EXPSPACE-complete. Here we prove that, under the homogeneity assumption, itsmodel checking problem is {\Delta}^p_2 = P^NP-complete (for the sake ofcomparison, the model checking problem for full HS is EXPSPACE-hard, and theonly known decision procedure is nonelementary). Moreover, we show that themodality for the Allen relation Met-by can be added to AB at no extra cost(AA'B is P^NP-complete as well).

Model Checking the Logic of Allen's Relations Meets and Started-by is $P^NP$-Complete