A comparison of SMT-solvers for timed weighted interpreted systems

• Autorzy: Zbrzezny A. M.

Identyfikatory

DOI

10.16926/m.2016.21.15

• Języki publikacji: EN

Abstrakty

EN

We compare four SMT-solvers for the same SMT-based bounded model checking algorithm for multi-agent systems modelled by timed weighted interpreted systems and for properties expressed in the existential fragment of epistemic weighted linear-time temporal logic (WELTLK). To this end, we use the timed weighted generic pipeline paradigm (TWGPP) and the timed weighted train controller system (TWTCS). We consider several properties of the problems that can be expressed in WELTLK, and we present the performance evaluation of the mentioned bounded model checking method using four different SMT-solvers: Z3, Yices, CVC4 and Mathsat, by means of the running time and the memory used.

Słowa kluczowe

EN

SMT; model (BMC); multi-agent (MAS)

PL

SMT; model (BMC); system wieloagentowy (MAS)

• Wydawca: Wydawnictwo Uniwersytetu Humanistyczno-Przyrodniczego im. Jana Długosza w Częstochowie
• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2016
• Tom: Vol. 21
• Strony: 189--206
• Opis fizyczny: Bibliogr. 14 poz.,. rys., tab.

Twórcy

autor

Zbrzezny A. M.

• Jan Długosz University in Częstochowa Institute of Mathematics and Computer Science al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Bibliografia

• 1] Rajeev Alur and David L. Dill. The theory of timed automata. In Proceedings of REX Workshop, pages 45–73, 1991.
• [2] Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, pages 171–177, 2011.
• [3] Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko. Program verification as satisfiability modulo theories. In 10th International Workshop on Satisfiability Modulo Theories, SMT 2012, Manchester, UK, June 30 - July 1, 2012, pages 3–11, 2012.
• [4] Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust weighted timed automata and games. In Proceedings of FORMATS 2013, pages 31–46, 2013.
• [5] Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. The mathsat5 SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, pages 93–107, 2013.
• [6] E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [7] Bruno Dutertre. Yices 2.2. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pages 737–744, 2014.
• [8] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.
• [9] Kim G. Larsen and Radu Mardare. Complete proof systems for weighted modal logic. Theor. Comput. Sci., 546:164–175, 2014.
• [10] B. Wozna-Szczesniak and A. Zbrzezny. Checking EMTLK properties of timed interpreted systems via bounded model checking. Studia Logica, pages 1–38, 2015.
• [11] B. Wozna-Szczesniak, A. M. Zbrzezny, and A. Zbrzezny. SAT-based bounded model checking for weighted interpreted systems and weighted linear temporal logic. In Proceedings of PRIMA’2013, volume 8291 of LNAI, pages 355–371. Springer-Verlag, 2013.
• [12] Agnieszka M. Zbrzezny and Andrzej Zbrzezny. Checking WECTLK Properties of Timed Real-Weighted Interpreted Systems via SMT-Based Bounded Model Checking. In Proceedings of EPIA 2015, volume 9273 of LNCS, pages 638–650. Springer, 2015.
• [13] Agnieszka M. Zbrzezny and Andrzej Zbrzezny. Checking WELTLK properties of weighted interpreted systems via smt-based bounded model checking. In Proceedings of PRIMA 2015, volume 9387 of LNCS, pages 660–669. Springer, 2015.
• [14] Agnieszka M. Zbrzezny, Andrzej Zbrzezny, and Franco Raimondi. Efficient Model Checking Timed and Weighted Interpreted Systems Using SMT and SAT Solvers, pages 45–55. Springer International Publishing, 2016.