Regular Model Checking with Regular Relations | SpringerLink
Skip to main content
Springer Nature Link
Log in

Regular Model Checking with Regular Relations

  • Conference paper
  • First Online:
Fundamentals of Computation Theory (FCT 2021)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12867))

Included in the following conference series:

  • 661 Accesses

Abstract

Regular model checking is an exploration technique for infinite state systems where state spaces are represented as regular languages and transition relations are expressed using rational relations over infinite (or finite) strings. We extend the regular model checking paradigm to permit the use of more powerful transition relations: the class of regular relations, of which the rational relations are a strict subset. We use the language of monadic second-order logic (MSO) on infinite strings to specify such relations and adopt streaming string transducers (SSTs) as a suitable computational model. We introduce nondeterministic SSTs over infinite strings (\(\omega \)-NSSTs) and show that they precisely capture the relations definable in MSO. We further explore theoretical properties of \(\omega \)-NSSTs required to effectively carry out regular model checking. In particular, we establish that the regular type checking problem for \(\omega \)-NSSTs is decidable in Pspace. Since the post-image of a regular language under a regular relation may not be regular (or even context-free), approaches that iteratively compute the image can not be effectively carried out in this setting. Instead, we utilize the fact that regular relations are closed under composition, which, together with our decidability result, provides a foundation for regular model checking with regular relations.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 10295
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 12869
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Abdulla, P.A., Jonsson, B., Nilsson, M., d’Orso, J.: Regular model checking made simple and effcient. In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 116–131. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45694-5_9

    Chapter  Google Scholar 

  2. Abdulla, P.A., Jonsson, B., Nilsson, M., d’Orso, J., Saksena, M.: Regular model checking for LTL(MSO). Int. J. Softw. Tools Technol. Transf. 14(2), 223–241 (2012). https://doi.org/10.1007/s10009-011-0212-z

    Article  MATH  Google Scholar 

  3. Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 35–48. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_3

    Chapter  Google Scholar 

  4. Alur, R., Cerný, P.: Expressiveness of streaming string transducers. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS. LIPIcs, vol. 8, pp. 1–12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010). https://doi.org/10.4230/LIPIcs.FSTTCS.2010.1

  5. Alur, R., Deshmukh, J.V.: Nondeterministic streaming string transducers. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 1–20. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22012-8_1

    Chapter  Google Scholar 

  6. Alur, R., Filiot, E., Trivedi, A.: Regular transformations of infinite strings. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS, pp. 65–74. IEEE Computer Society (2012). https://doi.org/10.1109/LICS.2012.18

  7. Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Log. 6(3), 614–633 (2005). https://doi.org/10.1145/1071596.1071601

    Article  MathSciNet  MATH  Google Scholar 

  8. Boigelot, B., Legay, A., Wolper, P.: Iterating Transducers in the Large. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 223–235. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_24

    Chapter  Google Scholar 

  9. Boigelot, B., Legay, A., Wolper, P.: Omega-regular model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 561–575. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_41

    Chapter  Google Scholar 

  10. Boigelot, B., Wolper, P.: Representing arithmetic constraints with finite automata: an overview. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 1–20. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45619-8_1

    Chapter  Google Scholar 

  11. Boker, U.: Why these automata types? In: LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 57, pp. 143–163. EasyChair (2018). https://easychair.org/publications/paper/G5dD

  12. Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372–386. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27813-9_29

    Chapter  Google Scholar 

  13. Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_31

    Chapter  Google Scholar 

  14. Bouajjani, A., Legay, A., Wolper, P.: Handling liveness properties in (omega-)regular model checking. In: Proceedings of the 6th International Workshop on Verification of Infinite-State Systems, INFINITY. Electronic Notes in Theoretical Computer Science, vol. 138, pp. 101–115. Elsevier (2004). https://doi.org/10.1016/j.entcs.2005.02.061

  15. Chaudhuri, S., Sankaranarayanan, S., Vardi, M.Y.: Regular real analysis. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pp. 509–518. IEEE Computer Society (2013). https://doi.org/10.1109/LICS.2013.57

  16. Courcelle, B.: Monadic second-order definable graph transductions: a survey. Theor. Comput. Sci. 126(1), 53–75 (1994). https://doi.org/10.1016/0304-3975(94)90268-2

  17. Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach, Encyclopedia of mathematics and its applications, vol. 138. Cambridge University Press (2012). http://www.cambridge.org/fr/knowledge/isbn/item5758776/?site_locale=fr_FR

  18. Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 286–297. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_27

    Chapter  Google Scholar 

  19. Dave, V., Dohmen, T., Krishna, S.N., Trivedi, A.: Regular model checking with regular relations. CoRR abs/1910.09072 (2019). http://arxiv.org/abs/1910.09072

  20. Engelfriet, J., Hoogeboom, H.J.: MSO definable string transductions and two-way finite-state transducers. ACM Trans. Comput. Log. 2(2), 216–254 (2001). https://doi.org/10.1145/371316.371512

    Article  MathSciNet  MATH  Google Scholar 

  21. Gorman, A.B., et al.: Continuous regular functions. Log. Methods Comput. Sci. 16(1) (2020). https://doi.org/10.23638/LMCS-16(1:17)2020

  22. Habermehl, P., Vojnar, T.: Regular model checking using inference of regular languages. In: Proceedings of the 6th International Workshop on Verification of Infinite-State Systems, INFINITY. Electronic Notes in Theoretical Computer Science, vol. 138, pp. 21–36. Elsevier (2004). https://doi.org/10.1016/j.entcs.2005.01.044

  23. Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 220–235. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46419-0_16

    Chapter  MATH  Google Scholar 

  24. Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theor. Comput. Sci. 256(12), 93–112 (2001). https://doi.org/10.1016/S0304-3975(00)00103-1

  25. Legay, A.: Extrapolating (omega-)regular model checking. Int. J. Softw. Tools Technol. Transf. 14(2), 119–143 (2012). https://doi.org/10.1007/s10009-011-0209-7

  26. Legay, A., Wolper, P.: On (omega-)regular model checking. ACM Trans. Comput. Log. 12(1), 2:1-2:46 (2010). https://doi.org/10.1145/1838552.1838554

    Article  MathSciNet  MATH  Google Scholar 

  27. Löding, C., Spinrath, C.: Decision problems for subclasses of rational relations over finite and infinite words. Discret. Math. Theor. Comput. Sci. 21(3) (2019). http://dmtcs.episciences.org/5141

  28. Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, Cambridge (2009). https://doi.org/10.1017/CBO9781139195218

  29. Schützenberger, M.: Sur les relations rationelles entre monoïdes libres. Theor. Comput. Sci. 243–259 (1976)

    Google Scholar 

  30. Touili, T.: Regular model checking using widening techniques. Electron. Notes Theor. Comput. Sci. 50(4), 342–356 (2001). https://doi.org/10.1016/S1571-0661(04)00187-2

  31. Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 88–97. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028736

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IIT Bombay, Mumbai, India

    Vrunda Dave & Shankara Narayanan Krishna

  2. Univeristy of Colorado, Boulder, USA

    Taylor Dohmen & Ashutosh Trivedi

Authors
  1. Vrunda Dave
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Taylor Dohmen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Shankara Narayanan Krishna
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ashutosh Trivedi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Taylor Dohmen .

Editor information

Editors and Affiliations

  1. Sorbonne University, Paris, France

    Evripidis Bampis

  2. National Technical University of Athens, Athens, Greece

    Aris Pagourtzis

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Dave, V., Dohmen, T., Krishna, S.N., Trivedi, A. (2021). Regular Model Checking with Regular Relations. In: Bampis, E., Pagourtzis, A. (eds) Fundamentals of Computation Theory. FCT 2021. Lecture Notes in Computer Science(), vol 12867. Springer, Cham. https://doi.org/10.1007/978-3-030-86593-1_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-86593-1_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-86592-4

  • Online ISBN: 978-3-030-86593-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation