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

The compositional specification and verification of the behavior of concurrent processes is a challenging research area. The assumption/commitmentapproach has emerged as one way to systematically achieve the desired modularity. However, it is generally limited to reasoning about safety properties which apply throughout the execution of a system. Liveness properties involving intermittent behavior are harder to address. We investigate the use of assumptions and commitments in Interval Temporal Logic and show how to augment them with some more information for handling liveness. The proposed techniques are a continuation of our previous research on formalizing assumptions and commitments through the use of fixpoints of certain simple temporal operators. Associated with this is a generalized notion of Owicki and Gries’ proof outlines. We illustrate the approach with examples including a mutual exclusion system with time stamps.

Using Temporal Fixpoints to Compositionally Reason about Liveness