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

By algorithmic metatheorems for a model checking problem P overinfinite-state systems we mean generic results that can be used to inferdecidability (possibly complexity) of P not only over a specific class ofinfinite systems, but over a large family of classes of infinite systems. Suchresults normally start with a powerful formalism of infinite-state systems,over which P is undecidable, and assert decidability when is restricted bymeans of an extra "semantic condition" C. We prove various algorithmicmetatheorems for the problems of model checking LTL and its two commonfragments LTL(Fs,Gs) and LTLdet over the expressive class of word/treeautomatic transition systems, which are generated by synchronized finite-statetransducers operating on finite words and trees. We present numerousapplications, where we derive (in a unified manner) many known and previouslyunknown decidability and complexity results of model checking LTL and itsfragments over specific classes of infinite-state systems including pushdownsystems; prefix-recognizable systems; reversal-bounded counter systems withdiscrete clocks and a free counter; concurrent pushdown systems with a boundednumber of context-switches; various subclasses of Petri nets; weakly extendedPA-processes; and weakly extended ground-tree rewrite systems. In all cases,weare able to derive optimal (or near optimal) complexity. Finally, we pinpointthe exact locations in the arithmetic and analytic hierarchies of the problemof checking a relevant semantic condition and the LTL model checking problemsover all word/tree automatic systems.

Algorithmic metatheorems for decidable LTL model checking over infinite systems