{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T04:16:47Z","timestamp":1749010607358,"version":"3.41.0"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319398822"},{"type":"electronic","value":"9783319398839"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-39883-9_4","type":"book-chapter","created":{"date-parts":[[2016,5,31]],"date-time":"2016-05-31T07:49:06Z","timestamp":1464680946000},"page":"45-55","source":"Crossref","is-referenced-by-count":3,"title":["Efficient Model Checking Timed and Weighted Interpreted Systems Using SMT and SAT Solvers"],"prefix":"10.1007","author":[{"given":"Agnieszka M.","family":"Zbrzezny","sequence":"first","affiliation":[]},{"given":"Andrzej","family":"Zbrzezny","sequence":"additional","affiliation":[]},{"given":"Franco","family":"Raimondi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,1]]},"reference":[{"unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)","key":"4_CR1"},{"key":"4_CR2","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning About Knowledge","author":"R Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)"},{"doi-asserted-by":"crossref","unstructured":"Bouyer, P., Markey, N., Sankur, O.: Robust weighted timed automata and games. In: Proceedings of FORMATS 2013, pp. 31\u201346 (2013)","key":"4_CR3","DOI":"10.1007\/978-3-642-40229-6_3"},{"key":"4_CR4","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1016\/j.tcs.2014.03.007","volume":"546","author":"KG Larsen","year":"2014","unstructured":"Larsen, K.G., Mardare, Radu: Complete proof systems for weighted modal logic. Theor. Comput. Sci. 546, 164\u2013175 (2014)","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: The theory of timed automata. In: Proceedings of REX Workshop, pp. 45\u201373 (1991)","key":"4_CR5","DOI":"10.1007\/BFb0031987"},{"doi-asserted-by":"crossref","unstructured":"Wo\u017ana-Szcze\u015bniak, B., Zbrzezny, A.: Checking EMTLK properties of timed interpreted systems via bounded model checking. Stud. Logica 1\u201338 (2015)","key":"4_CR6","DOI":"10.1007\/s11225-015-9637-9"},{"doi-asserted-by":"crossref","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. In: Proceedings of CAV\u20192009. LNCS, vol. 5643, pp. 682\u2013688. Springer (2009)","key":"4_CR7","DOI":"10.1007\/978-3-642-02658-4_55"},{"doi-asserted-by":"crossref","unstructured":"Gammie, P., van\u00a0der Meyden, R.: MCK: model checking the logic of knowledge. In: Proceedings of CAV\u20192004, LNCS, vol. 3114, pp. 479\u2013483. Springer (2004)","key":"4_CR8","DOI":"10.1007\/978-3-540-27813-9_41"},{"doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Proceedings of TOOLS 2002, pp. 200\u2013204 (2002)","key":"4_CR9","DOI":"10.1007\/3-540-46029-2_13"},{"doi-asserted-by":"crossref","unstructured":"Zbrzezny, A.M., Zbrzezny, A.: Checking WECTLK properties of timed real-weighted interpreted systems via SMT-based bounded model checking. In: Proceedings of EPIA 2015. LNCS, vol. 9273, pp. 638\u2013650. Springer (2015)","key":"4_CR10","DOI":"10.1007\/978-3-319-23485-4_64"},{"doi-asserted-by":"crossref","unstructured":"Wo\u017ana-Szcze\u015bniak, B., Zbrzezny, A.M., Zbrzezny, A.: SAT\u2013based bounded model checking for weighted interpreted systems and weighted linear temporal logic. In: Proceedings of PRIMA\u20192013. LNAI, vol. 8291, pp. 355\u2013371. Springer (2013)","key":"4_CR11","DOI":"10.1007\/978-3-642-44927-7_24"},{"issue":"3\u20134","key":"4_CR12","first-page":"377","volume":"120","author":"A Zbrzezny","year":"2012","unstructured":"Zbrzezny, A.: A new translation from ECTL $$^*$$ to SAT. Fundamenta Informaticae 120(3\u20134), 377\u2013397 (2012)","journal-title":"Fundamenta Informaticae"},{"doi-asserted-by":"crossref","unstructured":"Zbrzezny, A.M., Zbrzezny, A.: Checking WELTLK properties of weighted interpreted systems via SMT\u2013based bounded model checking. In: Proceedings of PRIMA 2015. LNCS, vol. 9387, pp. 660\u2013669. Springer (2015)","key":"4_CR13","DOI":"10.1007\/978-3-319-25524-8_49"},{"doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proceedings of TACAS\u20192008. LNCS, vol. 4963, pp. 337\u2013340. Springer (2008)","key":"4_CR14","DOI":"10.1007\/978-3-540-78800-3_24"},{"unstructured":"Biere, A.: PicoSAT essentials. J. Satisfiability, Boolean Model. Comput. (JSAT) 4, 75\u201397 (2008)","key":"4_CR15"}],"container-title":["Smart Innovation, Systems and Technologies","Agent and Multi-Agent Systems: Technology and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-39883-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T20:02:07Z","timestamp":1748980927000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-39883-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319398822","9783319398839"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-39883-9_4","relation":{},"ISSN":["2190-3018","2190-3026"],"issn-type":[{"type":"print","value":"2190-3018"},{"type":"electronic","value":"2190-3026"}],"subject":[],"published":{"date-parts":[[2016]]}}}