Group synthesis for parametric temporal-epistemic logic
Andrew V. Jones, Michał Knapik, Wojciech Penczek, Alessio R. Lomuscio · 2012
We investigate parameter synthesis in the context of temporal-epistemic logic. We introduce CTLPK, a parametric extension to the branching time temporal-epistemic logic CTLK with free variables representing groups of agents. We give algo-rithms for automatically synthesising the groups of agents that make a given parametric formula satisfied. We discuss an implementation of the technique on top of the open-source model checker mcmas and demonstrate its attractiveness by reporting the experimental results obtained.