{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T09:51:20Z","timestamp":1747216280424,"version":"3.40.5"},"reference-count":0,"publisher":"IOS Press","isbn-type":[{"type":"print","value":"9781643684369"},{"type":"electronic","value":"9781643684376"}],"license":[{"start":{"date-parts":[[2023,9,28]],"date-time":"2023-09-28T00:00:00Z","timestamp":1695859200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,9,28]]},"abstract":"<jats:p>The paper presents a novel SMT-based method for testing the satisfiability of formulae that express strategic properties of timed multi-agent systems represented by networks of timed automata. Strategic Metric Temporal Logic (SMTL) is introduced, which extends Metric Temporal Logic (MTL) with strategy operators. SMTL is interpreted over maximal continuous time runs of timed automata. We define a procedure that synthesises a model for a given SMTL formula if such a model exists. The method exploits Satisfiability Modulo Theories (SMT) techniques and Parametric Bounded Model Checking algorithms. The presented approach enables bounded satisfiability checking, where the model is partially given and needs to be completed in line with the given specification. Our method has been implemented, and its application is demonstrated through an example of the well-known dining philosophers problem extended with clocks and strategies. The experimental results are quite encouraging.<\/jats:p>","DOI":"10.3233\/faia230394","type":"book-chapter","created":{"date-parts":[[2023,9,29]],"date-time":"2023-09-29T09:11:24Z","timestamp":1695978684000},"source":"Crossref","is-referenced-by-count":0,"title":["SMT-Based Satisfiability Checking of Strategic Metric Temporal Logic"],"prefix":"10.3233","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9464-7686","authenticated-orcid":false,"given":"Magdalena","family":"Kacprzak","sequence":"first","affiliation":[{"name":"Faculty of Computer Science, Bialystok University of Technology, Bialystok, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9652-5092","authenticated-orcid":false,"given":"Artur","family":"Niewiadomski","sequence":"additional","affiliation":[{"name":"Siedlce University, Faculty of Exact and Natural Sciences, Siedlce, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6477-4863","authenticated-orcid":false,"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[{"name":"Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2771-9683","authenticated-orcid":false,"given":"Andrzej","family":"Zbrzezny","sequence":"additional","affiliation":[{"name":"Faculty of Science and Technology, Jan Dlugosz University in Czestochowa, Czestochowa, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"7437","container-title":["Frontiers in Artificial Intelligence and Applications","ECAI 2023"],"original-title":[],"link":[{"URL":"https:\/\/ebooks.iospress.nl\/pdf\/doi\/10.3233\/FAIA230394","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,29]],"date-time":"2023-09-29T09:11:26Z","timestamp":1695978686000},"score":1,"resource":{"primary":{"URL":"https:\/\/ebooks.iospress.nl\/doi\/10.3233\/FAIA230394"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,28]]},"ISBN":["9781643684369","9781643684376"],"references-count":0,"URL":"https:\/\/doi.org\/10.3233\/faia230394","relation":{},"ISSN":["0922-6389","1879-8314"],"issn-type":[{"type":"print","value":"0922-6389"},{"type":"electronic","value":"1879-8314"}],"subject":[],"published":{"date-parts":[[2023,9,28]]}}}