We develop a game semantics for process algebra with two independent, interacting agents. The purpose of the semantics is to make manifest the role of knowledge and information flow in the interactions between agents and to control the information available to interacting agents. We define games and strategies on process algebras, so that two agents interacting according to their strategies determine the execution of the process, replacing the traditional scheduler. We show that different restrictions on strategies represent different information being available to a scheduler. We also show that a certain class of strategies corresponds to the syntactic schedulers of Chatzikokolakis and Palamidessi, which were developed to overcome problems with traditional schedulers modelling interaction. The restrictions on these strategies have an explicit epistemic flavour. We extend these results to a probabilistic process algebra. Finally, we define a modal logic with both epistemic and temporal modalities to capture how information flows through the system. We give a logical characterization of a concept called introspection which is used to place restrictions on the allowed strategies of an agent. Thus, the logic makes precise what agents "know." / Je présente dans ce thèse une sémantique des jeux pour l'algèbre de processus avec deux agents indépendants qui interagissent. Le but de cette sémantique est de permettre de comprendre le flux d'information et le rôle de la conaissance, ainsi que de contrôler l'information qui est disponible aux agents qui interagissent. Je définis les jeux et les stratégies pour les algèbres de processus, de façon à ce que les deux agents qui suivent ces stratégies lors de leurs interactions déterminent l'exécution du processus, remplaçant ainsi l'ordonnanceur traditionnel. Je démontre que différentes contraintes de stratégie représentent des informations différentes disponibles pour l'ordonnanceur. Je démontre aussi qu'une certaine classe de stratégies correspond aux les ordonnanceurs traditionnels qui modelisent les interactions entre agents. Les contraintes de stratégie ont des aspectes épistémiques explicites. Je généralise ces resultats à l'algébre de processus. Enfin, je présente une logique modale avec des modalités épistémiques et temporales, afin de comprendre le flux d'information dans le système. Je présente une caractérisation logique d'un concept appelé l'introspection, qui est utilisé pour contraindre la stratégie d'un agent, faisant ainsi en sorte que la logique précise ce que les agents conaissent.
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QMM.66667 |
| Date | January 2009 |
| Creators | Knight, Sophia |
| Contributors | Prakash Panangaden (Internal/Supervisor) |
| Publisher | McGill University |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation |
| Format | application/pdf |
| Coverage | Master of Science (School of Computer Science) |
| Rights | All items in eScholarship@McGill are protected by copyright with all rights reserved unless otherwise indicated. |
| Relation | Electronically-submitted theses. |
Page generated in 0.002 seconds