{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:04Z","timestamp":1740123364723,"version":"3.37.3"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:00:00Z","timestamp":1594684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:00:00Z","timestamp":1594684800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004871","name":"Technische Universit\u00e4t Braunschweig","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004871","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,10]]},"abstract":"Abstract<\/jats:title>We study the fine-grained complexity of Leader Contributor Reachability ($${\\textsf {LCR}} $$<\/jats:tex-math>\nLCR<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula>) and Bounded-Stage Reachability ($${\\textsf {BSR}} $$<\/jats:tex-math>\nBSR<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula>), two variants of the safety verification problem for shared memory concurrent programs. For both problems, the memory is a single variable over a finite data domain. Our contributions are new verification algorithms and lower bounds. The latter are based on the Exponential Time Hypothesis ($${\\textsf {ETH}} $$<\/jats:tex-math>\nETH<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula>), the problem $${\\textsf {Set~Cover}} $$<\/jats:tex-math>\n\nSet<\/mml:mi>\n\nCover<\/mml:mi>\n<\/mml:mrow>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula>, and cross-compositions. $${\\textsf {LCR}} $$<\/jats:tex-math>\nLCR<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula> is the question whether a designated leader thread can reach an unsafe state when interacting with a certain number of equal contributor threads. We suggest two parameterizations: (1) By the size of the data domain $${\\texttt {D}}$$<\/jats:tex-math>\nD<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula> and the size of the leader $${\\texttt {L}}$$<\/jats:tex-math>\nL<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula>, and (2) by the size of the contributors $${\\texttt {C}}$$<\/jats:tex-math>\nC<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula>. We present algorithms for both cases. The key techniques are compact witnesses and dynamic programming. The algorithms run in $${\\mathcal {O}}^*(({\\texttt {L}}\\cdot ({\\texttt {D}}+1))^{{\\texttt {L}}\\cdot {\\texttt {D}}} \\cdot {\\texttt {D}}^{{\\texttt {D}}})$$<\/jats:tex-math>\n\n\n\nO<\/mml:mi>\n<\/mml:mrow>\n\u2217<\/mml:mo>\n<\/mml:msup>\n\n(<\/mml:mo>\n\n\n(<\/mml:mo>\nL<\/mml:mi>\n\u00b7<\/mml:mo>\n\n(<\/mml:mo>\nD<\/mml:mi>\n+<\/mml:mo>\n1<\/mml:mn>\n)<\/mml:mo>\n<\/mml:mrow>\n)<\/mml:mo>\n<\/mml:mrow>\n\nL<\/mml:mi>\n\u00b7<\/mml:mo>\nD<\/mml:mi>\n<\/mml:mrow>\n<\/mml:msup>\n\u00b7<\/mml:mo>\n\n\nD<\/mml:mi>\n<\/mml:mrow>\nD<\/mml:mi>\n<\/mml:msup>\n)<\/mml:mo>\n<\/mml:mrow>\n<\/mml:mrow>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula> and $${\\mathcal {O}}^*(2^{{\\texttt {C}}})$$<\/jats:tex-math>\n\n\n\nO<\/mml:mi>\n<\/mml:mrow>\n\u2217<\/mml:mo>\n<\/mml:msup>\n\n(<\/mml:mo>\n\n2<\/mml:mn>\nC<\/mml:mi>\n<\/mml:msup>\n)<\/mml:mo>\n<\/mml:mrow>\n<\/mml:mrow>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula> time, showing that both parameterizations are fixed-parameter tractable. We complement the upper bounds by (matching) lower bounds based on $${\\textsf {ETH}} $$<\/jats:tex-math>\nETH<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula> and $${\\textsf {Set~Cover}} $$<\/jats:tex-math>\n\nSet<\/mml:mi>\n\nCover<\/mml:mi>\n<\/mml:mrow>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula>. Moreover, we prove the absence of polynomial kernels. For $${\\textsf {BSR}} $$<\/jats:tex-math>\nBSR<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula>, we consider programs involving $${\\texttt {t}}$$<\/jats:tex-math>\nt<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula> different threads. We restrict the analysis to computations where the write permission changes $${\\texttt {s}}$$<\/jats:tex-math>\ns<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula> times between the threads. $${\\textsf {BSR}} $$<\/jats:tex-math>\nBSR<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula> asks whether a given configuration is reachable via such an $${\\texttt {s}}$$<\/jats:tex-math>\ns<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula>-stage computation. When parameterized by $${\\texttt {P}}$$<\/jats:tex-math>\nP<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula>, the maximum size of a thread, and $${\\texttt {t}}$$<\/jats:tex-math>\nt<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula>, the interesting observation is that the problem has a large number of difficult instances. Formally, we show that there is no polynomial kernel, no compression algorithm that reduces the size of the data domain $${\\texttt {D}}$$<\/jats:tex-math>\nD<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula> or the number of stages $${\\texttt {s}}$$<\/jats:tex-math>\ns<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula> to a polynomial dependence on $${\\texttt {P}}$$<\/jats:tex-math>\nP<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula> and $${\\texttt {t}}$$<\/jats:tex-math>\nt<\/mml:mi>\n<\/mml:math><\/jats:alternatives><\/jats:inline-formula>. This indicates that symbolic methods may be harder to find for this problem.<\/jats:p>","DOI":"10.1007\/s10817-020-09572-x","type":"journal-article","created":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T02:02:21Z","timestamp":1594692141000},"page":"1419-1444","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Fine-Grained Complexity of Safety Verification"],"prefix":"10.1007","volume":"64","author":[{"given":"Peter","family":"Chini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Prakash","family":"Saivasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,14]]},"reference":[{"key":"9572_CR1","unstructured":"Atig, M.F., Bouajjani, A., Kumar, K.N., Saivasan, P.: On bounded reachability analysis of shared memory systems. In: FSTTCS, LIPIcs, vol. 29, pp. 611\u2013623. Schloss Dagstuhl (2014)"},{"key":"9572_CR2","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. In: TACAS, LNCS, vol. 5505, pp. 107\u2013123. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-00768-2_11"},{"key":"9572_CR3","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Touili, T.: On the reachability analysis of acyclic networks of pushdown systems. In: CONCUR, LNCS, vol. 5201, pp. 356\u2013371. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-85361-9_29"},{"issue":"2","key":"9572_CR4","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1007\/s00453-015-9981-1","volume":"74","author":"A Bj\u00f6rklund","year":"2016","unstructured":"Bj\u00f6rklund, A., Kaski, P., Kowalik, L.: Constrained multilinear detection and generalized graph motifs. Algorithmica 74(2), 947\u2013967 (2016)","journal-title":"Algorithmica"},{"issue":"8","key":"9572_CR5","first-page":"423","volume":"75","author":"HL Bodlaender","year":"2009","unstructured":"Bodlaender, H.L., Downey, R.G., Fellows, M.R., Hermelin, D.: On problems without polynomial kernels. JCSS 75(8), 423\u2013434 (2009)","journal-title":"JCSS"},{"issue":"1","key":"9572_CR6","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1137\/120880240","volume":"28","author":"HL Bodlaender","year":"2014","unstructured":"Bodlaender, H.L., Jansen, B.M.P., Kratsch, S.: Kernelization lower bounds by cross-composition. SIDAM 28(1), 277\u2013305 (2014)","journal-title":"SIDAM"},{"key":"9572_CR7","doi-asserted-by":"crossref","unstructured":"Calabro, C., Impagliazzo, R., Paturi, R.: The complexity of satisfiability of small depth circuits. In: IWPEC, LNCS, vol. 5917, pp. 75\u201385. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-11269-0_6"},{"key":"9572_CR8","doi-asserted-by":"crossref","unstructured":"Cantin, J.F., Lipasti, M.H., Smith, J.E.: The complexity of verifying memory coherence. In: SPAA, pp. 254\u2013255. ACM (2003)","DOI":"10.1145\/777412.777457"},{"key":"9572_CR9","unstructured":"Chini, P., Kolberg, J., Krebs, A., Meyer, R., Saivasan, P.: On the complexity of bounded context switching. In: ESA, LIPIcs, vol. 87, pp. 27:1\u201327:15. Schloss Dagstuhl (2017)"},{"key":"9572_CR10","doi-asserted-by":"crossref","unstructured":"Chini, P., Meyer, R., Saivasan, P.: Fine-grained complexity of safety verification. In: TACAS, LNCS, vol. 10806, pp. 20\u201337. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-89963-3_2"},{"key":"9572_CR11","doi-asserted-by":"crossref","unstructured":"Chini, P., Meyer, R., Saivasan, P.: Fine-grained complexity of safety verification. CoRR 2018. arXiv:1802.05559","DOI":"10.1007\/978-3-319-89963-3_2"},{"issue":"3","key":"9572_CR12","first-page":"41:1","volume":"12","author":"M Cygan","year":"2016","unstructured":"Cygan, M., Dell, H., Lokshtanov, D., Marx, D., Nederlof, J., Okamoto, Y., Paturi, R., Saurabh, S., Wahlstr\u00f6m, M.: On problems as hard as CNF-SAT. ACM TALG 12(3), 41:1\u201341:24 (2016)","journal-title":"ACM TALG"},{"key":"9572_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21275-3","volume-title":"Parameterized Algorithms","author":"M Cygan","year":"2015","unstructured":"Cygan, M., Fomin, F.V., Kowalik, \u0141., Lokshtanov, D., Marx, D., Pilipczuk, M., Pilipczuk, M., Saurabh, S.: Parameterized Algorithms. Springer, Berlin (2015)"},{"key":"9572_CR14","doi-asserted-by":"crossref","unstructured":"Demri, S., Laroussinie, F., Schnoebelen, P.: A parametric analysis of the state explosion problem in model checking. In: STACS, LNCS, vol. 2285, pp. 620\u2013631. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45841-7_51"},{"key":"9572_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-5559-1","volume-title":"Fundamentals of Parameterized Complexity","author":"RG Downey","year":"2013","unstructured":"Downey, R.G., Fellows, M.R.: Fundamentals of Parameterized Complexity. Springer, Berlin (2013)"},{"key":"9572_CR16","doi-asserted-by":"crossref","unstructured":"Durand-Gasselin, A., Esparza, J., Ganty, P., Majumdar, R.: Model checking parameterized asynchronous shared-memory systems. In: CAV, LNCS, vol. 9206, pp. 67\u201384. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-21690-4_5"},{"key":"9572_CR17","doi-asserted-by":"crossref","unstructured":"Enea, C., Farzan., A.: On atomicity in presence of non-atomic writes. In: TACAS, LNCS, vol. 9636, pp. 497\u2013514. Springer, Berlin (2016)","DOI":"10.1007\/978-3-662-49674-9_29"},{"key":"9572_CR18","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. In: CAV, LNCS, vol. 8044, pp. 124\u2013140. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39799-8_8"},{"issue":"3","key":"9572_CR19","doi-asserted-by":"publisher","first-page":"9:1","DOI":"10.1145\/2629644","volume":"36","author":"J Esparza","year":"2014","unstructured":"Esparza, J., Ganty, P., Poch, T.: Pattern-based verification for multithreaded programs. ACM TOPLAS 36(3), 9:1\u20139:29 (2014)","journal-title":"ACM TOPLAS"},{"key":"9572_CR20","doi-asserted-by":"crossref","unstructured":"Farzan, A., Madhusudan, P.: The complexity of predicting atomicity violations. In: TACAS, LNCS, vol. 5505, pp. 155\u2013169. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-00768-2_14"},{"issue":"4","key":"9572_CR21","first-page":"747","volume":"81","author":"H Fernau","year":"2015","unstructured":"Fernau, H., Heggernes, P., Villanger, Y.: A multi-parameter analysis of hard problems on deterministic finite automata. JCSS 81(4), 747\u2013765 (2015)","journal-title":"JCSS"},{"key":"9572_CR22","doi-asserted-by":"crossref","unstructured":"Fernau, H., Krebs, A.: Problems on finite automata and the exponential time hypothesis. In: CIAA, LNCS, vol. 9705, pp. 89\u2013100. Springer, Berlin (2016)","DOI":"10.1007\/978-3-319-40946-7_8"},{"key":"9572_CR23","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: ESOP, LNCS, vol. 2305, pp. 262\u2013277. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45927-8_19"},{"key":"9572_CR24","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: SPIN, LNCS, vol. 2648, pp. 213\u2013224. Springer, Berlin (2003)","DOI":"10.1007\/3-540-44829-2_14"},{"key":"9572_CR25","doi-asserted-by":"crossref","unstructured":"Fomin, F.V., Kratsch, D., Woeginger, G.J.: Exact (exponential) algorithms for the dominating set problem. In: WG, LNCS, vol. 3353, pp. 245\u2013256. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30559-0_21"},{"key":"9572_CR26","unstructured":"Fortin, M., Muscholl, A., Walukiewicz, I.: On parametrized verification of asynchronous, shared-memory pushdown systems. CoRR (2016). arXiv:1606.08707"},{"key":"9572_CR27","doi-asserted-by":"crossref","unstructured":"Fortin, M., Muscholl, A., Walukiewicz, I.: Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems. In: CAV, LNCS, vol. 10427, pp. 155\u2013175. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-63390-9_9"},{"issue":"1","key":"9572_CR28","first-page":"91","volume":"77","author":"L Fortnow","year":"2011","unstructured":"Fortnow, L., Santhanam, R.: Infeasibility of instance compression and succinct PCPs for NP. JCSS 77(1), 91\u2013106 (2011)","journal-title":"JCSS"},{"issue":"4","key":"9572_CR29","first-page":"63:1","volume":"14","author":"F Furbach","year":"2015","unstructured":"Furbach, F., Meyer, R., Schneider, K., Senftleben, M.: Memory-model-aware testing: A unified complexity analysis. ACM TECS 14(4), 63:1\u201363:25 (2015)","journal-title":"ACM TECS"},{"issue":"4","key":"9572_CR30","doi-asserted-by":"publisher","first-page":"1208","DOI":"10.1137\/S0097539794279614","volume":"26","author":"PB Gibbons","year":"1997","unstructured":"Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208\u20131244 (1997)","journal-title":"SIAM J. Comput."},{"key":"9572_CR31","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI, pp. 266\u2013277. ACM (2007)","DOI":"10.1145\/1273442.1250765"},{"key":"9572_CR32","unstructured":"Hague, M.: Parameterised pushdown systems with non-atomic writes. In: FSTTCS, LIPIcs, vol. 13, pp. 457\u2013468. Schloss Dagstuhl (2011)"},{"key":"9572_CR33","doi-asserted-by":"crossref","unstructured":"Hague, M., Lin, A.W.: Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In: CAV, LNCS, vol. 7358, pp. 260\u2013276. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31424-7_22"},{"key":"9572_CR34","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Meyer, R., Vojnar, T., Wolff, S.: Effect summaries for thread-modular analysis\u2013sound analysis despite an unsound heuristic. In: SAS, LNCS, vol. 10422, pp. 169\u2013191. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-66706-5_9"},{"issue":"2","key":"9572_CR35","first-page":"367","volume":"62","author":"R Impagliazzo","year":"2001","unstructured":"Impagliazzo, R., Paturi, R.: On the complexity of k-sat. JCSS 62(2), 367\u2013375 (2001)","journal-title":"JCSS"},{"key":"9572_CR36","doi-asserted-by":"crossref","unstructured":"Kahlon, V.: Parameterization as abstraction: a tractable approach to the dataflow analysis of concurrent programs. In: LICS, pp. 181\u2013192. IEEE (2008)","DOI":"10.1109\/LICS.2008.37"},{"key":"9572_CR37","doi-asserted-by":"crossref","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Complexity of Computer Computations, The IBM Research Symposia Series, pp. 85\u2013103. Plenum Press (1972)","DOI":"10.1007\/978-1-4684-2001-2_9"},{"key":"9572_CR38","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: CAV, LNCS, vol. 6174, pp. 629\u2013644. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6_54"},{"key":"9572_CR39","doi-asserted-by":"crossref","unstructured":"Lokshtanov, D., Marx, D., Saurabh, S.: Slightly superexponential parameterized problems. In: SODA, pp. 760\u2013776. SIAM (2011)","DOI":"10.1137\/1.9781611973082.60"},{"key":"9572_CR40","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: TACAS, LNCS, vol. 3440, pp. 93\u2013107. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"9572_CR41","doi-asserted-by":"crossref","unstructured":"Wareham, T.: The parameterized complexity of intersection and composition operations on sets of finite-state automata. In: CIAA, LNCS, vol. 2088, pp. 302\u2013310. Springer, Berlin (2000)","DOI":"10.1007\/3-540-44674-5_26"},{"key":"9572_CR42","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0304-3975(83)90020-8","volume":"26","author":"CK Yap","year":"1983","unstructured":"Yap, C.K.: Some consequences of non-uniform conditions on uniform classes. TCS 26, 287\u2013300 (1983)","journal-title":"TCS"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09572-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09572-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09572-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,14]],"date-time":"2021-07-14T00:16:25Z","timestamp":1626221785000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09572-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,14]]},"references-count":42,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["9572"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09572-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,7,14]]},"assertion":[{"value":"19 June 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 June 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 July 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}