Conversion of 1-Place-Unbounded Synchronized Petri Nets into Weighted Automata
| Autor: | Alessandro Giua, Changshun Wu, Isabel Demongodin |
|---|---|
| Přispěvatelé: | Laboratoire des Sciences de l'Information et des Systèmes (LSIS), Centre National de la Recherche Scientifique (CNRS)-Arts et Métiers Paristech ENSAM Aix-en-Provence-Université de Toulon (UTLN)-Aix Marseille Université (AMU), Modèles et Formalismes à Evénements Discrets (MOFED), Laboratoire d'Informatique et Systèmes (LIS), Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU), Department of Electrical and Electronic Engineering [University of Cagliari] (DIEE), University of Cagliari, Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Arts et Métiers Paristech ENSAM Aix-en-Provence-Centre National de la Recherche Scientifique (CNRS) |
| Rok vydání: | 2017 |
| Předmět: |
030213 general clinical medicine
0209 industrial biotechnology Theoretical computer science Computer science 02 engineering and technology Petri net Graph Automaton [SPI]Engineering Sciences [physics] 03 medical and health sciences 020901 industrial engineering & automation 0302 clinical medicine Control and Systems Engineering Stochastic Petri net State space Systems design ComputingMilieux_MISCELLANEOUS |
| Zdroj: | 20th IFAC World Congress 20th IFAC World Congress, Jul 2017, Toulouse, France. pp.13434-13440, ⟨10.1016/j.ifacol.2017.08.2300⟩ |
| ISSN: | 2405-8963 |
| DOI: | 10.1016/j.ifacol.2017.08.2300 |
| Popis: | Testing is a fundamental technique for system design and verification to ensure security and reliability. However its application to discrete event systems modeled by unbounded synchronized Petri nets is not straightforward because there exists no finite exact representation for the infinite state space of these models. In this paper, we consider a special class of synchronized Petri nets, called 1-place-unbounded, that contain a single unbounded place. We show how a coverability graph that precisely describes the state space of such a model can be constructed extending to synchronized nets a technique previously presented for place/transition nets. In addition, this algorithm can also be used to verify whether a given synchronized Petri net contains exactly a single unbounded place. Next, we show that any net belonging to this special class can be converted into an equivalent weighted automaton. Based on this conversion, we observe that the testing of 1-place-unbounded synchronized Petri nets can be approached using the methods and results existing in the literature for the testing of weighted automata. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|