{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:34:43Z","timestamp":1762522483863,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030576271"},{"type":"electronic","value":"9783030576288"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-57628-8_10","type":"book-chapter","created":{"date-parts":[[2020,8,24]],"date-time":"2020-08-24T23:19:22Z","timestamp":1598311162000},"page":"161-177","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Computation of the Transient in Max-Plus Linear Systems via SMT-Solving"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5627-9093","authenticated-orcid":false,"given":"Alessandro","family":"Abate","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1315-6990","authenticated-orcid":false,"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6370-1061","authenticated-orcid":false,"given":"Andrea","family":"Micheli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0817-1106","authenticated-orcid":false,"given":"Muhammad Syifa\u2019ul","family":"Mufid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,8,25]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., Cimatti, A., Micheli, A., Mufid, M.S.: Computation of the transient in max-plus linear systems via SMT-solving. arXiv e-prints, July 2020. https:\/\/arxiv.org\/abs\/2007.00505v2","DOI":"10.1007\/978-3-030-57628-8_10"},{"issue":"2","key":"10_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.3182\/20140514-3-FR-4046.00056","volume":"47","author":"D Adzkiya","year":"2014","unstructured":"Adzkiya, D., De Schutter, B., Abate, A.: Backward reachability of autonomous max-plus-linear systems. IFAC Proc. Vol. 47(2), 117\u2013122 (2014)","journal-title":"IFAC Proc. Vol."},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Alirezaei, M., van den Boom, T.J., Babuska, R.: Max-plus algebra for optimal scheduling of multiple sheets in a printer. In: Proceedings of the 31st American Control Conference (ACC), pp. 1973\u20131978, June 2012","DOI":"10.1109\/ACC.2012.6315457"},{"key":"10_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, New York (1992)"},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825\u2013885. IOS Press (2009). https:\/\/doi.org\/10.3233\/978-1-58603-929-5-825","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"10_CR6","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)","journal-title":"J. Theor. Biol."},{"issue":"2\u20133","key":"10_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1016\/j.laa.2006.10.004","volume":"421","author":"P Butkovi\u010d","year":"2007","unstructured":"Butkovi\u010d, P., Schneider, H., et al.: Generators, extremals and bases of max cones. Linear Algebra Appl. 421(2\u20133), 394\u2013406 (2007)","journal-title":"Linear Algebra Appl."},{"key":"10_CR8","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.dam.2016.11.003","volume":"219","author":"B Charron-Bost","year":"2017","unstructured":"Charron-Bost, B., F\u00fcgger, M., Nowak, T.: New transience bounds for max-plus linear systems. Discrete Appl. Math. 219, 83\u201399 (2017)","journal-title":"Discrete Appl. Math."},{"key":"10_CR9","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). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_9"},{"issue":"1","key":"10_CR10","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. Theoret. Comput. Sci. 293(1), 189\u2013217 (2003)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"issue":"1","key":"10_CR12","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10626-016-0235-4","volume":"27","author":"K Fahim","year":"2017","unstructured":"Fahim, K., Subiono, S., van der Woude, J.: On a generalization of power algorithms over max-plus algebra. Discrete Event Dyn. Syst. 27(1), 181\u2013203 (2017)","journal-title":"Discrete Event Dyn. Syst."},{"issue":"3","key":"10_CR13","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10801-010-0246-4","volume":"33","author":"S Gaubert","year":"2011","unstructured":"Gaubert, S., Katz, R.D.: Minimal half-spaces and external representation of tropical polyhedra. J. Algebraic Comb. 33(3), 325\u2013348 (2011)","journal-title":"J. Algebraic Comb."},{"key":"10_CR14","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":"10_CR15","doi-asserted-by":"crossref","unstructured":"Imaev, A., Judd, R.P.: Hierarchial modeling of manufacturing systems using max-plus algebra. In: Proceedings of the American Control Conference 2008, pp. 471\u2013476 (2008)","DOI":"10.1109\/ACC.2008.4586536"},{"key":"10_CR16","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.laa.2014.07.027","volume":"461","author":"G Merlet","year":"2014","unstructured":"Merlet, G., Nowak, T., Sergeev, S.: Weak CSR expansions and transience bounds in max-plus algebra. Linear Algebra Appl. 461, 163\u2013199 (2014)","journal-title":"Linear Algebra Appl."},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Mufid, M.S., Adzkiya, D., Abate, A.: Symbolic reachability analysis of high dimensional max-plus linear systems. arXiv e-prints, July 2020. https:\/\/arxiv.org\/abs\/2007.04510, accepted at the International Workshop on Discrete Event Systems (WODES)","DOI":"10.1016\/j.ifacol.2021.04.060"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-030-29662-9_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Syifaul Mufid","year":"2019","unstructured":"Syifaul Mufid, M., Adzkiya, D., Abate, A.: Bounded model checking of max-plus linear systems via predicate Abstractions. In: Andr\u00e9, \u00c9., Stoelinga, M. (eds.) FORMATS 2019. LNCS, vol. 11750, pp. 142\u2013159. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29662-9_9"},{"key":"10_CR19","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1090\/conm\/616\/12306","volume":"616","author":"T Nowak","year":"2014","unstructured":"Nowak, T., Charron-Bost, B.: An overview of transience bounds in max-plus algebra. Trop. Idempot. Math. Appl. 616, 277\u2013289 (2014)","journal-title":"Trop. Idempot. Math. Appl."},{"key":"10_CR20","unstructured":"Soto Y Koelemeijer, G.: On the behaviour of classes of min-max-plus systems. Ph.D. thesis, Delft University of Technology (2003)"}],"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-57628-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,9]],"date-time":"2022-11-09T19:28:21Z","timestamp":1668022101000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-57628-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030576271","9783030576288"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-57628-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"25 August 2020","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":"Vienna","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"formats2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/formats-2020.cs.ru.nl\/","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":"36","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":"16","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":"0","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":"44% - 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","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":"3","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)"}},{"value":"Due to the Corona pandemic FORMATS 2020 was held as a virtual event.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}