Symbolic Synthesis and Verification of Hierarchical Interface-based Supervisory Control
Pourquoi ce travail est dans la base
Une base qui oublie comment elle a trouvé un travail ne peut pas être vérifiée. Voici les voies qui ont admis celui-ci.
Notice bibliographique
Résumé
Hierarchical interface-based supervisory control (HISC) decomposes a discrete-event system (DES) into a high-level subsystem which communicates with n ges 1 low-level subsystems, through separate interfaces which restrict the interaction of the subsystems. It provides a set of local conditions that can be used to verify global conditions such as nonblocking and controllability. The current HISC verification and synthesis algorithms are based upon explicit state and transition listings which limit the size of a given level to about 10 <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">7</sup> states when 1GB of memory is used. In this paper, we extend the HISC approach by introducing a set of predicate based fixed point operators that allow us to do a per level synthesis to construct for each level a maximally permissive supervisor that satisfies the corresponding HISC conditions. We prove that these fixpoint operators compute the required level-wise supremal languages. We then present algorithms that implement the fixpoint operators. Based on these algorithms, a symbolic implementation is briefly discussed which can be implemented using binary decision diagrams. We also discuss a method to implement our synthesized supervisors in a more compact manner. A large manufacturing system example (worst case state space on the order of 10 <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">30</sup> ) extended from the ALP example is briefly discussed. The example showed that we can now handle a given level with a statespace as large as 10 <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">15</sup> states, using less than 160MB of memory. This represents a significant improvement in the size of systems that can be handled by the HISC approach. A software tool for synthesis and verification of HISC systems using our approach was also developed
Récupéré en direct depuis OpenAlex et désinversé. Les résumés ne sont pas conservés dans cette base de données : les index inversés représentent 8,6 Go des 9,3 Go de texte de la base, et le serveur dispose de 13 Go libres.
Prédiction distillée sur la base complète
Imitation des enseignantsNi prévalence calibrée, ni vérité terrain. Validation humaine à venir. Apprise à partir de 10 348 étiquettes directes de Codex et de 10 348 étiquettes directes de Gemma. Le mode candidate est l'union des têtes enseignantes seuillées; le consensus est leur intersection. Ces sorties portent le statut machine_predicted_unvalidated et ne sont ni des étiquettes humaines ni des étiquettes directes de modèles de pointe.
Scores Codex et Gemma par catégorie
| Catégorie | Codex | Gemma |
|---|---|---|
| Métarecherche | 0,000 | 0,000 |
| Méta-épidémiologie (sens strict) | 0,000 | 0,000 |
| Méta-épidémiologie (sens large) | 0,000 | 0,000 |
| Bibliométrie | 0,000 | 0,000 |
| Études des sciences et des technologies | 0,000 | 0,000 |
| Communication savante | 0,000 | 0,000 |
| Science ouverte | 0,000 | 0,000 |
| Intégrité de la recherche | 0,000 | 0,000 |
| Charge utile insuffisante (le modèle a refusé de juger) | 0,000 | 0,000 |
Scores machine (provisoires)
Les deux têtes enseignantes du modèle étudiant, lues sur ce travail. Un score ordonne la base pour la relecture; il n'affirme jamais une catégorie, et le statut de validation accompagne chaque rangée tel quel.
Scores de référence d'un modèle non mature (critères de maturité non atteints, 7 itérations). Un score ordonne; il n'affirme jamais une catégorie.
score_only:v0-immature-baseline · tel quel depuis la passe de notation : score_only signifie que le nombre peut ordonner les travaux, et qu'aucune étiquette de catégorie n'en découle