Loading...
Please wait, while we are loading the content...
Similar Documents
Vérification de réseaux de Petri avec états sous une sémantique d'ordres partiels
| Content Provider | Semantic Scholar |
|---|---|
| Author | Avellaneda, Florent Morin, Rémi |
| Copyright Year | 2013 |
| Abstract | Afin de munir le formalisme des MSG de compteurs, de timers et d'autres aspects, nous introduisons le modele des reseaux de Petri avec etats et une semantique de processus non-branchants. Ce modele est non seulement plus expressif que les MSG, mais il permet egalement des specifications plus concises. Nous nous interessons a trois problemes de verification classiques sur l'ensemble des marquages accessibles par les prefixes des processus : le caractere borne, la couverture et l'accessibilite. Nous montrons comment reduire ces problemes au cas particulier des reseaux de Petri de telle sorte que tous les resultats de complexite et de decidabilite s'etendent des reseaux de Petri aux reseaux avec etats sous la semantique des processus. Nous introduisons aussi la notion de borne semi-structurelle afin de considerer des systemes parametres. Cela consiste a fixer le marquage initial d'un sous-ensemble approprie de places, puis a verifier que le systeme est borne quel que soit les valeurs des parametres. Nous montrons comment un depliage conduit a un probleme plus simple a verifier a l'aide de la Programmation Lineaire. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | https://core.ac.uk/download/pdf/52440995.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
