[en] Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the set of reachable states of a system requires acceleration techniques that can finitely compute the effect of an unbounded number of transitions. Among the acceleration techniques that have been proposed, one finds both specific and generic techniques. Specific techniques exploit the particular type of system being analyzed, for example, a system manipulating queues or integers, whereas generic techniques only assume that the transition relation is represented by a finite-state transducer, which has to be iterated. In this article, we investigate the possibility of using generic techniques in cases where only specific techniques have been exploited so far. Finding that existing generic techniques are often not applicable in cases easily handled by specific techniques, we have developed a new approach to iterating transducers. This new approach builds on earlier work, but exploits a number of new conceptual and algorithmic ideas, often induced with the help of experiments, that give it a broad scope, as well as good performances.
Disciplines :
Computer science
Author, co-author :
Legay, Axel ; Université de Liège - ULiège > Département d'Electricité, Electronique et Informatique
Wolper, Pierre ; Université de Liège - ULiège > Département d'Electricité, Electronique et Informatique
Language :
English
Title :
On (Omega-)regular model checking
Publication date :
2010
Journal title :
ACM Transactions on Computational Logic
ISSN :
1529-3785
Publisher :
Association for Computing Machinery, New-York, United States - New York
scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.
Bibliography
ABDULLA, P.A., BOUAJJANI, A., JONSSON, B., AND NILSSON, M. 1999. Handling global conditions in parameterized system verification. In Proceedings of the 11th International Conference on Computer-Aided Varification (CAV). Lecture Notes in Computer Science, vol. 1633. Springer, Berlin, Germany. 134-145.
ABDULLA, P.A., CERANS, K., JONSSON, B., AND TSAY, Y. 2000. Algorithmic analysis of programs with well quasi-ordered domains. Inform. Comput. 160, 1-2, 109-127.
ABDULLA, P.A. AND JONSSON, B. 1996. Verifying programs with unreliable channels. Inform. Comput. 127, 2, 91-101.
ABDULLA, P.A., JONSSON, B., MAHATA, P., AND D'ORSO, J. 2002. Regular tree model checking. In Proceedings of the 14th International Conference on Computer-Aided Varification (CAV) .Lecture Notes in Computer Science, vol. 2404. Springer, Berlin, Germany, 555-568.
ABDULLA, P.A., JONSSON, B., NILSSON, M., AND D'ORSO, J. 2003. Algorithmic improvements in regular model checking. In Proceedings of the 15th International Conference on Computer-Aided Varification (CAV). Lecture Notes in Computer Science, vol. 2725. Springer, Berlin, Germany, 236-248.
ABDULLA, P.A., JONSSON, B., NILSSON, M., D'ORSO, J., AND SAKSENA, M. 2004. Regular model checking for ltl(mso). In Proceedings of the 16th International Conference on Computer-Aided Varification (CAV). Lecture Notes in Computer Science, vol. 3114. Springer, Berlin, Germany, 348-360.
ALUR, R., COURCOUBETIS, C., HALBWACHS, N., HENZINGER, T.A., HO, P., NICOLLIN, X., OLIVERO, A., SIFAKIS, J., AND YOVINE, S. 1995. The algorithmic analysis of hybrid systems. Theoret. Comput. Sci. 138, 1, 3-34.
ANGLUIN, D. 1987. Learning regular sets from queries and counterexamples. Inform. Comput. 75, 2, 87-106.
APT, K.R. AND KOZEN, D. 1986. Limits for automatic verification of finite-state concurrent systems. Inform. Process. Lett. 22, 6, 307-309.
BARDIN, S., FINKEL, A., AND LEROUX, J. 2004. Faster acceleration of counter automata in practice. in Proceedings of the 10th Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 2988. Springer, Berlin, Germany, 576-590.
BARDIN, S., FINKEL, A., LEROUX, J., AND SCHNOEBELEN, P. 2005. Flat acceleration in symbolic model checking. In Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA). Lecture Notes in Computer Science, vol. 3707. Springer, Berlin, Germany, 474-488.
BOIGELOT, B. 1999. Symbolic Methods for Exploring Infinite State Spaces. Collection des publications de la Faculté des Sciences Appliquées de l'Université de Liège, Liège, Belgium.
BOIGELOT, B. AND GODEFROID, P. 1996. Symbolic verification of communication protocols with infinite state spaces using qdds. In Proceedings of the 8th International Conference on Computer- Aided Varification (CAV). Lecture Notes in Computer Science, vol. 1102. Springer, Berlin, Germany, 1-12.
BOIGELOT, B., GODEFROID, P., Willems, B., and Wolper, P. 1997. The power of qdds. In Proceedings of the 4th International Static Analysis Symposium (SAS). Lecture Notes in Computer Science, vol. 1302. Springer, Berlin, Germany, 172-186.
BOIGELOT, B. AND HERBRETEAU, F. 2006. The power of hybrid acceleration. In Proceedings of the 18th International Conference on Computer-Aided Varification (CAV). Lecture Notes in Computer Science, vol. 4144. Springer, Berlin, Germany, 438-451.
BOIGELOT, B., HERBRETEAU, F., and JODOGNE, S. 2003a. Hybrid acceleration using real vector automata. In Proceedings of the 15th International Conference on Computer-Aided Varification (CAV). Lecture Notes in Computer Science, vol. 2725. Springer, Berlin, Germany, 193-205.
BOIGELOT, B., JODOGNE, S., AND WOLPER, P. 2001. On the use of weak automata for deciding linear arithmetic with integer and real variables. In Proceedings of IJCAR. Lecture Notes in Computer Science, vol. 2083. Springer, Berlin, Germany, 611-625.
BOIGELOT, B., JODOGNE, S., AND WOLPER, P. 2005. An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Logic 6, 3, 614-633.
BOIGELOT, B., LEGAY, A., AND WOLPER, P. 2003b. Iterating transducers in the large. In Proceedings of the 15th International Conference on Computer-Aided Varification (CAV). Lecture Notes in Computer Science, vol. 2725. Springer, Berlin, Germany, 223-235.
BOIGELOT, B., LEGAY, A., AND WOLPER, P. 2004. Omega-regular model checking. In Proceedings of the 10th Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 2988. Springer, Berlin, Germany, 561-575.
BOIGELOT, B., RASSART, S., AND WOLPER, P. 1998. On the expressiveness of real and integer arithmetic automata. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 1443. Springer, Berlin, Germany, 152-163.
BOIGELOT, B. AND WOLPER, P. 2002. Representing arithmetic constraints with finite automata: An overview. In Proceedings of the International Conference on Logic Programming (ICLP).Lecture Notes in Computer Science, vol. 2401. Springer, Berlin, Germany, 1-19.
BOUAJJANI, A., ESPARZA, J., AND MALER, O. 1997. Reachability analysis of pushdown automata: Application to model-checking. In Proceedings of the International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 1243. Springer, Berlin, Germany, 135-150.
BOUAJJANI, A. AND HABERMEHL, P. 1997. Symbolic reachability analysis of FIFO channel systems with nonregular sets of configurations. In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 1256. Springer, Berlin, Germany, 560-570.
BOUAJJANI, A., HABERMEHL, P., MORO, P., AND VOJNAR, T. 2005. Verifying programs with dynamic 1-selector-linked structures in regular model checking. In Proceedings of the 11th Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS).Lecture Notesin Computer Science, vol. 3440. Springer, Berlin, Germany, 13-29.
BOUAJJANI, A., HABERMEHL, P., ROGALEWICZ, A., AND VOJNAR, T. 2006. Abstract regular tree model checking of complex dynamic data structures. In Proceedings of the 13th International Static Analysis Symposium (SAS). Lecture Notes in Computer Science, vol. 4134. Springer, Berlin, Germany, 52-70.
BOUAJJANI, A., HABERMEHL, P., AND VOJNAR, T. 2004a. Abstract regular model checking. In Proceedings of the 16th International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 3114. Springer, Berlin, Germany, 372-386.
BOUAJJANI, A., JONSSON, B., NILSSON, M., AND TOUILI, T. 2000. Regular model checking. In Proceedings of the 12th International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1855. Springer, Berlin, Germany, 403-418.
BOUAJJANI, A., LEGAY, A., AND WOLPER, P. 2004b. Handling liveness properties in (omega-)regular model checking. In Proceedings of the 6th International Workshop on Verification of Infinity-State Systems (INFINITY).ENTCS, 138, 3. Elsevier Science Publishers, Amsterdam, The Netherlands.
BOUAJJANI, A. AND TOUILI, T. 2002. Extrapolating tree transformations. In Proceedings of the 14th International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2404. Springer, Berlin, Germany, 539-554.
CANTIN, F., LEGAY, A., AND WOLPER, P. 2007. Computing convex hulls by automata iteration. In Proceedings of the AUTOMATHA. Also, Tech rep. 2007. 83, Centre in Verification, Brussels, Belgium.
CANTIN, F., LEGAY, A., AND WOLPER, P. 2008. Computing convex hull by automata iteration. In Proceedings of the 13th International Conference on Implementation and Application of Automata (CIAA). Lecture Notes in Computer Science, vol. 5148. Springer, Berlin, Germany, 112-121.
DAMS, D., LAKHNECH, Y., AND STEFFEN, M. 2002. Iterating transducers. J. Logic Alg. Program. 52-53, 109-127.
FINKEL, A. AND LEROUX, J. 2002. How to compose presburger-accelerations: Applications to broadcast protocols. In Proceedings of the 22nd Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS). Lecture Notes in Computer Science, vol. 2556. Springer, Berlin, Germany, 145-156.
FINKEL, A., WILLEMS, B., AND WOLPER, P. 1997. A direct symbolic approach to model checking pushdown systems. In Proceedings of the International Workshop on Verification of Infinity-State Systems (INFINITY). ENTCS, vol. 9. Elsevier Science Publishers, Amsterdam, The Netherlands.
GEERAERTS, G., RASKIN, J.-F., AND BEGIN, L. V. 2005. Expand, enlarge and check ... made efficient. In Proceedings of the 17th International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 3576. Springer, Berlin, Germany, 394-407.
HABERMEHL, P. AND VOJNAR, T. 2004. Regular model checking using inference of regular languages. In Proceedings of the International Workshop on Verification of Infinity-State Systems (INFINITY).ENTCS, 138 3. Elsevier Science Publishers, Amsterdam, The Netherlands.
HOPCROFT, J. E. 1971. An n log n algorithm for minimizing states in a finite automaton. Theor. Mach. Comput. 189-196.
IBARRA, O. H. 1978. Reversal-bounded multicounter machines and their decision problems. J. ACM 25, 1, 116-133.
JONSSON, B. AND NILSSON, M. 2000. Transitive closures of regular relations for verifying infinite- state systems. In Proceedings of the 6th Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 1785. Springer, Berlin, Germany, 220-234.
KESTEN, Y., MALER, O., MARCUS, M., PNUELI, A., AND SHAHAR, E. 1997. Symbolic model checking with rich assertional languages. In Proceedings of the 9th International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1254. Springer, Berlin, Germany, 424-435.
KESTEN, Y., PNUELI, A., SHAHAR, E., AND ZUCK, L. D. 2002. Network invariants in action. In Proceedings of the 13th International Conference on Concurency Theory (CONCUR). Lecture Notes in Computer Science, vol. 2421. Springer, Berlin, Germany, 101-115.
LEGAY, A. 2007. Generic Techniques for the Verification of Infinite-State Systems. Collection des publications de la Faculté des Sciences Appliquées de l'Université de Liège, Liège, Belgium.
LEGAY, A. 2008. T(o)rmc: A tool for (omega-)regular model checking. In Proceedings of the 20th International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 5123. Springer, Berlin, Germany, 548-551.
LÖDING, C. 2001. Efficient minimization of deterministic weak ω-automata. Inform. Process. Lett. 79, 3, 105-109.
MULLER, D.E., SAOUDI, A., AND SCHUPP, P. E. 1986. Alternating automata, the weak monadic theory of the tree and its complexity. In Proceedings of the 13th International Colloquium on Automata, Languages and Programming. Springer, Berlin, Germany, 275-283.
NILSSON, M. 2001. Regular model checking. M.S. thesis. Uppsala University, Uppsala, Sweden.
NILSSON, M. 2005. Regular model checking. Ph.D. dissertation. Uppsala University, Uppsala, Sweden.
PNUELI, A. AND SHAHAR, E. 2000. Liveness and acceleration in parameterized verification. In Proceedings of the 12th International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1855. Springer, Berlin, Germany, 328-343.
RIVEST, R.L. AND SHAPIRE, R. E. 1993. Inference of finite automata using homing sequences. Inform. Comput. 103, 2, 299-347.
ROOS, R. S. 1988. Deciding equivalence of deterministic one-counter automata in polynomial time with applications to learning. Ph.D. dissertation, Smith College, Northampton, MA.
SAFRA, S. 1992. Exponential determinization for ω-automata with strong-fairness acceptance condition. In Proceedings of the 24th ACM Symposium on Theory of Computing.
SIMONS, D.P.L. AND STOELINGA, M. 2001. Mechanical verification of the IEEE 1394a root contention protocol using uppaal2k. Int. J. Softw. Tools Tech. Transf. 3, 4, 469-485.
TOUILI, T. 2001. Regular model checking using widening techniques. Elec. Notes Thoret. Comp. Sci. 50, 4, 342-356.
TOUILI, T. 2003. Analyse symbolique de systèmes infinis basée sur les automates: Application à la vérification de systèmes paramétrés. Ph.D. dissertation. Université de Paris 7, Paris, France.
TOUILI, T. AND D'ORSO, J. 2006. Regular hedge model checking. In Proceedings of the 4th International IFIP Conference on Theoretical Computer Science (TCS).
VARDHAN, A. 2006. Learning to verify systems. Ph.D. dissertation, Univeristy of Illinois, Urbana, IL.
VARDHAN, A., SEN, K., VISWANATHAN, M., AND AGHA, G. 2004. Actively learning to verify safety for FIFo automata. In Proceedings of the 24th Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS). Lecture Notes in Computer Science, vol. 3328. Springer, Berlin, Germany, 494-505.
VARDHAN, A., SEN, K., VISWANATHAN, M., AND AGHA, G. 2005. Using language inference to verify omega-regular properties. In Proceedings of the 11th Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 3440. Springer, Berlin, Germany, 45-60.
VARDHAN, A. AND VISWANATHAN, M. 2006. Lever: A tool for learning based verification. In Proceedings of the 18th International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 4144. Springer, Berlin, Germany, 471-474.
VARDI, M. Y. 2007. From church and prior to PSL. http://www.cs.rice.edu/ vardi/papers/index.html.
WOLPER, P. AND BOIGELOT, B. 1995. An automata-theoretic approach to presburger arithmetic constraints. In Proceedings of the 2nd International Static Analysis Symposium (SAS).Lecture Notes in Computer Science, vol. 983. Springer, Berlin, Germany, 21-32.
WOLPER, P. AND BOIGELOT, B. 1998. Verifying systems with infinite but regular state spaces. In Proceedings of the 10th International Conference on Computer-Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1427. Springer, Berlin, Germany, 88-97.
WOLPER, P. AND BOIGELOT, B. 2000. On the construction of automata from linear arithmetic constraints. In Proceedings of the 6th Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 1785. Springer, Berlin, Germany, 1-19.
Similar publications
Sorry the service is unavailable at the moment. Please try again later.
This website uses cookies to improve user experience. Read more
Save & Close
Accept all
Decline all
Show detailsHide details
Cookie declaration
About cookies
Strictly necessary
Performance
Strictly necessary cookies allow core website functionality such as user login and account management. The website cannot be used properly without strictly necessary cookies.
This cookie is used by Cookie-Script.com service to remember visitor cookie consent preferences. It is necessary for Cookie-Script.com cookie banner to work properly.
Performance cookies are used to see how visitors use the website, eg. analytics cookies. Those cookies cannot be used to directly identify a certain visitor.
Used to store the attribution information, the referrer initially used to visit the website
Cookies are small text files that are placed on your computer by websites that you visit. Websites use cookies to help users navigate efficiently and perform certain functions. Cookies that are required for the website to operate properly are allowed to be set without your permission. All other cookies need to be approved before they can be set in the browser.
You can change your consent to cookie usage at any time on our Privacy Policy page.
