APPLICATION DES METHODES D'ORDRE PARTIEL AUX EQUIVALENCES COMPORTEMENTALES DES SYSTEMES CONCURRENTS / MONICA LARA DE SOUZA ROBERT ; SOUS LA DIRECTION DE R. DE SIMONE

Date :

Editeur / Publisher : [S.l.] : [s.n.] , 1995

Format : 105 P.

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Université de Nice (1965-2019) (Organisme de soutenance / degree-grantor)

Résumé / Abstract : CETTE THESE ABORDE LE PROBLEME DE L'EXPLOSION D'ETATS DANS LA VERIFICATION DE SYSTEMES CONCURRENTS. NOUS CHERCHONS A COMBINER DEUX APPROCHES COMPLEMENTAIRES: D'UNE PART, LES METHODES D'ORDRE PARTIEL QUI PRODUISENT UN AUTOMATE PARTIEL EN ELIMINANT LES ENTRELACEMENTS REDONDANTS PROVENANT DE COMPORTEMENTS INDEPENDANTS D'UN AUTOMATE COMPLET, D'AUTRE PART, LES REDUCTIONS CLASSIQUES FONDEES SUR LES QUOTIENTS PAR EQUIVALENCE COMPORTEMENTALES ENTRE ETATS. ETANT DONNE UNE RELATION D'INDEPENDANCE ENTRE ACTIONS, NOUS DONNONS UNE CARACTERISATION AXIOMATIQUE DES AUTOMATES COMPLETS, PUIS DES AUTOMATES PARTIELS A L'AIDE DE PREDICATS D'ETATS INDIQUANT LES COMPORTEMENTS OMIS, SOIT PAR ANTICIPATION SOIT PAR RETARDEMENT. NOUS DEFINISSONS LES NOTIONS D'INCLUSION ET D'EGALITE DE LANGAGES, DE RAFFINEMENT DE SIMULATION ET D'EQUIVALENCE DE BISIMULATION SUR LES AUTOMATES PARTIELS. A L'AIDE DES AXIOMES INTRODUITS, NOUS MONTRONS QUE L'INCLUSION OU L'EGALITE DES LANGAGES DE TRACES GLOBAUX EST PRESERVEE AU TRAVERS DE PREORDRES OU EQUIVALENCES COMPORTEMENTALES SUR LES AUTOMATES PARTIELS. DES FORMES CANONIQUES PEUVENT ETRE DEFINIES ET DONNER LIEU A UNE CERTAINE FORME DE COMPOSITIONNALITE SUR LE QUOTIENT D'AUTOMATES PARTIELS. NOUS EXPLORONS LES PROBLEMES POSES PAR L'INTRODUCTION D'ACTIONS LOCALES INVISIBLES ET LES EQUIVALENCES DE TYPE FAIBLE. NOUS DEFINISSONS LA P-BISIMULATION ARBORESCENTE ENTRE LES ETATS D'UN AUTOMATE PARTIEL, ET NOUS DEMONTRONS QU'ELLE PRESERVE L'EGALITE DE LANGAGES AVEC MORPHISMES EFFACANTS POUR LES AUTOMATES COMPLETS. LA THEORIE DEVELOPPEE A ETE IMPLEMENTEE SOUS LA FORME D'UN PROTOTYPE QUI, A PARTIR D'UN RESEAU D'AUTOMATES, PRODUIT UN AUTOMATE PARTIEL QUI PEUT ETRE UTILISE POUR TESTER LES EQUIVALENCES DE LANGAGES OU LA BISIMULATION PAR RAPPORT A UN AUTOMATE PARTIEL DETERMINISTE