Probabilistic Swarm Verification

This page includes a number of software packages for the verification of unbounded probabilistic systems. For tools that verify unbounded non-probabilistic systems, please visit this page.

PSV-BD

Probabilistic Swarm Verifier for BoundeD time properties is a software package for the verification of emergence of bounded time properties in probabilistic swarm systems. Further information can be found in the corresponding paper (published at IJCAI 2018).

Click here to download the source code: PSV-BD

PSV-CA

Probabilistic Swarm Verifier using Couner Abstraction is a software package for the verification of properties in probabilistic swarm systems. Further information can be found in the corresponding paper (published at AAMAS 2019).

Click here to download the source code: PSV-CA

PSV-S

Probabilistic Swarm Verifier for Strategic properties is a software package for the verification of strategic properties in probabilistic swarm systems. Further information can be found in the corresponding paper (published at AAMAS 2020).

Click here to download the source code: PSV-S

PSV-F

Probabilistic Swarm Verifier for Faulty systems is a software package for the verification of properties in probabilistic swarm systems that may exhibit faults. Further information can be found in the corresponding paper (published at IJCAI 2020).

Click here to download the source code: PSV-F