Translation from Multisingular Hybrid Petri Nets to Multisingular Hybrid Automata

• Autorzy: Motallebi H. , Azgomi M. A.

Identyfikatory

DOI

10.3233/FI-2014-993

• Języki publikacji: EN

Abstrakty

EN

In this paper, we investigate some important aspects of a new formalism for modelling and verification of hybrid dynamic systems (HDS), which is called multisingular hybrid Petri nets (MSHPNs). This new hybrid formalism is aimed to bridge the gap between hybrid automata (HA) and hybrid Petri nets (HPNs) by equipping the HPN model with the capabilities of HA to control the execution and firing of timed transitions. Practically, MSHPNs can be considered as the counterpart with the same expressive power as multisingular hybrid automata (MSHA). In order to analyse MSHPN models, a speed-based partitioning technique has been introduced in which the variable space is partitioned based on the balance of continuous places. In this paper, we formalize the notions of conflicts and conflict resolution and the challenging issue of speed computation. Then, we focus on considering a translation from a bounded MSHPN to a multisingular hybrid automaton that preserves the behavioural semantics of the original MSHPN in terms of weak timed bisimulation. The translation algorithm uses the speed-based partitioning method and obtains a speed-based partitioning hybrid automaton for a given bounded MSHPN. Model checking a timed property for an MSHPN amounts to model checking its equivalent property on the obtained speed-based partitioning hybrid automaton, thus MSHPN models can be analysed using the existing tools. The advantages of the proposed method are twofold: (1) hybrid systems can be described more succinctly and therefore more readably as MSHPNs, and (2) one can use the existing tools (like HYTECH) to analyse MSHPN models.

Słowa kluczowe

EN

hybrid dynamic systems; multisingular hybrid Petri nets; MSHPNs; multisingular hybrid automata; MSHA; translation; speed-based partitioning hybrid automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 130, nr 3
• Strony: 275--315
• Opis fizyczny: Bibliogr. 44 poz., rys., tab.

Twórcy

autor

Motallebi H.

• School of Computer Engineering, Iran University of Science and Technology, Tehran, Iran

autor

Azgomi M. A.

• School of Computer Engineering, Iran University of Science and Technology, Tehran, Iran

Bibliografia

• [1] Silva, M., Recalde L.: On Fluidification of Petri Nets: From Discrete to Hybrid and Continuous Models, Annual Reviews in Control, 28(2), 2004, 253–266.
• [2] Henzinger T. A.: The Theory of Hybrid Automata, Proc. 11th Annual Symposium on Logic in Computer Science, pages 278–292, 1996.
• [3] Sava A. T., Alla H.: Combining Hybrid Petri Nets and Hybrid Automata, IEEE Transactions on Robotics and Automation, 17(5), 2001, 670–678.
• [4] David R., Alla H.: Discrete, Continuous, and Hybrid Petri Nets, Springer-Verlag, 2005.
• [5] Brard B., Cassez F., Haddad S., Lime D., Roux O. H.: Comparison of the Expressiveness of Timed Automata and Time Petri Nets, Proc. 3rd International Conference on Formal Modelling and Analysis of Timed Systems, pages 211–225, 2005.
• [6] Recalde L., Haddad S., Silva M.: Continuous Petri Nets: Expressive Power and Decidability Issues, International Journal of Foundations of Computer Science, 21(2), 2010, 235–256.
• [7] Srba J.: Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets, Proc. 6th International Conference on Formal Modelling and Analysis of Timed Systems, pages 15–32, 2008.
• [8] Berthomieu B., Peres F., Vernadat F.: Bridging the Gap Between Timed Automata and Bounded Time Petri Nets, Proc. 4th International Conference on Formal Modelling and Analysis of Timed Systems, pages 82–97, 2006.
• [9] Balduzzi F., Febbraro A. D., Giua A., Seatzu C.: Decidability Results in First-Order Hybrid Petri Nets, Discrete Event Dynamic Systems, 11(1–2), 2001, 41–57.
• [10] Lime D., Roux O. H.: Formal Verification of Real-Time Systems with Preemptive Scheduling, Real-Time Systems 41(2), 2009, 118–151.
• [11] Ghomri L., Alla H., Sari Z.: Structural and Hierarchical Translation of Hybrid Petri Nets in Hybrid Automata, International Meeting on Automated Compliance Systems, 2005.
• [12] Cassez F., Roux O. H.: Structural Translation from Time Petri Nets to Timed Automata, Journal of Systems and Software, 79(10), 2006, 1456–1468.
• [13] Lime D., Roux O. H.: A Translation-Based Method for the Timed Analysis of Scheduling Extended Time Petri Nets, Proc. 25th IEEE Real-Time Systems Symposium, pages 187-196, 2004.
• [14] Hanzlek Z.: Continuous Petri Nets and Polytopes, Proc. 2003 IEEE International Conference on Systems, Man & Cybernetics, Washington, pages 1513-1520, 2003.
• [15] Pettersson P., Larsen K. G.: Uppaal2k, Bulletin of the European Association for Theoretical Computer Science, No. 70, pages 40-44, 2000.
• [16] Aceto L., Bouyer P., Burgueo A., Larsen K. G.: The Power of Reachability Testing for Timed Automata, Theoretical Computer Science, 300(1–3), 2003, 411–475.
• [17] Henzinger T. A., Ho P. H, Wong-Toi H.: HYTECH: A Model Checker for Hybrid Systems, Proc. 6th International Conference on Computer Aided Verification, pages 460–463, 1997.
• [18] B. Marius, Daws C., Maler O., Olivero A., Tripakis S., Yovine S.: Kronos: A Model Checking Tool for Real-Time Systems, Proc. 10th International Conference on Computer Aided Verification, pages 546–550, 1998.
• [19] Frehse G., Guernic C. L., Donz A., Cotton S., Ray R., Lebeltel O., Ripado R., Girard A., Dang T., Maler O.: Space Ex: Scalable Verification of Hybrid Systems, Proc. 23rd International Conference on Computer Aided Verification, pages 379–395, 2011.
• [20] Motallebi H., Azgomi M. A.: Modelling and Verification of Hybrid Dynamic Systems Using Multisingular Hybrid Petri Nets, Theoretical Computer Science, 446, 2012, 48–74.
• [21] Dahl G.: An Introduction to Convexity, Polyhedral Theory and Combinatorial Optimization, Komp. 67, University of Oslo, 1996.
• [22] Alur R., Courcoubetis C., Halbwachs n., Henzinger T. A., Ho P. H., Nicollin X., Olivero A., Sifakis J., Yovine S.: The Algorithmic Analysis of Hybrid Systems, Theoretical Computer Science, 138(1), 1995, 3–34.
• [23] Henzinger T. A., Kopke P., Puri A., Varaiya P.: What’s Decidable about Hybrid Automata?, Journal of Computer and System Sciences, 57(1), 1998, 94–124.
• [24] Alur R., Dill D. L.: A Theory of Timed Automata, Theoretical Computer Science, 126(2), 1994, 183–235.
• [25] Cassez F., Larsen K. G.: The Impressive Power of Stopwatches, Proc. 11th International Conference on Concurrency Theory, pages 138–152, 2000.
• [26] McManis J., Varaiya P: Suspension Automata: A Decidable Class of Hybrid Automata, Proc. 6th International Conference on Computer Aided Verification, pages 105–117, 1994.
• [27] Fersman E., Krcl P., Pettersson P., Yi W.: Task Automata: Schedulability, Decidability and Undecidability, Information and Computation, 205(8), 2007, 1149–1172.
• [28] Roux O. H., Dplanche A. M.: A T-Time Petri Net Extension for Real Time Task Scheduling Modelling, European Journal of Automation, 36(7), 2002, 973-987.
• [29] Roux O. H., Lime D.: Time Petri Nets with Inhibitor Hyperarcs. Formal Semantics and State Space Computation, Proc. 25th International Conference on Applications and Theory of Petri Nets, pages 371–390, 2004.
• [30] Okawa Y., Yoneda T.: Schedulability Verification of Real-Time Systems with Extended Time Petri Nets, International Journal of Mini and Microcomputers, 18(3), 1996, 148–156.
• [31] Lime D., Roux O. H., Seidner C., Traonouez L. M.: Romeo: A Parametric Model Checker for Petri Nets with Stopwatches, Proc. 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 54–57, 2009.
• [32] Berthomieu B., Vernadat F.: Time Petri Nets Analysis with TINA, Proc. 3rd International Conference on the Quantitative Evaluation of Systems, pages 123-124, 2006.
• [33] Bucci G., Sassoli L., Vicario E.: ORIS: A Tool for State-Space Analysis of Real-Time Preemptive Systems, Proc. 1st International Conference on Quantitative Evaluation of Systems, pages 70-79, 2004.
• [34] David R., Alla H.: Continuous Petri Nets, Proc. 8th European Workshop on Application and Theory of Petri Nets, pages 275–294, 1987.
• [35] David R., Alla H.: On Hybrid Petri Nets, Discrete Event Dynamic Systems, 11(1–2), 2001, 9–40.
• [36] Hybrid Petri Net Bibliography, URL: http://bode.diee.unica.it/ hpn/
• [37] David R., Alla H.: Autonomous and Timed Continuous Petri Nets, Proc. 11th International Conference on Application and Theory of Petri Nets, pages 367–386, 1990.
• [38] Bagnara R., Ricci E., Zaffanella E., Hill P. M.: Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library, Proc. 9th International Static Analysis Symposium, pages 213–229, 2002.
• [39] Ngatchou P., Zarei A., El-Sharkawi M. A: Pareto Multi Objective Optimization, Proc. 13th International Conference on Intelligent Systems Application to Power Systems, pages 84–91, 2005.
• [40] Bornot S., Sifakis J., Tripakis S.: Modeling Urgency in Timed Systems, Proc. International Symposium on Compositionality: The Significant Difference, pages 103–129, 1997.
• [41] Bornot S., Sifakis J.: Relating time progress and deadlines in hybrid systems, Proc. International Workshop on Hybrid and Real-Time Systems, LNCS Vol. 1201, pages 286–300, Springer, 1997.
• [42] Gribaudo M.: Hybrid Formalism for Performance Evaluation: Theory and Applications, Ph.D. Thesis, University of Torino, 2001.
• [43] Ajmone Marsan M., Balbo G., Conte G., Donatelli S., Franceschinis G.: Modelling with Generalized Stochastic Petri Nets, John Wiley & Sons, 1995.
• [44] Kutil M., Hanzlek Z.: Light Controlled Intersection Model Based on the Continuous Petri Net, Proc. 12th IFAC Symposium on Control in Transportation Systems, 2009.