www.prismmodelchecker.org
[GKL21] Romulo Meira-Goes, Raymond H. Kwong and Stephane Lafortune. Synthesis of optimal multi-objective attack strategies for controlled systems modeled by probabilistic automata. IEEE Transactions on Automatic Control. 2021. [Considers multi-objective synthesis of attack strategies using MDP models and solution via PRISM.]
Links: [Google] [Google Scholar]

Publications