Using State Equation to Prove Non-Reachability in Timed Petrinets

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

Abstrakty

EN

Non-reachability proofs in Timed Petrinets were usually done by proving the non-reachability within the underlying timeless net. However, in many cases this approach fails. In this paper, we present an approach to prove non-reachability within the actual Timed Petrinet. For this purpose, we introduce a state equation for Timed Petrinets in analogy to timeless nets. Using this state equation, we can express reachability as a system of equations and inequations, which is solvable in polynomial time.

Słowa kluczowe

EN

timed Petri nets; duration nets; state equation; non-reachability

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 55, nr 2
• Strony: 187--202
• Opis fizyczny: bibliogr. 6 poz.

Twórcy

autor

Popova-Zeugmann L.

autor

Werner M.

autor

Richling J.

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

Bibliografia

• [1] Ramchandani, C.: Analysis of Asynchronous Concurrent Systems by Timed Petri Nets, Project MAC-TR 120, MIT, Febr. 1974.
• [2] 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 2000), 4, Jun 2000.
• [3] Richling, J., M.Werner, Popova-Zeugmann, L.: Automatic Composition of Timed Petrinet Specifications for a Real-Time Architecture, Proceedings of 2002 IEEE International Conference on Robotics and Automation, Washington DC, May 2002.
• [4] Richling, J., Popova-Zeugmann, L., Werner, M.: Verification of Non-functional Properties of a Composable Architecture with Petrinets, Fundamenta Informaticae, 51, 2002, 185-200.
• [5] Starke, P. H.: Analyse von Petri-Netz-Modellen, B.G. Teubner, Stuttgart, 1990.
• [6] Starke, P. H.: INA - Integrated Net Analyzer, Berlin, 1997, Manual.