LOGICS TOWARDS POMDP WITH AND/OR WITHOUT REWARDS

Reachability anaysis in continuous-time Markov decision processes
Logics towards POMDP with and/or without rewards
Energy consumption in Ad-Hoc and Sensor Networks
Stochastic Interfaces
An eclipse environment for Modest (finished)
Analysis of an Airbag Control Unit (finished)

Title

Logics towards POMDP (with and/or without rewards)


Content

The paper [ZHJ05] introduced the logic POCTL* for the discrete-time HMMs, which can be considered as DTMCs but with hidden states. With POCTL* one can express state-based, path-based and believe-state based properties over discrete-time HMMs. The authors presented the model checking algorithm of POCTL* over discrete-time HMMs.

 

De Alfaro introduced the model checking algorithm of the logic PCTL* over the model DTMDPs, where a state have to choose first an action nondeterministically, and then a successor state according a probabilistic distribution based on the selected action. This thesis should extend the logics POCTL* for HMMs and PCTL* for DTMDPs such that it can be interpreted over POMDPs, the partially observable Markov decision processes. Also model checking algorithms should be investigated.


Status

Available.

 


Contact

Lijun Zhang


References

[ZHJ05]: Lijun Zhang, Holger Hermanns, and David N. Jansen. Logic and model checking for hidden markov models. AVACS Technical Report No. 6, SFB/TR 14 AVACS, July 2005. ISSN: 1860-9821, www.avacs.org. This report is the full version of a paper which appeared in FORTE'05