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/

Zendy Plus

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

Zendy Tools

Zendy Open

Recently, LTL extended with atomic formulas built over a constraint language interpreting variables in ℤ has been shown to have a decidable satisfiability and model-checking problem. This language allows to compare the variables at different states of the model and include periodicity constraints, comparison constraints, and a restricted form of quantification. On the other hand, the CTL counterpart of this logic (and hence also its CTL* counterpart which subsumes both LTL and CTL) has an undecidable model-checking problem. In this paper, we substantially extend the decidability border, by considering a meaningful fragment of CTL* extended with such constraints (which subsumes both the universal and existential fragments, as well as the EF-like fragment) and show that satisfiability and model-checking over relational automata that are abstraction of counter machines are decidable. The correctness and the termination of our algorithm rely on a suitable well quasi-ordering defined over the set of variable valuations.

Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints