×

zbMATH — the first resource for mathematics

Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques. (English) Zbl 1309.68140
Summary: Multisingular hybrid Petri net (MSHPN) is an extension of hybrid Petri nets enriched with the capabilities of hybrid automata to achieve the practical expressive power of multisingular hybrid automata. In this paper, we define parametric multisingular hybrid Petri nets (\(\mathcal{P}\)-MSHPNs), as a parametric extension of MSHPNs. We present the parametric reachability analysis techniques and algorithms and prove that the parametric reachability analysis of \(\mathcal{P}\)-MSHPNs amounts to the analysis of standard MSHPNs. Once the parametric state space of a \(\mathcal{P}\)-MSHPNs model is computed, it can either be used for parametric model checking analysis using the existing techniques or be instantiated to obtain non-parametric state spaces. \(\mathcal{P}\)-MSHPNs models can be analysed to obtain the set of feasible configurations for the system parameters. We also give a method for deriving the set of constraints on the parameters that ensure the correctness of an invariant property and a method for finding the optimum parameter configuration.
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q45 Formal languages and automata
Software:
HyTech; Kronos; PPL
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Silva, Manuel; Recalde, Laura, On fluidification of Petri nets: from discrete to hybrid and continuous models, Annu. Rev. Control, 28, 2, 253-266, (2004)
[2] Recalde, Laura; Haddad, Serge; Silva, Manuel, Continuous Petri nets: expressive power and decidability issues, Int. J. Found. Comput. Sci., 21, 2, 235-256, (2010) · Zbl 1200.68164
[3] Henzinger, Thomas A., The theory of hybrid automata, (Proceedings of the 11th Annual Symposium on Logic in Computer Science, New Brunswick, USA, (1996)), 278-292 · Zbl 0959.68073
[4] Alur, Rajeev; Courcoubetis, Costas; Halbwachs, Nicolas; Henzinger, Thomas A.; Ho, Pei-Hsin; Nicollin, Xavier; Olivero, Alfredo; Sifakis, Joseph; Yovine, Sergio, The algorithmic analysis of hybrid systems, Theor. Comput. Sci., 138, 1, 3-34, (1995)
[5] Alur, Rajeev; Dill, David L., A theory of timed automata, Theor. Comput. Sci., 126, 2, 183-235, (1994) · Zbl 0803.68071
[6] Henzinger, Thomas A.; Nicollin, Xavier; Sifakis, Joseph; Yovine, Sergio, Symbolic model checking for real-time systems, Inf. Comput., 111, 2, 193-244, (1994) · Zbl 0806.68080
[7] David, René; Alla, Hassane, Discrete, continuous and hybrid Petri nets, (2005), Springer-Verlag · Zbl 1074.93002
[8] Lime, Didier; Roux, Olivier, Formal verification of real-time systems with preemptive scheduling, Real-Time Syst., 41, 2, 118-151, (2009) · Zbl 1185.68429
[9] David, René; Alla, Hassane, Autonomous and timed continuous Petri nets, (Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, France, (1990)), 367-386
[10] Balduzzi, Fabio; Di Febbraro, Angela; Giua, Alessandro; Seatzu, Carla, Decidability results in first-order hybrid Petri nets, Discrete Event Dyn. Syst., 11, 1-2, 41-57, (2001) · Zbl 0971.93051
[11] David, René; Alla, Hassane, On hybrid Petri nets, Discrete Event Dyn. Syst., 11, 1-2, 9-40, (2001) · Zbl 0969.93024
[12] Bérard, Béatrice; Cassez, Franck; Haddad, Serge; Lime, Didier; Roux, Olivier, Comparison of the expressiveness of timed automata and time Petri nets, (Proceedings of the 3rd International Conference on Formal Modelling and Analysis of Timed Systems, Uppsala, Sweden, (2005)), 211-225 · Zbl 1175.68270
[13] Srba, Jirí, Comparing the expressiveness of timed automata and timed extensions of Petri nets, (Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems, Saint-Malo, France, (2008)), 15-32 · Zbl 1171.68579
[14] Berthomieu, Bernard; Peres, Florent; Vernadat, François, Bridging the gap between timed automata and bounded time Petri nets, (Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems, Paris, France, (2006)), 82-97 · Zbl 1141.68426
[15] Bouyer, Patricia; Haddad, Serge; Reynier, Pierre-Alain, Timed Petri nets and timed automata: on the discriminating power of Zeno sequences, Inf. Comput., 206, 1, 73-107, (2008) · Zbl 1133.68053
[16] Sava, Alexandru Tiberiu; Alla, Hassane, Combining hybrid Petri nets and hybrid automata, IEEE Trans. Robot. Autom., 17, 5, 670-678, (2001)
[17] Cassez, Franck; Roux, Olivier H., Structural translation from time Petri nets to timed automata, J. Syst. Softw., 79, 10, 1456-1468, (2006)
[18] Motallebi, Hassan; Azgomi, Mohammad Abdollahi, Translation from multisingular hybrid Petri nets to multisingular hybrid automata, J. Fundam. Inform., 130, 1-41, (2013) · Zbl 1308.68083
[19] Ghomri, Latéfa; Alla, Hassane; Sari, Zaki, Structural and hierarchical translation of hybrid Petri nets in hybrid automata, (International Meeting on Automated Compliance Systems, Paris, France, (2005))
[20] Motallebi, Hassan; Azgomi, Mohammad Abdollahi, Modelling and verification of hybrid dynamic systems using multisingular hybrid Petri nets, Theor. Comput. Sci. (TCS), 446, 48-74, (2012) · Zbl 1262.68139
[21] Traonouez, Louis-Marie; Lime, Didier; Roux, Olivier H., Parametric model-checking of stopwatch Petri nets, J. Univers. Comput. Sci., 15, 17, 3273-3304, (2009) · Zbl 1217.68140
[22] Henzinger, Thomas A.; Ho, Pei-Hsin; Wong-Toi, Howard, \schytech: a model checker for hybrid systems, (Proceedings of the 6th International Conference on Computer Aided Verification, Haifa, Israel, (1997)), 460-463 · Zbl 1060.68603
[23] Henzinger, Thomas A.; Kopke, Peter; Puri, Anuj; Varaiya, Pravin, What’s decidable about hybrid automata?, J. Comput. Syst. Sci., 57, 1, 94-124, (1998) · Zbl 0920.68091
[24] Aceto, Luca; Bouyer, Patricia; Burgueño, Augusto; Larsen, Kim Guldstrand, The power of reachability testing for timed automata, Theor. Comput. Sci., 300, 1-3, 411-475, (2003) · Zbl 1023.68060
[25] Bozga, Marius; Daws, Conrado; Maler, Oded; Olivero, Alfredo; Tripakis, Stavros; Yovine, Sergio, Kronos: a model checking tool for real-time systems, (Proceedings of the 10th International Conference on Computer Aided Verification, Vancouver, Canada, (1998)), 546-550
[26] McManis, Jennifer; Varaiya, Pravin, Suspension automata: a decidable class of hybrid automata, (Proceedings of the 6th International Conference on Computer Aided Verification, Stanford, USA, (1994)), 105-117
[27] Fersman, Elena; Krcál, Pavel; Pettersson, Paul; Yi, Wang, Task automata: schedulability, decidability and undecidability, Inf. Comput., 205, 8, 1149-1172, (2007) · Zbl 1121.68062
[28] Cassez, Franck; Larsen, Kim, The impressive power of stopwatches, (Proceedings of the 11th International Conference on Concurrency Theory, Pennsylvania, USA, (2000)), 138-152 · Zbl 0999.68112
[29] Bérard, Béatrice; Haddad, Serge, Interrupt timed automata, (Proceedings of the 12th International Conference on Foundations of Software Science and Computation Structure, York, UK, (2009)), 197-211 · Zbl 1234.68195
[30] Bérard, Béatrice; Haddad, Serge; Sassolas, Mathieu, Interrupt timed automata: verification and expressiveness, Form. Methods Syst. Des., 40, 1, 41-87, (2012) · Zbl 1247.68124
[31] Lime, Didier; Roux, Olivier, Model checking of time Petri nets using the state class timed automaton, Discrete Event Dyn. Syst., 16, 2, 179-205, (2006) · Zbl 1113.68068
[32] Okawa, Yasukichi; Yoneda, Tomohiro, Schedulability verification of real-time systems with extended time Petri nets, Int. J. Mini Microcomput., 18, 3, 148-156, (1996)
[33] Horton, Graham; Kulkarni, Vidyadhar G.; Nicol, David M.; Trivedi, Kishor S., Fluid stochastic Petri nets: theory, applications, and solution techniques, Eur. J. Oper. Res., 105, 184-201, (1998) · Zbl 0957.90011
[34] Ciardo, Gianfranco; Nicol, David M.; Trivedi, Kishor S., Discrete-event simulation of fluid stochastic Petri nets, IEEE Trans. Softw. Eng., 25, 2, 207-217, (1999)
[35] Gribaudo, Marco; Sereno, Matteo; Horváth, András; Bobbio, Andrea, Fluid stochastic Petri nets augmented with flush-out arcs: modelling and analysis, Discrete Event Dyn. Syst., 11, 1-2, 97-117, (2001) · Zbl 0972.93040
[36] Ghasemieh, Hamed; Remke, Anne; Haverkort, Boudewijn R.; Gribaudo, Marco, Region-based analysis of hybrid Petri nets with a single general one-shot transition, (Proceedings of the 10th International Conference on Formal Modelling and Analysis of Timed Systems, London, UK, (2012)), 139-154 · Zbl 1374.68329
[37] Gribaudo, Marco; Remke, Anne, Hybrid Petri nets with general one-shot transitions for dependability evaluation of fluid critical infrastructures, (Proceedings of the 12th IEEE High Assurance Systems Engineering Symposium, San Jose, CA, USA, (2010)), 84-93
[38] David, René; Alla, Hassane, Continuous Petri nets, (Proceedings of the 8th European Workshop on Application and Theory of Petri Nets, Saragossa, Spain, (1987)), 275-294
[39] Hanzálek, Zdenek, Continuous Petri nets and polytopes, (Proceedings of the 2003 IEEE International Conference on Systems, Man & Cybernetics, Washington, D.C., USA, (2003)), 1513-1520
[40] Alur, Rajeev; Henzinger, Thomas A.; Vardi, Moshe Y., Parametric real-time reasoning, (Proceedings of the 25th Annual ACM Symposium on Theory of Computing, (1993)), 592-601 · Zbl 1310.68139
[41] Hune, Thomas; Romijn, Judi; Stoelinga, Marielle; Vaandrager, Frits, Linear parametric model checking of timed automata, J. Log. Algebr. Program., 52-53, 183-220, (2002) · Zbl 1008.68069
[42] Bozzelli, Laura; La Torre, Salvatore, Decision problems for lower/upper bound parametric timed automata, Form. Methods Syst. Des., 35, 2, 121-151, (2009) · Zbl 1186.68245
[43] Doyen, Laurent, Robust parametric reachability for timed automata, Inf. Process. Lett., 102, 5, 208-213, (2007) · Zbl 1184.68337
[44] Jovanovic, Aleksandra; Lime, Didier; Roux, Olivier H., Integer parameter synthesis for timed automata, (Proceedings of the 19th International Conference on Tools and Algorithms for Construction and Analysis of Systems, Rome, Italy, (2013)), 401-415 · Zbl 1381.68121
[45] Bruyere, Veronique; Raskin, Jean-Francois, Real-time model-checking: parameters everywhere, Log. Methods Comput. Sci., 3, 1, 1-30, (2007) · Zbl 1128.68052
[46] Bagnara, Roberto; Hill, Patricia M.; Zaffanella, Enea, The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Sci. Comput. Program., 72, 1-2, 3-21, (2004)
[47] Wang, Farn, Parametric timing analysis for real-time systems, Inf. Comput., 130, 2, 131-150, (1996) · Zbl 0872.68041
[48] Bérard, Béatrice; Haddad, Serge; Jovanovic, Aleksandra; Lime, Didier, Parametric interrupt timed automata, (Proceedings of the 7th International Workshop on Reachability Problems, Uppsala, Sweden, (2013)), 24-26 · Zbl 1355.68148
[49] Virbitskaite, Irina; Pokozy, E., Parametric behavior analysis for time Petri nets, (Proceedings of the 5th International Conference on Parallel Computing Technologies, St. Petersburg, Russia, (1999)), 134-140
[50] Roux, Olivier; Lime, Didier, Time Petri nets with inhibitor hyperarcs. formal semantics and state space computation, (Proceedings of the 25th International Conference on Applications and Theory of Petri Nets, Bologna, Italy, (2004)), 371-390 · Zbl 1094.68594
[51] Lime, Didier; Roux, Olivier; Seidner, Charlotte; Traonouez, Louis-Marie, Romeo: a parametric model-checker for Petri nets with stopwatches, (Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, York, UK, (2009)), 54-57
[52] Knapik, Michal; Penczek, Wojciech, Bounded model checking for parametric timed automata, (Transactions on Petri Nets and Other Models of Concurrency, vol. 5, (2012)), 141-159 · Zbl 1350.68183
[53] Bornot, Sébastien; Sifakis, Joseph, Relating time progress and deadlines in hybrid systems, (Proceedings of the International Workshop on Hybrid and Real-Time Systems, Grenoble, France, (1997)), 286-300
[54] Bornot, Sébastien; Sifakis, Joseph; Tripakis, Stavros, Modeling urgency in timed systems, (Proceedings of the International Symposium on Compositionality: the Significant Difference, Bad Malente, Germany, (1997)), 103-129
[55] Ajmone Marsan, Marco; Balbo, Gianfranco; Conte, Gianni; Donatelli, Susanna; Franceschinis, Giuliana, Modelling with generalized stochastic Petri nets, (1995), John Wiley & Sons · Zbl 0843.68080
[56] Alur, Rajeev; Courcoubetis, Costas; Dill, David, Model-checking in dense real-time, Inf. Comput., 104, 1, 2-34, (1993) · Zbl 0783.68076
[57] Baier, Christel; Katoen, Joost-Pieter, Principles of model checking, (2007), The MIT Press · Zbl 1179.68076
[58] Lime, Didier; Roux, Olivier; Seidner, Charlotte; Traonouez, Louis-Marie, Romeo: a parametric model-checker for Petri nets with stopwatches, (Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, York, UK, (2009)), 54-57
[59] Bagnara, Roberto; Ricci, Elisa; Zaffanella, Enea; Hill, Patricia M., Possibly not closed convex polyhedra and the parma polyhedra library, (Proceedings of the 9th International Static Analysis Symposium, Madrid, Spain, (2002)), 213-229 · Zbl 1015.68215
[60] Le Boudec, Jean-Yves; Thiran, Patrick, Network calculus - a theory of deterministic queuing systems for the Internet, Lecture Notes in Computer Science, vol. 2050, (2001), Springer-Verlag · Zbl 0974.90003
[61] Thiele, Lothar; Chakraborty, Samarjit; Naedele, Martin, Real-time calculus for scheduling hard real-time systems, (Proceedings of 2000 IEEE International Symposium on Circuits and Systems, vol. 4, Geneva, Switzerland, (2000)), 101-104
[62] Chakraborty, Samarjit; Künzli, Simon; Thiele, Lothar, A general framework for analysing system properties in platform-based embedded system designs, (Proceedings of the Conference on Design, Automation and Test in Europe, vol. 1, Munich, Germany, (2003)), 10190-10195
[63] Phan, Linh T. X.; Chakraborty, Samarjit; Thiagarajan, P. S., A multi-mode real-time calculus, (Proceedings of the 29th IEEE Real-Time Systems Symposium (RTSS), Barcelona, Spain, (2008)), 59-69
[64] Chakraborty, Samarjit; Phan, Linh T. X.; Thiagarajan, P. S., Event count automata: a state-based model for stream processing systems, (Proceedings of the 26th IEEE Real-Time Systems Symposium (RTSS), Miami, Florida, (2005)), 87-98
[65] Babcock, Brian; Babu, Shivnath; Datar, Mayur; Motwani, Rajeev; Thomas, Dilys, Operator scheduling in data stream systems, Int. VLDB J., 13, 4, 333-353, (2004)
[66] Maxiaguine, Alexander; Künzli, Simon; Chakraborty, Samarjit; Thiele, Lothar, Rate analysis for streaming applications with on-chip buffer constraints, (Proceedings of the 2004 Conference on Asia South Pacific Design Automation, Yokohama, Japan, (2004)), 131-136
[67] Geilen, Marc; Basten, Twan; Stuijk, Sander, Minimising buffer requirements of synchronous dataflow graphs with model checking, (Proceedings of the 42nd Design Automation Conference, San Diego, CA, USA, (2005)), 819-824
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.