Checking Untimed and Timed Linear Properties of the Interval Timed Colored Petri Net Model

Verificación de las propiedades lineales síncronas y asíncronas del Modelo de la Red de Petri Coloreado Intervalo Tiempo

dc.contributores-ES
dc.contributoren-US
dc.creatorBOUCHENEB, HANIFA
dc.date2009-10-05
dc.date.accessioned2018-03-16T14:24:09Z
dc.date.available2018-03-16T14:24:09Z
dc.identifierhttp://ojs.unam.mx/index.php/cys/article/view/2715
dc.identifier.urihttp://repositorioslatinoamericanos.uchile.cl/handle/2250/1190587
dc.descriptionESTE ARTÍCULO SE OCUPA DE LA VERIFICACIÓN DE LAS PROPIEDADES LINEALES TEMPORIZADAS Y NO TEMPORIZADAS DEL MODELO DE REDES DE PETRI COLOREADAS CON INTERVALOS TEMPORIZADOS. ESTE MODELO PUEDE SIMULAR OTRAS REDES DE PETRI COLOREADAS TEMPORIZADAS Y PERMITE DESCRIBIR GRANDES Y COMPLEJOS SISTEMAS EN TIEMPO REAL. NOSOTROS PROPONEMOS CONTRAER EL ESPACIO GENERALMENTE INFINITO, EN UN GRAFO QUE CAPTURE TODAS LAS PROPIEDADES LINEALES DEL MODELO. EL GRAFO RESULTANTE ES FINITO, SI Y SOLAMENTI SI, EL MODELO TIENE LÍMITES (EL CONJUNTO DE SUS MARCAS ACCESIBLES ES FINITO). EN ESTE CASO, LAS PROPIEDADES LINEALES DEL MODELO SE PUEDEN VERIFICAR EN EL GRAFO RESULTANTE, UTILIZANDO, POR EJEMPLO, TÉCNICAS DE COMPROBACIÓN DEL MODELO LINEAL CLÁSICO.es-ES
dc.descriptionTHIS PAPER DEALS WITH VERIFICATION OF TIMED AND UNTIMED LINEAR PROPERTIES OF THE INTERVAL 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.en-US
dc.formatapplication/pdf
dc.languagespa
dc.publisherComputación y Sistemases-ES
dc.relationhttp://ojs.unam.mx/index.php/cys/article/view/2715/2276
dc.sourceComputación y Sistemas; Vol 10, No 002 (2006)es-ES
dc.source1405-5546
dc.subjectMÉTODOS FORMALES; COMPROBACIÓN MODELO; MODELOS TEMPORIZADOS; RED DE PETRI COLOREADA CON INTERVALOS TEMPORIZADOS; CONTRACCIÓN DEL ESPACIO DEL ESTADO; PROPIEDADES LINEARESes-ES
dc.subjectFormal methods; model checking; timed models; timed colored Petri net; state space contraction; linear propertiesen-US
dc.titleChecking Untimed and Timed Linear Properties of the Interval Timed Colored Petri Net Modelen-US
dc.titleVerificación de las propiedades lineales síncronas y asíncronas del Modelo de la Red de Petri Coloreado Intervalo Tiempoes-ES
dc.typeArtículos de revistas
dc.typeArtículos de revistas


Este ítem pertenece a la siguiente institución