{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T07:54:51Z","timestamp":1726041291532},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030296612"},{"type":"electronic","value":"9783030296629"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-29662-9_9","type":"book-chapter","created":{"date-parts":[[2019,8,19]],"date-time":"2019-08-19T19:03:06Z","timestamp":1566241386000},"page":"142-159","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions"],"prefix":"10.1007","author":[{"given":"Muhammad","family":"Syifa\u2019ul Mufid","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dieky","family":"Adzkiya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Abate","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,8,13]]},"reference":[{"issue":"12","key":"9_CR1","doi-asserted-by":"publisher","first-page":"3039","DOI":"10.1109\/TAC.2013.2273299","volume":"58","author":"D Adzkiya","year":"2013","unstructured":"Adzkiya, D., De Schutter, B., Abate, A.: Finite abstractions of max-plus-linear systems. IEEE Trans. Autom. Control. 58(12), 3039\u20133053 (2013). \n                      https:\/\/doi.org\/10.1109\/TAC.2013.2273299","journal-title":"IEEE Trans. Autom. Control."},{"issue":"1","key":"9_CR2","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10626-015-0218-x","volume":"26","author":"D Adzkiya","year":"2016","unstructured":"Adzkiya, D., Zhang, Y., Abate, A.: \n                      \n                        \n                      \n                      $$\\text{VeriSiMPL}$$\n                     2: an open-sourcesoftware for the verification of max-plus-linear systems. Discrete Event Dyn. Syst. 26(1), 109\u2013145 (2016). \n                      https:\/\/doi.org\/10.1007\/s10626-015-0218-x","journal-title":"Discrete Event Dyn. Syst."},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/3-540-36580-X_4","volume-title":"Hybrid Systems: Computation and Control","author":"R Alur","year":"2003","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107, F.: Progress on reachability analysis of hybrid systems using predicate abstraction. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 4\u201319. Springer, Heidelberg (2003). \n                      https:\/\/doi.org\/10.1007\/3-540-36580-X_4"},{"key":"9_CR4","volume-title":"Synchronization and Linearity: An Algebra for Discrete Event Systems","author":"F Baccelli","year":"1992","unstructured":"Baccelli, F., Cohen, G., Olsder, G.J., Quadrat, J.P.: Synchronization and Linearity: An Algebra for Discrete Event Systems. Wiley, Chichester (1992)"},{"key":"9_CR5","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"5","key":"9_CR6","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/381694.378846","volume":"36","author":"Thomas Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proceedings of Programming Language Design and Implementation 2001 (PLDI 2001), vol. 36, pp. 203\u2013213. ACM (2001). \n                      https:\/\/doi.org\/10.1145\/381694.378846","journal-title":"ACM SIGPLAN Notices"},{"key":"9_CR7","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 and 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.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). \n                      https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"issue":"11","key":"9_CR8","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y., et al.: Bounded model checking. Adv. Comput. 58(11), 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"issue":"5","key":"9_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-2(5:5)2006","volume":"2","author":"A Biere","year":"2006","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. 2(5), 1\u201364 (2006). \n                      https:\/\/doi.org\/10.2168\/LMCS-2(5:5)2006","journal-title":"Log. Methods Comput. Sci."},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1016\/j.jtbi.2012.03.007","volume":"303","author":"CA Brackley","year":"2012","unstructured":"Brackley, C.A., Broomhead, D.S., Romano, M.C., Thiel, M.: A Max-plus model of ribosome dynamics during mRNA translation. J. Theor. Biol. 303, 128\u2013140 (2012). \n                      https:\/\/doi.org\/10.1016\/j.jtbi.2012.03.007","journal-title":"J. Theor. Biol."},{"key":"9_CR11","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., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-45069-6_14","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Talupur, M., Wang, D.: Making predicate abstraction efficient. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 126\u2013140. Springer, Heidelberg (2003). \n                      https:\/\/doi.org\/10.1007\/978-3-540-45069-6_14"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-540-24622-0_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 85\u201396. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24622-0_9"},{"issue":"2\u20133","key":"9_CR15","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Form. Methods Syst. Des. 25(2\u20133), 105\u2013127 (2004). \n                      https:\/\/doi.org\/10.1023\/B:FORM.0000040025.89719.f3","journal-title":"Form. Methods Syst. Des."},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-24605-3_7","volume-title":"Theory and Applications of Satisfiability Testing","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Talupur, M., Veith, H., Wang, D.: SAT based predicate abstraction for hardware verification. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 78\u201392. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24605-3_7"},{"issue":"5","key":"9_CR17","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(5), 1512\u20131542 (1994). \n                      https:\/\/doi.org\/10.1145\/186025.186051","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"1","key":"9_CR18","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/S0304-3975(02)00237-2","volume":"293","author":"JP Comet","year":"2003","unstructured":"Comet, J.P.: Application of max-plus algebra to biological sequence comparisons. Theor. Comput. Sci. 293(1), 189\u2013217 (2003). \n                      https:\/\/doi.org\/10.1016\/S0304-3975(02)00237-2","journal-title":"Theor. Comput. Sci."},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160\u2013171. Springer, Heidelberg (1999). \n                      https:\/\/doi.org\/10.1007\/3-540-48683-6_16"},{"issue":"1\u20133","key":"9_CR20","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0024-3795(00)00013-6","volume":"307","author":"B Schutter De","year":"2000","unstructured":"De Schutter, B.: On the ultimate behavior of the sequence of consecutive powers of a matrix in the max-plus algebra. Linear Algebra Its Appl. 307(1\u20133), 103\u2013117 (2000). \n                      https:\/\/doi.org\/10.1016\/S0024-3795(00)00013-6","journal-title":"Linear Algebra Its Appl."},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proceedings of the 29th Principles of Programming Languages (POPL 2002), vol. 37, pp. 191\u2013202. ACM (2002). \n                      https:\/\/doi.org\/10.1145\/503272.503291","DOI":"10.1145\/503272.503291"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). \n                      https:\/\/doi.org\/10.1007\/3-540-63166-6_10"},{"issue":"7","key":"9_CR23","doi-asserted-by":"publisher","first-page":"1085","DOI":"10.1016\/S0005-1098(01)00059-0","volume":"37","author":"W Heemels","year":"2001","unstructured":"Heemels, W., De Schutter, B., Bemporad, A.: Equivalence of hybrid dynamical models. Automatica 37(7), 1085\u20131091 (2001). \n                      https:\/\/doi.org\/10.1016\/S0005-1098(01)00059-0","journal-title":"Automatica"},{"key":"9_CR24","volume-title":"Max Plus at Work: Modeling and Analysis of Synchronized Systems: A Course on Max-Plus Algebra and Its Applications","author":"B Heidergott","year":"2014","unstructured":"Heidergott, B., Olsder, G.J., Van der Woude, J.: Max Plus at Work: Modeling and Analysis of Synchronized Systems: A Course on Max-Plus Algebra and Its Applications. Princeton University Press, Princeton (2014)"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11513988_10","volume-title":"Computer Aided Verification","author":"K Heljanko","year":"2005","unstructured":"Heljanko, K., Junttila, T., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 98\u2013111. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11513988_10"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the ACM Symposium on Principles of Programming Languages (POPL 2002), pp. 58\u201370 (2002). \n                      https:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/503272.503279"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Imaev, A., Judd, R.P.: Hierarchial modeling of manufacturing systems using max-plus algebra. In: Proceedings of American Control Conference 2008, pp. 471\u2013476 (2008)","DOI":"10.1109\/ACC.2008.4586536"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-540-30579-8_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Latvala","year":"2005","unstructured":"Latvala, T., Biere, A., Heljanko, K., Junttila, T.: Simple is better: efficient bounded model checking for past LTL. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 380\u2013395. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/978-3-540-30579-8_25"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-030-00151-3_16","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"MS Mufid","year":"2018","unstructured":"Mufid, M.S., Adzkiya, D., Abate, A.: Tropical abstractions of max-plus linear systems. In: Jansen, D.N., Prabhakar, P. (eds.) FORMATS 2018. LNCS, vol. 11022, pp. 271\u2013287. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-030-00151-3_16"},{"key":"9_CR30","unstructured":"Mufid, M.S., Adzkiya, D., Abate, A.: Bounded model checking of max-plus linear systems via predicate abstractions. arXiv e-prints \n                      arXiv:1907.03564\n                      \n                    , July 2019"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29662-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,19]],"date-time":"2019-08-19T19:04:19Z","timestamp":1566241459000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-29662-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030296612","9783030296629"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29662-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"13 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORMATS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Modeling and Analysis of Timed Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Amsterdam","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"formats2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/lipn.univ-paris13.fr\/formats2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"42","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4.4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}