{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:24:30Z","timestamp":1742912670996,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030591519"},{"type":"electronic","value":"9783030591526"}],"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-59152-6_28","type":"book-chapter","created":{"date-parts":[[2020,10,11]],"date-time":"2020-10-11T23:02:35Z","timestamp":1602457355000},"page":"501-517","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Minimal Witnesses for Probabilistic Timed Automata"],"prefix":"10.1007","author":[{"given":"Simon","family":"Jantsch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Funke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christel","family":"Baier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,10,12]]},"reference":[{"issue":"1","key":"28_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2\u201334 (1993). https:\/\/doi.org\/10.1006\/inco.1993.1024","journal-title":"Inf. Comput."},{"issue":"2","key":"28_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-01702-5_15","volume-title":"Hardware and Software: Verification and Testing","author":"ME Andr\u00e9s","year":"2009","unstructured":"Andr\u00e9s, M.E., D\u2019Argenio, P., van Rossum, P.: Significant diagnostic counterexamples in probabilistic model checking. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 129\u2013148. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-01702-5_15"},{"key":"28_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804090","volume-title":"Computational Complexity - A Modern Approach","author":"S Arora","year":"2009","unstructured":"Arora, S., Barak, B.: Computational Complexity - A Modern Approach. Cambridge University Press, Cambridge (2009)"},{"key":"28_CR5","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). MIT Press, Cambridge (2008)"},{"issue":"1","key":"28_CR6","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0304-3975(01)00215-8","volume":"292","author":"D Beauquier","year":"2003","unstructured":"Beauquier, D.: On probabilistic timed automata. Theor. Comput. Sci. 292(1), 65\u201384 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(01)00215-8","journal-title":"Theor. Comput. Sci."},{"key":"28_CR7","doi-asserted-by":"publisher","unstructured":"Behrmann, G., et al.: Uppaal 4.0. In: Quantitative Evaluation of Systems, QEST (2006). https:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87\u2013124. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27755-2_3"},{"key":"28_CR9","doi-asserted-by":"publisher","unstructured":"Berendsen, J., Jansen, D.N., Katoen, J.: Probably on time and within budget: on reachability in priced probabilistic timed automata. In: Quantitative Evaluation of Systems QEST (2006). https:\/\/doi.org\/10.1109\/QEST.2006.43","DOI":"10.1109\/QEST.2006.43"},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-030-30942-8_8","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"M \u010ce\u0161ka","year":"2019","unstructured":"\u010ce\u0161ka, M., Hensel, C., Junges, S., Katoen, J.-P.: Counterexample-driven synthesis for probabilistic program sketches. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 101\u2013120. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_8"},{"key":"28_CR11","doi-asserted-by":"publisher","unstructured":"Chen, T., Han, T., Katoen, J.: Time-abstracting bisimulation for probabilistic timed automata. In: International Symposium on Theoretical Aspects of Software Engineering, pp. 177\u2013184 (2008). https:\/\/doi.org\/10.1109\/TASE.2008.29","DOI":"10.1109\/TASE.2008.29"},{"key":"28_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-75454-1_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"H Dierks","year":"2007","unstructured":"Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 114\u2013129. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_10"},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"DL Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197\u2013212. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_17"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-030-45190-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Funke","year":"2020","unstructured":"Funke, F., Jantsch, S., Baier, C.: Farkas certificates and minimal witnesses for probabilistic reachability constraints. TACAS 2020. LNCS, vol. 12078, pp. 324\u2013345. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_18"},{"key":"28_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-0924-6_17","volume-title":"Polytopes: Abstract Convex and Computational","author":"P Gritzmann","year":"1994","unstructured":"Gritzmann, P., Klee, V.: On the complexity of some basic problems in computational convexity. In: Bisztriczky, T., McMullen, P., Schneider, R., Weiss, A.I. (eds.) Polytopes: Abstract Convex and Computational. Springer, Dordrecht (1994). https:\/\/doi.org\/10.1007\/978-94-011-0924-6_17"},{"key":"28_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-70545-1_16","volume-title":"Computer Aided Verification","author":"H Hermanns","year":"2008","unstructured":"Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 162\u2013175. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_16"},{"key":"28_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-642-24372-1_33","volume-title":"Automated Technology for Verification and Analysis","author":"N Jansen","year":"2011","unstructured":"Jansen, N., \u00c1brah\u00e1m, E., Katelaan, J., Wimmer, R., Katoen, J.-P., Becker, B.: Hierarchical counterexamples for discrete-time Markov chains. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 443\u2013452. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_33"},{"key":"28_CR18","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.scico.2014.02.001","volume":"91","author":"N Jansen","year":"2014","unstructured":"Jansen, N., et al.: Symbolic counterexample generation for large discrete-time Markov chains. Sci. Comput. Program. 91, 90\u2013114 (2014). https:\/\/doi.org\/10.1016\/j.scico.2014.02.001","journal-title":"Sci. Comput. Program."},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Jantsch, S., Funke, F., Baier, C.: Minimal witnesses for probabilistic timed automata. arXiv:2007.00637 (2020)","DOI":"10.1007\/978-3-030-59152-6_28"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-642-04081-8_28","volume-title":"CONCUR 2009 - Concurrency Theory","author":"M Jurdzi\u0144ski","year":"2009","unstructured":"Jurdzi\u0144ski, M., Kwiatkowska, M., Norman, G., Trivedi, A.: Concavely-priced probabilistic timed automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 415\u2013430. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04081-8_28"},{"key":"28_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-540-71209-1_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Jurdzi\u0144ski","year":"2007","unstructured":"Jurdzi\u0144ski, M., Laroussinie, F., Sproston, J.: Model checking probabilistic timed automata with one or two clocks. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 170\u2013184. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_15"},{"key":"28_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-030-25540-4_5","volume-title":"Computer Aided Verification","author":"M K\u00f6lbl","year":"2019","unstructured":"K\u00f6lbl, M., Leue, S., Wies, T.: Clock bound repair for timed systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 79\u201396. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_5"},{"issue":"1","key":"28_CR23","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101\u2013150 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00046-9","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"28_CR24","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s001650300007","volume":"14","author":"M Kwiatkowska","year":"2003","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Form. Asp. Comput. 14(3), 295\u2013318 (2003). https:\/\/doi.org\/10.1007\/s001650300007","journal-title":"Form. Asp. Comput."},{"key":"28_CR25","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"MZ Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Form. Method Syst. Des. 29, 33\u201378 (2006). https:\/\/doi.org\/10.1007\/s10703-006-0005-2","journal-title":"Form. Method Syst. Des."},{"issue":"7","key":"28_CR26","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"MZ Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027\u20131077 (2007). https:\/\/doi.org\/10.1016\/j.ic.2007.01.004","journal-title":"Inf. Comput."},{"issue":"6","key":"28_CR27","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1016\/j.ipl.2007.01.003","volume":"102","author":"F Laroussinie","year":"2007","unstructured":"Laroussinie, F., Sproston, J.: State explosion in almost-sure probabilistic reachability. Inf. Process. Lett. 102(6), 236\u2013241 (2007). https:\/\/doi.org\/10.1016\/j.ipl.2007.01.003","journal-title":"Inf. Process. Lett."},{"key":"28_CR28","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/s10703-012-0177-x","volume":"43","author":"G Norman","year":"2013","unstructured":"Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Form. Methods Syst. Des. 43, 164\u2013190 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0177-x","journal-title":"Form. Methods Syst. Des."},{"issue":"12","key":"28_CR29","doi-asserted-by":"publisher","first-page":"2302","DOI":"10.1287\/mnsc.1100.1248","volume":"56","author":"\u00d6 \u00d6zpeynirci","year":"2010","unstructured":"\u00d6zpeynirci, \u00d6., K\u00f6ksalan, M.: An exact algorithm for finding extreme supported nondominated points of multiobjective mixed integer programs. Manag. Sci. 56(12), 2302\u20132315 (2010). https:\/\/doi.org\/10.1287\/mnsc.1100.1248","journal-title":"Manag. Sci."},{"issue":"1","key":"28_CR30","doi-asserted-by":"publisher","first-page":"020039","DOI":"10.1063\/1.5090006","volume":"2070","author":"W Pettersson","year":"2019","unstructured":"Pettersson, W., Ozlen, M.: Multi-objective mixed integer programming: an objective space algorithm. AIP Conf. Proc. 2070(1), 020039 (2019). https:\/\/doi.org\/10.1063\/1.5090006","journal-title":"AIP Conf. Proc."},{"key":"28_CR31","doi-asserted-by":"publisher","unstructured":"Sproston, J.: Discrete-time verification and control for probabilistic rectangular hybrid automata. In: Eight International Conference on Quantitative Evaluation of Systems, QEST 2011, pp. 79\u201388 (2011). https:\/\/doi.org\/10.1109\/QEST.2011.18","DOI":"10.1109\/QEST.2011.18"},{"key":"28_CR32","unstructured":"Tripakis, S.: L\u2019analyse formelle des syst\u00e8mes temporis\u00e8s en pratique. Ph.D. thesis, Universit\u00e9 Joseph Fourier (1998)"},{"key":"28_CR33","doi-asserted-by":"publisher","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Katoen, J.P.: High-level counterexamples for probabilistic automata. Log. Methods Comput. Sci. 11(1) (2015). https:\/\/doi.org\/10.2168\/LMCS-11(1:15)2015","DOI":"10.2168\/LMCS-11(1:15)2015"},{"key":"28_CR34","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.tcs.2014.06.020","volume":"549","author":"R Wimmer","year":"2014","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Katoen, J., Becker, B.: Minimal counterexamples for linear-time probabilistic verification. Theor. Comput. Sci. 549, 61\u2013100 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2014.06.020","journal-title":"Theor. Comput. Sci."},{"key":"28_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-030-45190-5_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Wimmer","year":"2020","unstructured":"Wimmer, S., Mutius, J.: Verified certification of reachability checking for timed automata. TACAS 2020. LNCS, vol. 12078, pp. 425\u2013443. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_24"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-59152-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,7]],"date-time":"2021-04-07T23:48:26Z","timestamp":1617839306000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-59152-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030591519","9783030591526"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-59152-6_28","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":"12 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hanoi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vietnam","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":"19 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 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":"atva2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/fit.uet.vnu.edu.vn\/atva2020\/","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":"75","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":"27","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":"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","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":"6","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)"}}]}}