PTA model checking with Digital clocks

[Wenhao Xing]

Hi, 

I was told by papers that digital clocks suffers from large number of clocks or a large number constant when doing the reachability checking. so the Stochastic games is a better way to check the reachability.

but when I run the model checking to check the reachability of a PTA,  I tried to do it with digital clocks, stochastic games and backward reachability respectively,  I used a big constant, but on me it seems different with the paper,  the stochastic games is always the slowest one, while digital clocks the fastest.

can anyone pls explain that for me ? thanks

sincerely,

Wenhao

[Dave Parker]

Hi Wenhao,

In general, yes, the performance of the digital clocks engine gets worse
for large numbers of clocks or with large clock constants, but this is
not completely predictable - it will depend on the model.

Best wishes,

Dave

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/ef3f9d96-9a9c-43c5-9f64-7750e8c572afn%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/ef3f9d96-9a9c-43c5-9f64-7750e8c572afn%40googlegroups.com?utm_medium=email&utm_source=footer>.