PRISM 4.3

[Dave Parker]

Dear PRISM users,

I am pleased to announce that a beta release of PRISM 4.3 is now
available. For full details and to download it, see:

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

New features include:

* Support for external LTL-to-automata converters via the HOA format
- including model checking for Generalised Rabin (GR) conditions

* New model checking functionality/optimisations
- lower time-bounds for properties of DTMCs/MDPs
- expected total rewards (R[C]) implemented for DTMCs
- backwards reachability algorithm for model checking PTAs
- exact (arbitrary precision) model checking (experimental)
- various LTL model checking optimisations
- faster precomputation by pre-computing predecessors

* Options/switches:
- new -pathviaautomata switch to force model checking via automata
- new "comment" option for exporting results (for regression tests)
- new -javamaxmem switch (equivalent to setting PRISM_JAVAMAXMEM)
- more convenient format for CUDD max memory setting (e.g. 50m, 4g)
- higher default values for CUDD/Java memory limits

* Additional functionality in prism-auto testing/benchmarking script
- export testing, .auto files, debug mode, colouring, ...

* New sbml2prism script

* Bug fixes

All feedback is very welcome.

Best wishes,

Dave.