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

  MONTH = OCT,
  NUMIRCYN = {C},
  PDF = {./ps-pdf-files/tpn-ta-03.pdf},
  TITLE = {{Traduction structurelle des R{\'e}seaux de {Petri} Temporels en Automates Temporis{\'e}s}},
  YEAR = {2003}
}

{"_id":"PEQqMBWRqtB8eTJyy","bibbaseid":"cassez-roux-traductionstructurelledesrseauxdepetritemporelsenautomatestemporiss-2003","downloads":0,"creationDate":"2015-12-22T04:31:53.096Z","title":"Traduction structurelle des Réseaux de Petri Temporels en Automates Temporisés","author_short":["Cassez, F.","Roux, O."],"year":2003,"bibtype":"inproceedings","biburl":"http://science.mq.edu.au/~fcassez/bib/mabib.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","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 \\^etre utilisés pour la vérification de RdPTs.","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"propositions":[],"lastnames":["Roux"],"firstnames":["Olivier Henri"],"suffixes":[]}],"booktitle":"4$<i>ème</i>}$ 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","bibtex":"@INPROCEEDINGS{cassez-msr-03,\n ABSTRACT = {Dans cet article, nous consid{\\'e}rons les r{\\'e}seaux de Petri\n t-temporels (RdPT) c'est {\\`a} dire pour lesquels le\n temps est associ{\\'e} aux transitions sous la forme d'un\n interval. Nous en donnons une s{\\'e}mantique formelle en\n terme de syst{\\`e}mes de transitions temporis{\\'e}s. Nous\n proposons ensuite une traduction structurelle des\n RdPTs en un produit synchronis{\\'e} d'automates\n temporis{\\'e}s (ATs) qui pr{\\'e}serve la s{\\'e}mantique\n comportementale (bisimilarit{\\'e} temporelle) des\n RdPTs. Les cons{\\'e}quences th{\\'e}oriques de ce r{\\'e}sultat\n sont: i) les probl{\\'e}mes d'accessibilit{\\'e} et plus\n g{\\'e}n{\\'e}ralement de model-checking de TCTL sont\n d{\\'e}cidables pour les RdPTs born{\\'e}s; ii) il est\n possible d'{\\'e}tendre les RdPTs en consid{\\'e}rant des\n contraintes temporelles strictes sur les transitions\n en pr{\\'e}servant les r{\\'e}sultats d{\\'e}crits plus haut en\n i). D'un point de vue pratique, les cons{\\'e}quences\n sont doubles: i) on peut sp{\\'e}cifier un syst{\\`e}me {\\`a}\n l'aide de RdPTs et d'automates temporis{\\'e}s et en\n donner une s{\\'e}mantique facilement; ii) les outils\n disponibles pour l'analyse des automates temporis{\\'e}s\n (comme \\textsf{KRONOS} ou \\textsf{UPPAAL} ou\n \\textsf{CMC}) peuvent {\\^e}tre utilis{\\'e}s pour la\n v{\\'e}rification de RdPTs.},\n AUTHOR = {Franck Cassez and Roux, {Olivier Henri}},\n BOOKTITLE = {4$\\textit{\\`eme}$ Colloque Francophone sur la Mod{\\'e}lisation des Syst{\\`e}mes R{\\'e}actifs, (MSR'03)},\n LEX = {Cb},\n CLASS = {natconference},\n CATEGORY = {tpn},\n\n MONTH = OCT,\n NUMIRCYN = {C},\n PDF = {./ps-pdf-files/tpn-ta-03.pdf},\n TITLE = {{Traduction structurelle des R{\\'e}seaux de {Petri} Temporels en Automates Temporis{\\'e}s}},\n YEAR = {2003}\n}\n\n","author_short":["Cassez, F.","Roux, O."],"key":"cassez-msr-03","id":"cassez-msr-03","bibbaseid":"cassez-roux-traductionstructurelledesrseauxdepetritemporelsenautomatestemporiss-2003","role":"author","urls":{},"metadata":{"authorlinks":{}},"html":""},"search_terms":["traduction","structurelle","des","seaux","petri","temporels","automates","temporis","cassez","roux"],"keywords":[],"authorIDs":[],"dataSources":["yYF8uwWqay28JyxZC"]}