Partial order reduction in SPOT

From LRDE

Revision as of 17:08, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Vincent Tourneur | title = Partial order reduction in SPOT | year = 2017 | number = 1709 | abstract = Nowadays, model-checking tools suffer from a scal...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Abstract

Nowadays, model-checking tools suffer from a scalling problem, due to their memory consuption. Partial order reduction is one way allowing to notably reduce it, by computing only needed data on-the-fly. There are many state-of-the-art algorithms, and this method is used in many softwares (such as SPIN or LTSmin). We are going to talk about the implementation of it in the Spot libraryand then the optimisation. The results show a great decrease of the memory consuption, which implies some gain in all subsequent steps.