[BR03] Parametrised Verification of Class of Resource Allocation systems
Conférence Internationale avec comité de lecture :
Actes de la Conférence Internationale sur la Productique, CIP’03, CDTA - Alger,
January 2003,
pp.52-59,
motcle:
Résumé:
The present work deal with two problems concerning behavioural properties for a large class of resource allocation systems (RAS) called G-systems generalising well-known models presented in the literature. The first problem is the well-formedness characterisation. It consists to prove the existence of an initial marking ensuring non-blockingness (from any state reachable from initial state, it is always possible to reach a desirable (or final) state). The second problem consists to show that under appropriate supervision non-blockingness of G-sytems can also be always ensured. Using structure theory of Petri nets, we state, a structural and parameterised characterisation for these two problems. In particular, the proposed solution for the second problem can be interpreted as a synthesis of a parameterised and modular supervisor.