This is Enea.


Personal Info





PHAVerLite: experimental evaluation

[Page last updated on "luglio 17, 2019, 09:14:51".]

PHAVerLite (version 0.1) participated to the ARCH-COMP 2019 friendly competition, for the HPWC category (hybrid systems with piecewice constant dynamics). In this page we repeat the corresponding experimental evaluation, using PHAVerLite version 0.2. The corresponding model and configuration files can be downloaded. People interested in details about some of the techniques used in PHAVerLite are referred to the following paper:

The HPWC category of the ARCH-COMP 2019 friendly competition featured 25 tests. These are divided into 15 safe tests (aiming at proving a valid safety property, so that an overapproximation of the reachable set is permitted) and 10 unsafe tests (aiming at disproving an invalid safety property, so that no overapproximation of the reachable set is permitted).

The following observations apply:

  • the one reported is the total time of the analysis tool: besides the time spent in the fixpoint computation of the reachable set, it includes the parsing of the automaton (quite often also requiring the computation of the parallel composition of several automata components), as well as the computation and output of the final result;
  • the timeout threshold for PHAVerLite was set to 10 minutes (PHAVer/SX and PHAVer-lite/SX were using a higher timeout threshold);
  • the time reported for PHAVer/SX and PHAVer-lite/SX are taken from the ARCH-COMP 2018 edition, where 20 tests were considered; the entry n/a means not available, i.e., no attempt was performed on that test;
  • PHAVer/SX was using a different machine, with a faster CPU.

The following is the table for the 15 safe tests. Note that, in all but the TTE tests, PHAVerLite overapproximates the reachable set by using a single polyhedron per location, also further approximating the convex polyhedral hull using the constraint hull (PHAVer/SX and PHAVerLite/SX perform no overapproximation).

Safe tests PHAVer/SX PHAVer-lite/SX PHAVerLite
ACCS05 9.4 1.0 0.1
ACCS06 461.0 38.1 0.5
ACCS07 timeout n/a 4.3
ACCS08 n/a n/a 47.2
DISC02 1.1 0.1 0.0
DISC03 timeout 548.0 0.6
DISC04 timeout timeout 75.4
DISC05 timeout timeout timeout
DRNW02-BDR03 528.1 113.0 16.3
FISCS04 90.5 12.3 0.2
FISCS05 timeout 14722.2 1.3
FISCS06 n/a n/a 10.96
TTES05 25.2 1.9 0.3
TTES07 113.0 7.7 1.9
TTES09 n/a n/a 13.8

The following is the table for the 10 unsafe tests. In this case no overapproximation is allowed, hence all tools compute on a domain of finite sets of NNC polyhedra (no use of convex polyhedral hull, constraint hull or widening operators). However, PHAVerLite checks for a violation of the safety property during the fixpoint computation, stopping as soon as possible; in contrast, PHAVer/SX and PHAVer-lite/SX compute the full reachable set and check for violation only at the end (this also explains why these tools obtain the same time on all of the variants of the DRNW02 test).

Unsafe tests PHAVer/SX PHAVer-lite/SX PHAVerLite
ACCU05 13.7 0.9 0.1
ACCU06 13430 22.4 0.3
ACCU07 timeout n/a 1.5
ACCU08 n/a n/a 8.8
DRNW02-BDR01 528.1 113.0 10.3
DRNW02-BDR02 528.1 113.0 9.8
DRNW02-BDR04 528.1 113.0 9.8
FISCU04 579 102.2 0.2
FISCU05 timeout timeout 1.0
FISCU06 n/a n/a 5.5

© Enea Zaffanella

| Home | Personal Info | Research | Papers | Teaching | About