CODEWITHSUNDEEP
formal-verificationmodel-checkingformal-methodsstate-spaceuppaal
Hachani Ahmed
Hachani Ahmed

Reputation: 19

State Space Explosion in UPPAAL

I modelled a timed model of two flip flop in UPPAAL , when i tried to verify some properties , I reached 6M states and my laptop was out of RAM, around 5Go was consumed, can anyone tell what it is the approximate state number that UPPAAL can deal with ? and what are the possible techniques to deal with state explosion in UPPAAL ?
Thank you

Upvotes: 1

Views: 673

Answers (1)

mariusm
mariusm

Reputation: 1678

The number of states depends on:

  1. the size of available memory. On 32bit architectures it is limited to 4GB.

  2. the size/footprint of individual states.

  3. the shape of state space and the order of exploration.

  4. granularity of symbolic states (how well the constraint intervals span: if the time is discretized then the symbolic techniques will scale poorly).

You could try the following techniques:

  1. Apply abstraction and remove unnecessary variables: make variables const, set variables to zero when unused, one-transition-communication-only variables can be marked "meta" (don't abuse this one! or you will get in trouble with bizarre behavior).

  2. optimize space consumption by setting state space reduction to aggressive.

  3. apply partial order reduction, symmetry reduction.

  4. apply sweep-line method (look for keyword "progress" in Uppaal help).

Look at Uppaal tutorial for further information.

Upvotes: 1

Related Questions