Rens, GMeyer, TLakemeyer, G2015-01-142015-01-142014-03Rens, G, Meyer, T and Lakemeyer, G. 2014. A logic for specifying stochastic actions and observations. In: 8th International Symposium on Foundations of Information and Knowledge Systems (FoIKS), Bordeaux, France, 3-7 March 2014http://link.springer.com/chapter/10.1007%2F978-3-319-04939-7_15http://hdl.handle.net/10204/78448th International Symposium on Foundations of Information and Knowledge Systems (FoIKS), Bordeaux, France, 3-7 March 2014We present a logic inspired by partially observable Markov decision process (POMDP) theory for specifying agent domains where the agent's actuators and sensors are noisy (causing uncertainty). The language features modalities for actions and predicates for observations. It includes a notion of probability to represent the uncertainties, and the expression of rewards and costs are also catered for. One of the main contributions of the paper is the formulation of a sound and complete decision procedure for checking validity of sentences: a tableau method which appeals to solving systems of equations. The tableau rules eliminate propositional connectives, then, for all open branches of the tableau tree, systems of equations are generated and checked for feasibility. This paper presents progress made on previously published work.enPartially observable Markov decision processPOMDPSpecification LogicProbabilityConference PresentationRens, G., Meyer, T., & Lakemeyer, G. (2014). A logic for specifying stochastic actions and observations. Springer. http://hdl.handle.net/10204/7844Rens, G, T Meyer, and G Lakemeyer. "A logic for specifying stochastic actions and observations." (2014): http://hdl.handle.net/10204/7844Rens G, Meyer T, Lakemeyer G, A logic for specifying stochastic actions and observations; Springer; 2014. http://hdl.handle.net/10204/7844 .TY - Conference Presentation AU - Rens, G AU - Meyer, T AU - Lakemeyer, G AB - We present a logic inspired by partially observable Markov decision process (POMDP) theory for specifying agent domains where the agent's actuators and sensors are noisy (causing uncertainty). The language features modalities for actions and predicates for observations. It includes a notion of probability to represent the uncertainties, and the expression of rewards and costs are also catered for. One of the main contributions of the paper is the formulation of a sound and complete decision procedure for checking validity of sentences: a tableau method which appeals to solving systems of equations. The tableau rules eliminate propositional connectives, then, for all open branches of the tableau tree, systems of equations are generated and checked for feasibility. This paper presents progress made on previously published work. DA - 2014-03 DB - ResearchSpace DP - CSIR KW - Partially observable Markov decision process KW - POMDP KW - Specification Logic KW - Probability LK - https://researchspace.csir.co.za PY - 2014 T1 - A logic for specifying stochastic actions and observations TI - A logic for specifying stochastic actions and observations UR - http://hdl.handle.net/10204/7844 ER -