{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:43Z","timestamp":1751660503460,"version":"3.38.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,8,25]],"date-time":"2011-08-25T00:00:00Z","timestamp":1314230400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10009-011-0212-z","type":"journal-article","created":{"date-parts":[[2011,8,24]],"date-time":"2011-08-24T19:01:47Z","timestamp":1314212507000},"page":"223-241","source":"Crossref","is-referenced-by-count":12,"title":["Regular model checking for LTL(MSO)"],"prefix":"10.1007","volume":"14","author":[{"given":"Parosh Aziz","family":"Abdulla","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":"Julien","family":"d\u2019Orso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mayank","family":"Saksena","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,8,25]]},"reference":[{"key":"212_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J., Saksena, M.: Regular model checking for LTL(MSO). In: Alur, R., Peled, D.A. (eds.) Proc. CAV\u201904, 16th Int. Conf. on Computer Aided Verification, LNCS 3114, pp. 348\u2013360, Springer (2004)","DOI":"10.1007\/978-3-540-27813-9_27"},{"key":"212_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Regular model checking made simple and efficient. In: Brim, L., Jancar, P., Kret\u00ednsk\u00fd, M., Kucera, A. (eds.) Proc. CONCUR 2002 13th Int. Conf. on Concurrency Theory, LNCS 2421, pp. 116\u2013130, Springer (2002)","DOI":"10.1007\/3-540-45694-5_9"},{"key":"212_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Algorithmic improvements in regular model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) Proc. CAV\u201903, 15th Int. Conf. on Computer Aided Verification, LNCS 2725, pp. 236\u2013248, Springer (2003)","DOI":"10.1007\/978-3-540-45069-6_25"},{"issue":"5","key":"212_CR4","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1145\/362946.362970","volume":"2","author":"K. Bartlett","year":"1969","unstructured":"Bartlett K., Scantlebury R., Wilkinson P.: A note on reliable full-duplex transmissions over half duplex lines. Commun. ACM 2(5), 260\u2013261 (1969)","journal-title":"Commun. ACM"},{"issue":"2","key":"212_CR5","first-page":"141","volume":"7","author":"K. Baukus","year":"2001","unstructured":"Baukus K., Lakhnech Y., Stahl K.: Verification of parameterized networks. J. Univ. Comp. Sci. 7(2), 141\u2013158 (2001)","journal-title":"J. Univ. Comp. Sci."},{"key":"212_CR6","unstructured":"Boigelot, B., Franois, J.-M., Latour, L.: The Li\u00e8ge automata-based symbolic handler (LASH). http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/ (2011)"},{"key":"212_CR7","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt Jr. W.A., Somenzi, F. (eds.) Proc. CAV\u201903, 15th Int. Conf. on Computer Aided Verification, LNCS 2725, pp. 223\u2013235, Springer (2003)","DOI":"10.1007\/978-3-540-45069-6_24"},{"key":"212_CR8","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A, Sistla, A.P. (eds.) Proc. CAV\u201900, 12th Int. Conf. on Computer Aided Verification, LNCS 1855, pp. 403\u2013418, Springer (2000)","DOI":"10.1007\/10722167_31"},{"issue":"3","key":"212_CR9","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.entcs.2005.02.061","volume":"138","author":"A. Bouajjani","year":"2004","unstructured":"Bouajjani A., Legay A., Wolper P.: Handling liveness properties in (\u03c9-)regular model checking. Electr. Notes Theor. Comp. Sci. 138(3), 101\u2013115 (2004)","journal-title":"Electr. Notes Theor. Comp. Sci."},{"key":"212_CR10","doi-asserted-by":"crossref","unstructured":"Delzanno, G.: Automatic verification of cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) Proc. CAV\u201900, 12th Int. Conf. on Computer Aided Verification, LNCS 1855, pp. 53\u201368, Springer (2000)","DOI":"10.1007\/10722167_8"},{"issue":"5","key":"212_CR11","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0020-0190(83)90092-3","volume":"16","author":"E.W. Dijkstra","year":"1983","unstructured":"van Dijkstra E.W., Feijen W.H.J., van Gasteren A.J.M.: Derivation of a termination detection algorithm for distributed computations. Inf. Process. Lett. 16(5), 217\u2013219 (1983)","journal-title":"Inf. Process. Lett."},{"key":"212_CR12","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D.A. (ed.) Proc. CADE-17, 17th International Conference on Automated Deduction, LNCS 1831, pp. 236\u2013254, Springer (2000)","DOI":"10.1007\/10721959_19"},{"key":"212_CR13","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Rapid parameterized model checking of snoopy cache coherence protocols. In: Garavel, H., Hatcliff, J. (eds.) Proc. TACAS\u201903, 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2619, pp. 144\u2013159, Springer (2003)","DOI":"10.1007\/3-540-36577-X_11"},{"key":"212_CR14","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proc. 22th ACM Symp. on Principles of Programming Languages. pp. 85\u201394 (1995)","DOI":"10.1145\/199448.199468"},{"key":"212_CR15","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kucera, A., Mayr, R.: Model-checking LTL with regular valuations for pushdown systems. In: Kobayashi, N., Pierce, B.C. (eds.) Proc. TACS2001, 4th Int. Conf. on Theoretical Aspects of Computer Software, LNCS 2215, pp. 316\u2013339, Springer (2001)","DOI":"10.1007\/3-540-45500-0_16"},{"issue":"3","key":"212_CR16","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s10009-005-0193-x","volume":"8","author":"Y. Fang","year":"2006","unstructured":"Fang Y., Piterman N., Pnueli A., Zuck L.: Liveness with invisible ranking. Softw. Tools Technol. Transf. 8(3), 261\u2013279 (2006)","journal-title":"Softw. Tools Technol. Transf."},{"key":"212_CR17","doi-asserted-by":"crossref","unstructured":"Fisman, D., Kupferman, O., Lustig, Y.: On verifying fault tolerance of distributed protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proc. TACAS\u201908, 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 4963, pp. 315\u2013331, Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_22"},{"issue":"3","key":"212_CR18","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German S.M., Sistla A.P.: Reasoning about systems with many processes. J ACM 39(3), 675\u2013735 (1992)","journal-title":"J ACM"},{"key":"212_CR19","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/978-3-642-59126-6_4","volume-title":"Handbook of Formal Languages, vol. 3, Beyond Words","author":"D. Giammarresi","year":"1997","unstructured":"Giammarresi D., Restivo A.: Two-dimensional languages. In: Salomaa, A., Rozenberg, G. (eds) Handbook of Formal Languages, vol. 3, Beyond Words, pp. 215\u2013267. Springer, Berlin (1997)"},{"key":"212_CR20","doi-asserted-by":"crossref","unstructured":"Gribomont, E.P., Zenner, G.: Automated verification of Szymanski\u2019s algorithm. In: Steffen, B. (ed.) Proc. TACAS\u201998, 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1384, pp. 424\u2013438, Springer (1998)","DOI":"10.1007\/BFb0054187"},{"key":"212_CR21","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., Cleaveland, R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) Proc. TACAS\u201995, 1st Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1019, pp. 89\u2013110, Springer (1995)","DOI":"10.1007\/3-540-60630-0_5"},{"key":"212_CR22","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Graf, S., Schwartzbach, M. (eds.) Proc. TACAS\u201900, 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1785, pp. 220\u2013234, Springer (2000)","DOI":"10.1007\/3-540-46419-0_16"},{"key":"212_CR23","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/S0304-3975(00)00103-1","volume":"256","author":"Y. Kesten","year":"2001","unstructured":"Kesten Y., Maler O., Marcus M., Pnueli A., Shahar E.: Symbolic model checking with rich assertional languages. Theor. Comp. Sci. 256, 93\u2013112 (2001)","journal-title":"Theor. Comp. Sci."},{"issue":"8","key":"212_CR24","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"issue":"3","key":"212_CR25","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"212_CR26","volume-title":"Distributed Algorithms","author":"N. Lynch","year":"1996","unstructured":"Lynch N.: Distributed Algorithms. Morgan Kaufmann, San Mateo (1996)"},{"key":"212_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Manna Z., Pnueli A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Berlin (1992)"},{"key":"212_CR28","unstructured":"Nilsson, M.: Regular model checking. PhD thesis, Uppsala University (2005)"},{"key":"212_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th Annual Symp. Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"212_CR30","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1982","unstructured":"Pnueli A.: The temporal semantics of concurrent programs. Theor. Comp. Sci. 13, 45\u201360 (1982)","journal-title":"Theor. Comp. Sci."},{"key":"212_CR31","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) Proc. TACAS\u201901, 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2031, pp. 82\u201397, Springer (2001)","DOI":"10.1007\/3-540-45319-9_7"},{"key":"212_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Shahar, E.: Liveness and acceleration in parameterized verification. In: Emerson E.A., Sistla, A.P. (eds.) Proc. CAV\u201900, 12th Int. Conf. on Computer Aided Verification, LNCS 1855, pp. 328\u2013343, Springer (2000)","DOI":"10.1007\/10722167_26"},{"key":"212_CR33","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1, \u221e)-counter abstraction. In: Brinskma, D., Larsen, K.G. (eds.) Proc. CAV\u201902, 14th Int. Conf. on Computer Aided Verification, LNCS 2404, pp. 107\u2013122, Springer (2002)","DOI":"10.1007\/3-540-45657-0_9"},{"key":"212_CR34","doi-asserted-by":"crossref","unstructured":"Sistla, A.P.: Parametrized verification of linear networks using automata as invariants. In: Grumberg, O. (ed.) Proc. CAV\u201997, 9th Int. Conf. on Computer Aided Verification, LNCS 1254, pp. 412\u2013423, Springer (1997)","DOI":"10.1007\/3-540-63166-6_40"},{"key":"212_CR35","doi-asserted-by":"crossref","unstructured":"Szymanski, B.K.: Mutual exclusion revisited. In: Proc. Fifth Jerusalem Conf. on Information Technology, pp. 110\u2013117, IEEE Computer Society Press (1990)","DOI":"10.1109\/JCIT.1990.128275"},{"key":"212_CR36","volume-title":"Computer Networks","author":"A.S. Tanenbaum","year":"1996","unstructured":"Tanenbaum A.S.: Computer Networks. Prentice-Hall, Upper Saddle River (1996)"},{"key":"212_CR37","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/B978-0-444-88074-1.50009-3","volume-title":"Handbook of Theoretical Computer Science, vol. B, Formal Models and Semantics","author":"W. Thomas","year":"1990","unstructured":"Thomas W.: Automata on infinite objects. In: van Leeuwen, J. (eds) Handbook of Theoretical Computer Science, vol. B, Formal Models and Semantics, pp. 133\u2013191. Elsevier, Amsterdam (1990)"},{"key":"212_CR38","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. LICS\u201986, 1st IEEE Int. Symp. on Logic in Computer Science, pp. 332\u2013344 (1986)"},{"issue":"1\u20132","key":"212_CR39","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0168-0072(91)90066-U","volume":"51","author":"M.Y. Vardi","year":"1991","unstructured":"Vardi M.Y.: Verification of concurrent programs: the automata-theoretic framework. Ann. Pure Appl. Logic 51(1\u20132), 79\u201398 (1991)","journal-title":"Ann. Pure Appl. Logic"},{"key":"212_CR40","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Hu, A.J., Vardi, M.Y. (eds.) Proc. CAV\u201998, 10th Int. Conf. on Computer Aided Verification, LNCS 1427, pp. 88\u201397, Springer (1998)","DOI":"10.1007\/BFb0028736"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0212-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0212-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0212-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,9]],"date-time":"2025-03-09T06:48:15Z","timestamp":1741502895000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0212-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,8,25]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["212"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0212-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2011,8,25]]}}}