SAT-based Bounded Model Checking for Weighted Deontic Interpreted Systems
Bożena Woźna-Szcześniak · Fundamenta Informaticae · 2016
We present WECTL*KD, a weighted branching time temporal logic to specify knowledge, and correct functioning behaviour in multi-agent systems (MAS). We interpret the formulae of the logic over models generated by weighted deontic interpreted systems (WDIS). Furthermore, we investigate a SAT-based bo unded model checking (BMC) technique for WDIS and for WECTL*KD.