{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T20:34:15Z","timestamp":1742934855534,"version":"3.40.3"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720155"},{"type":"electronic","value":"9783030720162"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Timed automata (TA) have shown to be a suitable formalism for modeling real-time systems. Moreover, modern model-checking tools allow a designer to check whether a TA complies with the system specification. However, the exact timing constraints of the system are often uncertain during the design phase. Consequently, the designer is able to build a TA with a correct structure, however, the timing constraints need to be tuned to make the TA comply with the specification.<\/jats:p><jats:p>In this work, we assume that we are given a TA together with an existential property, such as reachability, that is not satisfied by the TA. We propose a novel concept of a minimal sufficient reduction (MSR) that allows us to identify the minimal set<jats:italic>S<\/jats:italic>of timing constraints of the TA that needs to be tuned to meet the specification. Moreover, we employ mixed-integer linear programming to actually find a tuning of<jats:italic>S<\/jats:italic>that leads to meeting the specification.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_16","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"291-310","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Timed Automata Relaxation for Reachability"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9784-3028","authenticated-orcid":false,"given":"Jaroslav","family":"Bend\u00edk","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4275-4655","authenticated-orcid":false,"given":"Ahmet","family":"Sencan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5813-9836","authenticated-orcid":false,"given":"Ebru Aydin","family":"Gol","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0711-9552","authenticated-orcid":false,"given":"Ivana","family":"\u010cern\u00e1","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Abdedda\u00efm, Y., Maler, O.: Job-shop scheduling using timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification. pp.478\u2013492. Springer Berlin Heidelberg, Berlin, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_46","DOI":"10.1007\/3-540-44585-4_46"},{"key":"16_CR2","doi-asserted-by":"publisher","unstructured":"Aichernig, B.K., Lorber, F., Ni\u010dkovi\u0107, D.: Time for mutants \u2014 model-based mutation testing with timed automata. In: Veanes, M., Vigan\u00f2, L. (eds.) Tests and Proofs. pp. 20\u201338. Springer Berlin Heidelberg, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38916-0_2","DOI":"10.1007\/978-3-642-38916-0_2"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R.: Timed automata. In: International Conference on Computer Aided Verification. pp. 8\u201322. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_3","DOI":"10.1007\/3-540-48683-6_3"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical computer science 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"16_CR5","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9.: A benchmark library for parametric timed model checking. In: Artho, C., \u00d6lveczky, P.C. (eds.) Formal Techniques for Safety-Critical Systems. pp. 75\u201383. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-12988-0_5","DOI":"10.1007\/978-3-030-12988-0_5"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, E.: What\u2019s decidable about parametric timed automata? Int. J. Softw. Tools Technol. Transf. 21(2), 203\u2013219 (Apr 2019). https:\/\/doi.org\/10.1007\/s10009-017-0467-0","DOI":"10.1007\/s10009-017-0467-0"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Arcaini, P., Gargantini, A., Radavelli, M.: Repairing timed automata clock guards through abstraction and testing. In: Beyer, D., Keller, C. (eds.) Tests and Proofs. pp. 129\u2013146. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31157-5_9","DOI":"10.1007\/978-3-030-31157-5_9"},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Chatain, T., De\u00a0Smet, O., Fribourg, L., Ruel, S.: Synth\u00e8se de contraintes temporis\u00e9es pour une architectured\u2019automatisation en r\u00e9seau. Journal Europ\u00e9en des Syst\u00e8mesAutomatis\u00e9s 43 (November 2009). https:\/\/doi.org\/10.3166\/jesa.43.1049-1064","DOI":"10.3166\/jesa.43.1049-1064"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., K\u00fchne, U., Soulat, R.: Imitator 2.5: A tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012: Formal Methods. pp. 33\u201336. Springer Berlin Heidelberg, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_6","DOI":"10.1007\/978-3-642-32759-9_6"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., Mota, J.M., Soulat, R.: Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking. In: Enea, C., Piskac, R. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 409\u2013424. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_19","DOI":"10.1007\/978-3-030-11245-5_19"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Hasuo, I., Waga, M.: Offline timed pattern matchingunder uncertainty. In: ICECCS. pp. 10\u201320. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/ICECCS2018.2018.00010","DOI":"10.1109\/ICECCS2018.2018.00010"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Knapik, M., Lime, D., Penczek, W., Petrucci, L.: Parametric verification: An introduction. Trans. Petri Nets Other Model. Concurr. 14, 64\u2013100 (2019). https:\/\/doi.org\/10.1007\/978-3-662-60651-3_3","DOI":"10.1007\/978-3-662-60651-3_3"},{"key":"16_CR13","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Lipari, G., Nguyen, H.G., Sun, Y.: Reachability preservation based parameter synthesis for timed automata. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NASA Formal Methods. pp. 50\u201365. Springer International Publishing, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_5","DOI":"10.1007\/978-3-319-17524-9_5"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Bacchus, F., Katsirelos, G.: Finding a collection of muses incrementally. In: CPAIOR. Lecture Notes in Computer Science, vol. 9676, pp. 35\u201344. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-33954-2_3","DOI":"10.1007\/978-3-319-33954-2_3"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"de\u00a0la Banda, M.G., Stuckey, P.J., Wazny, J.: Finding all minimal unsatisfiable subsets. In: PPDP. pp. 32\u201343. ACM (2003). https:\/\/doi.org\/10.1145\/888251.888256","DOI":"10.1145\/888251.888256"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Barnat, J., Bauch, P., Bene\u0161, N., Brim, L., Beran, J., Kratochv\u00edla, T.: Analysing sanity of requirements for avionics systems. FAoC pp. 1\u201319 (2016). https:\/\/doi.org\/10.1007\/s00165-015-0348-9","DOI":"10.1007\/s00165-015-0348-9"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems. pp. 125\u2013126. QEST \u201906, IEEE Computer Society, Washington, DC, USA (2006). https:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"16_CR18","doi-asserted-by":"publisher","unstructured":"Bend\u00edk, J.: Consistency checking in requirements analysis. In: ISSTA. pp. 408\u2013411. ACM (2017). https:\/\/doi.org\/10.1145\/3092703.3098239","DOI":"10.1145\/3092703.3098239"},{"key":"16_CR19","doi-asserted-by":"publisher","unstructured":"Bend\u00edk, J., Bene\u0161, N., \u010cern\u00e1, I., Ji\u0159\u00ed: Tunable online MUS\/MSS enumeration. In: FSTTCS. LIPIcs, vol.\u00a065, pp. 50:1\u201350:13. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2016.50","DOI":"10.4230\/LIPIcs.FSTTCS.2016.50"},{"key":"16_CR20","doi-asserted-by":"publisher","unstructured":"Bend\u00edk, J., \u010cern\u00e1, I.: Replication-guided enumeration of minimal unsatisfiable subsets. In: CP. LNCS, vol. 12333, pp. 37\u201354. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-58475-7_3","DOI":"10.1007\/978-3-030-58475-7_3"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Bend\u00edk, J., \u010cern\u00e1, I.: Rotation based MSS\/MCS enumeration. In: LPAR. EPiC Series in Computing, vol.\u00a073, pp. 120\u2013137. EasyChair (2020). https:\/\/doi.org\/10.29007\/8btb","DOI":"10.29007\/8btb"},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"Bend\u00edk, J., \u010cern\u00e1, I., Bene\u0161, N.: Recursive online enumeration of all minimal unsatisfiable subsets. In: ATVA. Lecture Notes in Computer Science, vol. 11138, pp. 143\u2013159. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_9","DOI":"10.1007\/978-3-030-01090-4_9"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Bend\u00edk, J., Ghassabani, E., Whalen, M.W., \u010cern\u00e1, I.: Online enumeration of all minimal inductive validity cores. In: SEFM. Lecture Notes in Computer Science, vol. 10886, pp. 189\u2013204. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-92970-5_12","DOI":"10.1007\/978-3-319-92970-5_12"},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Bene\u0161, N., Bezd\u011bk, P., Larsen, K.G., Srba, J.: Language emptiness of continuous-time parametric timed automata. In: ICALP (2). Lecture Notes in Computer Science, vol.\u00a09135, pp. 69\u201381. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_6","DOI":"10.1007\/978-3-662-47666-6_6"},{"key":"16_CR25","doi-asserted-by":"publisher","unstructured":"Bezd\u011bk, P., Bene\u0161, N., Barnat, J., \u010cern\u00e1, I.: LTL parameter synthesis of parametric timed automata. In: De\u00a0Nicola, R., K\u00fchn, E. (eds.) Software Engineering and Formal Methods. pp. 172\u2013187. Springer International Publishing, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41591-8_12","DOI":"10.1007\/978-3-319-41591-8_12"},{"key":"16_CR26","doi-asserted-by":"publisher","unstructured":"Bezd\u011bk, P., Bene\u0161, N., \u010cern\u00e1, I., Barnat, J.: On clock-aware LTL parameter synthesis of timed automata. J. Log. Algebraic Methods Program. 99, 114\u2013142 (2018). https:\/\/doi.org\/10.1016\/j.jlamp.2018.05.004","DOI":"10.1016\/j.jlamp.2018.05.004"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Bouyer, P., Brihaye, T., Bruy\u00e8re, V., Raskin, J.F.: On the optimal reachability problem of weighted timed automata. Formal Methods in System Design 31, 135\u2013175 (2007). https:\/\/doi.org\/10.1007\/s10703-007-0035-4","DOI":"10.1007\/s10703-007-0035-4"},{"key":"16_CR28","unstructured":"Collomb-Annichini, A., Sighireanu, M.: Parameterized reachability analysis of the IEEE 1394 root contention protocol using trex (08 2001)"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"David, A., Illum, J., Larsen, K.G., Skou, A.: Model-based framework for schedulability analysis using UPPAAL 4.1. In: Model-based design for embedded systems, pp. 117\u2013144 (2009)","DOI":"10.1201\/9781420067859-c4"},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Fehnker, A.: Scheduling a steel plant with timed automata. In: Proceedings Sixth International Conference on Real-Time Computing Systems and Applications. RTCSA\u201999 (Cat. No.PR00306). pp. 280\u2013286 (1999). https:\/\/doi.org\/10.1109\/RTCSA.1999.811256","DOI":"10.1109\/RTCSA.1999.811256"},{"key":"16_CR31","doi-asserted-by":"publisher","unstructured":"Feo-Arenis, S., Westphal, B., Dietsch, D., Mu\u00f1iz, M., Andisha, A.S.: The wireless fire alarm system: Ensuring conformance to industrial standards through formal verification. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods. pp. 658\u2013672. Springer International Publishing, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_44","DOI":"10.1007\/978-3-319-06410-9_44"},{"key":"16_CR32","doi-asserted-by":"publisher","unstructured":"Ghassabani, E., Whalen, M.W., Gacek, A.: Efficient generation of all minimal inductive validity cores. In: FMCAD. pp. 31\u201338. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102238","DOI":"10.23919\/FMCAD.2017.8102238"},{"key":"16_CR33","doi-asserted-by":"publisher","unstructured":"Guan, N., Gu, Z., Deng, Q., Gao, S., Yu, G.: Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking. In: Proc. of SEUS. pp. 263\u2013272 (2007). https:\/\/doi.org\/10.1007\/978-3-540-75664-4_26","DOI":"10.1007\/978-3-540-75664-4_26"},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Preussig, J., Wong-Toi, H.: Some lessons from the hytech experience. In: Proceedings of the 40th IEEE Conference on Decision and Control (Cat. No.01CH37228). vol.\u00a03, pp. 2887\u20132892 vol.3 (2001)","DOI":"10.1109\/CDC.2001.980714"},{"key":"16_CR35","doi-asserted-by":"publisher","unstructured":"Hoxha, B., Abbas, H., Fainekos, G.: Benchmarks for temporal logic requirements for automotive systems. In: Frehse, G., Althoff, M. (eds.) ARCH14-15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a034, pp. 25\u201330. EasyChair (2015). https:\/\/doi.org\/10.29007\/xwrs, https:\/\/easychair.org\/publications\/paper\/4bfq","DOI":"10.29007\/xwrs"},{"key":"16_CR36","doi-asserted-by":"publisher","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. In: Margaria, T., Yi, W. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 189\u2013203. Springer Berlin Heidelberg, Berlin, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_14","DOI":"10.1007\/3-540-45319-9_14"},{"key":"16_CR37","doi-asserted-by":"publisher","unstructured":"Ivrii, A., Malik, S., Meel, K.S., Vardi, M.Y.: On computing minimal independent support and its applications to sampling and counting. Constraints An Int. J. 21(1), 41\u201358 (2016). https:\/\/doi.org\/10.1007\/s10601-015-9204-z","DOI":"10.1007\/s10601-015-9204-z"},{"key":"16_CR38","doi-asserted-by":"publisher","unstructured":"Jiang, Z., Pajic, M., Alur, R., Mangharam, R.: Closed-loop verification of medical devices with model abstraction and refinement. Int. J. Softw. Tools Technol. Transf. 16(2), 191\u2013213 (Apr 2014). https:\/\/doi.org\/10.1007\/s10009-013-0289-7, https:\/\/doi.org\/10.1007\/s10009-013-0289-7","DOI":"10.1007\/s10009-013-0289-7"},{"key":"16_CR39","doi-asserted-by":"publisher","unstructured":"Jovanovic, A., Lime, D., Roux, O.H.: Integer parameter synthesis for real-time systems. IEEE Transactions on Software Engineering 41(5), 445\u2013461 (2015). https:\/\/doi.org\/10.1109\/TSE.2014.2357445","DOI":"10.1109\/TSE.2014.2357445"},{"key":"16_CR40","doi-asserted-by":"publisher","unstructured":"Jovanovi\u0107, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 401\u2013415. Springer Berlin Heidelberg, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_28","DOI":"10.1007\/978-3-642-36742-7_28"},{"key":"16_CR41","unstructured":"Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. Trans. Petri Nets Other Model. Concurr. 5, 141\u2013159 (2010)"},{"key":"16_CR42","doi-asserted-by":"publisher","unstructured":"K\u00f6lbl, M., Leue, S., Wies, T.: Clock bound repair for timed systems. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification. pp. 79\u201396. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_5","DOI":"10.1007\/978-3-030-25540-4_5"},{"key":"16_CR43","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Mereacre, A., Paoletti, N., Patan\u00e8, A.: Synthesising robust and optimal parameters for cardiac pacemakers using symbolic and evolutionary computation techniques. In: Abate, A., \u0160afr\u00e1nek, D. (eds.) Hybrid Systems Biology. pp. 119\u2013140. Springer International Publishing, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-26916-0_7","DOI":"10.1007\/978-3-319-26916-0_7"},{"key":"16_CR44","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Yi, W.: Time abstracted bisimulation: Implicit specifications and decidability. In: International Conference on Mathematical Foundations of Programming Semantics. pp. 160\u2013176. Springer (1993). https:\/\/doi.org\/10.1006\/inco.1997.2623","DOI":"10.1006\/inco.1997.2623"},{"key":"16_CR45","doi-asserted-by":"publisher","unstructured":"Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223\u2013250 (2016). https:\/\/doi.org\/10.1007\/s10601-015-9183-0","DOI":"10.1007\/s10601-015-9183-0"},{"key":"16_CR46","doi-asserted-by":"publisher","unstructured":"Lime, D., Roux, O.H., Seidner, C., Traonouez, L.: Romeo: A parametric model-checker for petri nets with stopwatches. In: TACAS. Lecture Notes in Computer Science, vol.\u00a05505, pp. 54\u201357. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_6","DOI":"10.1007\/978-3-642-00768-2_6"},{"key":"16_CR47","unstructured":"Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: IJCAI. pp. 615\u2013622. IJCAI\/AAAI (2013)"},{"key":"16_CR48","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in boolean formulae. In: CAV. Lecture Notes in Computer Science, vol.\u00a08044, pp. 592\u2013607. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_39","DOI":"10.1007\/978-3-642-39799-8_39"},{"key":"16_CR49","doi-asserted-by":"publisher","unstructured":"Marques-Silva, J., Janota, M., Menc\u00eda, C.: Minimal sets on propositional formulae. problems and reductions. Artif. Intell. 252, 22\u201350 (2017). https:\/\/doi.org\/10.1016\/j.artint.2017.07.005","DOI":"10.1016\/j.artint.2017.07.005"},{"key":"16_CR50","unstructured":"Perron, L., Furnon, V.: Or-tools, https:\/\/developers.google.com\/optimization\/"},{"key":"16_CR51","doi-asserted-by":"crossref","unstructured":"Sperner, E.: Ein satz \u00fcber untermengen einer endlichen menge. Mathematische Zeitschrift 27(1), 544\u2013548 (1928)","DOI":"10.1007\/BF01171114"},{"key":"16_CR52","doi-asserted-by":"publisher","unstructured":"Wang, F.: Formal verification of timed systems: a survey and perspective. Proceedings of the IEEE 92(8), 1283\u20131305 (Aug 2004). https:\/\/doi.org\/10.1109\/JPROC.2004.831210","DOI":"10.1109\/JPROC.2004.831210"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,26]],"date-time":"2024-08-26T11:50:19Z","timestamp":1724673019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","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":"141","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":"41","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":"21","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":"29% - 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":"12","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":"The conference changed to an online format due to the COVID-19 pandemic","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)"}}]}}