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

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 monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

When automatically verifying specifications of reactive systems (reactive systems are at least nonterminating programs that react on some input, e.g. operating systems, communication protocols, chipcard-/smartcard-protocols) one major problem is the verification algorit hm’s complexity. To make verification practically possible a successful approach is to lower the size of the model that describes the specified system’s full behaviour. This can be done by formal language methods. We think of homomorphic images h(L) of the language L describing the specified system’s full behaviour. A finite state representation of h(L) is usually—i.e. if we have defined the homomorphism in a clever way—much smaller than a representation for L. We call h(L) the abstraction of L. In such an approach it is an important problem how one has to deal with liveness properties. To describe some special liveness properties we can define a temporal logic that is a subclass of the full computation tree logic CTL* [Eme90]. We will call this logic A GEF-kytc because of the preceding operators in each of its formulae: If q is a PLTL-formula (PLTL stands for Propositional Linear Temporaf Logic) [Eme90] then AQCF(7)) is an AGEFformula and no other formulae are formulae of the AGEFlogic. An AGEF-formula AGEF(q) is satisfied in lim(L) for some language L (we write lim (L) ~ AG~~(7/)) if and only if for all finite prefixes w of w-words in li~n(L) there is a word rJ such that wv is a finite prefix of some u-word in l,rn(L) and there is an w-word u such that wvu c /iT71(L) and the PLTL-formnla q is satisfied in u (i.e. u + r)). The intuitive meaning of AGEF-formnlae is that “whatever has happened before, something might happen such that after a finitely long period of time the property 7/ is satisfied. ” Our definition implies that ~(q) is a liveness property that is satisfied in each model where d~t~(q) is satisfied. We can define a mapping R on PLTL-fornlulae such that for each language L ~ Z*, each alphabetic language hon~o-

A verification method based on homomorphic model abstractions (abstract)