Automated adaptation via Quantitative Partial Model Checking

We propose a formal framework to model an automated adaptation protocol based on Quantitative Partial Model Checking (QPMC). An agent seeks the collaboration of a second agent to satisfy some (fixed) condition on the actions to be executed. The provided protocol allows the two agents to automatically agree by iteratively applying QPMC.