Homepage: http://www.inf.ethz.ch/personal/daxc/psl2ba/
Note that psl2ba is a prototype implementation by now. Optimization techniques such as formula rewriting or simplifications of the automata structures will be implemented soon.
The model is included in the NuSMV package. Follow the link ./abp to find the model instances and the properties given as PLTL and PSL formulas.
| translator | property | abp10 | abp11 | abp12 | abp13 | abp14 | abp15 |
|---|---|---|---|---|---|---|---|
| ltl2smv-2.4.3 | 1/LTL | 0m11.931s | 2m4.156s | 21m9.058s | |||
| psl2ba | 1/LTL | 0m12.102s | 2m22.968s | 20m23.692s | |||
| psl2ba | 1/PSL | 0m11.363s | 2m9.250s | 21m25.684s | |||
| psl2ba -dgo | 1/PSL | 0m11.484s | 2m10.282s | 21m42.916s |
The model is included in the NuSMV package. Follow the link ./brp to find the model instances and the properties given as PLTL and PSL formulas.
| modelchecker | translator | property | brp |
|---|---|---|---|
| NuSMV-2.2.2 | ltl2smv | property.ltl | 0m5.322s |
| NuSMV-2.2.2 | psl2ba | property.rtl | 0m5.494s |
| NuSMV-2.2.2 | psl2ba | property.ltl | 0m5.427s |
The Model stack is available at http://www.science.unitn.it/~stonetta/CAV05/. Follow the link ./stack to find the model instances and the properties given as PLTL and PSL formulas.
| translator | property | stack11 | stack12 | stack13 | stack14 | stack15 |
|---|---|---|---|---|---|---|
| ltl2smv-2.4.3 | 1/LTL | 0m1.390s | 0m5.656s | 0m12.140s | 0m25.094s | mem |
| psl2ba | 1/LTL | 0m2.531s | 0m8.812s | 0m20.297s | 0m45.562s | mem |
| psl2ba -dgo | 1/LTL | 0m2.515s | 0m7.906s | 0m24.063s | 0m45.594s | mem |
| psl2ba | 1/PSL | 0m24.641s | 1m39.433s | 6m11.047s | >23m | |
| psl2ba -dgo | 1/PSL | 0m36.203s | 2m21.125s | 9m18.427s |
| translator | property | stack500 | stack600 | stack700 | stack800 | stack900 |
|---|---|---|---|---|---|---|
| ltl2smv-2.4.3 | 2/LTL | 0m13.000s | 0m20.328s | 0m30.515s | 0m41.625s | 0m57.171s |
| psl2ba | 2/LTL | 0m12.390s | 0m19.765s | 0m29.000s | 0m41.687s | 0m52.859s |
| psl2ba -dgo | 2/LTL | 0m12.406s | 0m20.843s | 0m28.437s | 0m39.562s | 0m52.609s |
| psl2ba | 2/PSL | 0m12.656s | 0m20.281s | 0m29.171s | 0m39.578s | 0m53.765s |
| psl2ba -dgo | 2/PSL | 0m12.640s | 0m20.625s | 0m28.578s | 0m40.718s | 0m54.415s |
| translator | property | stack500 | stack600 | stack700 | stack800 | stack900 |
|---|---|---|---|---|---|---|
| ltl2smv-2.4.3 | 3/LTL | 0m14.093s | 0m21.061s | 0m31.719s | 0m43.078s | 0m58.031s |
| psl2ba | 3/LTL | 0m14.281s | 0m20.578s | 0m31.250s | 0m40.328s | 0m57.922s |
| psl2ba -dgo | 3/LTL | 0m12.728s | 0m20.484s | 0m28.563s | 0m39.703s | 0m51.141s |
| psl2ba | 3/PSL | 0m12.844s | 0m20.563s | 0m29.015s | 0m39.641s | 0m52.281s |
| psl2ba -dgo | 3/PSL | 0m12.906s | 0m20.563s | 0m29.156s | 0m42.328s | 0m53.781s |