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 Parameterised Model Checking Problem asks whether an implementationImpl(t) satisfies a specification Spec(t) for all instantiations of parametert. In general, t can determine numerous entities: the number of processes usedin a network, the type of data, the capacities of buffers, etc. The main themeof this paper is automation of uniform verification of a subclass of PMCP withthe parameter of the first kind, i.e. the number of processes in the network.We use CSP as our formalism. We present a type reduction theory, which, for agiven verification problem, establishes a function \phi that maps all(sufficiently large) instantiations T of the parameter to some fixed type T^and allows us to deduce that if Spec(T^) is refined by \phi(Impl(T)), then(subject to certain assumptions) Spec(T) is refined by Impl(T). The theory canbe used in practice by combining it with a suitable abstraction method thatproduces a t-independent process Abstr that is refined by {\phi}(Impl(T)) forall sufficiently large T. Then, by testing (with a model checker) if theabstract model Abstr refines Spec(T^), we can deduce a positive answer to theoriginal uniform verification problem. The type reduction theory relies onsymbolic representation of process behaviour. We develop a symbolic operationalsemantics for CSP processes that satisfy certain normality requirements, and weprovide a set of translation rules that allow us to concretise symbolictransition graphs. Based on this, we prove results that allow us to inferbehaviours of a process instantiated with uncollapsed types from knownbehaviours of the same process instantiated with a reduced type. One of themain advantages of our symbolic operational semantics and the type reductiontheory is their generality, which makes them applicable in a wide range ofsettings.

A type reduction theory for systems with replicated components