SMT4SMTL: A Tool for SMT-Based Satisfiability Checking of SMTL

Artur Niewiadomski (University of Siedlce), Maciej Nazarczuk (University of Siedlce), Mateusz Przychodzki (University of Siedlce), Magdalena Kacprzak (Bialystok University of Technology), Wojciech Penczek (Institute of Computer Science, PAS), Andrzej Zbrzezny (Jan Dlugosz University in Czestochowa)

Abstract

We present SMT4SMTL-the first tool for deciding the bounded satisfiability of Metric Temporal Logic (MTL) and the existential fragment of Strategic Metric Temporal Logic (SMTL), interpreted over timed multi-agent systems represented by networks of timed automata. The tool combines Satisfiability Modulo Theories (SMT) techniques and Parametric Bounded Model Checking algorithms.