Skip to Main content Skip to Navigation
Theses

Efficient Verification and New Reasoning Techniques for Concurrent Constraint Programming

Luis Fernando Pino Duque 1, 2
2 COMETE - Concurrency, Mobility and Transactions
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
Résumé : La Programmation Concurrente par Contraintes (CCP) est un formalisme linguistique mature de la famille des algèbres de processus, il traite les processus de la même façon que le lambda-calcul traite les fonctions calculables. CCP est basé sur la communication à mémoire partagée où les processus interagissent en ajoutant et en interrogeant des informations partielles représentées comme des contraintes (par exemple, "x > 42") dans une mémoire globale. Cette thèse se concentre sur le développement de nouvelles techniques de raisonnement pour l’équivalence des processus dans CCP et leur vérification efficace. La première partie de cette thèse décrit un algorithme pour calculer la bisimilarité forte pour des processus finis du CCP. Ceci est accompli en montrant d'abord que l'approche de raffinement des partitions standard ne fonctionne pas pour CCP. Ensuite, il est montré comment adapter l'approche standard pour le cas de CCP. En outre, il est prouvé que cette procédure souffre de l'explosion combinatoire, commune à la vérification de systèmes concurrents, principalement en raison de la présence de choix non-déterministe. La deuxième partie est consacrée à l'élaboration d'une sémantique faible pour CCP. Comme il est souligné dans la littérature, on peut utiliser la procédure de bisimilarité forte pour décider la faible. L'idée est de définir une nouvelle relation de transition basée sur la sémantique opérationnelle, cette méthode est connue comme la saturation. La saturation standard est définie par l'omission des transitions silencieuses dans le calcul. Cela fonctionne pour le CCS et d'autres calculs, mais dans le cas de la CCP, en raison de ses transitions plus complexes, il est démontré que la technique standard n'est pas complète pour CCP. Ensuite, une nouvelle saturation est définie, nous l'appelons sémantique faible pour CCP. Elle consiste à la fermeture réflexive et transitive dans CCP au lieu de simplement la clôture sur les transitions silencieuses. Surtout, il est prouvé que la sémantique faible proposée est correcte pour CCP. En conséquence, la nouvelle saturation peut être utilisée pour le calcul de la bisimilarité faible. La troisième partie est dédiée à l'efficacité de la vérification de la bisimilarité faible. Pour ce faire, un sous-langage représentant du CCP est considérée: le fragment sans choix non-déterministe (CCP\+). Tout d'abord, il est montré que les algorithmes de vérification précédents ont une complexité exponentielle même pour les processus de CCP\+. Ensuite, en exploitant la confluence, une caractéristique distinctive de ce fragment, deux algorithmes en temps polynomiales alternatifs pour la bisimilarité faible CCP\+ sont proposés. Chacune de ces deux procédures a un avantage sur l'autre. La première présente une meilleure complexité en temps, alors que la seconde peut être facilement adaptée pour produire des importants améliorations dans l’algorithme pour tout le langage de CCP. La dernière partie aborde la question de la congruence dans tout CCP. Il est montré que la bisimilarité faible n'est pas une congruence pour CCP, comme c'est le cas pour CCS. Ce problème est abordé par l'introduction d'une nouvelle notion qui caractérise l'équivalence la plus faible incluse dans la congruence induite par la bisimilarité faible pour CCP. Nous appelons cette nouvelle notion bisimilarité faible pleine. Plus important encore, il est prouvé que la bisimilarité faible pleine est une congruence pour CCP avec de choix non-déterministe. Il est également montré que la bisimilarité faible pleine coïncide avec la notion classique de l'équivalence observationnelle de CCP\+.
Complete list of metadatas

Cited literature [69 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/tel-01111979
Contributor : Luis Fernando Pino Duque <>
Submitted on : Monday, February 2, 2015 - 8:27:21 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Document(s) archivé(s) le : Wednesday, May 27, 2015 - 3:25:57 PM

Identifiers

  • HAL Id : tel-01111979, version 1

Collections

Citation

Luis Fernando Pino Duque. Efficient Verification and New Reasoning Techniques for Concurrent Constraint Programming. Data Structures and Algorithms [cs.DS]. Ecole Polytechnique, 2014. English. ⟨tel-01111979⟩

Share

Metrics

Record views

760

Files downloads

872