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

Regular model checking is a well-established technique for the verificationof infinite-state systems whose configurations can be represented as finitewords over a suitable alphabet. It applies to systems whose set of initialconfigurations is regular, and whose transition relation is captured by alength-preserving transducer. To verify safety properties, regular modelchecking iteratively computes automata recognizing increasingly larger regularsets of reachable configurations, and checks if they contain unsafeconfigurations. Since this procedure often does not terminate, acceleration,abstraction, and widening techniques have been developed to compute a regularsuperset of the set of reachable configurations.  In this paper we develop a complementary approach. Instead of approaching theset of reachable configurations from below, we start with the set of allconfigurations and compute increasingly smaller regular supersets of it. We usethat the set of reachable configurations is equal to the intersection of allinductive invariants of the system. Since the intersection is in generalnon-regular, we introduce $b$-bounded invariants, defined as thoserepresentable by CNF-formulas with at most $b$ clauses. We prove that, forevery $b \geq 0$, the intersection of all $b$-bounded inductive invariants isregular, and show how to construct an automaton recognizing it. We study thecomplexity of deciding if this automaton accepts some unsafe configuration. Weshow that the problem is in \textsc{EXPSPACE} for every $b \geq 0$, and\textsc{PSPACE}-complete for $b=1$. Finally, we study how large must $b$ be toprove safety properties of a number of benchmarks.

Regular Model Checking Upside-Down: An Invariant-Based Approach