@inproceedings{ cassez-msr-03,
  abstract = {Dans cet article, nous considérons les réseaux de Petri
                  t-temporels (RdPT) c'est à dire pour lesquels le
                  temps est associé aux transitions sous la forme d'un
                  interval. Nous en donnons une sémantique formelle en
                  terme de systèmes de transitions temporisés. Nous
                  proposons ensuite une traduction structurelle des
                  RdPTs en un produit synchronisé d'automates
                  temporisés (ATs) qui préserve la sémantique
                  comportementale (bisimilarité temporelle) des
                  RdPTs. Les conséquences théoriques de ce résultat
                  sont: i) les problémes d'accessibilité et plus
                  généralement de model-checking de TCTL sont
                  décidables pour les RdPTs bornés; ii) il est
                  possible d'étendre les RdPTs en considérant des
                  contraintes temporelles strictes sur les transitions
                  en préservant les résultats décrits plus haut en
                  i). D'un point de vue pratique, les conséquences
                  sont doubles: i) on peut spécifier un système à
                  l'aide de RdPTs et d'automates temporisés et en
                  donner une sémantique facilement; ii) les outils
                  disponibles pour l'analyse des automates temporisés
                  (comme \textsf{KRONOS} ou \textsf{UPPAAL} ou
                  \textsf{CMC}) peuvent être utilisés pour la
                  vérification de RdPTs.},
  author = {Cassez, Franck and Roux, Olivier Henri},
  booktitle = {4$\textit{̀eme}$ Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'03)},
  lex = {Cb},
  class = {natconference},
  category = {tpn},
  month = {October},
  numircyn = {C},
  pdf = {./ps-pdf-files/tpn-ta-03.pdf},
  title = {{Traduction structurelle des Réseaux de {Petri} Temporels en Automates Temporisés}},
  year = {2003}
}

{"_id":"KeYvNGTbc55akghmE","bibbaseid":"cassez-roux-henri-traductionstructurelledesrseauxdepetritemporelsenautomatestemporiss-2003","downloads":0,"creationDate":"2015-03-18T11:11:41.401Z","title":"Traduction structurelle des Réseaux de Petri Temporels en Automates Temporisés","author_short":["Cassez, F.","Roux","Henri, O."],"year":2003,"bibtype":"inproceedings","biburl":"http://www.irccyn.fr/franck/bib/mabib.bib","bibdata":{"abstract":"Dans cet article, nous considérons les réseaux de Petri t-temporels (RdPT) c'est à dire pour lesquels le temps est associé aux transitions sous la forme d'un interval. Nous en donnons une sémantique formelle en terme de systèmes de transitions temporisés. Nous proposons ensuite une traduction structurelle des RdPTs en un produit synchronisé d'automates temporisés (ATs) qui préserve la sémantique comportementale (bisimilarité temporelle) des RdPTs. Les conséquences théoriques de ce résultat sont: i) les problémes d'accessibilité et plus généralement de model-checking de TCTL sont décidables pour les RdPTs bornés; ii) il est possible d'étendre les RdPTs en considérant des contraintes temporelles strictes sur les transitions en préservant les résultats décrits plus haut en i). D'un point de vue pratique, les conséquences sont doubles: i) on peut spécifier un système à l'aide de RdPTs et d'automates temporisés et en donner une sémantique facilement; ii) les outils disponibles pour l'analyse des automates temporisés (comme \\textsfKRONOS ou \\textsfUPPAAL ou \\textsfCMC) peuvent être utilisés pour la vérification de RdPTs.","author":["Cassez, Franck","Roux","Henri, Olivier"],"author_short":["Cassez, F.","Roux","Henri, O."],"bibtex":"@inproceedings{ cassez-msr-03,\n abstract = {Dans cet article, nous considérons les réseaux de Petri\n t-temporels (RdPT) c'est à dire pour lesquels le\n temps est associé aux transitions sous la forme d'un\n interval. Nous en donnons une sémantique formelle en\n terme de systèmes de transitions temporisés. Nous\n proposons ensuite une traduction structurelle des\n RdPTs en un produit synchronisé d'automates\n temporisés (ATs) qui préserve la sémantique\n comportementale (bisimilarité temporelle) des\n RdPTs. Les conséquences théoriques de ce résultat\n sont: i) les problémes d'accessibilité et plus\n généralement de model-checking de TCTL sont\n décidables pour les RdPTs bornés; ii) il est\n possible d'étendre les RdPTs en considérant des\n contraintes temporelles strictes sur les transitions\n en préservant les résultats décrits plus haut en\n i). D'un point de vue pratique, les conséquences\n sont doubles: i) on peut spécifier un système à\n l'aide de RdPTs et d'automates temporisés et en\n donner une sémantique facilement; ii) les outils\n disponibles pour l'analyse des automates temporisés\n (comme \\textsf{KRONOS} ou \\textsf{UPPAAL} ou\n \\textsf{CMC}) peuvent être utilisés pour la\n vérification de RdPTs.},\n author = {Cassez, Franck and Roux, Olivier Henri},\n booktitle = {4$\\textit{̀eme}$ Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'03)},\n lex = {Cb},\n class = {natconference},\n category = {tpn},\n month = {October},\n numircyn = {C},\n pdf = {./ps-pdf-files/tpn-ta-03.pdf},\n title = {{Traduction structurelle des Réseaux de {Petri} Temporels en Automates Temporisés}},\n year = {2003}\n}","bibtype":"inproceedings","booktitle":"4$\\textit̀eme$ Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'03)","category":"tpn","class":"natconference","id":"cassez-msr-03","key":"cassez-msr-03","lex":"Cb","month":"October","numircyn":"C","pdf":"./ps-pdf-files/tpn-ta-03.pdf","title":"Traduction structurelle des Réseaux de Petri Temporels en Automates Temporisés","type":"inproceedings","year":"2003","bibbaseid":"cassez-roux-henri-traductionstructurelledesrseauxdepetritemporelsenautomatestemporiss-2003","role":"author","urls":{},"downloads":0},"search_terms":["traduction","structurelle","des","seaux","petri","temporels","automates","temporis","cassez","roux","henri"],"keywords":[],"authorIDs":[],"dataSources":["YiaWb6rdBC8TdWyXv"]}