Project topics and materials
Get Complete Project Material File(s) Now! »
Epistemic Logic
Epistemic logic is a species of modal logic where the basic modality is of the form \Agent i knows fact phi »: it is the logic of knowledge. Philosophers from all cultures, particularly Indian and Chinese Buddhist philosophers, Aristotle and other Greeks, the Port-Royal modal logicians of the middle ages and modern analytic philosophers, such as Chisholm, Ayer and Gettier, have debated the meaning of knowledge. The kind of epistemic logic that we consider is a philosophically simple variant that is nevertheless well adapted to the computational situations that we consider in our applications. For these applications it is not necessary to enter into the philosophical issues of what constitutes human knowledge: it su ces to consider a very simple notion of knowledge that justi es certain actions being taken at certain states of a protocol.
Although epistemic logic was discussed as a variety of modal logic ear-lier, particularly by von Wright [vW51], the speci c form of epistemic logic we focus on was rst really developed by Jaakko Hintikka [Hin62] and was based on Saul Kripke’s so-called \possible worlds » semantics for modal log-ics. Hintikka’s presentation was essentially semantic and it was an observa-tion by Lemmon that this was an example of one of the well-known modal logics.
Epistemic logic began to be applied to computer science in the 1980s [HM84, FHMV95], when it was realized that epistemic concepts were in-volved in many important coordination and agreement protocols in dis-tributed systems. Epistemic logic is usually used to verify that protocols respect desired properties and as such form a powerful adjunct to other pro-gram logics. The kind of properties that are particularly well captured by epistemic logic are those related to agreement and coordination as already mentioned, but also to security properties when it becomes important to know what information is potentially being leaked out of a system in the course of the execution of a protocol.
Concurrency
The rst models of computation, for example Turing Machines [Tur37], were fundamentally sequential: there was no ambiguity about the order in which computational steps could occur. The sequential computation paradigm evolved around some key central concepts: the -calculus as the basic uni-fying formalism and the notion of state and state transformation as the basic semantic framework. This framework accommodates a rich variety of developments: types and higher-type computation, program logics, oper-ational semantics and denotational semantics to mention a few examples. The world of concurrent computation, by contrast, lacks a single central unifying concept like the -calculus.
Concurrency theory involves a much greater variety of possible phe-nomena than sequential computation. Once there are multiple autonomous processes functioning independently it is possible that these processes coop-erate, compete for resources, act simultaneously, communicate but remain autonomous, or synchronize. The very basic temporal notions that we take so much for granted in sequential computing become major decision points when setting up a framework for concurrent computing. These features make concurrent systems quite general and allow them to be a relevant model of systems that are now common, but they also necessitate more decisions about the models of computation. Originally, concurrency was concerned mainly with operating systems, but now that new types of dis-tributed systems such as social networks, interacting mobile devices, and cloud computing have become ubiquitous, concurrency theory is even more relevant and important.
Since concurrent systems are both widespread and inherently di erent from sequential systems of computation, many e orts have been made to develop accurate and understandable models for them. Ideally, these models are simple but still able to capture all the essential aspects of concurrent sys-tems, and are also capable of being formally analyzed, to allow reasoning about the systems, as well as proofs of desired properties.
The rst well known model of concurrent systems was Petri nets, which represent systems as a kind of graph with resources or tokens enabling transitions between states [Pet63]. Since then, there has been a wide variety of models of concurrent systems. For example, a labelled transition system is an extremely simple model of a concurrent system, consisting only of states and actions which may transition from one state to another.
Communication between agents is one of the fundamental aspects of concurrent systems, and models treat communication in one of two ways: synchronous or asynchronous. In a synchronous system, agents synchronize and communicate together at the same time, like in a telephone call. In asynchronous communication, one agent sends a message, which is later received by the other agent at an unspeci ed time. Email communication, for example, is asynchronous.
An early asynchronous model of concurrent systems was Jack Den-nis’ data ow model [Den74]. This model had a xed network of au-tonomous computing agents with unidirectional communication channels linking them. The processes could read from and write to the communica-tion channels, but if a process tried to read from an empty channel, where no message had yet arrived, it was blocked until it received a message on this channel. As we shall see later, the Concurrent Constraint Programming (CCP) paradigm has exactly this kind of asynchronous communication.
On the other hand, process calculi are another important class of models, on which we shall focus in this thesis. Besides a few exceptions, such as CCP, process calculi use synchronous communication. They are quite diverse, but the general idea is to represent computing agents or processes as algebraic terms built from simple operators, and to provide an operational semantics de ning the computational steps a process can take, based on its semantic form. Once a system is represented as a process calculus term, it should be easy to reason about important aspects of its behaviour, for example, what other systems it can be considered as equivalent to, and what behaviours it may or may not do.
One of the earliest process calculi was Robin Milner’s Calculus of Com-municating Systems, or CCS [Mil80]. This process calculus is quite simple but includes features that became common to many future process calculi, such as basic actions de ned based on the intended application, nondeter-ministic choice between subprocesses, parallel execution of subprocesses, communication between two subprocesses, recursion, and restricting a sub-process from interacting with its environment in speci c ways. CCS allows all of these kinds of behaviours but still is simple and general, so it became an important calculus for modelling computations. However, the simplicity of CCS masked a semantic complexity that took a long time to understand. Semantic models of CCS were slow to develop and, in the end were very operational in character.
Besides CCS, many other process calculi were developed for di erent purposes and with di erent advantages. For example, Hoare’s Communicat-ing Sequential Processes (CSP) was another early process calculus [Hoa85], with a more restricted notion of choice than in CCS. The Pi-Calculus is another process calculus [MPW92]. Pi-Calculus introduced the notion of mobility: instead of a xed network of communicating agents, in the Pi-Calculus, channel names can be communicated over channels, making it possible for the communication structure between agents to change during the execution of a process. There have also been process calculi developed for speci c purposes, such as the Spi-calculus [AG99], an extension of the Pi-calculus with built in cryptographic primitives such as encryption and decryption of messages. Innovation continues to occur in process calculi, for example, the family of process calculi known as Ambient Calculi allow a more general notion of mobile processes, to be better able to model mod-ern computational situations such as mobile computing devices [CG00]. A recent development is the Psi-Calculus [BJPV09], a process calculus with nominal data types which is general enough to encompass all the calculi mentioned above, and can model both synchronous and asynchronous com-munication.
Concurrent Constraint Programming
For this thesis, the process calculus called Concurrent Constraint Program-ming (CCP) [SRP91] is one of our main areas of interest. CCP is another formalism for concurrency, more closely based on logic than other process calculi. It was the rst process calculus with asynchronous communication. In CCP, communication between agents occurs through shared variables in a store. The store contains partial information about variables: rather than simply assigning values to variables, the store can contain more complex in-formation, called constraints, for example, \X > 5″ or \X + Y is even. » Agents in CCP processes can add information to the store or ask the store for information, allowing a kind of synchronization between agents, because asking agents cannot continue until the store entails the information they are asking for.
In fact, the action of the process on the store is one of the most important aspects of CCP. The structure underlying the store is called the constraint system and is in fact a complete lattice. One of the important properties of basic CCP is con uence, meaning in essence that all reasonable computa-tions of the same process will eventually reach the same outcome. A process can, therefore, be viewed as a function on the underlying constraint system, taking the original store as input and returning the nal store that results from the execution of the process. Furthermore, CCP processes can only add information to a store, never remove it, and the nal store of a process is a xed point for that process: even if the process executed again starting from this store, it would not change it. These properties of CCP mean that processes can in fact be viewed as closure operators on the constraint system. Thus, there is a simple and elegant mathematical semantics for CCP. These results are presented in detail in Section 3.2, but the essential point is that the asynchronous nature of CCP and its close ties to logic make elegant mathematical characterizations of its behaviour possible.
This Thesis: Epistemic Reasoning in Concurrent Systems
The goal of this thesis is to develop formalisms for concurrent systems that make epistemic information directly accessible within the formalism. Recently, concurrent systems have changed substantially with the advent of phenomena such as social networks and cloud computing. In past research on concurrent distributed systems [Lyn96] the emphasis has mostly been on consistency, fault tolerance, resource management and related topics; these aspects were all characterized by interaction between processes. The new era of concurrent systems is marked by the importance of managing access to information to a much greater degree than before.
Although this kind of analysis has not been common in process calculus research, epistemic concepts have long been understood to be crucial in distributed computing scenarios. Their importance was realized as early as the mid 1980s with Halpern and Moses’ groundbreaking paper on common knowledge [HM84]. These ideas led to a urry of activity in the following few years [FHMV95] with many distributed protocols being understood from an epistemic point of view. The impact of epistemic ideas in the concurrency theory community has been slower in coming.
There has been, however, some work concerning epistemic ideas in con-currency theory. For example, the goal of [CP07] was to restrict the epis-temic information available to the scheduler in a probabilistic variant of the Pi-calculus, in order to avoid security problems of information leakage in the execution of processes. But even though epistemic ideas are central to this paper, formal epistemic logic is not used. Epistemic logic has, however, been used to analyse concurrent systems, for example in [CDK09], an epis-temic logic is developed whose models are terms in the applied Pi-calculus. Similarly, [DMO07] presents a temporal epistemic logic for reasoning about terms in a certain process calculus. In [HS04], a method is presented for formalizing information hiding properties in many process calculi, which is more general than the two approaches mentioned above, but still falls into the category of using an epistemic logic to analyze the properties of a term in a process calculus. In fact, as far as we know, all applications of epistemic logic to process calculi have consisted of using epistemic logic to analyze process calculus terms which are completely outside of the epis-temic logic. In this thesis, we will present several approaches to including epistemic information directly within process calculi. This will allow us to encode agents’ knowledge directly within processes, control information ow, analyze the e ects of actions on agents’ knowledge, and limit the ac-tions agents are able to take based on the epistemic information available to them.
Outline and Contributions
This thesis has three parts. In Part I, we introduce a new constraint pro-cess calculus that allows the expression of epistemic information within the calculus. We also develop a notion of modal constraint system, underlying the process calculus and enabling us to use epistemic information to do computations, and we discuss characterizations of observable behaviour for these processes. In Part II, we present a variant of dynamic epistemic logic adapted to labelled transition systems. This logic allows us to examine the e ects of actions on agents’ knowledge in labelled transition systems. We give a sound and complete axiomatization of the logic. Finally, in Part III, we describe a game semantics for agents’ interaction which makes mani-fest the role of knowledge and information ow in the interactions between agents, and makes it possible to control the information available to the interacting agents.
Besides these three parts, there are two introductory chapters, the rst being the present introduction. Chapter 2 introduces some preliminary information about modal logic, which will be used throughout the rest of the thesis.
Part I- Epistemic Logic as a Programming Language
In Chapter 3 we review some notions in domain theory and concurrent con-straint programming. Next, in Chapter 4, we introduce domain-theoretical structures to represent spatial and epistemic information. In Chapter 5, we present two new process calculi, based on the above-mentioned under-lying constraint systems: Spatial CCP, with a new operator to represent a computation happening in a space belonging to an agent, and Epistemic CCP, with a new operator to represent an agent’s knowledge of a compu-tation. We also give an operational semantics for this process calculus. In Chapter 6, we present three notions of behaviour for the processes we have de ned: limits, barbs, and denotational semantics. We prove that these three notions of behaviour coincide. Finally, in Chapter 7, we present some preliminary work on methods of approximating common knowledge as a compact or nite element, rather than as an in nite limit.
Table of contents :
1 Introduction
1.1 Context
1.1.1 Epistemic Logic
1.1.2 Concurrency
1.2 This Thesis: Epistemic Reasoning in Concurrent Systems
1.3 Outline and Contributions
1.3.1 Part I- Epistemic Logic as a Programming Language
1.3.2 Part II- How Knowledge Evolves
1.3.3 Part III- Epistemic Strategies for Concurrent Processes
1.4 Publications
2 Preliminaries on Modal Logic
2.1 Relational Structures and the Semantics of Modal Logic
2.2 Validity, Soundness and Completeness
2.3 Specic Modal Logics
2.3.1 Kn
2.3.2 S4
2.3.3 S5
I Epistemic Logic as a Programming Language: Epistemic Modalities in Process Calculi
Introduction
3 Preliminaries
3.1 Domain theory
3.2 Concurrent constraint programming
3.2.1 Constraint systems
3.2.2 Processes
4 Space and Knowledge in Constraint Systems
4.1 Spatial Constraint Systems
4.1.1 Inconsistency Connement
4.2 Epistemic Constraint Systems
4.3 Examples
5 Space and Knowledge in Processes
5.1 Syntax
5.1.1 Basic Processes
5.1.2 Spatial Processes
5.1.3 Epistemic Processes
5.1.4 Innite Processes
5.2 Reduction Semantics
5.2.1 Operational Semantics for SCCP
5.2.2 Operational Semantics for ECCP
6 Observable Behaviour of Space and Knowledge
6.1 Observing Limits
6.2 Observing Barbs
6.3 Denotational Semantics
7 Future Work and Conclusions
7.1 Compact Approximation of Space and Knowledge
7.2 Related Work
7.3 Future Work
7.4 Conclusion
II How Knowledge Evolves: Epistemic Logic for Labelled Transition Systems
Introduction
8 Histories
8.1 Labelled transition systems with agents
8.2 History Systems
9 The Logic and its Semantics
9.1 Syntax and Models
9.2 Semantics
9.3 An example
10 A Complete Axiomatization
10.1 Axioms
10.2 Soundness and Completeness
Conclusions and Related Work
III Knowing What You Are Doing: Epistemic Strate- gies for Concurrent Processes
Introduction
11 Background
12 Games and Strategies
12.1 Valid Positions
12.2 Strategies
12.3 Execution of Processes According to Strategies
12.4 Epistemic Restrictions on Strategies
13 Correspondence between Strategies and Schedulers
13.1 Background on Schedulers
13.2 Correspondence Theorem
14 Games for Processes with Probabilistic Choice
14.1 Syntax and Semantics
14.2 Games, Valid Positions and Strategies
14.2.1 Valid Positions
14.2.2 Strategies
14.2.3 Execution of a probabilistic process with a strategy
15 A Modal Logic for Strategies
15.1 Syntax and Semantics
15.2 Basic Properties Captured in Modal Logic
15.3 Logical Characterization of Indistinguishability Relations
15.4 Properties Following from Logical Characterizations of Equivalence Relations
Conclusions and Related Work
16 Conclusion
Bibliography
