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

We address the problem of verifying message passing programs, defined as aset of parallel processes communicating through unbounded FIFO buffers. Weintroduce a bounded analysis that explores a special type of computations,called k-synchronous. These computations can be viewed as (unbounded) sequencesof interaction phases, each phase allowing at most k send actions (by differentprocesses), followed by a sequence of receives corresponding to sends in thesame phase. We give a procedure for deciding k-synchronizability of a program,i.e., whether every computation is equivalent (has the same happens-beforerelation) to one of its k-synchronous computations. We also show thatreachability over k-synchronous computations and checking k-synchronizabilityare both PSPACE-complete. Furthermore, we introduce a class of programs called{\em flow-bounded} for which the problem of deciding whether there exists a k>0for which the program is k-synchronizable, is decidable.

On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony