Skip to content
The main development version of the PRISM-games model checker, an extension of PRISM which supports stochastic games.
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
cudd
manual
prism-examples
prism-tests
prism
.classpath
.gitignore
.travis.yml
CHANGELOG.txt
COPYING.txt
README.md

README.md

PRISM-games

This is PRISM-games, an extension of the PRISM model checker for verification and strategy synthesis for stochastic multi-player games.

Installation

Up-to-date installation instructions can be found here:

http://www.prismmodelchecker.org/games/installation.php

Documentation

Included in this release is a manual for the version of PRISM on which PRISM-games is based.

Documentation specifically for PRISM-games can be found here:

http://www.prismmodelchecker.org/games/

Licensing

PRISM-games is distributed under the GNU General Public License (GPL), version 2. A copy of this license can be found in the file COPYING.txt. For more information, see:

http://www.gnu.org/licenses/

PRISM-games uses the CUDD (Colorado University Decision Diagram) library of Fabio Somenzi, which is freely available. For more information about this library, see:

http://vlsi.colorado.edu/~fabio/CUDD/

PRISM-games also uses various other libraries (mainly to be found in the lib directory). For details of those, and for links to source where we distribute only binaries, see:

http://www.prismmodelchecker.org/other-downloads.php

Acknowledgements

PRISM was created and is still actively maintained by:

  • Dave Parker (University of Birmingham)
  • Gethin Norman (University of Glasgow)
  • Marta Kwiatkowska (University of Oxford)

Development of the tool is currently led from Birmingham by Dave Parker. Other current key developers are:

  • Joachim Klein (formerly Technische Universität Dresden)

We gratefully acknowledge contributions to the PRISM code-base from various sources, including (in approximately reverse chronological order):

  • Steffen Märcker: Fixes and improvements, especially in explicit engine
  • Chris Novakovic: Build infrastructure and explicit engine improvements
  • Clemens Wiltsche: Multi-objective and compositional synthesis for stochastic games
  • Ernst Moritz Hahn: Parametric model checking, fast adaptive uniformisation + various other features
  • Frits Dannenberg: Fast adaptive uniformisation
  • Vojtech Forejt: Various model checking code, including multi-objective + GUI enhancements
  • Hongyang Qu: Multi-objective model checking
  • Mateusz Ujma: Bug fixes and GUI improvements
  • Christian von Essen: Symbolic/explicit-state model checking
  • Vincent Nimal: Approximate (simulation-based) model checking techniques
  • Mark Kattenbelt: Wide range of enhancements/additions, especially in the GUI
  • Carlos Bederian (working with Pedro D'Argenio): LTL model checking for MDPs
  • Gethin Norman: Precomputation algorithms, abstraction
  • Alistair John Strachan: Port to 64-bit architectures
  • Alistair John Strachan, Mike Arthur and Zak Cohen: Integration of JFreeChart into PRISM
  • Charles Harley and Sebastian Vermehren: GUI enhancements
  • Rashid Mehmood: Improvements to low-level data structures and numerical solution algorithms
  • Stephen Gilmore: Support for the stochastic process algebra PEPA
  • Paolo Ballarini & Kenneth Chan: Port to Mac OS X
  • Andrew Hinton: Original versions of the GUI, Windows port and simulator
  • Joachim Meyer-Kayser: Original implementation of the "Fox-Glynn" algorithm

For more details see:

http://www.prismmodelchecker.org/people.php

Contact

If you have problems or questions regarding PRISM, please use the help forum provided. See:

http://www.prismmodelchecker.org/support.php

Other comments and feedback about any aspect of PRISM are also very welcome. Please contact:

Dave Parker (d.a.parker@cs.bham.ac.uk) School of Computer Science University of Birmingham Edgbaston Birmingham B15 2TT ENGLAND

You can’t perform that action at this time.