question

[Marek Golonka]

In attachment I have my proposition of crosswalk nearing algorithm for autonomous car behaviour.

I want to ask what properties in PRISM I can validate and verify for this situation. Can me give some kind of proposition? I checked manual but I do not know what can be used in this situation.

I wrote code for prism:

=============================

dtmc

module crosswalk

// local state

s : [0..6] init 0;

[] s=0 -> (s'=1);

[] s=1 -> 0.6 : (s'=3) + 0.4 : (s'=2);

[] s=2 -> (s'=3);

[] s=3 -> 0.6 : (s'=4) + 0.4 : (s'=2);

[] s=4 -> 0.6 : (s'=6) + 0.4 : (s'=5);

[] s=5 -> 1 : (s'=4);

[] s=6 -> (s'=6);

endmodule

=============================

[Dave Parker]

Hi Marek,

Have a look here for some common types of property:

https://prismmodelchecker.org/manual/PropertySpecification/ThePOperator

Fo your model, you could check for example "What is the probability of
getting to END without going through STOP": P=?[ !(s=2 | s=5) U s=6]

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/e958f240-d3c1-4820-a11c-b7dbe7cdaeccn%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/e958f240-d3c1-4820-a11c-b7dbe7cdaeccn%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Marek Golonka]

Thank you. The link that you gave me is already known by me because I already read tutorial during my past year. Is there any more simple examples how to use temporal logic in properties fold of Prim. I ask because I am planning to heavily base my doctoral thesis on Prism usage.Now I gather examples from autonomous car to be used during analysis in Prism.

best regards

Marek Golonka

AGH Doctoral Student

[Gethin Norman]

Hi Marek,

if you look at the different case studies:

http://www.prismmodelchecker.org/casestudies/index.php

these all have different properties that use temporal logic. Most are simple and should help you to understand how to use write properties in temporal logic.

You could also read the relevant chapters and do the exercises from a book on model checking such as:

Principles of Model Checking
Christel Baier, Joost-Pieter Katoen
MIT Press

thanks

Gethin

> To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchec...@googlegroups.com.
> To view this discussion on the web, visit https://groups.google.com/d/msgid/prismmodelchecker/3cf66a04-34fb-4c86-b617-8a4f8757f597n%40googlegroups.com.