On (Omega-)regular model checking

Legay, Axel; Wolper, Pierre

doi:10.1145/1838552.1838554

Download

Article (Scientific journals)

On (Omega-)regular model checking

Legay, Axel; Wolper, Pierre

2010 • In ACM Transactions on Computational Logic, 12 (1), p. 46

Peer Reviewed verified by ORBi

Permalink
https://hdl.handle.net/2268/81696

DOI
10.1145/1838552.1838554

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

paper.pdf

Author postprint (697.62 kB)

Download

© ACM, 2010. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Transactions on Computational Logic, Vol 12, Number 1, October 2010 http://dx.doi.org/10.1145/1838552.1838554

All documents in ORBi are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

verification; model-checking; automata

Abstract :

[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

Volume :

Issue :

Pages :

46 p.

Peer reviewed :

Peer Reviewed verified by ORBi

Available on ORBi :

since 12 January 2011

Statistics

Number of views

112 (17 by ULiège)

Number of downloads

203 (7 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

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.