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

Model checking is a powerful and widespread technique for the verification of finite distributed systems. It takes as input a formal model of a system and a formal specification (formula) of a property to be checked, and states whether the system satisfies the property or not. Since it is based on state space traversal algorithms, the model checking approach suffers from the well known state space explosion problem. Indeed the space (and consequently the time) requirements increase exponentially with the size of the models. One way to deal with this problem is symbolic model checking. It aims at checking the property on a compact representation of the system by using Binary Decision Diagram (BDD) techniques. Another way is to parallelize the construction/traversal of the state space on multiple processors. In this paper, we combine the two mentioned approaches by proposing an efficient multi-threaded algorithm for the construction of the so called Symbolic Observation Graph (SOG). It is a hybrid structure where the transitions of the system are divided into observed and unobserved ones. The nodes of this graph are then defined as sets of states linked with unobserved transitions (and encoded symbolically with a BDD) and edges are labeled with observed transitions only (and represented explicitly). The basic idea is that each thread owns one part of the SOG construction. We measured the runtime of the parallel SOG construction algorithm on several models, and the obtained results are very competitive. The preliminary evaluations we have done on standard examples show that our method outperforms the sequential method which makes it attractive.

A Parallel Construction of the Symbolic Observation Graph: the Basis for Efficient Model Checking of Concurrent Systems