STV+KH: Towards Practical Verification of Strategic Ability for Knowledge and Information Flow

Mateusz Kamiński (Institute of Computer Science, Polish Academy of Sciences & Faculty of Mathematics and Computer Science, Nicolaus Copernicus University in Toruń), Damian Kurpiewski (Institute of Computer Science, Polish Academy of Sciences & Faculty of Mathematics and Computer Science, Nicolaus Copernicus University in Toruń), Wojciech Jamroga (Interdisciplinary Centre for Security, Reliability and Trust, SnT, University of Luxembourg & Institute of Computer Science, Polish Academy of Sciences)

Abstract

We present an expanded version of our tool STV for model checking of strategic abilities. The new version adds support for knowledge and uncertainty operators, thus enabling the verification of properties such as privacy, anonymity, and strategic information flow. All of that is available through a web interface, with no need to install or configure the software by the user.