SMT-based Bounded Model Checking for Weighted Interpreted Systems and for Weighted Epistemic ECTL

We define the SMT-based bounded model checking (BMC) method for Weighted Interpreted Systems and for the existential fragment of the Weighted Epistemic Computation Tree Logic. We implemented the new BMC algorithm and compared it with the SATbased BMC method for the same systems and the same property language on several benchmarks for multi-agent systems.