{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T01:05:36Z","timestamp":1725757536507},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642449260"},{"type":"electronic","value":"9783642449277"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-44927-7_24","type":"book-chapter","created":{"date-parts":[[2013,11,19]],"date-time":"2013-11-19T01:33:06Z","timestamp":1384824786000},"page":"355-371","source":"Crossref","is-referenced-by-count":6,"title":["SAT-Based Bounded Model Checking for Weighted Interpreted Systems and Weighted Linear Temporal Logic"],"prefix":"10.1007","author":[{"given":"Bo\u017cena","family":"Wo\u017ana-Szcze\u015bniak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Agnieszka M.","family":"Zbrzezny","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"Zbrzezny","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., Sergot, M.: Violation, error recovery, and enforcement in the bit transmission problem. Imperial College Press (2002)","DOI":"10.1145\/544862.544961"},{"key":"24_CR2","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT)\u00a04, 75\u201397 (2008)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation (JSAT)"},{"issue":"1","key":"24_CR3","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E. Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"key":"24_CR4","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"24_CR5","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, ch. 16, pp. 996\u20131071. Elsevier Science Publishers (1990)"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Fabre, E., Jezequel, L.: Distributed optimal planning: an approach by weighted automata calculus. In: Proceedings of CDC 2009, pp. 211\u2013216. IEEE (2009)","DOI":"10.1109\/CDC.2009.5400084"},{"key":"24_CR7","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press (1995)"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-540-27813-9_41","volume-title":"Computer Aided Verification","author":"P. Gammie","year":"2004","unstructured":"Gammie, P., van der Meyden, R.: MCK: Model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 479\u2013483. Springer, Heidelberg (2004)"},{"issue":"1-4","key":"24_CR9","first-page":"313","volume":"85","author":"M. Kacprzak","year":"2008","unstructured":"Kacprzak, M., Nabialek, W., Niewiadomski, A., Penczek, W., P\u00f3lrola, A., Szreter, M., Wo\u017ana, B., Zbrzezny, A.: VerICS 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae\u00a085(1-4), 313\u2013328 (2008)","journal-title":"Fundamenta Informaticae"},{"key":"24_CR10","unstructured":"Levesque, H.: A logic of implicit and explicit belief. In: Proceedings of the 6th National Conference of the AAAI, pp. 198\u2013202. Morgan Kaufman (1984)"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/978-3-642-02658-4_55","volume-title":"Computer Aided Verification","author":"A. Lomuscio","year":"2009","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 682\u2013688. Springer, Heidelberg (2009)"},{"issue":"1","key":"24_CR12","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1023\/A:1026176900459","volume":"75","author":"A. Lomuscio","year":"2003","unstructured":"Lomuscio, A., Sergot, M.: Deontic interpreted systems. Studia Logica\u00a075(1), 63\u201392 (2003)","journal-title":"Studia Logica"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: On model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"issue":"2","key":"24_CR14","first-page":"167","volume":"55","author":"W. Penczek","year":"2003","unstructured":"Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae\u00a055(2), 167\u2013185 (2003)","journal-title":"Fundamenta Informaticae"},{"issue":"3-4","key":"24_CR15","doi-asserted-by":"crossref","first-page":"373","DOI":"10.3233\/FI-2012-743","volume":"119","author":"W. Penczek","year":"2012","unstructured":"Penczek, W., Wo\u017ana-Szcze\u015bniak, B., Zbrzezny, A.: Towards SAT-based BMC for LTLK over Interleaved Interpreted Systems. Fundamenta Informaticae\u00a0119(3-4), 373\u2013392 (2012)","journal-title":"Fundamenta Informaticae"},{"key":"24_CR16","unstructured":"Wooldridge, M.: An introduction to multi-agent systems. John Wiley (2002)"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Wo\u017ana-Szcze\u015bniak, B.: SAT-based bounded model checking for weighted deontic interpreted systems. In: Correia, L., Reis, L.P., Cascalho, J. (eds.) EPIA 2013. LNCS, vol.\u00a08154, pp. 444\u2013455. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-40669-0_38"},{"issue":"3-4","key":"24_CR18","doi-asserted-by":"crossref","first-page":"377","DOI":"10.3233\/FI-2012-768","volume":"120","author":"A. Zbrzezny","year":"2012","unstructured":"Zbrzezny, A.: A new translation from ECTL* to SAT. Fundamenta Informaticae\u00a0120(3-4), 377\u2013397 (2012)","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","PRIMA 2013: Principles and Practice of Multi-Agent Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-44927-7_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,12]],"date-time":"2022-03-12T22:19:54Z","timestamp":1647123594000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-44927-7_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642449260","9783642449277"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-44927-7_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}