From Many Places to Few: Automatic Abstraction Refinement for Petri Nets

• Autorzy: Ganty P. , Raskin J-F. , Van Begin L.
• Języki publikacji: EN

Abstrakty

EN

Current algorithms for the automatic verification of Petri nets suffer from the explosion caused by the high dimensionality of the state spaces of practical examples. In this paper, we develop an abstract interpretation based analysis that reduces the dimensionality of state spaces that are explored during verification. In our approach, the dimensionality is reduced by trying to gather places that may not be important for the property to establish. If the abstraction that is obtained is too coarse, an automatic refinement is performed and a more precise abstraction is obtained. The refinement is computed by taking into account information about the inconclusive analysis. The process is iterated until the property is proved to be true or false.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 88, nr 3
• Strony: 275--305
• Opis fizyczny: bibliogr. 26 poz., tab., wykr.

Twórcy

autor

Ganty P.

autor

Raskin J-F.

autor

Van Begin L.

• Département d’Informatique Université Libre de Bruxelles (U.L.B.), Belgium,

Bibliografia

• [1] Abdulla, P. A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems, LICS '96: Proc. 11th Annual IEEE Symp. on Logic in Computer Science, IEEE Computer Society, 1996.
• [2] Abdulla, P. A., Iyer, S. P., Nylén, A.: Unfoldings of Unbounded Petri Nets., CAV '00: Proc. 12th Int. Conf. on Computer Aided Verification, 1855, Springer, 2000.
• [3] Berthelot, G., Roucairol, G., Valk, R.: Reductions of Nets and Parallel Prgrams, Advanced Course: Net Theory and Applications, 84, Springer, 1975.
• [4] Burris, S., Sankappanavar, H. P.: A Course in Universal Algebra, Springer, New York, 1981.
• [5] Ciardo, G., Miner, A.: Storage Alternatives for Large Structured State Space, Proc. Computer Performance Evaluation 1997: 9th Int. Conf. on Modelling Techniques and Tools, 1245, Springer, 1997.
• [6] Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking, J. ACM, 50(5), 2003, 752-794.
• [7] Cousot, P.: Semantic Foundations of Program Analysis, in: Program Flow Analysis: Theory and Applications (S. Muchnick, N. Jones, Eds.), chapter 10, Prentice-Hall, Inc., 1981, 303-342.
• [8] Cousot, P.: Partial Completeness of Abstract Fixpoint Checking, invited paper, SARA '00: Proc. 4th Int. Symp. on Abstraction, Reformulations and Approximation, 1864, Springer, 2000.
• [9] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL '77: Proc. 4th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, ACM Press, 1977.
• [10] Delzanno, G., Raskin, J.-F., Van Begin, L.: Attacking Symbolic State Explosion, CAV '01: Proc. 13th Int. Conf. on Computer Aided Verification, 2102, Springer, 2001.
• [11] Dickson, L. E.: Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors, Amer. J. Math., 35, 1913, 413-422.
• [12] Evangelista, S., Haddad, S., Pradat-Peyre, J.-F.: Syntactical Colored Petri Nets Reductions, ATVA '05: Proc. 3rd Int ˙ Symp˙on Automated Technology for Verification and Analysis, 3707, Springer, 2005.
• [13] Finkel, A.: The minimal coverability graph for Petri nets, APN '93: Proc. 14th Int. Conf. on Application and Theory of Petri Nets, 674, Springer, 1993.
• [14] Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!, Theoretical Computer Science, 256(1-2), 2001, 63-92.
• [15] Ganty, P., Meuter, C., Delzanno, G., Kalyon, G., Raskin, J.-F., Van Begin, L.: Symbolic Data Structure for sets of k-uples, Technical report, Université Libre de Bruxelles, Belgium, 2007.
• [16] Ganty, P., Raskin, J.-F., Van Begin, L.: A Complete Abstract Interpretation Framework for Coverability Properties of WSTS, VMCAI '06: Proc. 7th Int. Conf. on Verification, Model Checking and Abstract Interpretation, 3855, Springer, 2006.
• [17] Ganty, P., Raskin, J.-F., Van Begin, L.: From Many Places to Few: Automatic Abstraction Refinement for Petri Nets, ICATPN '07: Proc. of 28th Int. Conf. on Application and Theory of Petri Nets and Other Models of Concurrency, 4546, Springer, 2007.
• [18] Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS, FSTTCS '04: Proc. 24th Int. Conf. on Fondation of Software Technology and Theoretical Computer Science, 3328, Springer, 2004.
• [19] Geeraerts, G., Raskin, J.-F., Van Begin, L.: On the efficient Computation of the Minimal Coverability set of Petri nets, ATVA '07: Proc. 5th Int. Symp. on Automated Technology for Verification and Analysis, 4762, Springer, 2007.
• [20] German, S. M., Sistla, A. P.: Reasoning about Systems with Many Processes, Journal of ACM, 39(3), 1992, 675-735.
• [21] Grahlmann, B.: The PEP Tool, CAV'97: Proc. 9th Int. Conf. on Computer Aided Verification, 1254, Springer, 1997.
• [22] Karp, R. M., Miller, R. E.: Parallel Program Schemata., Journal of Comput. Syst. Sci., 3(2), 1969, 147-195.
• [23] Manolopoulos, Y.: Binomial coefficient computation: Recursion or Iteration, ACM SIGCSE Bulletin, 34(4), 2002, 65-67.
• [24] Marsan, M. A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets, Wiley series in parallel computing, Wiley, 1995.
• [25] Park, D.: Fixpoint Induction and Proofs of Program Properties, in: Machine Intelligence, vol. 5, American Elsevier, 1969, 59-78.
• [26] Van Begin, L.: Efficient Verification of Counting Abstractions for Parametric systems, Ph.D. Thesis, Université Libre de Bruxelles, Belgium, 2003.