Efficient Verification and New Reasoning Techniques for Concurrent Constraint Programming
Vérification Efficace Et Nouvelles Techniques De Raisonnement Pour La Programmation Concurrente Par Contraintes
Résumé
Concurrent constraint programming (CCP) is a mature linguistic formalism from the family of process calculi and hence it treats processes much like the lambda-calculus treats computable functions. CCP is based on shared-memory communication where processes interact by adding and querying partial information represented as constraints (e.g., "x > 42") in a global store. This dissertation is focused on the development of novel reasoning techniques for program equivalence in CCP and their efficient verification.
The first part of the thesis describes an algorithm for deciding strong bisimilarity for finite CCP processes. This is accomplished by first showing that the standard partition refinement approach does not work for CCP. Then it is shown how to adapt the standard approach for the case of CCP. Furthermore, it is proven that this procedure suffers from the state explosion, common in the verification of concurrent systems, due mostly to the presence of non-deterministic choices.
The second part is devoted to the development of a weak semantics for CCP. As pointed out in the literature, one can use the procedure for strong bisimilarity to decide weak bisimilarity. The idea is to define a new transition relation based on the operational semantics. This method is known as saturation. The standard saturation is defined by omitting the silent transitions in the calculus. This works for CCS and other calculi, however in the case of CCP, because of its involved labeled transitions, it is shown that the standard technique is not complete. Then a new saturation is defined called weak semantics for CCP. It consists of the reflexive and transitive closure under any constraint in CCP instead of just closing with respect to the silent transitions. Most importantly, it is proven that the proposed weak semantics is sound and complete for CCP. As a consequence, the new saturation can be used for checking weak bisimilarity.
In the third part the focus is shifted toward efficiency on the verification of weak bisimilarity. To achieve this, a representative sub-language of CCP is considered: the choice-free fragment (CCP\+). First, it is shown that the verification algorithms described above have an exponential-time complexity even for programs from CCP\+. Then by exploiting confluence, a distinctive feature from this fragment, two alternative polynomial-time decision procedures for CCP\+ weak bisimilarity are proposed. Each of these two procedures has an advantage over the other. One has a better time complexity, while the other can be easily adapted for the full language of CCP to produce significant state space reductions. The relevance of both procedures derives from the importance of CCP\+. This fragment, which has been the subject of much theoretical study, has strong ties to first-order logic and an elegant denotational semantics, and it can be used to model real-world situations. Most importantly, previously it was proven that weak bisimilarity in CCP\+ coincides with the standard observational equivalence for CCP\+. Hence from the results presented in this part, two efficient algorithms for checking program equivalence in CCP\+ are obtained.
The last part addresses the congruence issue for the full language of CCP. It is shown that weak saturated barbed bisimilarity is not a congruence for CCP, as is the case for weak bisimilarity in CCS. This problem is tackled by introducing a new notion that characterizes the weakest equivalence included in the congruence induced by weak bisimilarity for CCP. We call this new notion weak full bisimilarity. More importantly, it is proven that weak full bisimilarity is a congruence for the full language of CCP. It is also shown that weak full bisimilarity coincides with the standard notion of observational equivalence in CCP\+. To the best of our knowledge, this is the first notion of weak bisimilarity that is a congruence for the full language of CCP.
This dissertation contributes to the study of program equivalence in CCP. It provides an exponential-time decision procedure for strong bisimilarity in finite CCP as well as its adaptation to checking weak bisimilarity. Furthermore, this dissertation proposes two alternative polynomial-time algorithms for the verification of observational equivalence in the absence of nondeterministic choice. It concludes by proving that the existing notions of bisimilarity are not adequate for CCP with choice. Finally, it defines a novel reasoning technique which is proven to be the right notion of equivalence for the full language of CCP.
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\+.
Fichier principal
THESE_version_definitive_PINODUQUE_LuisFernando.pdf (2.19 Mo)
Télécharger le fichier
Loading...