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

The problem of model checking procedural programs has fostered much researchtowards the definition of temporal logics for reasoning on context-freestructures. The most notable of such results are temporal logics on NestedWords, such as CaRet and NWTL. Recently, the logic OPTL was introduced, basedon the class of Operator Precedence Languages (OPLs), more powerful than NestedWords. We define the new OPL-based logic POTL and prove its FO-completeness.POTL improves on NWTL by enabling the formulation of requirements involvingpre/post-conditions, stack inspection, and others in the presence ofexception-like constructs. It improves on OPTL too, which instead we show notto be FO-complete; it also allows to express more easily stack inspection andfunction-local properties. In a companion paper we report a model checkingprocedure for POTL and experimental results based on a prototype tool developedtherefor. For completeness a short summary of this complementary result isprovided in this paper too.

A First-Order Complete Temporal Logic for Structured Context-Free Languages