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

We define a new method for taking advantage of net reductions in combinationwith a SMT-based model checker. Our approach consists in transforming areachability problem about some Petri net, into the verification of an updatedreachability property on a reduced version of this net. This method relies on anew state space abstraction based on systems of constraints, called polyhedralabstraction. We prove the correctness of this method using a new notion ofequivalence between nets. We provide a complete framework to define and checkthe correctness of equivalence judgements; prove that this relation is acongruence; and give examples of basic equivalence relations that derive fromstructural reductions. Our approach has been implemented in a tool, named SMPT,that provides two main procedures: Bounded Model Checking (BMC) and PropertyDirected Reachability (PDR). Each procedure has been adapted in order to usereductions and to work with arbitrary Petri nets. We tested SMPT on a largecollection of queries used in the Model Checking Contest. Our experimentalresults show that our approach works well, even when we only have a moderateamount of reductions.

A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking