Abstract
Many infinite state systems can be seen as well-structured transition systems (WSTS), i.e., systems equipped with a well-quasi-ordering on states that is also a simulation relation. WSTS are an attractive target for formal analysis because there exist generic algorithms that decide interesting verification problems for this class. Among the most popular algorithms are acceleration-based forward analyses for computing the covering set. Termination of these algorithms can only be guaranteed for flattable WSTS. Yet, many WSTS of practical interest are not flattable and the question whether any given WSTS is flattable is itself undecidable. We therefore propose an analysis that computes the covering set and captures the essence of acceleration-based algorithms, but sacrifices precision for guaranteed termination. Our analysis is an abstract interpretation whose abstract domain builds on the ideal completion of the well-quasi-ordered state space, and a widening operator that mimics acceleration and controls the loss of precision of the analysis. We present instances of our framework for various classes of WSTS. Our experience with a prototype implementation indicates that, despite the inherent precision loss, our analysis often computes the precise covering set of the analyzed system.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313–321 (1996)
Abdulla, P.A., Collomb-Annichini, A., Bouajjani, A., Jonsson, B.: Using forward reachability analysis for verification of lossy channel systems. FMSD 25(1), 39–65 (2004)
Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: LICS, pp. 160–170 (1993)
Azzopardi, T.: Generic compute server in Scala using remote actors (2008), http://tiny.cc/yjzva (accessed November 2011)
Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. Software Tools for Technology Transfer 8(4/5), 449–466 (2006)
Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL, pp. 289–300 (2009)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282. ACM (1979)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992)
Dufourd, C., Finkel, A., Schnoebelen, P.: Reset Nets Between Decidability and Undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103–115. Springer, Heidelberg (1998)
Engelfriet, J., Gelsema, T.: Multisets and structural congruence of the pi-calculus with replication. Theor. Comput. Sci. 211(1-2), 311–337 (1999)
Finkel, A., Goubault-Larrecq, J.: Forward Analysis for WSTS, Part I: Completions. In: STACS. Dagstuhl Sem. Proc., vol. 09001, pp. 433–444 (2009)
Finkel, A., Goubault-Larrecq, J.: Forward Analysis for WSTS, Part II: Complete WSTS. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 188–199. Springer, Heidelberg (2009)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63–92 (2001)
Ganty, P., Raskin, J.-F., Van Begin, L.: A Complete Abstract Interpretation Framework for Coverability Properties of WSTS. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 49–64. Springer, Heidelberg (2005)
Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, Enlarge and Check: New algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72(1), 180–203 (2006)
Goubault-Larrecq, J.: On noetherian spaces. In: LICS, pp. 453–462. IEEE Computer Society (2007)
Haller, P., Odersky, M.: Scala actors: Unifying thread-based and event-based programming. Theor. Comput. Sci. 410(2-3), 202–220 (2009)
Joshi, S., König, B.: Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 214–226. Springer, Heidelberg (2008)
Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)
Lift. Lift web framework, http://liftweb.net/
Meyer, R.: On boundedness in depth in the pi-calculus. In: IFIP TCS. IFIP, vol. 273, pp. 477–489. Springer, Boston (2008)
Milner, E.C.: Basic wqo- and bqo-theory. Graphs and order (1985)
Milner, R.: The polyadic pi-calculus: A tutorial. In: Logic and Algebra of Specification. Computer and Systems Sciences. Springer, Heidelberg (1993)
Petri, C.A., Reisig, W.: Scholarpedia 3(4), 6477 (2008), http://www.scholarpedia.org/article/Petri_net
Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5) (2007)
Schnoebelen, P.: Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010)
Wies, T., Zufferey, D., Henzinger, T.A.: Forward Analysis of Depth-Bounded Processes. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 94–108. Springer, Heidelberg (2010)
Zufferey, D., Wies, T.: Picasso Analyzer, http://ist.ac.at/~zufferey/picasso/
Zufferey, D., Wies, T., Henzinger, T.A.: On ideal abstractions for well-structured transition systems. Technical Report IST-2011-10, IST Austria (November 2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zufferey, D., Wies, T., Henzinger, T.A. (2012). Ideal Abstractions for Well-Structured Transition Systems. In: Kuncak, V., Rybalchenko, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2012. Lecture Notes in Computer Science, vol 7148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27940-9_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-27940-9_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27939-3
Online ISBN: 978-3-642-27940-9
eBook Packages: Computer ScienceComputer Science (R0)