|
|
@ -8,9 +8,9 @@ Version 4.3 (first released ???) |
|
|
|
|
|
|
|
|
* New model checking functionality/optimisations |
|
|
* New model checking functionality/optimisations |
|
|
- lower time-bounds for properties of DTMCs/MDPs (e.g. P=? [ F>=2 "target" ]) |
|
|
- lower time-bounds for properties of DTMCs/MDPs (e.g. P=? [ F>=2 "target" ]) |
|
|
- arbitrary precision computation via the parametric engine (switch -exact) |
|
|
|
|
|
- expected total rewards (R[C]) implemented for DTMCs in symbolic engine |
|
|
- expected total rewards (R[C]) implemented for DTMCs in symbolic engine |
|
|
- backwards reachability algorithm implemented for model checking PTAs |
|
|
- backwards reachability algorithm implemented for model checking PTAs |
|
|
|
|
|
- exact (arbitrary precision) model checking via the parametric engine (experimental) |
|
|
- various LTL model checking optimisations |
|
|
- various LTL model checking optimisations |
|
|
- faster precomputation by pre-computing predecessors |
|
|
- faster precomputation by pre-computing predecessors |
|
|
|
|
|
|
|
|
|
Dave Parker
11 years ago