Stephen Cole Kleene was one of the greatest logicians of the twentieth century and this book is the influential textbook he wrote to teach the subject to the next generation. It was first published in 1952, some twenty years after the publication of Godel's paper on the incompleteness of arithmetic, which marked, if not the beginning of modern logic. The 1930s was a time of creativity and ferment in the subject, when the notion of computable moved from the realm of (...) philosophical speculation to the realm of science. This was accomplished by the work of Kurt Gode1, Alan Turing, and Alonzo Church, who gave three apparently different precise definitions of computable. When they all turned out to be equivalent, there was a collective realization that this was indeed the right notion. Kleene played a key role in this process. One could say that he was there at the beginning of modern logic. He showed the equivalence of lambda calculus with Turing machines and with Godel's recursion equations, and developed the modern machinery of partial recursive functions. This textbook played an invaluable part in educating the logicians of the present. It played an important role in their own logical education.". (shrink)

A variety of logical frameworks have been developed to study rational agents interacting over time. This paper takes a closer look at one particular interface, between two systems that both address the dynamics of knowledge and information flow. The first is Epistemic Temporal Logic (ETL) which uses linear or branching time models with added epistemic structure induced by agents’ different capabilities for observing events. The second framework is Dynamic Epistemic Logic (DEL) that describes interactive processes in terms of epistemic event (...) models which may occur inside modalities of the language. This paper systematically and rigorously relates the DEL framework with the ETL framework. The precise relationship between DEL and ETL is explored via a new representation theorem characterizing the largest class of ETL models corresponding to DEL protocols in terms of notions of Perfect Recall, No Miracles, and Bisimulation Invariance. We then focus on new issues of completeness. One contribution is an axiomatization for the dynamic logic of public announcements constrained by protocols, which has been an open problem for some years, as it does not fit the usual ‘reduction axiom’ format of DEL. Finally, we provide a number of examples that show how DEL suggests an interesting fine-structure inside ETL. (shrink)

Modern modal logic originated as a branch of philosophical logic in which the concepts of necessity and possibility were investigated by means of a pair of dual operators that are added to a propositional or first-order language. The field owes much of its flavor and success to the introduction in the 1950s of the “possible-worlds” semantics in which the modal operators are interpreted via some “accessibility relation” connecting possible worlds. In subsequent years, modal logic has received attention as an attractive (...) approach towards formalizing such diverse notions as time, knowledge, or action. Nowadays, modal logics are applied in various disciplines, ranging from economics to linguistics and computer science. Consequently, there is by now a large variety of modal languages, with an even greater wealth of interpretations. For instance, many applications require a poly-modal framework consisting of a language with a family of modal operators and a semantics in which the corresponding accessibility relations are connected somehow. (shrink)

Suppose we have a stack of cards that is divided over some players. For certain distributions of cards it is possible to communicate your hand of cards to another player by public announcements, without yet another player learning any of your cards. A solution to this problem consists of some sequence of announcements and is called an exchange. It is called a direct exchange if it consists of (the minimum of) two announcements only. The announcements in an exchange have a (...) special form: they are safe communications, an interesting new form of update. Certain unsafe communications turn out to be unsuccessful updates. A communication is a public announcement that is known to be true. Each communication may be about a set of alternative card deals only, and even about a set of alternatives to the communicating player's own hand only. We list the direct exchanges for a deal of seven cards where the two players holding three cards communicate their hands to each other. Our work may be applicable to the design of cryptographic protocols. (shrink)

A variety of logical frameworks have been developed to study rational agents interacting over time. This paper takes a closer look at one particular interface, between two systems that both address the dynamics of knowledge and information flow. The first is Epistemic Temporal Logic (ETL) which uses linear or branching time models with added epistemic structure induced by agents’ different capabilities for observing events. The second framework is Dynamic Epistemic Logic (DEL) that describes interactive processes in terms of epistemic event (...) models which may occur inside modalities of the language. This paper systematically and rigorously relates the DEL framework with the ETL framework. The precise relationship between DEL and ETL is explored via a new representation theorem characterizing the largest class of ETL models corresponding to DEL protocols in terms of notions of Perfect Recall , No Miracles , and Bisimulation Invariance . We then focus on new issues of completeness . One contribution is an axiomatization for the dynamic logic of public announcements constrained by protocols, which has been an open problem for some years, as it does not fit the usual ‘reduction axiom’ format of DEL. Finally, we provide a number of examples that show how DEL suggests an interesting fine-structure inside ETL. (shrink)

This book provides the first comprehensive introduction to Dynamic Logic. Among the many approaches to formal reasoning about programs, Dynamic Logic enjoys the singular advantage of being strongly related to classical logic. Its variants constitute natural generalizations and extensions of classical formalisms. For example, Propositional Dynamic Logic (PDL) can be described as a blend of three complementary classical ingredients: propositional calculus, modal logic, and the algebra of regular events. In First-Order Dynamic Logic (DL), the propositional calculus is replaced by classical (...) first-order predicate calculus. Dynamic Logic is a system of remarkable unity that is theoretically rich as well as of practical value. It can be used for formalizing correctness specifications and proving rigorously that those specifications are met by a particular program. Other uses include determining the equivalence of programs, comparing the expressive power of various programming constructs, and synthesizing programs from specifications. This book provides the first comprehensive introduction to Dynamic Logic. It is divided into three parts. The first part reviews the appropriate fundamental concepts of logic and computability theory and can stand alone as an introduction to these topics. The second part discusses PDL and its variants, and the third part discusses DL and its variants. Examples are provided throughout, and exercises and a short historical section are included at the end of each chapter. (shrink)

This modern, advanced textbook reviews modal logic, a field which caught the attention of computer scientists in the late 1970's.

Reasoning About Knowledge is the first book to provide a general discussion of approaches to reasoning about knowledge and its applications to distributed ...

Dynamic Epistemic Logic This article tells the story of the rise of dynamic epistemic logic, which began with epistemic logic, the logic of knowledge, in the 1960s. Then, in the late 1980s, came dynamic epistemic logic, the logic of change of knowledge. Much of it was motivated by puzzles and paradoxes. The number … Continue reading Dynamic Epistemic Logic →.

Dynamic Epistemic Logic This article tells the story of the rise of dynamic epistemic logic, which began with epistemic logic, the logic of knowledge, in the 1960s. Then, in the late 1980s, came dynamic epistemic logic, the logic of change of knowledge. Much of it was motivated by puzzles and paradoxes. The number … Continue reading Dynamic Epistemic Logic →.

Many logical systems today describe intelligent interacting agents over time. Frameworks include Interpreted Systems (IS, Fagin et al. [8]), Epistemic-Temporal Logic (ETL, Parikh & Ramanujam [22]), STIT (Belnap et al. [5]), Process Algebra and Game Semantics (Abramsky [1]). This variety is an asset, as different modeling tools can be fine-tuned to specific applications. But it may also be an obstacle, when barriers between paradigms and schools go up. This paper takes a closer look at one particular interface, between two systems (...) that both address the dynamics of knowledge and information flow in multi-agent systems. One is IS/ETL (IS and ETL are, from a technical point of view, the same up to model transformations, cf. [20]), which uses linear or branching time models with added epistemic structure induced by agents’ different capabilities for observing events. These models provide a Grand Stage where histories of some process unfold constrained by a protocol, and a matching epistemic-temporal language describes what happens. The other framework is Dynamic Epistemic Logic (DEL, [10, 4, 34]) that describes interactive processes in terms of epistemic event models which may occur inside modalities of the language. Temporal evolution is then computed from some initial epistemic model through a process of successive ‘product updates’. It has long been unclear how to best compare IS/ETL and DEL. Various aspects have been investigated in [10, 30, 32], but in this paper, we study the interface in a more systematic way. Often, DEL and ETL are presented as alternative ways of adding dynamics to multi-agent epistemic models. In this paper, we rather focus on how merging the two different modeling choices leads to interesting new questions. Our leading interest here will be a view of informational processes as evolving over time. To see what we mean, consider the simplest version of DEL, viz. the logic of public announcements PAL ([23]) which adds a very specific type of communicative 1 action to epistemic models: a public announcement.. (shrink)

Classical epistemic logic describes implicit knowledge of agents about facts and knowledge of other agents, based on semantic information. The latter is produced by acts of observation or communication, that are described well by dynamic epistemic logics. What these logics do not describe, however, is how significant information is also produced by acts of inference – and key axioms of the system merely postulate “deductive closure”. In this paper, we take the view that all information is produced by acts, and (...) hence we also need a dynamic logic of inference steps showing what effort on the part of the agent makes a conclusion explicit knowledge. Strong omniscience properties of agents should be seen not as static idealizations, but as the result of dynamic processes that agents engage in. This raises two questions: (a) how to define suitable information states of agents and matching notions of explicit knowledge, (b) how to define natural processes over these states that generate new explicit knowledge. To this end, we extend earlier epistemic “awareness models” into a dynamic system that includes acts of public observation, but also adding and dropping formulas from the currently ‘entertained’ set, we give a completeness theorem, and we show how this dynamics updates explicit knowledge. Similar ideas have been proposed before, but they were restricted to update with factual propositions; our new dynamic system applies to arbitrary formulas. We also extend our approach to multi-agent scenarios where awareness changes may happen privately. Finally, we mention further directions and related approaches. (shrink)

Current dynamic epistemic logics for analyzing effects of informational events often become cumbersome and opaque when common knowledge is added for groups of agents. Still, postconditions involving common knowledge are essential to successful multi-agent communication. We propose new systems that extend the epistemic base language with a new notion of ‘relativized common knowledge’, in such a way that the resulting full dynamic logic of information flow allows for a compositional analysis of all epistemic postconditions via perspicuous ‘reduction axioms’. We also (...) show how such systems can deal with factual alteration, rather than just information change, making them cover a much wider range of realistic events. After a warm-up stage of analyzing logics for public announcements, our main technical results are expressivity and completeness theorems for a much richer logic that we call LCC. This is a dynamic epistemic logic whose static base is propositional dynamic logic (PDL), interpreted epistemically. This system is capable of expressing all model-shifting operations with finite action models, while providing a compositional analysis for a wide range of informational events. This makes LCC a serious candidate for a standard in dynamic epistemic logic, as we illustrate by analyzing some complex communication scenarios, including sending successive emails with both ‘cc’ and ‘bcc’ lines, and other private announcements to subgroups. Our proofs involve standard modal techniques, combined with a new application of Kleene’s theorem on finite automata, as well as new Ehrenfeucht games of model comparison. (shrink)