Article

Efficient state-based analysis by introducing bags in Petri nets color domains

Authors:

Fabrice Kordon,

Laure Petrucci,

Jean-François Pradat-Peyre,

Nicolas TrèvesAuthors Info & Claims

ACC'09: Proceedings of the 2009 conference on American Control Conference

Pages 5018 - 5025

Published: 10 June 2009 Publication History

Abstract

The use of high-level nets, such as coloured Petri nets, is very convenient for modelling complex controllable systems in order to have a compact, readable and structured specification. However, when coming to the analysis phase, using too elaborate types becomes a burden.

A good trade-off between expressiveness and analysis capabilities is then to have only simple types, which is achieved with symmetric nets. These latter nets enjoy the possibility of generating a symbolic reachability graph, which is much smaller than the whole state space and still allows for exhaustive analysis.

In this paper, we extend the symmetric net model with bags on arcs. Hence, variables can be bags of tokens, leading to more flexible models. We show that symmetric nets with bags also allow for applying the symbolic reachability graph technique with application to deadlock detection and more generally for safety properties.

References

[1]

K. Jensen, "Coloured Petri nets and the invariant-method," Theor. Comput. Sci., vol. 14. pp. 317-336. 1981.

[2]

M. Beaudouin-Lafon. W. Mackay. M. Jensen. P. Andersen. P. Janecek. H. Lassen. K. Lund. K. Monensen. S. Munck. A. Ratzer. K. Ravn. S. Christensen. and K. Jensen, "CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS," in Tools and Algorithms for the Construction and Analysis of Systems. 7th International Conference. TACAS 2001, L. Springer Verlag, Ed., vol. 2031. 2001 pp. 574-577.

Digital Library

[3]

K. Jensen. L. Kristensen. and L. Wells, "Coloured Petri Ncts and CPN Tools for modelling and validation of concurrent systems," STIT, vol. 9. no. 3-4. pp. 213-254. 2007.

[4]

W. Reisig. "Petri nets and algebraic specifications," Theoretical Computer Science, vol. 80, pp. 1-34, 1991, newsletterInfo: 38, 39.

Digital Library

[5]

H. Genrich and K. Lautenbach, "System modeling with high-level Petri-nets," in Theoretical Computer Science, no. 13. 1981. pp. 103-136.

[6]

L. Hillah, F. Kordon, L. Petrucci, and N. Trèves, "PN standardisation : a survey," in International Conference on Formal Methods for Networked and Distributed Systems (FORTE'06), vol. 4229. Paris, France: Springer Verlag, LNCS, September 2006, pp. 307-322.

Digital Library

[7]

G. Chiola, C. Dutheillet, G. Francesehinis, and S. Haddad, "Stochastic well-formed colored nets and symmetric modeling applications," IEEE Transactions on Computers, vol. 42, no. 11, pp. 1343-1360, 1993. {Online}. Available: citeseer.ist.psu.edu/chiola93stochastic.html

Digital Library

[8]

G. Chiola, C. Dutheillet, G. Francesehinis, and S. Haddad, "A symbolic reachability graph for coloured Petri nets," Theoretical Computer Science, vol. 176, no. 1-2, pp. 39-65, 1997.

Digital Library

[9]

H. Klauck, "Algorithms for parity games," in Automata, Logics, and Infinite Games, ser. LNCS, vol. 2500. Springer, 2002, pp. 107-129.

Digital Library

[10]

A. de Groot, J. Hooman, F. Kordon, E. Paviot-Adet, I. Vernier-Mounier, M. Lemoine, G. Gaudiere, V. Winter, and D. Kapur, "A survey: Applying formal methods to a software intensive system," in 6th International Symposium on High-Assurance Systems Engineering. IEEE Computer Society, 2001, pp. 55-64.

Digital Library

[11]

F. Bonnefoi, L. Hillah, F. Kordon, and G. Frémont, "An approach to model variations of a scenario: Application to Intelligent Transport Systems," in Workshop on Modelling of Objects, Components, and Agents (MOCA'06), Turku, Finland, June 2006.

[12]

P. Huber, A. M. Jensen, L. O. Jepsen, and K. Jensen, "Reachability trees for high-level petri nets," Theoretical Computer Science, Vol 45, no. 3, pp. 261-292, 1986, newsletterInfo: 27.

Digital Library

[13]

T. Junttila, "On the symmetry reduction method for petri nets and similar fonnalisms," Ph.D. dissertation, Helsinki University of Technology, Espoo, Finland, 2003.

[14]

F. A. Emerson and A. P. Sistla, "Symmetry and model checking," Formal Methods in System Design: An International Journal, vol. 9, no. 1/2, pp. 105-131, August 1996. {Online}. Available: citeseer.ist.psu.edu/emerson94symmetry.html

Digital Library

[15]

K. Schmidt, "How to calculate symmetries of petri nets," Acta Inf., vol. 36, no. 7, pp. 545-590, 2000.

[16]

E. A. Emerson and R. J. Trefler, "From asymmetry to full symmetry: New techniques for symmetry reduction in model checking," in CHARME, ser. Lecture Notes in Computer Science, vol. 1703. Springer, 1999, pp. 142-156.

Digital Library

[17]

S. Baarir, C. Dutheillet, S. Haddad, and J.-M. Ilié, "On the use of exact lumpability in partially symmetrical well-formed nets," in QEST. IEEE Computer Society, 2005, pp. 23-32.

Digital Library

[18]

S. Haddad, F. Kordon, L. Petrucci, J.-F. Pradat-Peyre, and N. Trèves, "Efficient State-Based Analysis by Introducing Bags in Petri Nets Color Domains," LSV, École Nonnal Supérieure de Cachan, Tech. Rep. RR LSV 09-07, March 2009.

[19]

A. Hamez, L. Hillah, F. Kordon, A. Linard. E. Paviot-Adet. X. Renault, and Y. Thierry-Mieg, "New features in CPN-AMI 3 : focusing on the analysis of complex distributed systems," in 6th International Conference on Application of Concurrency to System Design (ACSD'06). Turku, Finland: IEEE Computer Society, June 2006, pp. 273-275.

Digital Library

Cited By

Yessad AMounier ILabat JKordon FCarron T(2014)Have You Found the Error? A Formal Framework for Learning Game VerificationProceedings of the 9th European Conference on Open Learning and Teaching in Educational Communities - Volume 871910.1007/978-3-319-11200-8_45(476-481)Online publication date: 16-Sep-2014
https://dl.acm.org/doi/10.1007/978-3-319-11200-8_45
Colange MHillah LKordon FParutto P(2012)Extreme symmetries in complex distributed systemsProceedings of the 17th Monterey conference on Large-Scale Complex IT Systems: development, operation and management10.1007/978-3-642-34059-8_17(330-352)Online publication date: 19-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-34059-8_17
Colange MBaarir SKordon FThierry-Mieg Y(2011)CrocodileProceedings of the 32nd international conference on Applications and theory of Petri Nets10.5555/2022192.2022215(338-347)Online publication date: 20-Jun-2011
https://dl.acm.org/doi/10.5555/2022192.2022215

Efficient state-based analysis by introducing bags in Petri nets color domains
1. Theory of computation

Recommendations

Non Equivalence between Time Petri Nets and Time Stream Petri Nets
PNPM '99: Proceedings of the The 8th International Workshop on Petri Nets and Performance Models

It had been shown that Merlin's Time Petri Nets are a special case of Time Stream Petri Nets. In this paper, we show that it does not exist a time equivalence between both models. We extend first this result to the nonequivalence of Timed Automata and ...
Efficient unfolding of contextual Petri nets

A contextual net is a Petri net extended with read arcs, which allows transitions to check for tokens without consuming them. Contextual nets allow for better modelling of concurrent read access than Petri nets, and their unfoldings can be exponentially ...
From Petri Nets to colored Petri Nets: a tutorial introduction to nets based formalism for modeling and simulation
WSC '19: Proceedings of the Winter Simulation Conference

Petri Net, a widely studied mathematical formalism, is a graphical notation for modeling systems. Petri Nets provide the foundation for modeling concurrency, communication, synchronization, and resource sharing constraints that are inherent to many ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ACC'09: Proceedings of the 2009 conference on American Control Conference

June 2009

5820 pages

ISBN:9781424445233

Publisher

IEEE Press

Publication History

Published: 10 June 2009

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 15 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Yessad AMounier ILabat JKordon FCarron T(2014)Have You Found the Error? A Formal Framework for Learning Game VerificationProceedings of the 9th European Conference on Open Learning and Teaching in Educational Communities - Volume 871910.1007/978-3-319-11200-8_45(476-481)Online publication date: 16-Sep-2014
https://dl.acm.org/doi/10.1007/978-3-319-11200-8_45
Colange MHillah LKordon FParutto P(2012)Extreme symmetries in complex distributed systemsProceedings of the 17th Monterey conference on Large-Scale Complex IT Systems: development, operation and management10.1007/978-3-642-34059-8_17(330-352)Online publication date: 19-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-34059-8_17
Colange MBaarir SKordon FThierry-Mieg Y(2011)CrocodileProceedings of the 32nd international conference on Applications and theory of Petri Nets10.5555/2022192.2022215(338-347)Online publication date: 20-Jun-2011
https://dl.acm.org/doi/10.5555/2022192.2022215

View Options

View options

Figures

Tables

Media

View Table of Conten