AKR: A Model Checker for an Adaptative Probabilistic Knowing-How Logic

Abstract

We present AKR , a model checking tool for an adaptative probabilistic knowing-how epistemic logic. The tool takes as input the specification of a scenario modeled via a probabilistic LTS (in PRISM notation), a collection of regular expressions acting as agent’s perception, a knowing-how property, and checks whether the formula holds in the model under the given perception. The tool combines automata-based techniques with calls to the PRISM tool to compute the result. AKR is a publicly available, open-source tool entirely programmed in Python . We describe the tool’s architecture and illustrate its use via some examples.