Checking Untimed and Timed Linear Properties of the Interval Timed Colored Petri Net Model
Fuente:
Redalyc
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Artículo científico |
| Lenguaje: | en |
| Publicado: |
Instituto Politécnico Nacional
2006
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1876443350705373184 |
|---|---|
| author | Hanifa Boucheneb |
| author_facet | Hanifa Boucheneb |
| contents | Checking Untimed and Timed Linear Properties of the Interval Timed Colored Petri Net Model Hanifa Boucheneb Computación timed models Formal methods model checking linear properties timed colored Petri net model. This model can simulate other timed colored Petri nets and allows describing large and complex real-time systems. We propose here to contract its generally infinite state space into a graph that captures all linear properties of the model. The resulting graph is finite iff, the model is bounded (the set of its reachable markings is finite). In this case, linear properties of the model can be verified on the graph using, for example, the classical linear model checking techniques. 2006 artículo científico 1405-5546 https://www.redalyc.org/articulo.oa?id=61500203 en http://www.redalyc.org/revista.oa?id=615 Computación y Sistemas application/pdf Instituto Politécnico Nacional Computación y Sistemas (México) Num.2 Vol.10 |
| format | Artículo científico |
| id | redalyc_61500203 |
| institution | Redalyc |
| language | en |
| publishDate | 2006 |
| publisher | Instituto Politécnico Nacional |
| spellingShingle | Checking Untimed and Timed Linear Properties of the Interval Timed Colored Petri Net Model Hanifa Boucheneb Computación timed models Formal methods model checking linear properties timed colored Petri net Checking Untimed and Timed Linear Properties of the Interval Timed Colored Petri Net Model Hanifa Boucheneb Computación timed models Formal methods model checking linear properties timed colored Petri net model. This model can simulate other timed colored Petri nets and allows describing large and complex real-time systems. We propose here to contract its generally infinite state space into a graph that captures all linear properties of the model. The resulting graph is finite iff, the model is bounded (the set of its reachable markings is finite). In this case, linear properties of the model can be verified on the graph using, for example, the classical linear model checking techniques. 2006 artículo científico 1405-5546 https://www.redalyc.org/articulo.oa?id=61500203 en http://www.redalyc.org/revista.oa?id=615 Computación y Sistemas application/pdf Instituto Politécnico Nacional Computación y Sistemas (México) Num.2 Vol.10 |
| title | Checking Untimed and Timed Linear Properties of the Interval Timed Colored Petri Net Model |
| topic | Computación timed models Formal methods model checking linear properties timed colored Petri net |
| url | https://www.redalyc.org/articulo.oa?id=61500203 |