Abstract
As some structural properties, like generative families of positive P-invariants, can only be computed in P/T nets, unfolding of Colored Petri Nets is of interest. However, it may generate huge nets that cannot be stored concretely in memory. In some cases, removing the dead parts of the unfolded net can dramatically reduce its size, but this operation requires the unfolded net to be represented anyway. This paper presents a symbolic representation of unfolded nets using Data Decision Diagrams. This technique allows to store very large models and manipulate them for optimization purpose.
Chapter PDF
Similar content being viewed by others
References
Bernardi, S., Donatelli, S., Merseguer, J.: From UML sequence diagrams and statecharts to analysable Petri net models. In: WOSP 2002: Proceedings of the 3rd int. workshop on Software and performance, pp. 35–45. ACM Press, New York (2002)
Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Chiola, G., Dutheillet, C., Franceschini, G., Haddad, S.: On Well-Formed Coloured Nets and their Symbolic Reachability Graph. In: High-Level Petri Nets. Theory and Application. LNCS. Springer, Heidelberg (1991)
Couvreur, J.-M., Encrenaz, E., Paviot-Adet, E., Poitrenaud, D., Wacrenier, P.-A.: Data decision diagrams for petri net analysis. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 101–120. Springer, Heidelberg (2002)
Couvreur, J.-M., Haddad, S., Peyre, J.F.: Generative families of positive invariants in coloured nets sub-classes. In: Rozenberg, G. (ed.) Applications and Theory of Petri Nets. LNCS, pp. 51–70. Springer, Heidelberg (1991)
de Groot, A., Hooman, J., Kordon, F., Paviot-Adet, E., Vernier-Mounier, I., Lemoine, M., Gaudiere, G., Winter, V., Kapur, D.: A survey: Applying formal methods to a software intensive system. In: 6th International Symposium on High-Assurance Systems Engineering, pp. 55–64. IEEE Computer Society, Los Alamitos (2001)
Hugues, J., Thierry-Mieg, Y., Kordon, F., Pautet, L., Baarir, S., Vergnaud, T.: On the Formal Verification of Middleware Behavioral Properties. In: Proceedings of the 9th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004). ENTCS, vol. 133, pp. 139–157. Elsevier, Amsterdam (2004)
Jensen, K.: Coloured Petri nets and the invariant-method. Theor. Comput. Sci. 14, 317–336 (1981)
Mäkelä, M.: Optimising enabling tests and unfoldings of algebraic system nets. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 283–302. Springer, Heidelberg (2001)
Peterson, G.L.: Myths about the mutual exclusion problem. Information Processing Letters 12(3), 115–116 (1981)
Valk, R.: Basic definitions. In: Girault, C., Valk, R. (eds.) Petri nets and system engineering, ch. 4, 1st edn., pp. 41–51. Springer, Heidelberg (2003)
Thierry-Mieg, Y., Dutheillet, C., Mounier, I.: Automatic Symmetry Detection in Well-Formed Nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 82–101. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Kordon, F., Linard, A., Paviot-Adet, E. (2006). Optimized Colored Nets Unfolding. In: Najm, E., Pradat-Peyre, JF., Donzeau-Gouge, V.V. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2006. FORTE 2006. Lecture Notes in Computer Science, vol 4229. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11888116_25
Download citation
DOI: https://doi.org/10.1007/11888116_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-46219-4
Online ISBN: 978-3-540-46220-0
eBook Packages: Computer ScienceComputer Science (R0)