SLAP: Specification logic of actions with probability |
| |
Affiliation: | 1. Centre for Artificial Intelligence Research, University of KwaZulu-Natal, and CSIR Meraka, South Africa;2. RWTH Aachen University, Germany |
| |
Abstract: | A logic for specifying probabilistic transition systems is presented. Our perspective is that of agents performing actions. A procedure for deciding whether sentences in this logic are valid is provided. One of the main contributions of the paper is the formulation of the decision procedure: a tableau system which appeals to solving systems of linear equations. The tableau rules eliminate propositional connectives, then, for all open branches of the tableau tree, systems of linear equations are generated and checked for feasibility. Proofs of soundness, completeness and termination of the decision procedure are provided. |
| |
Keywords: | Probabilistic actions Modal logic Tableau method Systems of linear inequalities |
本文献已被 ScienceDirect 等数据库收录! |
|