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

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

A key problem in mixing operational (e.g., process-algebraic) and declarative (e.g., logical) styles of specification is how to deal with inconsistencies arising when com- posing processes under conjunction. This article introduces a conjunction operator on labelled transition systems capturing the basic intuition of "a and b = false", and considers a naive preorder that demands that an inconsistent specification can only be refined by an inconsistent implementation. The main body of the article is concerned with characterising the largest pre- congruence contained in the naive preorder. This characterisation will be based on what we call ready-tree semantics, which is a variant of path-based possible-worlds semantics. We prove that the induced ready-tree preorder is compositional and fully-abstract, and that the conjunction operator indeed reflects conjunction. The article's results provide a foundation for, and an important step towards a unified framework that allows one to freely mix operators from process algebras and linear-time temporal logics.

Conjunction on Processes: Full–Abstraction Via Ready–Tree Semantics