{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T23:47:13Z","timestamp":1761954433761,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032068460","type":"print"},{"value":"9783032068477","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:00:00Z","timestamp":1761955200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:00:00Z","timestamp":1761955200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-06847-7_4","type":"book-chapter","created":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T23:42:28Z","timestamp":1761954148000},"page":"66-87","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["0-1 Laws for\u00a0LTL and\u00a0CTL over\u00a0Random Transition Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5577-4845","authenticated-orcid":false,"given":"Yanni","family":"Dong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5687-854X","authenticated-orcid":false,"given":"Milan","family":"Lopuha\u00e4-Zwakenberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6793-8165","authenticated-orcid":false,"given":"Mari\u00eblle","family":"Stoelinga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,1]]},"reference":[{"key":"4_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1126\/science.286.5439.509","volume":"286","author":"AL Barab\u00e1si","year":"1999","unstructured":"Barab\u00e1si, A.L., Albert, R.: Emergence of scaling in random networks. Science 286, 509\u2013512 (1999)","journal-title":"Science"},{"issue":"1\u20133","key":"4_CR3","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/S0019-9958(85)80027-9","volume":"67","author":"A Blass","year":"1985","unstructured":"Blass, A., Gurevich, Y., Kozen, D.: A zero-one law for logic with a fixed-point operator. Inf. Control 67(1\u20133), 70\u201390 (1985)","journal-title":"Inf. Control"},{"issue":"3","key":"4_CR4","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1002\/jgt.3190030305","volume":"3","author":"A Blass","year":"1979","unstructured":"Blass, A., Harary, F.: Properties of almost all graphs and complexes. J. Graph Theor. 3(3), 225\u2013240 (1979)","journal-title":"J. Graph Theor."},{"issue":"25","key":"4_CR5","doi-asserted-by":"publisher","first-page":"15879","DOI":"10.1073\/pnas.252631999","volume":"99","author":"F Chung","year":"2002","unstructured":"Chung, F., Lu, L.: The average distances in random graphs with given expected degrees. Proc. Natl. Acad. Sci. 99(25), 15879\u201315882 (2002)","journal-title":"Proc. Natl. Acad. Sci."},{"key":"4_CR6","unstructured":"Compton, K.: 0-1 laws in logic and combinatorics. In: Rival, I. (ed.) Proceedings of the NATO Advanced Study Institute on Algorithms and Order, pp. 1\u201329. D. Reidel, Dordrecht (1988)"},{"issue":"4","key":"4_CR7","first-page":"351","volume":"98","author":"A Dawar","year":"2010","unstructured":"Dawar, A., Gr\u00e4del, E.: Properties of almost all graphs and generalized quantifiers. Fund. Inform. 98(4), 351\u2013372 (2010)","journal-title":"Fund. Inform."},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"290","DOI":"10.5486\/PMD.1959.6.3-4.12","volume":"6","author":"P Erd\u00f6s","year":"1959","unstructured":"Erd\u00f6s, P., R\u00e9nyi, A.: On random graphs I. Publicationes Mathematicae Debrecen 6, 290\u2013297 (1959)","journal-title":"Publicationes Mathematicae Debrecen"},{"issue":"1","key":"4_CR9","doi-asserted-by":"publisher","first-page":"50","DOI":"10.2307\/2272945","volume":"41","author":"R Fagin","year":"1976","unstructured":"Fagin, R.: Probabilities on finite models. J. Symbolic Logic 41(1), 50\u201358 (1976)","journal-title":"J. Symbolic Logic"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1023\/B:AUSE.0000028537.84347.9c","volume":"11","author":"M Franceschet","year":"2004","unstructured":"Franceschet, M., Montanari, A., Rijke, M.: Model checking for combined logics with an application to mobile systems. Autom. Softw. Eng. 11, 289\u2013321 (2004)","journal-title":"Autom. Softw. Eng."},{"key":"4_CR11","volume-title":"Introduction to Random Graphs","author":"A Frieze","year":"2016","unstructured":"Frieze, A., Karo\u0144ski, M.: Introduction to Random Graphs. Cambridge University Press, Cambridge (2016)"},{"issue":"1\u20132","key":"4_CR12","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1002\/(SICI)1098-2418(199701\/03)10:1\/2<5::AID-RSA2>3.0.CO;2-Z","volume":"10","author":"A Frieze","year":"1997","unstructured":"Frieze, A., McDiarmid, C.: Algorithmic theory of random graphs. Random Struct. Algorithms 10(1\u20132), 5\u201342 (1997)","journal-title":"Random Struct. Algorithms"},{"issue":"2","key":"4_CR13","first-page":"142","volume":"5","author":"YV Glebskii","year":"1969","unstructured":"Glebskii, Y.V., Kogan, D.I., Liogon\u2019kii, M.I., Talanov, V.A.: Range and degree of realizability of formulas in the restricted predicate calculus. Cybern. Syst. Analysis, Translated Kibernetika 5(2), 142\u2013154 (1969)","journal-title":"Cybern. Syst. Analysis, Translated Kibernetika"},{"issue":"3","key":"4_CR14","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1016\/S0019-9958(83)80043-6","volume":"57","author":"E Grandjean","year":"1983","unstructured":"Grandjean, E.: Complexity of the first-order theory of almost all finite structures. Inf. Control 57(3), 180\u2013204 (1983)","journal-title":"Inf. Control"},{"key":"4_CR15","unstructured":"Haber, S., Hershko, T., Mirabi, M., Shelah, S.: First-order logic with equicardinality in random graphs. In: Endrullis, J., Schmitz, S. (eds.) 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0326, pp. 12:1\u201312:17. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2025)"},{"key":"4_CR16","unstructured":"van Hee, K.M., Liu, Z.: Generating benchmarks by random stepwise refinement of Petri nets. In: Donatelli, S., Kleijn, J., Machado, R.J., Fernandes, J.M. (eds.) Proceedings of the Workshops of the 31st International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (PETRI NETS 2010) and of the 10th International Conference on Application of Concurrency to System Design (ACSD 2010), Braga, Portugal, June, 2010. CEUR Workshop Proceedings, vol.\u00a0827, pp. 403\u2013417. CEUR-WS.org (2010)"},{"key":"4_CR17","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1016\/j.jctb.2017.12.002","volume":"130","author":"P Heinig","year":"2018","unstructured":"Heinig, P., M\u00fcller, T., Noy, M., Taraz, A.: Logical limit laws for minor-closed classes of graphs. J. Comb. Theory Ser. B 130, 158\u2013206 (2018)","journal-title":"J. Comb. Theory Ser. B"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Huisman, M., Wijs, A.: Concise Guide to Software Verification - From Model Checking to Annotation Checking, 2. Texts in Computer Science, Springer (2023)","DOI":"10.1007\/978-3-031-30167-4"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Hussain, I., Csallner, C., Grechanik, M., Fu, C., Xie, Q., Park, S., Taneja, K., Hossain, B.M.M.: Evaluating program analysis and testing tools with the rugrat random benchmark application generator. In: Proceedings of the Ninth International Workshop on Dynamic Analysis, pp. 1\u20136. WODA 2012, Association for Computing Machinery, New York, NY, USA (2012)","DOI":"10.1145\/2338966.2336798"},{"key":"4_CR20","unstructured":"Kaufmann, M.: A counterexample to the 0-1 law for existential monadic second-order logic. Computational Logic Inc, pp.\u00a01\u20135 (1988)"},{"issue":"3","key":"4_CR21","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/0012-365X(85)90112-8","volume":"54","author":"M Kaufmann","year":"1985","unstructured":"Kaufmann, M., Shelah, S.: On random models of finite power and monadic logic. Discret. Math. 54(3), 285\u2013293 (1985)","journal-title":"Discret. Math."},{"key":"4_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0171-7","volume-title":"Automata Theory and Its Applications","author":"B Khoussainov","year":"2001","unstructured":"Khoussainov, B., Nerode, A.: Automata Theory and Its Applications. Birkhauser Boston Inc, USA (2001)"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Kolaitis, P.G., Vardi, M.Y.: The decision problem for the probabilities of higher-order properties. In: Proceedings of the Nineteenth Annual ACM Symposium on Theory of Computing, pp. 425\u2013435. STOC \u201987, Association for Computing Machinery, New York (1987)","DOI":"10.1145\/28395.28441"},{"issue":"2","key":"4_CR24","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1016\/0890-5401(92)90021-7","volume":"98","author":"PG Kolaitis","year":"1992","unstructured":"Kolaitis, P.G., Vardi, M.Y.: Infinitary logics and 0\u20131 laws. Inf. Comput. 98(2), 258\u2013294 (1992)","journal-title":"Inf. Comput."},{"issue":"1","key":"4_CR25","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1002\/rsa.3240030105","volume":"3","author":"JF Lynch","year":"1992","unstructured":"Lynch, J.F.: Probabilities of sentences about very sparse random graphs. Random Struct. Algorithms 3(1), 33\u201353 (1992)","journal-title":"Random Struct. Algorithms"},{"key":"4_CR26","doi-asserted-by":"publisher","DOI":"10.1016\/j.spl.2021.109061","volume":"173","author":"YA Malyshkin","year":"2021","unstructured":"Malyshkin, Y.A., Zhukovskii, M.E.: MSO 0\u20131 law for recursive random trees. Stat. Probab. Lett. 173, 109061 (2021)","journal-title":"Stat. Probab. Lett."},{"issue":"5","key":"4_CR27","doi-asserted-by":"publisher","first-page":"1045","DOI":"10.1002\/j.1538-7305.1955.tb03788.x","volume":"34","author":"GH Mealy","year":"1955","unstructured":"Mealy, G.H.: A method for synthesizing sequential circuits. Bell Syst. Tech. J. 34(5), 1045\u20131079 (1955)","journal-title":"Bell Syst. Tech. J."},{"key":"4_CR28","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780199206650.001.0001","volume-title":"Networks: An Introduction","author":"ME Newman","year":"2010","unstructured":"Newman, M.E.: Networks: An Introduction. Oxford University Press, Oxford (2010)"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: 20th Annual IEEE Symposium on Logic in Computer Science, pp. 188\u2013197. LICS\u2019 05, IEEE, Chicago (2005)","DOI":"10.1109\/LICS.2005.33"},{"key":"4_CR30","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1147\/rd.32.0114","volume":"3","author":"M Rabin","year":"1959","unstructured":"Rabin, M., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3, 114\u2013125 (1959)","journal-title":"IBM J. Res. Dev."},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Razafimahatratra, A.S., Zhukovskii, M.E.: Zero\u2013one laws for k-variable first-order logic of sparse random graphs. Discrete Appl. Math. 276, 121\u2013128 (2020), 2nd Russian\u2013Hungarian Combinatorial Workshop","DOI":"10.1016\/j.dam.2019.02.032"},{"key":"4_CR32","unstructured":"Scheidgen, M.: Generation of large random models for benchmarking. In: Kolovos, D.S., Ruscio, D.D., Matragkas, N.D., Cuadrado, J.S., R\u00e1th, I., Tisi, M. (eds.) Proceedings of the 3rd Workshop on Scalable Model Driven Engineering part of the Software Technologies: Applications and Foundations (STAF 2015) Federation of Conferences, L\u2019Aquila, Italy, July 23, 2015. CEUR Workshop Proceedings, vol.\u00a01406, pp. 1\u201310. CEUR-WS.org (2015)"},{"key":"4_CR33","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-319-23534-9_18","volume-title":"Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday","author":"S Shelah","year":"2015","unstructured":"Shelah, S.: On failure of 0\u20131 laws. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, pp. 293\u2013296. Springer, Cham (2015)"},{"issue":"3","key":"4_CR34","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"issue":"1","key":"4_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2275320","volume":"58","author":"J Spencer","year":"1993","unstructured":"Spencer, J.: Zero-one laws with variable probability. J. Symb. Log. 58(1), 1\u201314 (1993)","journal-title":"J. Symb. Log."},{"key":"4_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04538-1","volume-title":"The Strange Logic of Random Graphs","author":"J Spencer","year":"2001","unstructured":"Spencer, J.: The Strange Logic of Random Graphs. Springer, New York (2001)"},{"key":"4_CR37","unstructured":"Talanov, V.: Asymptotic solvability of logical formulas. Comb.-Algebraic Methods Appl. Math., 118\u2013126 (1981)"},{"key":"4_CR38","unstructured":"Talanov, V., Knyazev, V.: The asymptotic truth of infinite formulas. In: Proceedings of All-Union Seminar on Discrete and Applied Mathematics and Its Applications, pp. 56\u201361 (1986)"},{"key":"4_CR39","unstructured":"TOOLS2009 - International Workshop on Graph-Based Tools (GraBaTs\u20192009): Satellite workshop to TOOLS 2009 (2009). http:\/\/is.tm.tue.nl\/staff\/pvgorp\/events\/grabats2009\/"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06847-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T23:42:31Z","timestamp":1761954151000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06847-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,1]]},"ISBN":["9783032068460","9783032068477"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06847-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,1]]},"assertion":[{"value":"1 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}