A Method to Prove Non-Reachability in Priority Duration Petri Nets

• Autorzy: Werner M. , Popova-Zeugmann L. , Richling J.
• Języki publikacji: EN

Abstrakty

EN

Times and priorities are important concepts that are frequently used to model real-world systems. Thus, there exist extensions for Petri nets which allow to model times and priorities. In contrast, many proof techniques are based on classical (time-less and priority-less) Petri nets. However, this approach fails frequently for timed and prioritized Petri nets. In this paper, we present an approach to prove non-reachability in a Priority Duration Petri net. We use for this proving technique a state equation as well as conditions for firing that include a priority rule and a maximal step rule. Our approach leads to a system of equations and inequalities, which provide us with a sufficient condition of non-reachability. We demonstrate the application of our approach with an example

Słowa kluczowe

EN

priority Duration Petri net; state equation; non-reachability

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 61, nr 3,4
• Strony: 351--368
• Opis fizyczny: Bibliogr. 9 poz., rys.

Twórcy

autor

Werner M.

• Communication and Operating Systems Group, Department for Electrical Engineering and Computer Science, TV Berlin, Germany

autor

Popova-Zeugmann L.

• Automata and System Theory Group, Department of Computer Science, Humboldt University of Berlin, Germany

autor

Richling J.

• Computer Architecture and Communication Group, Department of Computer Science, Humboldt University of Berlin, Germany

Bibliografia

• [1] Lui. C. L., Layland, J. W.: Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Enviroment, 20(1), January 1973,46-61.
• [2] Marsan, M. A., Balbo. G., Conte, G., Donatelli, S., Franceschinis. G.: Modelling with Generalized Stochastic Petri Nets, John Wiley and Sons, 1996.
• [3] Popova-Zeugmann, L., Werner, M., Richling, J.: Using slate-equation to prove non-reachability in Timed Petrinets, Fundamenta Informaticae, 2003.
• [4] Ramchandani, C: Analysis of Asynchronous Concurrent Systems by Timed Petri Nets, Project MAC-TR 120, February 1974.
• [5] Richling, J.: Message Scheduled System - A Composable Architecture for Embedded Real-Time-Systems, Prooceedings of 2000 Int. Conference on Parallel and Distributed Processing techniques and Applications (PDPTA 20001 vol. 4, Jun 2000, 2143-2150.
• [6] Richling, J., M. Werner, Popova-Zeugmann, L.: Automatic Composition of Timed Petri net Specifications for a Real-Time Architecture, Proceedings of 2002 IEEE International Conference on Robotics and Automation, Washington DC. May 2002.
• [7] Richling, J., Popova-Zeugmann, L., Werner, M.: Verification of Non-functional Properties of a Composable Architecture with Petri nets, Fundamenta Informaticae, 51, 2002, 185-200.
• [8] Starke, P H.: Analyse von Petri-Netz-Modellen, B.G. Teubner, Stuttgart, 1990.
• [9] Starke, P. H.: A Memo on Time Constraints in Petri Nets, Informatik-Bericht 46, Humboldt University of Berlin. 1995.