Domain-specific regular acceleration

Boigelot, Bernard

doi:10.1007/s10009-011-0206-x

Download

Article (Scientific journals)

Domain-specific regular acceleration

Boigelot, Bernard

2012 • In International Journal on Software Tools for Technology Transfer, 14 (2), p. 193-206

Peer Reviewed verified by ORBi

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

DOI
10.1007/s10009-011-0206-x

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

paper.pdf

Author postprint (236.77 kB)

Download

The original publication is available at www.springerlink.com

All documents in ORBi are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

verification; infinite-state systems; acceleration

Abstract :

[en] The regular model-checking approach is a set of techniques aimed at exploring symbolically infinite state spaces. These techniques proceed by representing sets of configurations of the system under analysis by regular languages, and the transition relation between these configurations by a transformation over such languages. The set of reachable configurations can then be computed by repeatedly applying the transition relation, starting from a representation of the initial set of configurations, until a fixed point is reached. In order for this computation to terminate, it is generally needed to introduce so-called acceleration operators, the purpose of which is to explore in one computation step infinitely many paths in the transition graph of the system. A simple form of acceleration operator is one that is associated to a cycle in the transition graph, computing the set of states that can be obtained by following this cycle arbitrarily many times. The computation of acceleration operators is strongly dependent on the type of the data values that are manipulated by the system, and on the symbolic representation chosen for handling sets of such values. In this survey, we describe acceleration operators suited for the regular state-space exploration of systems relying on FIFO communication channels, as well as those based on integer and real variables.

Disciplines :

Computer science

Author, co-author :

Boigelot, Bernard ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique

Language :

English

Title :

Domain-specific regular acceleration

Publication date :

2012

Journal title :

International Journal on Software Tools for Technology Transfer

ISSN :

1433-2779

eISSN :

1433-2787

Publisher :

Springer

Volume :

Issue :

Pages :

193-206

Peer reviewed :

Peer Reviewed verified by ORBi

Name of the research project :

Interuniversity Attraction Poles program MoVES

Funders :

BELSPO - Belgian Federal Science Policy Office [BE]
F.R.S.-FNRS - Fonds de la Recherche Scientifique [BE]

Funding text :

Work partially supported by the Interuniversity Attraction Poles program MoVES of the Belgian Federal Science Policy Office, and by the grants 2.4530.02 and 2.4607.08 of the Belgian Fund for Scientific Research (F.R.S.-FNRS).

Available on ORBi :

since 27 November 2012

Statistics

Number of views

132 (23 by ULiège)

Number of downloads

215 (11 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

Bibliography

Abdulla, P. A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: Proceedings of 10th International Conference on Computer-Aided Verification (CAV'98). Lecture Notes in Computer Science, vol. 1427, pp. 305-318. Springer, Berlin (1998).
Aziz Abdulla P., Collomb-Annichini A., Bouajjani A., Jonsson B.: Using forward reachability analysis for verification of lossy channel systems. Formal Methods Syst. Des. 25(1), 39-65 (2004).
Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceedings of 5th Symposium on Logic in Computer Science (LICS'90), pp. 414-425, Philadelphia (1990).
Alur R., Courcoubetis C., Halbwachs N., Henzinger T. A., Ho P.-H., Nicollin X., Olivero A., Sifakis J., Yovine S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 3-34 (1995).
Alur, R., Henzinger, T. A., Ho, P. H.: Automatic symbolic verification of embedded systems. In: Proceedings of 14th annual IEEE Real-Time Systems Symposium, pp. 2-11 (1993).
Abdulla P. A., Jonsson B.: Verifying programs with unreliable channels. Inf. Comput. 127(2), 91-101 (1996).
Abdulla, P. A., Jonsson, B., Nilsson, M., d'Orso, J.: Regular model checking made simple and efficient. In: Proceedings of 15th International Conference on Computer-Aided Verification (CAV'03). Lecture Notes in Computer Science, vol. 2725, pp. 237-248, Boulder, USA. Springer, Berlin (2003).
Abdulla, P. A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Proceedings of 15th International Conference on Concurrency Theory (CONCUR'04). Lecture Notes in Computer Science, vol. 3170, pp. 35-48. Springer, Berlin (2004).
Boigelot, B., Brusten, J., Leroux, J.: A generalization of Semenov's theorem to automata over real numbers. In: Proceedings of 22nd International Conference on Automated Deduction (CADE'09). Lecture Notes in Computer Science, vol. 5663, pp. 469-484. Springer, Berlin (2009).
Boigelot, B., Bronne, L., Rassart, S.: An improved reachability analysis method for strongly linear hybrid systems. In: Proceedings of 9th International Conference on Computer-Aided Verification (CAV'97). LNCS, vol. 1254, pp. 167-177, Haifa. Springer, Berlin (1997).
Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Proceedings of 21st International Colloquium on Trees in Algebra and Programming (CAAP'96). Lecture Notes in Computer Science, vol. 1059, pp. 30-43. Springer, Berlin (1996).
Burch J. R., Clarke E. M., McMillan K. L., Dill D. L., Hwang L. J.: Symbolic model checking: 10 20 states and beyond. Inf. Comput. 98(2), 142-170 (1992).
Bardin, S., Finkel, A., Leroux, J., Petrucci, L: Fast: fast acceleration of symbolic transition systems. In: Proceedings of 15th International Conference on Computer-Aided Verification (CAV'03). Lecture Notes in Computer Science, vol. 2725, pp. 118-121. Springer, Berlin (2003).
Boigelot, B., Godefroid, P., Willems, B. Wolper, P.: The power of QDDs. In: Proceedings of 4th International Symposium on Static Analysis (SAS'97). Lecture Notes in Computer Science, vol. 1302, pp. 172-186, Paris. Springer, Berlin (1997).
Bouajjani A., Habermehl P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Theor. Comput. Sci. 221(1-2), 211-250 (1999).
Boigelot, B., Herbreteau, F.: The power of hybrid acceleration. In: Proceedings of 18th International Conference on Computer-Aided Verification (CAV'06). Lecture Notes in Computer Science, vol. 4144, pp. 438-451. Springer, Berlin (2006).
Boigelot, B., Herbreteau, F., Jodogne, S.: Hybrid acceleration using real vector automata. In: Proceedings of 15th International Conference on Computer-Aided Verification (CAV'03). Lecture Notes in Computer Science, vol. 2725, pp. 193-205. Springer, Berlin (2003).
Bruyère V., Hansel G., Michaux C., Villemaire R.: Logic and p-recognizable sets of integers. Bull. Belgian Math. Soc. 1(2), 191-238 (1994).
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).
Boigelot B., Latour L.: Counting the solutions of Presburger equations without enumerating them. Theor. Comput. Sci. 313(1), 17-29 (2004).
Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Proceedings of 15th International Conference on Computer-Aided Verification (CAV'03). Lecture Notes in Computer Science, vol. 2725, pp. 223-235, Boulder, USA. Springer, Berlin (2003).
Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Université de Liège (1998).
Boigelot B.: On iterating linear transformations over recognizable sets of integers. Theor. Comput. Sci. 309(1-3), 413-468 (2003).
Bryant R.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293-318 (1992).
Bouajjani, A., Touili T.: Widening techniques for regular tree model checking. Special Section on Regular Model Checking STTT in this volume (2011). doi: 10. 1007/s10009-011-0208-8.
Boigelot, B., Wolper, P.: Symbolic verification with periodic sets. In: Proceedings of 6th International Conference on Computer-Aided Verification (CAV'94). Lecture Notes in Computer Science, vol. 818, pp. 55-67, Stanford. Springer, Berlin (1994).
Brand D., Zafiropoulo P.: On communicating finite-state machines. J. ACM 30(2), 323-342 (1983).
Büchi, J. R.: On a decision method in restricted second order arithmetic. In: Proceedings of International Congress on Logic, Methodoloy and Philosophy of Science, pp. 1-12. Stanford University Press, Stanford (1962).
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings od 4th ACM Symposium on Principles of Programming Languages (POPL'77), pp. 238-252, Los Angeles, California. ACM Press, New York (1977).
Cécé G., Finkel A., Iyer S. P.: Unreliable channels are easier to verify than perfect channels. Inf. Comput. 124(1), 20-31 (1996).
Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and Presburger arithmetic. In: Proceedings of 10th International Conference on Computer-Aided Verification (CAV'98). Lecture Notes in Computer Science, vol. 1427, pp. 268-279. Springer, Berlin (1998).
Cobham A.: On the base-dependence of sets of numbers recognizable by finite automata. Math. Syst. Theory 3, 186-192 (1969).
Dill, D. L.: Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of Automatic Verification Methods for Finite-State Systems. LNCS, vol. 407, pp. 197-212. Springer, Berlin (1989).
Eisinger J., Klaedtke F.: Don't care words with an application to the automata-based approach for real addition. Formal Methods Syst. Des. 33(1-3), 85-115 (2008).
Fribourg, L.: A closed-form evaluation for extended timed automata. Research Report LSV-98-2, LSV (1998).
Finkel A., Willems B., Wolper P.: A direct symbolic approach to model checking pushdown systems. Electr. Notes Theor. Comput. Sci. 9, 27-37 (1997).
Henzinger, T. A.: The theory of hybrid automata. In: Proceedings of 11th Symposium on Logic in Computer Science (LICS'96), pp. 278-292. IEEE Computer Society Press (1996).
Holtzmann G.: Design and Validation of Computer Protocols. Prentice Hall, New Jersey (1991).
Klarlund, N.: Progress measures for complementation of omega-automata with applications to temporal logic. In: Proceedings of 32nd Annual Symposium on Foundations of Computer Science (FOCS'91), pp. 358-367, San Juan, Puerto Rico. IEEE (1991).
Klaedtke, F.: Bounds on the automata size for Presburger arithmetic. ACM Trans. Comput. Log. 9(2), 11: 1-11: 34 (2008).
Kupferman, O., Vardi, M. Y.: Complementation constructions for nondeterministic automata on infinite words. In: Proceedings of 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05). Lecture Notes in Computer Science, vol. 3440, pp. 206-221, Edinburgh. Springer, Berlin (2005).
The Liège Automata-based Symbolic Handler (LASH). http://www. montefiore. ulg. ac. be/~boigelot/research/lash/.
Löding C.: Efficient minimization of deterministic weak ω-automata. Inf. Process. Lett. 79(3), 105-109 (2001).
Legay, A.: Extrapolating (omega-)regular model checking. Int. J. Softw. Tools Technol. Transfer (2011), doi: 10. 1007/s10009-011-0209-7.
Linear Integer/Real Arithmetic solver (LIRA). http://lira. gforge. avacs. org/.
McMillan K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993).
Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du Premier Congrès des Mathématiciens des Pays Slaves, pp. 92-101, Warsaw (1929).
Safra, S.: On the complexity of ω-automata. In: Proceedings of 29th Symposium on Foundations of Computer Science (FOCS'88), pp. 319-327. IEEE Computer Society (1988).
Schrijver A.: Theory of Linear and Integer Programming. Wiley, New York (1986).
Semenov A. L.: Presburgerness of predicates regular in two number systems. Sib. Math. J. 18, 289-299 (1977).
Staiger L., Wagner K.: Automatentheoretische und automatenfreie charakterisierungen topologischer klassen regulärer folgenmengen. Elektron. Informationsverarbeitung und Kybernetik EIK 10, 379-392 (1974).
Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger arithmetic constraints. In: Proceedings of 2nd International Symposium on Static Analysis (SAS'95). LNCS, vol. 983, pp. 21-32. Springer, Berlin (1995).
Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Proceedings of 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00). Lecture Notes in Computer Science, vol. 1785, pp. 1-19. Springer, Berlin (2000).
Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: ISSAC: Proceedings of the ACM SIGSAM International Symposium on Symbolic and Algebraic Computation, pp. 129-136. ACM Press, Vancouver (1999).
Wilke, T.: Locally threshold testable languages of infinite words. In: Proceedings of 10th Annual Symposium on Theoretical Aspects of Computer Science (STACS'93). LNCS, vol. 665, pp. 607-616. Springer, Würzburg (1993).