State Space Reduction for Dynamic Process Creation

Published in Volume XX, 2010, pages 131-157

Authors: H. Klaudel, M. Koutny, E. Pelz, and F. Pommereau

Abstract

Automated verification of dynamic multi-threaded computing systems is severely affected by problems relating to dynamic process creation. In this paper, we describe an abstraction technique aimed at generating reduced state space representations for such systems. To make the new technique applicable to a wide range of different system models, we express it in terms of general labelled transition systems.

Full Text (PDF)

References

[1] D. Bosnacki, D. Dams, and L. Holenderski. Symmetric Spin. International Journal on Software Tools for Technology Transfer, 4(1):92-106, 2002.

[2] G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad. A Symbolic Reachability Graph for Coloured Petri Nets. Theoretical Computer Science, 176:39-65, 1997.

[3] E. M. Clarke, E. A. Emerson, S. Jha, and A. P. Sistla. Symmetry Reductions in Model Checking. In Proceedings of the 10th International Conference on Computer Aided Verication (CAV’98), vol. 1427 of Lecture Notes in Computer Science, pp. 147-158, 1998.

[4] L. P. Cordella, P. Foggia, C. Sansone, and M. Vento. A (Sub)Graph Isomorphism Algorithm for Matching Large Graphs. IEEE Transactions on Pattern Analysis and Machine Intelligence, 26:1367-1372, 2004

[5] A.Hagberg, D. Schult, P. Swart. NetworkX, High Productivity Software for Complex Networks. http://networkx.lanl.gov

[6] M. Hendriks, G. Behrmann, K.G. Larsen, P. Niebert, and F.W. Vaandrager. Adding Symmetry Reduction to UPPAAL. In Proceedings of the First International Workshop on Formal Modeling and Analysis of Timed Systems (FORMATS’03), vol. 2791 of Lecture Notes in Computer Science, pp. 46-59, 2004.

[7] C. Norris Ip and David L. Dill. Better Verication Through Symmetry. Formal Methods in System Design, 9:41-75, 1996.

[8] J. B. Jørgensen and L. M. Kristensen. Verication of Coloured Petri Nets Using State Spaces with Equivalence Classes. LINCOM Studies in Computer Science, 1:17-34, 2003.

[9] T. Junttila. On the Symmetry Reduction Method for Petri Nets and Similar Formalisms. PhD Thesis, HUT, Espoo, Finland, 2003.

[10] V. Khomenko. Model Checking Based on Prexes of Petri Net Unfoldings. PhD Thesis, School of Computing Science, University of Newcastle, 2003.

[11] H. Klaudel, M. Koutny, E. Pelz, and F. Pommereau. Towards Ecient Verication of Systems with Dynamic Process Creation. In Proceedings of the 5th International Colloquium on Theoretical Aspects of Computing (ICTAC’08), vol. 5160 of Lecture Notes in Computer Science, pp. 186-200, 2008.

[12] H. Klaudel, M. Koutny, E. Pelz, and F. Pommereau. An Approach to State Space Reduction for Systems with Dynamic Process Creation. In Proceedings of the 24th International Symposium on Computer and Information Sciences (ISCIS’09), pp. 543-548, 2009.

[13] K. Jensen and L.M. Kristensen Coloured Petri Nets: Modelling and Validation of Concurrent Systems. Springer, 2009.

[14] B. D. McKay. Practical Graph Isomorphism. Congressus Numerantium, 30: 45-87, 1981.

[15] K. McMillan. Symbolic Model Checking. Kluwer Academic, 1993.

[16] A. Miller, A. Donaldson, and M. Calder. Symmetry in Temporal Logic Model Checking. ACM Computer Surveys, 38(3):Article 8, 2006.

[17] W. Stein. Sage Mathematics Software. The Sage Group (2007) http://www.sagemath.org

Bibtex

@article{sacscuza:klaudel2010ssrfdpc,
  title={State Space Reduction for Dynamic Process Creation},
  author={H. Klaudel and M. Koutny and E. Pelz and F. Pommereau},
  journal={Scientific Annals of Computer Science},
  volume={20},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2010},
  pages={131--157},
  publisher={``A.I. Cuza'' University Press}
}