Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets.

*(English)*Zbl 1262.68139Summary: The aim of this research has been to associate the modeling capacities of hybrid Petri nets with the analysis power of hybrid automata in order to perform formal verification of hybrid dynamic systems. In this paper, we propose an extension of hybrid Petri nets, called multisingular hybrid Petri nets (MSHPNs), for modeling and verification of hybrid dynamic systems. This extension consists of enriching hybrid Petri nets with the capabilities of hybrid automata to control the execution and firing of transitions and some modeling facilities for describing some repeatedly encountered aspects of timed and hybrid systems.

We discuss the challenging issues of speed computation raised by addition of execution predicates and introduce a speed-based partitioning technique, which is essential for state space computation. We also introduce a method for reachability analysis of MSHPNs, consisting of computing the state class graph. Thus, the verification of timing properties of MSHPNs can be conducted using the existing techniques and tools. The proposed formalism has the expressiveness of multisingular hybrid automata besides the capabilities of Petri nets for modeling concurrent and distributed systems. Some illustrative examples of the proposed formalism are also presented in this paper.

We discuss the challenging issues of speed computation raised by addition of execution predicates and introduce a speed-based partitioning technique, which is essential for state space computation. We also introduce a method for reachability analysis of MSHPNs, consisting of computing the state class graph. Thus, the verification of timing properties of MSHPNs can be conducted using the existing techniques and tools. The proposed formalism has the expressiveness of multisingular hybrid automata besides the capabilities of Petri nets for modeling concurrent and distributed systems. Some illustrative examples of the proposed formalism are also presented in this paper.

##### MSC:

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

68Q45 | Formal languages and automata |

##### Keywords:

hybrid dynamic systems; timed systems; hybrid Petri nets (HPNs); hybrid automata; multisingular hybrid Petri nets (MSHPNs); speed-based partitioning
PDF
BibTeX
XML
Cite

\textit{H. Motallebi} and \textit{M. A. Azgomi}, Theor. Comput. Sci. 446, 48--74 (2012; Zbl 1262.68139)

Full Text:
DOI

##### References:

[1] | Silva, Manuel; Recalde, Laura, On fluidification of Petri nets: from discrete to hybrid and continuous models, Annual reviews in control, 28, 2, 253-266, (2004) |

[2] | Recalde, Laura; Haddad, Serge; Silva, Manuel, Continuous Petri nets: expressive power and decidability issues, International journal of foundations of computer science, 21, 2, 235-256, (2010) · Zbl 1200.68164 |

[3] | 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, Theoretical computer science, 138, 1, 3-34, (1995) |

[4] | Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Tini, Simone, Concurrency in timed automata, Theoretical computer science, 309, 1-3, 503-527, (2003) · Zbl 1070.68073 |

[5] | Kesten, Yonit; Pnueli, Amir, A compositional approach to CTL* verification, Theoretical computer science, 331, 2-3, 397-428, (2005) · Zbl 1079.68059 |

[6] | Latéfa Ghomri, Hassane Alla, Zaki Sari, Structural and hierarchical translation of hybrid petri nets in hybrid automata, in: Proceedings of the International Meeting on Automated Compliance Systems, Paris, France, 2005. |

[7] | Thomas A. Henzinger, The theory of hybrid automata, in: Proceedings of the 11th Annual Symposium on Logic in Computer Science, New Brunswick, USA, 1996, pp. 278-292. · Zbl 0959.68073 |

[8] | David, René; Alla, Hassane, Discrete, continuous and hybrid Petri nets, (2005), Springer-Verlag · Zbl 1074.93002 |

[9] | Zdenek Hanzálek, Continuous petri nets and polytopes, in: Proceedings of the 2003 IEEE International Conference on Systems, Man & Cybernetics, Washington, D.C., USA, 2003, pp. 1513-1520. |

[10] | Michal Kutil, Zdenek Hanzálek, Light controlled intersection model based on the continuous petri net, in: Proceedings of the 12th IFAC Symposium on Control in Transportation Systems, California, USA, 2009. |

[11] | Lime, Didier; Roux, Olivier, Formal verification of real-time systems with preemptive scheduling, Real-time systems, 41, 2, 118-151, (2009) · Zbl 1185.68429 |

[12] | Henzinger, Thomas A.; Kopke, Peter; Puri, Anuj; Varaiya, Pravin, What’s decidable about hybrid automata?, Journal of computer and system sciences, 57, 1, 94-124, (1998) · Zbl 0920.68091 |

[13] | Henzinger, Thomas A.; Ho, Pei-Hsin; Wong-Toi, Howard, HYTECH: a model checker for hybrid systems, Software tools for technology transfer, 1, 460-463, (1997) · Zbl 1060.68603 |

[14] | Henzinger, Thomas A.; Kopke, Peter W., Discrete-time control for rectangular hybrid automata, Theoretical computer science, 221, 1-2, 369-392, (1999) · Zbl 0930.68086 |

[15] | Alur, Rajeev; Dill, David L., A theory of timed automata, Theoretical computer science, 126, 2, 183-235, (1994) · Zbl 0803.68071 |

[16] | Pettersson, Paul; Larsen, Kim, Uppaal2k, Bulletin of the European association for theoretical computer science, 70, 40-44, (2000) |

[17] | Aceto, Luca; Bouyer, Patricia; Burgueño, Augusto; Guldstrand Larsen, Kim, The power of reachability testing for timed automata, Theoretical computer science, 300, 1-3, 411-475, (2003) · Zbl 1023.68060 |

[18] | Bozga, Marius; Daws, Conrado; Maler, Oded; Olivero, Alfredo; Tripakis, Stavros; Yovine, Sergio, Kronos: a model-checking tool for real-time systems, (), 546-550 |

[19] | Franck Cassez, Kim Larsen, The impressive power of stopwatches, in: Proceedings of the 11th International Conference on Concurrency Theory, Pennsylvania, USA, 2000, pp. 138-152. · Zbl 0999.68112 |

[20] | Bouyer, Patricia; Dufourd, Catherine; Fleury, Emmanuel; Petit, Antoine, Updatable timed automata, Theoretical computer science, 321, 2-3, 291-345, (2004) · Zbl 1070.68063 |

[21] | Dang, Zhe; Ibarra, Oscar H.; Kemmerer, Richard A., Generalized discrete timed automata: decidable approximations for safety verification, Theoretical computer science, 296, 1, 59-74, (2003) · Zbl 1044.68086 |

[22] | Jennifer McManis, Pravin Varaiya, Suspension automata: a decidable class of hybrid automata, in: Proceedings of the 6th International Conference on Computer Aided Verification, Stanford, USA, 1994, pp. 105-117. · Zbl 0828.93002 |

[23] | Fersman, Elena; PavelKrcál; Pettersson, Paul; Yi, Wang, Task automata: schedulability, decidability and undecidability, Information and computation, 205, 8, 1149-1172, (2007) · Zbl 1121.68062 |

[24] | Roux, Olivier; Déplanche, Anne-Marie, A T-time Petri net extension for real time task scheduling modelling, European journal of automation, 36, 7, 973-987, (2002) |

[25] | Olivier Roux, Didier Lime, Time petri nets with inhibitor hyperarcs. Formal semantics and state space computation, in: Proceedings of the 25th International Conference on Applications and Theory of Petri Nets, Bologna, Italy, 2004, pp. 371-390. · Zbl 1094.68594 |

[26] | Boucheneb, Hanifa; Hadjidj, Rachid, CTL* model checking for time Petri nets, Theoretical computer science, 353, 1-3, 208-227, (2006) · Zbl 1088.68101 |

[27] | Didier Lime, Olivier Roux, A translation-based method for the timed analysis of scheduling extended time petri nets, in: Proceedings of the 25th IEEE Real-Time Systems Symposium, Lisbon, Portugal, 2004, pp. 187-196. |

[28] | Lime, Didier; Roux, Olivier, Model-checking of time Petri nets using the state class timed automaton, Discrete event dynamic systems, 16, 2, 179-205, (2006) · Zbl 1113.68068 |

[29] | Okawa, Yasukichi; Yoneda, Tomohiro, Schedulability verification of real-time systems with extended time Petri nets, International journal of mini and microcomputers, 18, 3, 148-156, (1996) |

[30] | Béatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, Olivier Roux, Comparison of the expressiveness of timed automata and time petri nets, in: Proceedings of the 3rd International Conference on Formal Modelling and Analysis of Timed Systems, Uppsala, Sweden, 2005, pp. 211-225. · Zbl 1175.68270 |

[31] | Jirí Srba, Comparing the expressiveness of timed automata and timed extensions of petri nets, in: Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems, Saint-Malo, France, 2008, pp. 15-32. · Zbl 1171.68579 |

[32] | René David, Hassane Alla, Continuous petri nets, in: Proceedings of the 8th European Workshop on Application and Theory of Petri Nets, Saragossa, Spain, 1987, pp. 275-294. |

[33] | David, René; Alla, Hassane, On hybrid Petri nets, Discrete event dynamic systems, 11, 1-2, 9-40, (2001) · Zbl 0969.93024 |

[34] | Hybrid Petri Net Bibliography. URL: http://bode.diee.unica.it/ hpn/. |

[35] | Balduzzi, Fabio; Di Febbraro, Angela; Giua, Alessandro; Seatzu, Carla, Decidability results in first-order hybrid Petri nets, Discrete event dynamic systems, 11, 1-2, 41-57, (2001) · Zbl 0971.93051 |

[36] | René David, Hassane Alla, Autonomous and timed continuous petri nets, in: Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, France, 1990, pp. 367-386. |

[37] | Doran Wilde, A library for doing polyhedral operations, IRISA Technical Report Internal Publication, No. 785, Rennes, France, 1993. · Zbl 0968.68172 |

[38] | Geir Dahl, An introduction to convexity, polyhedral theory and combinatorial optimization, in: Komp. vol. 67, University of Oslo, 1996. |

[39] | Roberto Bagnara, Elisa Ricci, Enea Zaffanella, Patricia M. Hill, Possibly not closed convex polyhedra and the parma polyhedra library, in: Proceedings of the 9th International Static Analysis Symposium, Madrid, Spain, 2002, pp. 213-229. · Zbl 1015.68215 |

[40] | Sébastien Bornot, Joseph Sifakis, Stavros Tripakis, Modeling urgency in timed systems, in: Proceedings of the International Symposium on Compositionality: The Significant Difference, Bad Malente, Germany, 1997, pp. 103-129. |

[41] | Sébastien Bornot, Joseph Sifakis, Relating time progress and deadlines in hybrid systems, in: Proceedings of the International Workshop on Hybrid and Real-Time Systems, Grenoble, France, 1997, pp. 286-300. |

[42] | Marco Gribaudo, Hybrid formalism for performance evaluation: theory and applications, Ph.D. Thesis, University of Torino, 2001. |

[43] | Ajmone Marsan, Marco; Balbo, Gianfranco; Conte, Gianni; Donatelli, Susanna; Franceschinis, Giuliana, Modelling with generalized stochastic Petri nets, (1995), John Wiley & Sons · Zbl 0843.68080 |

[44] | Baier, Christel; Katoen, Joost-Pieter, Principles of model checking, (2007), The MIT Press · Zbl 1179.68076 |

[45] | Didier Lime, Olivier Roux, Charlotte Seidner, Louis-Marie Traonouez, Romeo: a parametric model-checker for petri nets with stopwatches, in: Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, York, UK, 2009, pp. 54-57. |

[46] | Zhang, Mu; Wong, Johnny; Tavanapong, Wallapak; Oh, Junghwan; Groen, Piet, Deadline-constrained media uploading systems, Journal of multimedia tools and applications, 38, 1, 51-74, (2008) |

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.