×

State space analysis of Petri nets with relation-algebraic methods. (English) Zbl 1156.68040

Summary: A large variety of systems can be modelled by Petri nets. Their formal semantics are based on linear algebra which in particular allows the calculation of a Petri net’s state space. Since state space explosion is still a serious problem, efficiently calculating, representing, and analysing the state space is mandatory. We propose a formal semantics of Petri nets based on executable relation-algebraic specifications. Thereupon, we suggest how to calculate the markings reachable from a given one simultaneously. We provide an efficient representation of reachability graphs and show in a correct-by-construction approach how to efficiently analyse their properties. Therewith we cover two aspects: modelling and model checking systems by means of one and the same logic-based approach. On a practical side, we explore the power and limits of relation-algebraic concepts for concurrent system analysis.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
03G15 Cylindric and polyadic algebras; relation algebras

Software:

RelView; KURE
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Behnke, R.; Berghammer, R.; Meyer, E.; Schneider, P., RelView — A system for calculating with relations and relational programming, (Astesiano, E., Proceedings of the 1st International Conference on Fundamental Approaches to Software Engineering. Proceedings of the 1st International Conference on Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science (LNCS), vol. 1382 (1996), Springer), 318-321
[2] Berghammer, R., Relation-algebraic computation of fixed points with applications, Journal of Logic and Algebraic Programming, 66, 112-126 (2006) · Zbl 1086.68095
[3] Berghammer, R.; Fronk, A., Exact computation of minimum feedback vertex sets with relational algebra, Fundamenta Informaticae, 70, 4, 301-316 (2006) · Zbl 1110.68093
[4] Berghammer, R.; Karger, B.; Ulke, C., Relational-algebraic analysis of Petri nets with RelView, (Margaria, T.; Steffen, B., Proceedings of the 2nd Workshop on Tools and Applications for the Construction and Analysis of Systems (TACAS ’96). Proceedings of the 2nd Workshop on Tools and Applications for the Construction and Analysis of Systems (TACAS ’96), Lecture Notes in Computer Science (LNCS), vol. 1055 (1996), Springer), 49-69
[5] Berghammer, R.; Leoniuk, B.; Milanese, U., Proceedings of the 6th International Workshop on Relational Methods in Computer Science, RelMiCS6, (de Swart, H., Lecture Notes in Computer Science (LNCS), vol. 2561 (2002), Springer), 241-257
[6] Bieber, B.; Fleischhack, H., Model checking of time Petri nets based on partial order semantics, (Baeten, J. C.M.; Mauw, S., Proceedings of the 10th International Conference on Concurrency Theory. Proceedings of the 10th International Conference on Concurrency Theory, Lecture Notes in Computer Science (LNCS), vol. 1664 (1999), Springer), 210-255 · Zbl 0940.68090
[7] Corradini, A.; Große-Rhode, M.; Heckel, R., A coalgebraic presentation of structured transition systems, Theoretical Computer Science, 260, 27-55 (2001) · Zbl 0973.68173
[8] Dingle, N.; Harrison, P.; Knottenbelt, W., Response time densities in generalised stochastic petri net models, (Proceedings of the 3rd International Workshop on Software and Performance (2002), ACM Press), 46-54
[9] Emerson, E.A., Namjoshi, K.S., 1998. On model checking for non-deterministic infinite-state systems. In: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science. pp. 70-80; Emerson, E.A., Namjoshi, K.S., 1998. On model checking for non-deterministic infinite-state systems. In: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science. pp. 70-80 · Zbl 0945.68523
[10] Esparza, J., Decidability of model checking for infinite-state concurrent systems, Acta Informatica, 34, 85-107 (1997) · Zbl 0865.68046
[11] Esparza, J.; Heljanko, K., A new unfolding approach to LTL model checking, (Montanari, U.; Rolim, J. D.P.; Welzl, E., Proceedings of the 27th International Colloquium on Automata, Languages, and Programming. Proceedings of the 27th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science (LNCS), vol. 1853 (2000), Springer-Verlag), 475-486 · Zbl 0973.68140
[12] Esparza, J.; Nielsen, M., Decidability issues for Petri nets — a survey, Journal of Information Processing and Cybernetics, 30, 3, 143-160 (1994) · Zbl 0838.68082
[13] Esparza, J.; Schröter, C., Unfolding based algorithms for the reachability problem, Fundamenta Informaticae, 47, 3-4, 231-245 (2001) · Zbl 1004.68113
[14] Finkel, A., The Minimal Coverability Graph for Petri Nets, (Rozenberg, G., Advances in Petri Nets. Advances in Petri Nets, Lecture Notes in Computer Science (LNCS), vol. 674 (1993), Springer), 210-243
[15] Fronk, A., Using relation algebra for the analysis of Petri nets in a CASE tool based approach, (2nd IEEE International Conference on Software Engineering and Formal Methods, SEFM (2004), IEEE: IEEE Beijing), 396-405
[16] Fronk, A., 2006. Relation-algebraic Analysis of Petri Nets. Script available at ftp://ls10-ftp.cs.uni-dortmund.de/pub/Lehre/PetRA-WiSe0506/Skript.pdf; Fronk, A., 2006. Relation-algebraic Analysis of Petri Nets. Script available at ftp://ls10-ftp.cs.uni-dortmund.de/pub/Lehre/PetRA-WiSe0506/Skript.pdf
[17] Fronk, A., Kehden, B., 2006. State space analysis of petri nets with relation-algebraic methods. Memorandum 163, Lehrstuhl Software-Technologie, Universität Dortmund; Fronk, A., Kehden, B., 2006. State space analysis of petri nets with relation-algebraic methods. Memorandum 163, Lehrstuhl Software-Technologie, Universität Dortmund · Zbl 1156.68040
[18] Fronk, A., Pleumann, J., 2005a. Petri net analysis based on relation algebra, http://ls10-www.cs.uni-dortmund.de/index.php?id=134; Fronk, A., Pleumann, J., 2005a. Petri net analysis based on relation algebra, http://ls10-www.cs.uni-dortmund.de/index.php?id=134 · Zbl 1185.05087
[19] Fronk, A.; Pleumann, J., Relation-algebraic analysis of petri nets: Concepts and implementation, Petri Net News Letters, 61-68 (2005)
[20] Fronk, A., Pleumann, J., Schönlein, R., Szymanski, O., 2005. KURE-Java, http://ls10-www.cs.uni-dortmund.de/index.php?id=136; Fronk, A., Pleumann, J., Schönlein, R., Szymanski, O., 2005. KURE-Java, http://ls10-www.cs.uni-dortmund.de/index.php?id=136
[21] Kehden, B., Evaluating sets of search points using relational algebra, (Proceedings of the 9th International Conference on Relational Methods in Computer Science, RelMiCS 9. Proceedings of the 9th International Conference on Relational Methods in Computer Science, RelMiCS 9, LNCS, vol. 4136 (2006), Springer), 266-280 · Zbl 1134.68497
[22] Konikowska, B.; Orlowska, E., A relational formalisation of a generic many-valued modal logic, (Orlowska, E.; Szalas, A., Relational methods for computer science applications. Studies in Fuzziness and Soft Computing (2001), Physica-Verlag), 183-202 · Zbl 0998.03018
[23] Latvala, T.; Heljanko, K., Coping with strong fairness, Fundamenta Informaticae, 34, 1-19 (2000) · Zbl 0965.68061
[24] Leuschel, M.; Massart, T., Infinite state model checking by abstract interpretation and program specialisation, (Bossi, A., Proceedings of Logic-Based Program Synthesis and Transformation. Proceedings of Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science (LNCS), vol. 1817 (1999), Springer), 63-82 · Zbl 0964.68086
[25] Milanese, U., 2003. KURE: Kiel University Relation Package, http://cvs.informatik.uni-kiel.de/ kure/; Milanese, U., 2003. KURE: Kiel University Relation Package, http://cvs.informatik.uni-kiel.de/ kure/
[26] Notomi, M.; Murata, T., Hierarchical reachability graph of bounded petri nets for concurrent-software analysis, IEEE Transactions on Software Engineering, 20, 5, 325-336 (1994) · Zbl 0810.68099
[27] Pastor, E.; Roig, O.; Cortadella, J.; Badia, R. M., Petri net analysis using boolean manipulation, (Valette, R., Proceedings of the 15th International Conference on Application and Theory of Petri Nets. Proceedings of the 15th International Conference on Application and Theory of Petri Nets, Lecture Notes in Computer Science (LNCS), vol. 815 (1994), Springer), 416-435
[28] Schlinghoff, H.; Heinle, W., Relation algebra and modal logics, (Relational Methods in Computer Science. Advances in Computer Science (1996), Springer), 70-89 · Zbl 0883.03050
[29] Schmidt, G.; Ströhlein, T., Relations and graphs, (EATCS Monographs on Theoretical Computer Science (1993), Springer) · Zbl 0581.05026
[30] Starke, P. H., Analyse von Petri-Netz-Modellen (1990), Teubner · Zbl 0724.68002
[31] Tarski, A.; Givant, S., A Formalization of Set Theory without Variables, (Amer. Math. Soc., vol. 41 (1987), Amer. Math. Soc. Colloq. Publ.) · Zbl 0654.03036
[32] Valmari, A., Stubborn sets for reduced state space generation, (Rozenberg, G., Advances in Petri Nets. Advances in Petri Nets, Lecture Notes in Computer Science (LNCS), vol. 483 (1990), Springer), 491-515
[33] Valmari, A., The state explosion problem, (Lectures on Petri nets: Advances in Petri nets (1998), Springer), 429-473
[34] Wegener, I., 2000. Branching programs and binary decision diagrams. In: SIAM Monographs on Discrete Mathematics and Applications; Wegener, I., 2000. Branching programs and binary decision diagrams. In: SIAM Monographs on Discrete Mathematics and Applications · Zbl 0956.68068
[35] Woodside, C.M., Li, Y., 1991. Performance petri net analysis of communication protocol software by delay-equivalent aggregation. In: Proceedings of the 4th International Workshop on Petri nets and Performance Models, pp. 64-73; Woodside, C.M., Li, Y., 1991. Performance petri net analysis of communication protocol software by delay-equivalent aggregation. In: Proceedings of the 4th International Workshop on Petri nets and Performance Models, pp. 64-73
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.