{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T13:58:05Z","timestamp":1773151085305,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540677703","type":"print"},{"value":"9783540450474","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722167_31","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T03:00:33Z","timestamp":1167447633000},"page":"403-418","source":"Crossref","is-referenced-by-count":147,"title":["Regular Model Checking"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcus","family":"Nilsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy info channels. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 305\u2013318. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0028754"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B., Nilsson, M.: Handling global conditions in parameterized system verification. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 134\u2013145. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48683-6_14"},{"key":"31_CR3","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098, 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pus- hdown Automata: Application to Model Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 1\u201312. Springer, Heidelberg (1996)","DOI":"10.1007\/3-540-61474-5_53"},{"key":"31_CR6","unstructured":"Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The power of QDDs. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol.\u00a01302. Springer, Heidelberg (1997)"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"[BH97] A. Bouajjani and P. Habermehl. Symbolic reachability analysis of _fo-channel systems with nonregular sets of con_gurations. In Proc. ICALP \u201997, volume 1256 of LNCS, 1997.","DOI":"10.1007\/3-540-63165-8_211"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Wolper, P.: Symbolic verification with periodic sets. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 55\u201367. Springer, Heidelberg (1994)","DOI":"10.1007\/3-540-58179-0_43"},{"issue":"1","key":"31_CR9","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0304-3975(92)90278-N","volume":"106","author":"D. Caucal","year":"1992","unstructured":"Caucal, D.: On the regular structure of prefix rewriting. Theoretical Computer Science\u00a0106(1), 61\u201386 (1992)","journal-title":"Theoretical Computer Science"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978. ACM, New York (1978)","DOI":"10.1145\/512760.512770"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0028751"},{"key":"31_CR13","doi-asserted-by":"crossref","unstructured":"Fribourg, L., Ols\u00e9n, H.: Reachability sets of parametrized rings as regular languages. In: Proc. 2nd INFINITY 1997. Electronical Notes in Theoretical Computer Science, vol.\u00a09. Elsevier Science Publishers, Amsterdam (1997)","DOI":"10.1016\/S1571-0661(05)80427-X"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems (extended abstract). In: Proc. Infinity 1997, Electronic Notes in Theoretical Computer Science, Bologna (August 1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"Halbwachs, N.: Delay Analysis in Synchronous Programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697. Springer, Heidelberg (1993)","DOI":"10.1007\/3-540-56922-7_28"},{"key":"31_CR16","doi-asserted-by":"crossref","unstructured":"Henriksen, J.G., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019. Springer, Heidelberg (1995) (to appear)","DOI":"10.7146\/brics.v2i21.19923"},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, p. 220. Springer, Heidelberg (2000)","DOI":"10.1007\/3-540-46419-0_16"},{"key":"31_CR18","series-title":"Lecture Notes in Computer Science","first-page":"424","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"1997","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 424\u2013435. Springer, Heidelberg (1997)"},{"key":"31_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BFb0035388","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Kelb","year":"1997","unstructured":"Kelb, P., Margaria, T., Mendler, M., Gsottberger, C.: Mosel: A flexible toolset for monadic second order logic. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217, pp. 183\u2013202. Springer, Heidelberg (1997)"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized linear networks of processes. In: 24th POPL, Paris (January 1997)","DOI":"10.1145\/263699.263747"},{"key":"31_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Shahar, E.: Liveness and acceleration in parameterized verification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)","DOI":"10.1007\/10722167_26"},{"key":"31_CR22","doi-asserted-by":"crossref","unstructured":"Prasad Sistla, A.: Parametrized verification of linear networks using automata as invariants. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 412\u2013423. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_40"},{"key":"31_CR23","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to au- tomatic program verification. In: Proc. 1st LICS, June 1986, pp. 332\u2013344 (1986)"},{"key":"31_CR24","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0028736"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722167_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:48:55Z","timestamp":1556020135000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722167_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677703","9783540450474"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/10722167_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000]]}}}