Paper: "Planning for Automated Vehicles with Human Trust" Shili Sheng, Erfan Pakdamanian, Kyungtae Han, Ziran Wang, John Lenneman, David Parker and Lu Feng
Included below are the models and properties for the POMDP analysed with PRISM. In particular, this illustrates the definitions of rewards structures, required for the different objectives.
Single-objective queries in the properties file can be used with the standard version of PRISM; multi-objective queries (currently commented out) require an extension of PRISM, to be released shortly.