{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:19:01Z","timestamp":1737436741571,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540741275"},{"type":"electronic","value":"9783540741282"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-74128-2_7","type":"book-chapter","created":{"date-parts":[[2007,8,27]],"date-time":"2007-08-27T06:05:15Z","timestamp":1188194715000},"page":"95-112","source":"Crossref","is-referenced-by-count":0,"title":["Bounded Model Checking Real-Time Multi-agent Systems with Clock Differences: Theory and Implementation"],"prefix":"10.1007","author":[{"given":"Alessio","family":"Lomuscio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bo\u017cena","family":"Wo\u017ana","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"Zbrzezny","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/BFb0014737","volume-title":"Hybrid and Real-Time Systems","author":"E. Asarin","year":"1997","unstructured":"Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Data-structures for the verification of Timed Automata. In: Maler, O. (ed.) HART 1997. LNCS, vol.\u00a01201, pp. 346\u2013360. Springer, Heidelberg (1997)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"1999","unstructured":"Behrmann, G., Larsen, K., Pearson, J., Weise, C., Yi, W.: Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 341\u2013353. Springer, Heidelberg (1999)"},{"issue":"2-3","key":"7_CR3","doi-asserted-by":"crossref","first-page":"145","DOI":"10.3233\/FI-1998-36233","volume":"36","author":"B. B\u00e9rard","year":"1998","unstructured":"B\u00e9rard, B., Petit, A., Diekert, V., Gastin, P.: Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae\u00a036(2-3), 145\u2013182 (1998)","journal-title":"Fundamenta Informaticae"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/11603009_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"P. Bouyer","year":"2005","unstructured":"Bouyer, P., Laroussinie, F., Reynier, P.: Diagonal constraints in timed automata: Forward analysis of timed systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol.\u00a03829, pp. 112\u2013126. Springer, Heidelberg (2005)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV2: An open-source tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/3-540-36577-X_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Dembi\u0144ski","year":"2003","unstructured":"Dembi\u0144ski, P., Janowska, A., Janowski, P., Penczek, W., P\u00f3lrola, A., Szreter, M., Wo\u017ana, B., Zbrzezny, A.: VerICS: A tool for verifying Timed Automata and Estelle specifications. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 278\u2013283. Springer, Heidelberg (2003)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D. Dill","year":"1990","unstructured":"Dill, D.: Timing assumptions and verification of finite state concurrent systems. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"key":"7_CR9","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSat, http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/"},{"key":"7_CR10","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)"},{"key":"7_CR11","first-page":"638","volume-title":"Proceedings of the Third International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004)","author":"M. Kacprzak","year":"2004","unstructured":"Kacprzak, M., Lomuscio, A., Penczek, W.: Verification of multiagent systems via unbounded model checking. In: Jennings, N.R., Sierra, C., Sonenberg, L., Tambe, M. (eds.) Proceedings of the Third International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004), vol.\u00a0II, pp. 638\u2013645. ACM, New York (2004)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/11691372_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Lomuscio","year":"2006","unstructured":"Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 450\u2013454. Springer, Heidelberg (2006)"},{"issue":"1","key":"7_CR13","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/j.jal.2004.01.005","volume":"2","author":"A. Lomuscio","year":"2004","unstructured":"Lomuscio, A., Sergot, M.: A formalisation of violation, error recovery, and enforcement in the bit transmission problem. Journal of Applied Logic\u00a02(1), 93\u2013116 (2004)","journal-title":"Journal of Applied Logic"},{"key":"7_CR14","unstructured":"Lomuscio, A., Wo\u017ana, B., Zbrzezny, A.: Bounded model checking real-time multi-agent systems with clock differences: theory and implementation. Technical Report RN\/06\/03, Department of Computer Science, University College London, Gower Street, London WC1E 6BT, United Kingdom (2006)"},{"key":"7_CR15","unstructured":"Nabialek, W., Niewiadomski, A., Penczek, W., P\u00f3lrola, A., Szreter, M.: VerICS 2004: A model checker for real time and multi-agent systems. In: Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P 2004), Informatik-Berichte,Humboldt University, vol. 170, pp. 88\u201399 (2004)"},{"issue":"2","key":"7_CR16","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"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-45739-9_17","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"W. Penczek","year":"2002","unstructured":"Penczek, W., Wo\u017ana, B., Zbrzezny, A.: Towards bounded model checking for the universal fragment of TCTL. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 265\u2013288. Springer, Heidelberg (2002)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic, 2007. Special issue on Logic-based agent verification (to appear, 2007)","DOI":"10.1016\/j.jal.2005.12.010"},{"issue":"1","key":"7_CR19","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1023\/A:1008734703554","volume":"18","author":"S. Tripakis","year":"2001","unstructured":"Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design\u00a018(1), 25\u201368 (2001)","journal-title":"Formal Methods in System Design"},{"key":"7_CR20","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1109\/CSFW.2004.1310747","volume-title":"Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW 2004)","author":"R. Meyden van der","year":"2004","unstructured":"van der Meyden, R., Su, K.: Symbolic model checking the knowledge of the dining cryptographers. In: Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW 2004), pp. 280\u2013291. IEEE Computer Society Press, Washington, DC, USA (2004)"},{"key":"7_CR21","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1145\/1082473.1082498","volume-title":"Proceedings of the 4st International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2005)","author":"B. Wo\u017ana","year":"2005","unstructured":"Wo\u017ana, B., Lomuscio, A., Penczek, W.: Bounded model checking for knowledge over real time. In: Proceedings of the 4st International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2005), July 2005, vol.\u00a01, pp. 165\u2013172. ACM Press, New York (2005)"},{"issue":"1-3","key":"7_CR22","first-page":"303","volume":"67","author":"A. Zbrzezny","year":"2005","unstructured":"Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae\u00a067(1-3), 303\u2013322 (2005)","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","Model Checking and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74128-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T17:24:14Z","timestamp":1737393854000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74128-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540741275","9783540741282"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74128-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}