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

In symbolic model checking, the behavior of a model to be verified is captured by the transition relation of the state space implied by the model. Unfortunately, the size of the transition relation grows rapidly with the number of states even for small models, rendering them impossible to verify. A recent work (5) described a method for partitioning the transition relation, thus reducing the overall space requi rement. Using this method, actions that require the transit ion relation can be executed by using one partition at a time. This process, however, strongly depends on the order in which the partitions are processed during the action. This paper describes a criterion for ordering partitions wh ich is independent of the circuit details. Based on this criterion, a heuristic algorithm for ordering partitions i s described. The algorithm, which may be used in preparation for each symbolic simulation step, has been successfully implemented and has resulted in significant speed-ups of symbolic model checking. Specifically, this algorithm has made it possible to verify blocks inside an example microprocessor. The run time results are given here.

Efficient model checking by automated ordering of transition relation partitions