We present techniques for verifying strategic abilities of multi-agent systems via SAT-based and Max-SAT-based bounded model checking. In our approach we focus on systems of agents that pursue goals with regard to the ...

In this article, we revise our constraint-based abstraction refinement technique for checking temporal logic properties of concurrent software systems. Our technique employs predicate abstraction and SAT-based three-valued ...

We present a technique for verifying concurrent software systems via SAT-based three-valued bounded model checking. It is based on a direct transfer of the system to be analysed and a temporal logic property into a ...