Joseph Y. Halpern (editor)
This is the proceedings of the first TARK conference, with papers by (among others) Aumann, Hintikka, Fagin, Moses, and Vardi. It includes my first overview on knowledge.
Published by Morgan Kaufmann, 1986.
Joseph Y. Halpern, Ronald Fagin, Yoram Moses, and Moshe Y. Vardi
This book covers much of my research on knowledge. Ordering information is available from MIT Press.
Published by MIT Press, 1995. A revised paperback edition was published in 2003.
Joseph Y. Halpern
This book covers much of my research on uncertainty. Ordering information is available from MIT Press.
Published by MIT Press, 2003. A slightly revised paperback edition was published in 2005.
Uncertainty in Artificial Intelligence: Proceedings of Twentieth Conference
Max Chickering and Joseph Y. Halpern (editors)
Published by AUAI Press, 2004
Towards a theory of knowledge and ignorance: preliminary report
Joseph Y. Halpern and Yoram Moses
Situations in which the information about a given domain is partial are common in many AI applications. In planning and analysis of scenarios involving partial information, the state of knowledge of an intelligent agent in such circumstances becomes important. This paper addresses the problem of characterizing this state of knowledge, with the emphasis on the single-agent case. We give a number of equivalent ways to characterize this state of knowledge, as well as an algorithm for computing the formulas that are true in this state. The relationship between this work and related works by Stark, Konolige, and Moore is discussed.
In Logics and Models of Concurrent Systems (ed. K. Apt), Springer-Verlag, 1985, pp. 459-476 and in Proceedings of the Workshop on Non-Monotonic Reasoning, 1984, pp. 125-143. The paper is available in postscript and pdf. There never was a journal version, but A theory of knowledge and ignorance for many agents does the multi-agent extension that we were hoping to do in the journal version.
Using Reasoning About Knowledge to Analyze Distributed Systems
Joseph Y. Halpern
An overview of work on using reasoning about knowledge to understand and analyze distributed systems.
In Annual Reviews of Computer Science, Vol. 2 (ed. J. F. Traub, B. J. Grosz, B. W. Lampson, and N. J. Nilsson), Annual Reviews Inc., 1987, pp. 37-68. A version is available in pdf.
I'm OK if you're OK: On the notion of trusting communication
We consider the issue of what an agent or a processor needs to know in order to know that its messages are true. This may be viewed as a first step to a general theory of cooperative communication in distributed systems. An honest message is one that is known to be true when it is sent (or said). If every message that is sent is honest, then of course every message that is sent is true. Various conditions weaker than honesty are investigated with the property that provided every message sent satisfies the condition, then every message sent is true.
In Philosophical Logic and Artificial Intelligence (ed. R. H. Thomason), Kluwer, 1989, pp. 9-34 and Journal of Philosophical Logic 17:4, 1988, pp. 329-354. A preliminary version appears in Proceedings of the Second IEEE Symposium on Logic in Computer Science, 1987, pp. 280-292.
Model checking vs. theorem proving: a manifesto
Joseph Y. Halpern and Moshe Y. Vardi
We argue that rather than representing an agent's knowledge as a collection of formulas, and then doing theorem proving to see if a given formula follows from an agent's knowledge base, it may be more useful to represent this knowledge by a semantic model, and then do model checking to see if the given formula is true in that model. We discuss how to construct a model that represents an agent's knowledge in a number of different contexts, and then consider how to approach the model-checking problem.
In Artificial Intelligence and Mathematical Theory of Computation (Papers in Honor of John McCarthy) (ed. V. Lifschitz), Academic Press, 1991, pp. 151-176. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version (which includes some material not in this book) appears in Principles of Knowledge Representation and Reasoning: Proceedings of the Second International Conference (J. A. Allen, R. Fikes, and E. Sandewall, eds.), 1991, pp. 325-334.
A new approach to updating beliefs
Ronald Fagin and Joseph Y. Halpern
We define a new notion of conditional belief, which plays the same role for Dempster-Shafer belief functions as conditional probability does for probability functions. Our definition is different from the standard definition given by Dempster, and avoids many of the well-known problems of that definition. Just as the conditional probability Pr(.|B) is a probability function which is the result of conditioning on B being true, so too our conditional belief function Bel(.|B) is a belief function which is the result of conditioning on B being true. We define the conditional belief as the lower envelope (that is, the inf) of a family of conditional probability functions, and provide a closed-form expression for it. An alternate way of understanding our definition of conditional belief is provided by considering ideas from an earlier paper, where we connect belief functions with inner measures. In particular, we show here how to extend the definition of conditional probability to nonmeasurable sets, in order to get notions of inner and outer conditional probabilities, which can be viewed as best approximations to the true conditional probability, given our lack of information. Our definition of conditional belief turns out to be an exact analogue of our definition of inner conditional probability.
In Uncertainty in Artificial Intelligence 6, (eds. P. P. Bonissone, M. Henrion, L. N. Kanal, and J. F. Lemmer), 1991, pp. 347-374. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the 6th Conference on Uncertainty in AI, 1990, pp. 317-325.
Reasoning about knowledge: a survey circa 1991
Joseph Y. Halpern
This is my second overview on knowledge. It's an update of the 1986 overview, and a predecessor of the 1995 survey.
Appears in both Encyclopedia of Computer Science and Technology, Vol. 27, Supplement 12 (ed. A. Kent and J. G. Williams), Marcel Dekker, 1993, pp. 275-296. and Encyclopedia of Microcumpters, Vol. 14 (ed. A. Kent and J. G. Williams), Marcel Dekker, 1994, pp. 287-308.
Reasoning about knowledge: a survey
Joseph Y. Halpern
In this survey, I attempt to identify and describe some of the common threads that tie together work in reasoning about knowledge in such diverse fields as philosophy, economics, linguistics, artificial intelligence, and theoretical computer science, with particular emphasis on work of the past five years, particularly in computer science.
In Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 4, D. Gabbay, C. J. Hogger, and J. A. Robinson, eds., Oxford University Press, 1995, pp. 1-34. A version of the paper similar to the published version is available in postscript and pdf. This is an update of two earlier surveys, one from 1986 and one from 1991. Of course, this material is all covered much more thoroughly in our book.
A logical approach to reasoning about uncertainty: a tutorial
Joseph Y. Halpern
I consider a logical framework for modeling uncertainty, based on the use of possible worlds, that incorporates knowledge, probability, and time. This turns out to be a powerful approach for modeling many problems of interest. I show how it can be used to give insights into (among other things) several well-known puzzles.
In Discourse, Interaction, and Communication, X. Arrazola, K. Korta, and F. J. Pelletier, eds., Kluwer, 1998, pp. 141-155. The paper is available postscript and pdf.
Axiomatic definitions of programming languages: a theoretical assessment
Albert R. Meyer and Joseph Y. Halpern
A precise definition is given of how partial correction or termination assertions serve to define the semantics of program schemes. Assertions involving only formulas of first-order predicate calculus are proved capable of defining program scheme semantics, and effective axiom systems for deriving such assertions are described. Such axiomatic definitions are possible despite the limited expressive power of predicate calculus.
In Journal of the ACM 29:2, April, 1982, pp. 555-576. A preliminary version appears Proceedings of 7th Annual ACM Symposium on Principles of Programming Languages, 1980, pp. 203-212. The journal paper also includes material from Joseph Y. Halpern and Albert R. Meyer, Axiomatic definitions of programming languages, II, Proceedings of 8th Annual ACM Symposium on Principles of Programming Languages, 1981, pp. 139-148.
Deterministic propositional dynamic logic: finite models, complexity, and completeness
Mordechai Ben-Ari, Joseph Y. Halpern, and Amir Pnueli
Let p be a formula in deterministic propositional dynamic logic. A decision procedure for the satisfiability of p is given along with a construction of a finite model for every satisfiable p. The decision procedure runs in deterministic exponential time and the size of the model are both exponential in the length of p. Finally, a complete axiomatization for deterministic propositional dynamic logic is given, based on the Segerberg axioms for propositional dynamic logic.
In Journal of Computer and Systems Science 25:3, 1982, pp. 402-417. A preliminary version with the title ``Finite models of deterministic propositional dynamic logic'', appears in Proceedings of the 8th International Colloquium on Automata, Languages, and Programming, 1981, pp. 249-263.
The propositional dynamic logic of deterministic, well-structured programs
Joseph Y. Halpern and John H. Reif
We consider a restricted propositional dynamic logic, Strict Deterministic Propositional Dynamic Logic (SDPDL), which is appropriate for reasoning about deterministic well-structured programs. In contrast to PDL, for which the validity problem is known to be complete in deterministic exponential time, the validity problem for SDPDL is shown to polynomial space complete. We also show that SDPDL is less expressive than PDL, and given a complete axiomatization for it. The results rely on structure theorems for models of satisfiable SDPDL formulas, and the proofs give insight into the effects of nondeterminism on intractability and expressiveness in program logics.
In Theoretical Computer Science 27, 1983, pp. 127-165. A preliminary version appears in Proceedings of the 22nd Annual Symposium on the Foundations of Computer Science, 1981, pp. 322-334.
Effective axiomatizations of Hoare Logics
Edmund M. Clarke, Joseph Y. Halpern, and Steven M. German
For a wide class of programming languages P and expressive interpretations I, it is shown that there exist sound and relatively complete Hoare logics for both partial correctness and termination assertions. In fact, under mild assumptions on P and I it is shown that the assertions true in I are uniformly decidable in the theory of I (Th(I)) iff the halting problem for P is decidable for finite interpretations. Moreover, the set of true terminations is uniformly recursively enumerable in Th(I) even if the halting problem for P is not decidable for finite interpretations. Since total-correctness assertions coincide with termination assertions for deterministic programming languages, this last result unexpectedly suggests that good axiom systems for total correctness may exist for a wider spectrum of languages than is the case for partial correctness.
In Journal of the ACM 30:3, 1983, pp. 612-637. A preliminary version appears in Proceeding of the 9th Annual ACM Symposium on Principles of Programming Languages, 1982, pp. 309-321.
Deterministic process logic is elementary
Joseph Y. Halpern
Process Logic (PL) is a language for reasoning about the behavior of a program during a computation, while Propositional Dynamic Logic (PDL) can only reason about the input-output states of a program. Nevertheless, we show that to each PL model M, there corresponds in a natural way a PDL model M' such that each path in M is represented by a state in M'. Moreover, to every PL formula p, there corresponds a PDL formula p', whose length is linear in that of p, such that p is true of a path in M iff p' is true of the state which represents that path in M'. We then show that p is satisfiable iff p' is satisfiable in a finite PDL model with special properties which we call a pseudomodel. The size of the pseudomodel is in general nonelementary but is bounded by both the depth of nesting of the suf operator and the alternation of the suf and diamond operators. However, for DPL, a deterministic version of PL, the pseudomodel has exponential size, giving us a deterministic exponential time procedure for deciding DPL validity. These results suggest that it is the interaction between nondeterministic programs and the suf operator that makes the general decision problem for PL so difficult.
In Information and Control 57:1, 1983, pp. 56-89. A preliminary version appears in Proceedings of 23rd Annual Symposium on the Foundations of Computer Science, 1982, pp. 204-216.
Decision procedures and expressiveness in the temporal logic of branching time
E. Allen Emerson and Joseph Y. Halpern
We consider the computation tree logic (CTL) proposed by Emerson and Clarke, which extends the unified time logic (UB) of Ben-Ari, Manna, and Pnueli by adding an until operator. It is established that CTL has the small model property by showing that any satisfiable CTL formula is satisfiable in a small finite model obtained from the small ``pseudomodel'' resulting from the Fischer-Ladner quotient construction. Then an exponential-time algorithm is given for deciding satisfiability in CTL, and the axiomatization of UB given by Ben-Ari, Manna, and Pnueli is extended to a complete axiomatization for CTL. Finally, the relative expressive power of a family of temporal logics obtained by extending or restricting the syntax of UB and CTL is studied.
In Journal of Computer and Systems Science 30:1, 1985, pp. 1-24; available in pdf. A preliminary version appears in Proceedings of the 14th ACM Symposium on Theory of Computing, 1982, pp. 169-180.
Optimal precision in the presence of uncertainty
Joseph Y. Halpern, Nimrod Megiddo, and Ashfaq Munshi
We consider the problem of achieving coordinated actions in a real-time distributed system. In particular, we consider how closely (in terms of real time) processors can be guaranteed to perform a particular action, in a system where message transmission is guaranteed, but there is some uncertainty in message transmission time. We present an algorithm to achieve optimal precision in arbitrary networks. In networks where clocks run at the rate of real time, the optimal precision achievable in a network is exactly how tightly clocks can be guaranteed to be synchronized.
In Journal of Complexity 1, 1985, pp. 170-196. A preliminary version appears in Proceedings of 17th ACM Symposium on the Theory of Computing, 1985, pp. 346-355.
Equations between regular terms and an application to process logic
Ashok K. Chandra, Joseph Y. Halpern, Albert R. Meyer, and Rohit Parikh
Regular terms with the Kleene operations union, concatenation, and * can be thought of as operators on languages, generating other languages. An equation T1 = T2 between two such terms is said to be satisfiable just in case languages exist which make this equation true. We show that the satisfiability problem even for *-free regular terms is undecidable. Similar techniques are used to show that a very natural extension of the Process Logic of Harel, Kozen, and Parikh is undecidable.
In SIAM J. Computing 14:4, 1985, pp. 935-942. A preliminary version appears in Proceedings of 13th ACM Symposium on Theory of Computing, 1981, pp. 384-390.
``Sometimes'' and ``not never'' revisited: on branching vs. linear time
E. Allen Emerson and Joseph Y. Halpern
The differences between and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs is studied. These issues have been previously considered by Lamport. To facilitate a careful examination of these issues, a language, CTL*, in which a universal or existential or existential path quantifier can prefix an arbitrary linear time assertion, is defined. The expressive power of a number of sublanguages is then compared. CTL* is also related to the logics MPL of Abrahamson and PL of Harel, Kozen, and Parikh. The paper concludes with a comparison of the utility of branching and linear time temporal logics.
In Journal of the ACM 33:1, 1986, pp. 151-178 on branching vs. linear time, Proceedings of the 10th Annual ACM Symposium on Principles of Programming Languages, 1983, pp. 127-140.
Joseph Y. Halpern, Michael C. Loui, Albert R. Meyer, and Daniel Weise
Paul and Reischuk devised space efficient simulations of logarithmic cost random access machines and multidimensional Turing machines. We simplify their general space reduction technique and extend it to other computational models, including pointer machines, which model computations on graphs and data structures. Every pointer machine of time complexity T(n) can be simulated by a pointer machine of space complexity O(T(n)/log T(n)).
In Math. Systems Theory 19, 1986, pp. 13-28.
On the possibility and impossibility of achieving clock synchronization
Danny Dolev, Joseph Y. Halpern, and H. Raymod Strong
It is known that clock synchronization can be achieved in the presence of faulty processors as long as the nonfaulty processors are connected, provided that some authentication technique is used. Without authentication the number of faults that can be tolerated has been an open question. Here we show that if we restrict logical clocks to running within some linear function of real time, then clock synchronization is impossible, without authentication, when one-third or more of the processors are faulty. However, if there is a bound on the rate at which a processor can generate messages, then we show that clock synchronization is achievable, without authentication, as long as the faults do not disconnect the network. Finally, we provide a lower bound on the closeness to which simultaneity can be achieved in the network as a function of the transmission and processing delay properties of the network.
In Journal of Computer and Systems Science 32:2, 1986, pp. 230-250. A preliminary version appears in Proceedings of the 16th ACM Symposium on the Theory of Computing, 1984, pp. 504-511.
Cheating husbands and other stories: a case study in knowledge, action, and communication
Y. O. Moses, Danny Dolev, and Joseph Y. Halpern
The relationship between knowledge and action is a fundamental one: a processor in a computer network (or a robot or a person, for that matter) should base its actions on the knowledge (or information) it has. One of the main uses of communication is passing around information that may eventually be required by the receiver in order to decide upon subsequent actions. Understanding the relationship between knowledge, action, and communication is fundamental to the design of computer network protocols, intelligent robots, etc. By looking at a number of variants of the cheating husbands puzzle, we illustrate the subtle relationship between knowledge, communication, and action in a distributed environment.
In Distributed Computing 1:3, 1986, pp. 167-176. A preliminary version appears in Proceedings of the 4th ACM Symposium on Principles of Distributed Computing, 1985, pp. 215-223.
Taken by surprise: the paradox of the surprise test revisited
Joseph Y. Halpern and Yoram Moses.
We reexamine the surprise test paradox (also called the hangman paradox) and translate it into a formal logic with a fixed-point operator and a provability operator. We consider four possible translations of the paradox. The first is contradictory, the second is consistent with the test being given any day of the week including the last, the third rules out the last day (but no others), while the fourth does not even admit of a reasonable semantic interpretation, and is paradoxical in that it is consistent if and only if it is inconsistent!
In Journal of Philosophical Logic 15:3, 1986, pp. 281-304. Available in pdf.
A new look at fault-tolerant network routing
Danny Dolev, Joseph Y. Halpern, Barbara B. Simons, and H. Raymond Strong
We model a communication network as a graph in which a processor is a node and a communication link is an edge. A routing for such a network is a fixed path, or route, between each pair of nodes. Given a network with a predefined routing, we study the effects of faulty components on the routing. Of particular interest is the number of routes along which a message must travel between any two non-faulty nodes. This problem is analyzed for specific families of graphs and for classes of routings. We also give some bounds for general versions of the problem. Finally, we conclude with one of the most important contributions of this paper, a list of interesting and apparently difficult open problems.
In Information and Computation 72:3, 1987, pp. 180-196. A preliminary version appears in Proceedings of the 16th ACM Symposium on the Theory of Computing, 1984, pp. 526-535.
A logic to reason about likelihood
Joseph Y. Halpern and Michael O. Rabin
We present a logic LL which uses a modal operator L to help capture the notion of likely. Despite the fact that no use is made of numbers, LL can capture many of the properties of likelihood in an intuitively appealing way. Using standard techniques of modal logic, we give a complete axiomatization for LL and show that satisfiability of LL formulas can be decided in exponential time. We discuss how the logic might be used in areas where decision making is crucial, such as management and medical diagnosis, and conclude by using LL to give a formal proof of correctness of a protocol for exchanging secrets.
In Artificial Intelligence 32:3, 1987, pp. 379-405; a version is available in pdf. A preliminary version appears in Proceedings of the 15th ACM Symposium on the Theory of Computing, 1983, pp. 310-319. See also Likelihood, probability, and knowledge.
Belief, awareness, and limited reasoning
Ronald Fagin and Joseph Y. Halpern
Several new logics for belief and knowledge are introduced and studied, all of which have the property that agents are not logically omniscient. In particular, in these logics, the set of beliefs of an agent does not necessarily contain all valid formulas. Thus, these logics are more suitable than traditional logics for modeling beliefs of humans (or machines) with limited reasoning capabilities. Our first logic is essentially an extension of Levesque's logic of implicit and explicit belief, where we extend to allow multiple agents and higher-level belief (i.e., beliefs about beliefs). Our second logic deals explicitly with ``awareness'', where, roughly speaking, it is necessary to be aware of a concept before one can have beliefs about it. Our third logic gives a model of ``local reasoning'', where an agent is viewed as a ``society of minds'', each with its own cluster of beliefs, which may contradict each other.
In Artificial Intelligence 34, 1988, pp. 39-76. A preliminary version appears in Proceedings of the 9th International Joint Conference on Artificial Intelligence (IJCAI 85), 1985, pp. 491-501.
The complexity of reasoning about knowledge and time, I: lower bounds
Joseph Y. Halpern and Moshe Y. Vardi
We study the propositional modal logic of knowledge and time for
distributed systems. We consider a number of logics (ninety-six in
all!), which vary according to the choice of language and the
assumptions made on the underlying system. The major
parameters in the language are whether there is a common knowledge
operator, whether we reason about the knowledge of one or more than
one processor, and whether our temporal operators are branching or linear.
The assumptions on distributed systems that we consider are:
whether or not processors forget, whether or not processors learn,
whether or not time is synchronous, and whether or not there is
a unique initial state in the system.
We completely characterize the complexity of the validity problem
for all the logics we consider. This paper focuses on lower bounds;
a sequel will deal with the corresponding upper bounds. Typical results
include a
-completeness
result for the language with
common knowledge with respect to systems where processors do not forget,
and a corresponding non-elementary-time result for the language
without common knowledge. It is shown that, in general, the assumption
that processors do not forget or do not learn greatly increases
the complexity of reasoning about knowledge and time.
In Journal of Computer and Systems Science 38:1, 1989, pp. 195-237. Preliminary versions of some of the material in this paper can be found in ``The complexity of reasoning about knowledge and time'', Proceedings of 18th ACM Symposium on the Theory of Computing, 1986, pp. 304-314 and ``Reasoning about knowledge and time in asynchronous systems'', oceedings of the 20th ACM Symposium on Theory of Computing, 1988, pp. 53-65. We hope to bring out part II on lower bounds in the reasonably near future.
Likelihood, probability, and knowledge
Joseph Y. Halpern and David A. McAllester
The modal logic LL was introduced by Halpern and Rabin as a means of doing qualitative reasoning about likelihood. Here the relationship between LL and probability theory is examined. It is shown that there is a way of translating probability assertions into LL in a sound manner, so that LL in some sense can capture the probabilistic interpretation of likelihood. However, the translation is subtle; several more obvious attempts are shown to lead to inconsistencies. We also extend LL by adding modal operators for knowledge. This allows us to reason about the interaction between knowledge and likelihood. The propositional version of the resulting logic LLK is shown to have a complete axiomatization and to be decidable in exponential time, provably the best possible.
In Computational Intelligence, 5, pp. 151-160, 1989; a version is available in pdf. A preliminary version appears in AAAI-84 (Proceedings of the Second National Conference on Artificial Intelligence, 1984, pp. 137-141.
Reasoning about procedures as parameters in the language L4
Steven M. German, Edmund M. Clarke, and Joseph Y. Halpern
We provide a sound and relatively complete axiom system for partial correctness assertions in an Algol-like language with procedures passed as parameters, but with no global values (known traditionally as L4). The axiom system allows us to reason syntactically about programs and to construct proofs for assertions about complicated programs from proofs of assertions about their components. Such an axiom system has been sought by a number of researchers, but no previously published solution has been entirely satisfactory. Our axiom system extends the natural style of reasoning used in previous Hoare systems to programs with procedures of higher type. The details of the proof that our axiom system is relatively complete in the sense of Cook may be of independent interest, because we introduce results about expressiveness for programs with higher types that are useful beyond the immediate problem of the language L4. We also prove a new incompleteness result that applies to our logic and to similar Hoare logics.
In Information and Computation, 83:3, 1989, pp. 265-359 (the whole volume). Some material in this paper appeared in preliminary form in ``True relative completeness of an axiom system for L4'', Proceedings of the IEEE Symposium on Logic in Computer Science, 1986, pp. 11-25 and ``Reasoning about procedures with parameters'' Proceedings of the CMU Logics of Programs Conference, Lecture Notes in Computer Science, 1983, pp. 206-220.
Modelling knowledge and action in distributed systems
Joseph Y. Halpern and Ronald Fagin
We present a formal model that captures the subtle interaction between knowledge and action in distributed systems. We view a distributed system as a set of runs, where a run is a function from time to global states and a global state is a tuple consisting of an environment state and a local state for each process in the system. This model is a generalization of those used in many previous papers. Actions in this model are associated with functions from global states to global states. A protocol is a function from local states to actions. We extend the standard notion of a protocol by defining knowledge-based protocols, ones in which a process' actions may depend explicitly on its knowledge. Knowledge-based protocols provide a natural way of describing how actions should take place in a distributed system. Finally, we show how the notion of one protocol implementing another can be captured in our model.
In Distributed Computing, 3:4, 1989, pp. 159-177. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of Concurrency-88, 1988, pp. 18-32; some material also appears in ``A formal model of knowledge, action, and communication in distributed systems'', Proceedings of the 4th ACM Symposium on Principles of Distributed Computing, 1985, pp. 224-236.
Completeness of rewrite rules and rewrite strategies for FP
Joseph Y. Halpern, John H. Williams and Edward L. Wimmers
We consider languages whose operational semantics is given by a set of rewrite rules. For such languages, it is important to be able to determine that there are enough rules to be able to compute the correct meaning of all expressions, but not so many that the system of rules is inconsistent. We develop a formal framework in which to give a precise treatment of these completeness and soundness issues, and then investigate them in the context of an extended version of the functional programming language FP. We show that the rewrite rules of FP are sound and complete with respect to three different notions of completeness. In the latter half of the paper we turn our attention to rewrite strategies. In order to implement a language based on rewrite rules, it does not suffice to know that there are ``enough'' rules in the language; we also need to have a good strategy for determining the order in which to apply them. But what is ``good''? Corresponding to each of our notions of completeness there is a notion of a good rewrite strategy. We examine and characterize these notions of goodness, and give examples of a number of natural good strategies. Although we have confined ourselves to FP here, we believe that our techniques (some of which are nontrivial extensions of techniques first used in the context of lambda-calculus) will apply well beyond the realm of FP rewriting systems.
In Journal of the ACM, 37:1, 1990, pp. 86-143. Some material in this paper appeared in preliminary form in ``Denotational semantics and rewrite rules for FP'', Joseph Y. Halpern, John H. Williams, Edward L. Wimmers, and Timothy C. Winkler, Proceedings of the 12th Annual ACM Symposium on Principles of Programming Languages, 1985, pp. 108-120 and ``Good rewriting strategies for FP'', Joseph Y. Halpern, John H. Williams, and Edward L. Wimmers, Proceedings of the IEEE Symposium on Logic in Computer Science, 1986, pp. 149-162.
Knowledge and common knowledge in a distributed environment
Joseph Y. Halpern and Yoram Moses
Reasoning about knowledge seems to play a fundamental role in distributed systems. Indeed, such reasoning is a central part of the informal intuitive arguments used in the design of distributed protocols. Communication in a distributed system can be viewed as the act of transforming the system's state of knowledge. This paper presents a general framework for formalizing and reasoning about knowledge in distributed systems. We argue that states of knowledge of groups of processors are useful concepts for the design and analysis of distributed protocols. In particular, distributed knowledge corresponds to knowledge that is ``distributed'' among the members of the group, while common knowledge corresponds to a fact being ``publicly known''. The relationship between common knowledge and a variety of desirable actions in a distributed system is illustrated. Furthermore, it is shown that, formally speaking, in practical systems common knowledge cannot be attained. A number of weaker variants of common knowledge that are attainable in many cases of interest are introduced and investigated.
In Journal of the ACM, 37:3, 1990, pp. 549-587. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the 3rd ACM Symposium on Principles of Distributed Computing, 1984, pp. 50-61.
A logic for reasoning about probabilities
Ronald Fagin, Joseph Y. Halpern, and Nimrod Megiddo
We consider a language for reasoning about probability which allows us to make statements such as ``the probability of E is less than 1/3'' and ``the probability of E is at least twice the probability of F'', where E and F are arbitrary events. We consider the case where all events are measurable (i.e., represent measurable sets) and the more general case, which is also of interest in practice, where they may not be measurable. The measurable case is essentially a formalization of (the propositional fragment of) Nilsson's probabilistic logic. As we show in a companion paper, the general (nonmeasurable) case corresponds precisely to replacing probability measures by Dempster-Shafer belief functions. In both cases, we provide a complete axiomatization and show that the problem of deciding satisfiability is NP-complete, no worse than that of propositional logic. As a tool for proving our complete axiomatizations, we give a complete axiomatization for reasoning about Boolean combinations of linear inequalities, which is of independent interest. This proof and others make crucial use of results from the theory of linear programming. We then extend the language to allow reasoning about conditional probability, and show that the resulting logic is decidable and completely axiomatizable, by making use of the theory of real closed fields.
In Information and Computation, 87:1,2, 1990, pp. 78-128. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the 3rd IEEE Conference on Logic in Computer Science, 1988, pp. 410-421.
An analysis of first-order logics of probability
Joseph Y. Halpern
We consider two approaches to giving semantics to first-order logics of probability. The first approach puts a probability on the domain, and is appropriate for giving semantics to formulas involving statistical information such as ``The probability that a randomly chosen bird flies is greater than .9.'' The second approach puts a probability on possible worlds, and is appropriate for giving semantics to formulas describing degrees of belief, such as ``The probability that Tweety (a particular bird) flies is greater than .9.'' We show that the two approaches can be easily combined, allowing us to reason in a straightforward way about statistical information and degrees of belief. We then consider axiomatizing these logics. In general, it can be shown that no complete axiomatization is possible. We provide axiom systems that are sound and complete in cases where a complete axiomatization is possible, showing that they do allow us to capture a great deal of interesting reasoning about probability.
In Artificial Intelligence 46, 1990, pp. 311-350. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the 11th International Joint Conference on Artificial Intelligence (IJCAI 89), 1989, pp. 1375-1381.
Let many flowers bloom: a response to ``An inquiry into computer understanding''
Joseph Y. Halpern Two main issues are addressed in this response to Peter Cheeseman's ``An inquiry into computer understanding'' and ``In defense of `An inquiry into computer understanding' '': (1) the ``right'' approach to reasoning about uncertainty and (2) the relationship between logic and probability.
In Computational Intelligence 6, 1990, pp. 184-188. A version of the paper similar to the published version is available in postscript and pdf.
Presburger arithmetic with unary predicates is
complete
Joseph Y. Halpern
We give a simple proof characterizing the complexity of Presburger
arithmetic augmented with additional predicates. We show that
Presburger arithmetic with additional predicates
is complete. Addinge unary predicate is enough to
get
hardness, while adding more predicates (of any arity)
does not make the complexity any worse.
In Journal of Symbolic Logic, 56:2, 1991, pp. 637-642. A version of the paper similar to the published version is available in postscript and pdf.
The relationship between knowledge, belief, and certainty
Joseph Y. Halpern
We consider the relation between knowledge and certainty, where a fact is known if it is true at all worlds an agent considers possible and is certain if it holds with probability 1. We identify certainty with belief, interpreted probabilistically. We show that if we assume one fixed probability assignment, then the logic KD45, which has been identified as perhaps the most appropriate for belief, provides a complete axiomatization for reasoning about certainty. Just as an agent may believe a fact p although p is false, he may be certain that a fact p is true although p is false. However, it is easy to see that an agent can have such false (probabilistic) beliefs only at a set of worlds of probability 0. If we restrict attention to structures where all worlds have positive probability, then S5 provides a complete axiomatization. If we consider a more general setting, where there might be a different probability assignment at each world, then by placing appropriate conditions on the support of the probability function (the set of worlds which have non-zero probability), we can capture many other well-known modal logics, such as T and S4. Finally, we consider Miller's principle, a well-known principle relating higher-order probabilities to lower-order probabilities, and show that in a precise sense KD45 characterizes certainty in those structures satisfying Miller's principle.
In Annals of Mathematics and Artificial Intelligence 4, 1991, pp. 301-322. A version of the paper similar to the published paper is available in postscript and pdf. There is a bug in the published version; a correction is available in postscript and pdf, and appears in Annals of Mathematics and Artificial Intelligence 26, 1999, pp. 253--256. A preliminary version appears in Proceedings of the 5th Workshop on Uncertainty in AI, 1989, pp. 142-151.
A model-theoretic analysis of knowledge
Ronald Fagin, Joseph Y. Halpern, and Moshe Y. Vardi
Understanding knowledge is a fundamental issue in many disciplines. In computer science, knowledge arises not only in the obvious contexts (such as knowledge-based systems), but also in distributed systems (where the goal is to have each processor ``know'' something, as in agreement protocols). A general semantic model of knowledge is introduced, to allow reasoning about statements such as ``He knows that I know whether or not she knows whether or not it is raining.'' This approach more naturally models a state of knowledge than previous proposals (including Kripke structures). Using this notion of model, a model theory for knowledge is developed. This theory enables one to interpret the notion of a ``finite amount of information''.
In Journal of the ACM, 38:2, 1991, pp. 382-428. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the 25th Annual Conference on Foundations of Computer Science, 1984, pp. 268-278.
A propositional modal interval logic
Joseph Y. Halpern and Yoav Shoham
In certain areas of artificial intelligence there is need to
represent continuous change and to make
statements that are interpreted with respect to time intervals rather
than time points. To this end we
develop a modal temporal logic based on time intervals, a logic which
can be viewed as a
generalization of point-based modal temporal logic.
We discuss related logics, give
an intuitive presentation of the new logic, and define its formal syntax
and semantics.
We make no assumption about the underlying nature of time, allowing it to be
discrete (such as the natural numbers) or continuous (such as the rationals or the reals),
linear or branching, complete (such as the reals) or not (such as the
rationals). We show, however, that there are formulas in the logic that
allow us to distinguish all these situations.
We also give a translation of our logic into first-order logic, which
allows us to apply some results on first-order logic to our modal one.
Finally, we consider the difficulty of validity
problems for the logic. This turns out to depend critically, and in surprising ways,
on our assumptions about time. For example, if we take our underlying temporal
structure to be the rationals, we can show that the validity problem is r.e.-complete,
if it is the reals then we can show that validity is
-hard, and if it
is the natural numbers,
then validity is
-complete.
In Journal of the ACM, 38:4, 1991, pp. 935-962. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the IEEE Symposium on Logic in Computer Science, 1986, pp. 279-292.
Clock synchronization and the power of broadcasting
Joseph Y. Halpern and Ichiro Suzuki
We investigate the power of a broadcast mechanism in a distributed network. We do so by considering the problem of synchronizing clocks in an error-free network, under the assumption that there is no upper bound on message transmission time, but that broadcast messages are guaranteed to be received within an interval of size d, for some fixed constant d. This is intended to be an idealization of what happens in multiple access networks, such as the Ethernet. We then consider tradeoffs between the type and number of broadcasts, and the tightness of synchronization. Our results include (1) matching upper and lower bounds of (1 + 1/K)d on the precision of clock synchronization attainable for processes using K (n-1)-casts, for K between 3 and n, (2) matching upper and lower bounds of (1 + 1/n)d on the precision of clock synchronization attainable for n > 2 processes using an arbitrary number of (n-1)-casts, and (3) matching upper and lower bounds of (1 + (n-2)/n)d on the precision attainable using 2-casting.
In Distributed Computing 5:2, 1991, pp. 73-83. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the 28th Annual Allerton Conference on Communication, Control, and Computing, 1990, pp. 588-597.
Uncertainty, belief, and probability
Ronald Fagin and Joseph Y. Halpern
We introduce a new probabilistic approach to dealing with uncertainty, based on the observation that probability theory does not require that every event be assigned a probability. For a nonmeasurable event (one to which we do not assign a probability), we can talk about only the inner measure and outer measure of the event. In addition to removing the requirement that every event be assigned a probability, our approach circumvents other criticisms of probability-based approaches to uncertainty. For example, the measure of belief in an event turns out to be represented by an interval (defined by the inner and outer measure), rather than by a single number. Further, this approach allows us to assign a belief (inner measure) to an event without committing to a belief about its negation (since the inner measure of an event plus the inner measure of its negation is not necessarily one). Interestingly enough, inner measures induced by probability measures turn out to correspond in a precise sense to Dempster-Shafer belief functions. Hence, in addition to providing promising new conceptual tools for dealing with uncertainty, our approach shows that a key part of the important Dempster-Shafer theory of evidence is firmly rooted in classical probability theory.
In Computational Intelligence 7, 1991, pp. 160-173. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the 11th International Joint Conference on Artificial Intelligence (IJCAI 89), 1989, pp. 1161-1167.
What can machines know? On the properties of knowledge in distributed systems
Ronald Fagin, Joseph Y. Halpern, and Moshe Y. Vardi
It has been argued that knowledge is a useful tool for designing and analyzing complex systems. The notion of knowledge that seems most relevant in this context is an external, information-based notion that can be shown to satisfy all the axioms of the modal logic S5. We carefully examine the properties of this notion of knowledge and show that they depend crucially, and in subtle ways, on assumptions we make about the system and about the language used for describing knowledge. We present a formal model in which we can capture various assumptions frequently made about systems, such as whether they are deterministic or nondeterministic, whether knowledge is cumulative (which means that processes never ``forget''), and whether or not the ``environment'' affects the state transitions of the processes. We then show that under some assumptions about the system and the language, certain states of knowledge are not attainable and the axioms of S5 do not completely characterize the properties of knowledge; extra axioms are needed. We provide complete axiomatizations for knowledge in a number of cases of interest.
In Journal of the ACM, 39:2, 1992, pp. 328-376. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears with the title ``What can machines know? On the epistemic properties of machines'' appears in AAAI-86 (Proceedings of Fourth National Conference on Artificial Intelligence, 1986, pp. 428-434.
Two views of belief: belief as generalized probability and belief as evidence
Joseph Y. Halpern and Ronald Fagin
Belief functions are mathematical objects defined to satisfy three axioms that look somewhat similar to the Kolmogorov axioms defining probability functions. We argue that there are (at least) two useful and quite different ways of understanding belief functions. The first is as a generalized probability function (which technically corresponds to the inner measure induced by a probability function). The second is as a way of representing evidence. Evidence, in turn, can be understood as a mapping from probability functions to probability functions. It makes sense to think of updating a belief if we think of it as a generalized probability. On the other hand, it makes sense to combine two beliefs (using, say, Dempster's rule of combination) only if we think of the belief functions as representing evidence. Many previous papers have pointed out problems with the belief function approach; the claim of this paper is that these problems can be explained as a consequence of confounding these two views of belief functions.
In Artificial Intelligence 54, 1992, pp. 275-317. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in AAAI-90 (Proceedings of the Eighth National Conference on Artificial Intelligence, 1990, pp. 112-119.
A guide to completeness and complexity for modal logics of knowledge and belief
Joseph Y. Halpern and Yoram Moses
We review and re-examine possible-worlds semantics for propositional logics of knowledge and belief with three particular points of emphasis: (1) we show how general techniques for finding decision procedures and complete axiomatizations apply to models for knowledge and belief, (2) we show how sensitive the difficulty of the decision procedure is to such issues as the choice of modal operators and the axiom system, and (3) we discuss how notions of common knowledge and distributed knowledge among a group of agents fit into the possible-worlds framework, As far as complexity is concerned, we show, among other results, that while the problem of deciding satisfiability of an S5 formula with one agent is NP-complete, the problem for many agents is PSPACE-complete. Adding a distributed knowledge operator does not change the complexity, but once a common knowledge operator is added to the language, the problem becomes complete for exponential time.
In Artificial Intelligence 54, 1992, pp. 319-379. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version, with the title ``A guide to the modal logics of knowledge and belief'' appears in Proceedings of the 9th International Joint Conference on Artificial Intelligence (IJCAI 85), 1985, pp. 480-490.
Joseph Y. Halpern and Lenore D. Zuck
We use a high-level, knowledge-based approach for deriving a family of protocols for the sequence transmission problem. The protocols of Aho, Ullman, and Yannakakis, the Alternating Bit protocol, and Stenning's protocol are all instances of one knowledge-based protocol that we derive. Our derivation leads to transparent and uniform correctness proofs for all these protocols.
In Journal of the ACM, 39:3, 1992, pp. 449-478. A version of the paper similar to the published version is available in postscript and pdf. of the paper similar to the published version. A preliminary version appears in Proceedings of the 6th ACM Symposium on Principles of Distributed Computing, 1987, pp. 269-280.
Ronald Fagin, Joseph Y. Halpern, and Moshe Y. Vardi
What is an inference rule? This question does not have a unique answer. One usually finds two distinct standard answers in the literature: validity inference (we can infer q from p if, for every substitution T, the validity of T[p] entails the validity of T[q]) and truth inference (we can infer q from p if, for every substitution T, the truth of T[p] entails the truth of T[q]). In this paper we introduce a general semantic framework that allows us to investigate the notion of inference more carefully. Validity inference and truth inference are in some sense the extremal points in our framework. We investigate the relationship between various types of inference in our general framework, and consider the complexity of deciding if an inference rule is sound, in the context of a number of logics of interest: classical propositional logic, a nonstandard propositional logic, various propositional modal logics, and first-order logic.
In Journal of Symbolic Logic 57:3, 1992, pp. 1018-1045. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the 5th Jerusalem Conference on Information Technology, 1990, pp. 391-401.
Message-optimal protocols for Byzantine agreement
Vassos Hadzilacos and Joseph Y. Halpern
It is often important for the correct processes in a distributed system to reach agreement, despite the presence of some faulty processes. Byzantine agreement (BA) is a paradigm problem that attempts to isolate the key features of reaching agreement. We focus here on the number of messages required to reach BA, with particular emphasis on the number of messages required in the failure-free runs, since these are the ones that occur most often in practice. The number of messages required is sensitive to the types of failures considered. In earlier work, Amdur et al. [1990] established tight upper and lower bounds on the worst- and average-case number of messages required in failure-free runs for crash failures. We provide tight upper and lower bounds for all remaining types of failures that have been considered in the literature on the BA problem: receiving omission, sending omission and general omission failures, as well as arbitrary failures with or without message authentication. We also establish a tradeoff between number of rounds and number of messages in the failure-free runs required to reach agreement in the case of crash, sending and general omission failures.
In Mathematical Systems Theory 26, 1993, pp. 41-102. A version of the paper similar to the published version is available in postscript and pdf. of the paper similar to the published version. A preliminary version of this paper appears in Proceedings of the 10th ACM Symposium on Principles of Distributed Computing, 1991, pp. 309-323.
Vassos Hadzilacos and Joseph Y. Halpern
We define a simple variant of the Byzantine agreement (BA) problem, called the Failure Discovery (FD) problem that, roughly speaking, amounts to reaching Byzantine Agreement provided that no failures are discovered. We show how a protocol for FD can be extended to one for BA, with no message overhead in the failure-free runs. We also show that, for so-called benign failures, if the FD protocol satisfies an additional property, the message-preserving extension to a BA protocol can be accomplished with minimal time overhead in the failure-free runs. Our results show that FD is a useful building block for BA; indeed, it it has been used in this way in a companion paper.
In Mathematical Systems Theory 26, 1993, pp. 103-129. A version of the paper similar to the published version is available in postscript and pdf.
Knowledge, probability, and adversaries
Joseph Y. Halpern and Mark Tuttle
What should it mean for an agent to know or believe an assertion is true with probability .99? Different papers give different answers, choosing to use quite different probability spaces when computing the probability that an agent assigns to an event. We show that each choice can be understood in terms of a betting game. This betting game itself can be understood in terms of three types of adversaries influencing three different aspects of the game. The first selects the outcome of all nondeterministic choices in the system; the second represents the knowledge of the agent's opponent in the betting game (this is the key place the papers mentioned above differ); the third is needed in asynchronous systems to choose the time the bet is placed. We illustrate the need for considering all three types of adversaries with a number of examples. Given a class of adversaries, we show how to assign probability spaces to agents in a way most appropriate for that class, where ``most appropriate'' is made precise in terms of this betting game. We conclude by showing how different assignments of probability spaces (corresponding to different opponents) yield different levels of guarantees in probabilistic coordinated attack.
In Journal of the ACM, 40:4, 1993, pp. 917-962. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the 8th ACM Symposium on Principles of Distributed Computing, 1989, pp. 103-118.
Naming and identity in epistemic logics, I: The propositional case
Adam J.Grove and Joseph Y. Halpern
Modal epistemic logics for many agents often assume a fixed one-to-one correspondence between agents and the names for agents that occur in the language. This assumption restricts the applicability of any logic because it prohibits, for instance, anonymous agents, agents with many names, named groups of agents, and relative (indexical) reference. Here we examine the principles involved in such cases, and give simple propositional logics that are expressive enough to cope with them all.
In Journal of Logic and Computation, 3:4, 1993, pp. 345-378. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version under the title ``Naming and identity in a multi-agent epistemic logic'' appears in Principles of Knowledge Representation and Reasoning: Proceedings of the Second International Conference (J. A. Allen, R. Fikes, and E. Sandewall, eds.), 1991, pp. 301-312. This preliminary version also contains material from Part II of the paper of which Adam Grove is the sole author; Part II appears in Artificial Intelligence 74, 1995, pp. 311-350.
A response to ``Believing on the basis of evidence''
Fahiem Bacchus, Adam J.Grove, Joseph Y. Halpern, and Daphne Koller
This is part of a special issue of Computational Intelligence devoted to ``Believing on the basis of evidence'', a paper by Henry Kyburg, and responses to it. Kyburg addresses the issue of how we can use our information to reason to a set of conclusions that are plausible but not certain. This set of conclusions goes beyond the set of deductive conclusions. His program is certainly ambitious and the approach he suggests meets with varying degrees of success and failure when it comes to particular issues. We examine and critique a few parts of his approach.
In Computational Intelligence, 10:1, 1994, pp. 21-25 A version of the paper similar to the published version is available in postscript and pdf.
Reasoning about knowledge and probability
Ronald Fagin and Joseph Y. Halpern
We provide a model for reasoning about knowledge and probability together. We allow explicit mention of probabilities in formulas, so that our language has formulas that essentially say ``according to agent i, formula p holds with probability at least a.'' The language is powerful enough to allow reasoning about higher-order probabilities, as well as allowing explicit comparisons of the probabilities an agent places on distinct events. We present a general framework for interpreting such formulas, and consider various properties that might hold of the interrelationship between agents' probability assignments at different states. We provide a complete axiomatization for reasoning about knowledge and probability, prove a small model property, and obtain decision procedures. We then consider the effects of adding common knowledge and a probabilistic variant of common knowledge to the language.
In Journal of the ACM, 41:2, 1994, pp. 340-367. A minor corrigendum appears in Journal of the ACM, 45:1, 1998, p. 214. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the Second Conference on Theoretical Aspects of Reasoning About Knowledge, 1988, pp. 277-294.
Decidability and expressiveness for first-order logics of probability
Martin Abadi and Joseph Y. Halpern
We consider decidability and expressiveness issues for
two first-order logics of probability.
In one, the probability is on possible worlds,
while in the other, it is on the domain. It turns out that in both
cases it takes very little to make reasoning about
probability highly undecidable.
We show that when the
probability is on the domain, if the language contains
only unary predicates then the validity problem is decidable.
However, if the language contains even one binary predicate, the
validity problem is -complete,
as hard as elementary analysis
with free predicate and function symbols.
With equality in the language, even with no other symbol,
the validity problem is at least as hard as that for
elementary analysis,
-hard.
Thus, the logic cannot be axiomatized in either case.
When we put the probability on the
set of possible worlds,
the validity problem is
-complete with as little as
one unary predicate in the language, even without equality.
With equality, we get
-hardness with only a constant symbol.
We then turn our attention to an analysis of what causes this overwhelming
complexity. For example, we show that if we require rational probabilities
then we drop from
to
In many contexts
it suffices to restrict attention
to domains of bounded size; fortunately, the logics are decidable
in this case.
Finally, we show that, although the two
logics capture quite different intuitions about probability,
there is a precise sense in which they are equi-expressive.
In Information and Computation, 112:1, 1994, pp. 1-36. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the 30th Annual Conference on Foundations of Computer Science, 1989, pp. 148-153.
Random worlds and maximum entropy
Adam J.Grove, Joseph Y. Halpern, and Daphne Koller
Given a knowledge base KB containing first-order and statistical facts, we consider a principled method, called the random-worlds method, for computing a degree of belief that some formula p holds given KB. If we are reasoning about a world or system consisting of N individuals, then we can consider all possible worlds, or first-order models, with domain 1,...,N that satisfy KB, and compute the fraction of them in which p is true. We define the degree of belief to be the asymptotic value of this fraction as N grows large. We show that when the vocabulary underlying p and KB uses constants and unary predicates only, we can naturally associate an entropy with each world. As N grows larger, there are many more worlds with higher entropy. Therefore, we can use a maximum-entropy computation to compute the degree of belief. This result is in a similar spirit to previous work in physics and artificial intelligence, but is far more general. Of equal interest to the result itself are the limitations on its scope. Most importantly, the restriction to unary predicates seems necessary. Although the random-worlds method makes sense in general, the connection to maximum entropy seems to disappear in the non-unary case. These observations suggest unexpected limitations to the applicability of maximum-entropy methods.
In Journal of Artificial Intelligence Research, 2, 1994, pp. 33-88. The paper is available in postscript and pdf. A preliminary version appears in Proceedings of Seventh Annual IEEE Symposium on Logic in Computer Science, 1992, p. 22-33.
Joseph Y. Halpern and Bruce M. Kapron
We show that a 0-1 law holds for propositional modal logic, both
for structure validity and frame validity. In the case of
structure validity, the result follows easily from the well-known
0-1 law for first-order logic. However, our proof gives considerably
more information. It leads to an elegant axiomatization
for almost-sure structure validity and to sharper complexity
bounds. Since frame validity can be reduced to a
formula,
the 0-1 law for frame validity helps delineate when 0-1 laws exist
for second-order logics.
In Annals of Pure and Applied Logic, 69, 1994, pp. 157-193. A version similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of Seventh Annual IEEE Symposium on Logic in Computer Science, 1992 pp. 369-380 (with B. M. Kapron). Unfortunately, one of the main theorems in the paper is incorrect. An erratum appears in Annals of Pure and Applied Logic 121, 2003, pp. 281--283, and is available in postscript and pdf.
Full abstraction and expressive completeness for FP
Joseph Y. Halpern and E. L. Wimmers
We consider issues related to the expressive power of the programming language FP. In particular, we consider whether a number of variants of FP are fully abstract and expressively complete. For example, we show that a version of FP with only one-sided sequences behave similarly to PCF in that the addition of parallel or is sufficient to make it fully abstract. However, the addition of parallel or to FP (with its two-sided infinite sequences) is not sufficient to achieve full abstraction. By considering these and other variants, we obtain a better understanding of what is required of a language and semantics in order to guarantee full abstraction and expressive completeness.
In Information and Computation 118:2, 1995, pp. 246-271. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the Second IEEE Symposium on Logic in Computer Science, 1987, pp. 257-271.
Dynamic fault-tolerant clock synchronization
Danny Dolev, Joseph Y. Halpern, Barbara B. Simons, and H. Raymond Strong
This paper gives two simple efficient distributed algorithms: one for keeping clocks in a network synchronized and one for allowing new processors to join the network with their clocks synchronized. Assuming a fault tolerant authentication protocol, the algorithms tolerate both link and processor failures of any type. The algorithm for maintaining synchronization works for arbitrary networks (rather than just completely connected networks) and tolerates any number of processor or communication link faults as long as the correct processors remain connected by fault-free paths. It thus represents an improvement over other clock synchronization algorithms such as those of Lamport and Melliar-Smith [1985] and Welch and Lynch [1988], although, unlike them, it does require an authentication protocol to handle Byzantine faults. Our algorithm for allowing new processors to join requires that more than half the processors be correct, a requirement that is provably necessary.
In Journal of the ACM 42:1, 1995, pp. 143-185. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version, with the title ``Fault-tolerant clock synchronization'' appears in Proceedings of the 3rd ACM Symposium on Principles of Distributed Computing, 1984, pp. 89-102.
Joseph Y. Halpern
A well-known result of Ladner says that the satisfiability problem for K45, KD45, and S5 is NP-complete. This result implicitly assumes that there are infinitely many primitive propositions in the language; it is easy to see that the satisfiability problem for these logics becomes linear time if there are only finitely many primitive propositions in the language. By way of contrast, we show that the PSPACE-completeness results of Ladner and Halpern and Moses hold for the modal logics K, T, S4, and for the multi-agent versions of K45, KD45, and S5 (provided there are at least two agents), even if there is only one primitive proposition in the language. We go on to examine the effect on complexity of bounding the depth of nesting of modal operators. If we restrict to finite nesting, then the satisfiability problem is NP-complete for all the modal logics considered but S4. If we then further restrict the language to having only finitely many primitive propositions, the complexity goes down to linear time in all cases.
In Artificial Intelligence, 75:2, 1995, pp. 361-372. A version of the paper similar to the published version is available in postscript and pdf.
Levesque's axiomatization of only knowing is incomplete
Joseph Y. Halpern and Gerhard Lakemeyer
Levesque introduced a notion of ``only knowing'', with the goal of capturing certain types of nonmonotonic reasoning. Levesque's logic dealt with only the case of a single agent. Recently, both Halpern and Lakemeyer independently attempted to extend Levesque's logic to the multi-agent case. Although there are a number of similarities in their approaches, there are some significant differences. In this paper, we reexamine the notion of only knowing, going back to first principles. In the process, we point out some problems with the earlier definitions. This leads us to reconsider what the properties of only knowing ought to be. We provide an axiom system that captures our desiderata, and show that it has a semantics that corresponds to it. The axiom system has an added feature of interest: it includes a modal operator for satisfiability, and thus provides a complete axiomatization for satisfiability in the logic K45.
In Artificial Intelligence 74:2, 1995, pp. 381-387. A version of the paper similar to the published version is available in postscript and pdf.
A nonstandard approach to the logical omniscience problem
Ronald Fagin, Joseph Y. Halpern, and Moshe Y. Vardi
We introduce a new approach to dealing with the well-known logical omniscience problem in epistemic logic. Instead of taking possible worlds where each world is a model of classical propositional logic, we take possible worlds which are models of a nonstandard propositional logic we call NPL, which is somewhat related to relevance logic. This approach gives new insights into the logic of implicit and explicit belief considered by Levesque and Lakemeyer. In particular, we show that in a precise sense agents in the structures considered by Levesque and Lakemeyer are perfect reasoners in NPL.
In Artificial Intelligence, 79:2, 1996, pp. 203-240. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the 3rd Conference on Theoretical Aspects of Reasoning About Knowledge, 1990, pp. 41-55.
Asymptotic conditional probabilities: the unary case
Adam J.Grove, Joseph Y. Halpern, and Daphne Koller
Motivated by problems that arise in computing degrees of belief, we consider the problem of computing asymptotic conditional probabilities for first-order sentences. Given first-order sentences p and q, we consider the structures with domain {1,..., N} that satisfy q, and compute the fraction of them in which p is true. We then consider what happens to this fraction as N gets large. This extends the work on 0-1 laws that considers the limiting probability of first-order sentences, by considering asymptotic conditional probabilities. As shown in by Liogonkii and in a companion paper), in the general case, asymptotic conditional probabilities do not always exist, and most questions relating to this issue are highly undecidable. These results, however, all depend on the assumption that q can use a nonunary predicate symbol. Liogonkii shows that if we condition on formulas q involving unary predicate symbols only (but no equality or constant symbols), then the asymptotic conditional probability does exist and can be effectively computed. This is the case even if we place no corresponding restrictions on p. We extend this result here to the case where q involves equality and constants. We show that the complexity of computing the limit depends on various factors, such as the depth of quantifier nesting, or whether the vocabulary is finite or infinite. We completely characterize the complexity of the problem in the different cases, and show related results for the associated approximation problem.
In SIAM Journal on Computing, 25:1, 1996, pp. 1-51. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version (which also includes results of a companion paper), with the title ``Asymptotic conditional probabilities for first-order logic'', appears in Proceedings of the 24th Annual ACM Symposium on Theory of Computing, 1992, pp. 294-305.
Asymptotic conditional probabilities: the non-unary case
Adam J.Grove, Joseph Y. Halpern, and Daphne Koller
Motivated by problems that arise in computing degrees of belief, we consider the problem of computing asymptotic conditional probabilities for first-order sentences. Given first-order sentences p and q, we consider the structures with domain {1,..., N} that satisfy q, and compute the fraction of them in which p is true. We then consider what happens to this fraction as N gets large. This extends the work on 0-1 laws that considers the limiting probability of first-order sentences, by considering asymptotic conditional probabilities. As shown by Liogonkii, if there is a non-unary predicate symbol in the vocabulary, asymptotic conditional probabilities do not always exist. We extend this result to show that asymptotic conditional probabilities do not always exist for any reasonable notion of limit. Liogonkii also showed that the problem of deciding whether the limit exists is undecidable. We analyze the complexity of three problems with respect to this limit: deciding whether it is well-defined, whether it exists, and whether it lies in some nontrivial interval. Matching upper and lower bounds are given for all three problems, showing them to be highly undecidable.
In Journal of Symbolic Logic, 61:1, 1996, pp. 250-275. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version (which also includes results of a companion paper), with the title ``Asymptotic conditional probabilities for first-order logic'', appears in Proceedings of the 24th Annual ACM Symposium on Theory of Computing, 1992, pp. 294-305.
Should knowledge entail belief?
Joseph Y. Halpern
The appropriateness of S5 as a logic of knowledge has been attacked at some length in the philosophical literature. Here one particular attack based on the interplay between knowledge and belief is considered: Suppose that knowledge satisfies S5, belief satisfies KD45, and both the entailment property (knowledge implies belief) and positive certainty (if the agent believes something, she believes she knows it) hold. Then it can be shown that belief reduces to knowledge: it is impossible to have false beliefs. While the entailment property has typically been viewed as perhaps the least controversial of these assumptions, an argument is presented that it can plausibly be viewed as the culprit. More precisely, it is shown that this attack fails if we weaken the entailment property so that it applies only to objective (nonmodal) formulas, rather than to arbitrary formulas. Since the standard arguments in favor of the entailment property are typically given only for objective formulas, this observation suggests that care must be taken in applying intuitions that seem reasonable in the case of objective formulas to arbitrary formulas.
In Journal of Philosophical Logic, 25:5, 1996, pp. 483-494. A version of the paper similar to the published version is available in postscript and pdf.
A theory of knowledge and ignorance for many agents
Joseph Y. Halpern
We extend the notion of ``only knowing'' introduced by Halpern and Moses (see ``Towards a theory of knowledge and ignorance'') to many agents and to a number of modal logics. In this approach, all an agent knows is p is true in a structure M if, in M, the agent knows p and has the maximum number of ``possibilities''. To extend this approach, we need to make precise what counts as a ``possibility''. In the single-agent case, we can identify a possibility with a truth assignment. In the multi-agent case, things are more complicated. We consider three notions of possibility (all related). We argue that the first is most appropriate for non-introspective logics, such as K, T, and S4, the second is most appropriate for K45 and KD45, and the last is most appropriate for S5. With the appropriate notion of possibility, we show that are reasonable extensions in all cases. These results also shed light on the single-agent case. It was always assumed that one of the key aspects of Halpern-Moses approach in the single-agent case was its use of S5, rather than K45 or KD45. Our results show that the notion is better understood in the context of K45 (or KD45). In the single-agent case, the notion remains unchanged if we use K45 instead of S5. However, in the multi-agent case, there are significant differences between K45 and S5. Moreover, in some sense, the K45 variants behave better: all results proved for the single-agent case extend more naturally to the multi-agent case of K45 than to the multi-agent of S5.
In Journal of Logic and Computation, 7:1, 1997, pp. 79-108. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears as ``Reasoning about only knowing with many agents'', AAAI-93 (Proceedings of the Eleventh National Conference on Artificial Intelligence) 1993, pp. 655-661.
From statistical knowledge bases to degrees of belief
Fahiem Bacchus, Adam J.Grove, Joseph Y. Halpern, and Daphne Koller
An intelligent agent will often be uncertain about various properties of its environment, and when acting in that environment it will frequently need to quantify its uncertainty. For example, if the agent wishes to employ the expected-utility paradigm of decision theory to guide its actions, she will need to assign degrees of belief (subjective probabilities) to various assertions. Of course, these degrees of belief should not be arbitrary, but rather should be based on the information available to the agent. This paper describes one approach for inducing degrees of belief from very rich knowledge bases, which might include information about particular individuals, statistical correlations, physical laws, and default rules. We call our approach the random-worlds method. This method is based on a principle of indifference: it treats all of the worlds the agent considers possible as being equally likely. It is able to integrate qualitative default reasoning with quantitative probabilistic reasoning by providing a language in which both types of information can be easily expressed. Our results show that a number of desiderata that arise in direct inference (reasoning from statistical information to conclusions about individuals) and default reasoning follow directly from the semantics of random worlds. For example, random worlds captures important patterns of reasoning such as specificity, inheritance, indifference to irrelevant information, and default assumptions of independence. Furthermore, the expressive power of the language used and the intuitive semantics of random worlds allow the method to deal well with problems that are beyond the scope of many other non-deductive reasoning systems.
In Artificial Intelligence 87:1-2, 1996, pp. 75-143, A version of the paper similar to the published version is available in postscript and pdf. Some material in this paper appeared in preliminary form in ``Statistical foundations for default reasoning'', Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI 93), 1993, pp. 563-569.
A critical reexamination of default logic, autoepistemic logic, and only knowing
Joseph Y. Halpern
Fifteen years of work on nonmonotonic logic has certainly increased our understanding of the area. However, given a problem in which nonmonotonic reasoning is called for, it is far from clear how one should go about modeling the problem using the various approaches. In particular, we return to the original technical definitions given in these papers, and examine the extent to which they capture the intuitions they were designed to capture.
In Computational Intelligence 13:1, 1997, pp. 144-163. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Computational Logic and Proof Theory (Proceedings of the Kurt Gödel Symposium, KGC '93), Lecture Notes in Computer Science, vol. 713, Springer, 1993, pp. 43-60.
On ambiguities in the interpretation of game trees
Joseph Y. Halpern
Piccione and Rubinstein have pointed out ambiguities in the interpretation of games of imperfect recall. They focus on the notion of time consistency, and argue that a player in a game of imperfect recall may be time inconsistent, changing his strategy despite no new information and no change in his preferences. In this paper, it is argued that the apparent time inconsistency arises from implicit assumptions made in the definition about what the driver knows when he reconsiders his strategy and what he will remember if he changes his strategy, and about how the node at which reconsideration takes place is chosen. A model is proposed, based on earlier work in the computer science literature, that allows us -- indeed, almost forces us -- to make these issues explicit. Once these issues are made explicit, time inconsistency seems less inconsistent.
In Games and Economic Behavior 20, 1997, pp. 66-96. A preliminary version appears in Proceedings of the Sixth Conference on Theoretical Aspects of Rationality and Knowledge, 1996, pp. 77-96. A version of the paper similar to the published version is available in postscript and pdf.
On the expected value of games with absentmindedness
Adam J. Grove and Joseph Y. Halpern
Piccione and Rubinstein have argued that a seemingly paradoxical form of time inconsistency can arise in games of imperfect recall. At the heart of this argument is a calculation of the expected value of a game, from the standpoint of a player who is in the middle of play. We claim that this concept is not well defined in games with absentmindedness (that is, games where two nodes in the same path can be in one information set). To make it well defined, additional assumptions must be made. We show that there are reasonable assumptions under which no time inconsistency arises. It is also possible to make assumptions that validate Piccione and Rubinstein's calculations, but the nature of these assumptions is generally such as to remove the appearance of paradox.
In Games and Economic Behavior 20, 1997, pp. 51-65. A version of the paper similar to the published version is available in postscript and pdf.
Performing work efficiently in the presence of faults
Cynthia Dwork, Joseph Y. Halpern, and Orli Waarts
We consider a system of t synchronous processes
that communicate only by sending messages to one another,
and that together
must perform n independent units of work.
Processes may fail by crashing;
we want to guarantee that
in every execution of the protocol
in which at least one process survives, all n units of
work will be performed.
We consider three parameters: the number of messages sent,
the total number of units of work performed (including
multiplicities), and time.
We present three protocols for solving the problem.
All three are
work-optimal, doing O(n+t) work.
The first
has moderate costs in the remaining two
parameters,
sending O() messages, and
taking (n+t) time.
This protocol can be easily modified to
run in any completely
asynchronous system equipped with a failure detection
mechanism.
The second
sends only O(
) messages, but
its running time is exponential in n and t.
The third is essentially time-optimal in the (usual) case
in which there are no failures, and its
time complexity degrades gracefully as the number of
failures increases.
SIAM Journal on Computing 27:5, 1998. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the Eleventh Annual ACM Symposium on Principles of Distributed Computing, 1992, pp. 91-102.
Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi
Reasoning about activities in a distributed system at the level of knowledge allows us to abstract away from many irrelevant details. We introduce two notions to facilitate designing and reasoning about systems in terms of knowledge. The first is knowledge-based programs, which improve upon Halpern and Fagin's definition of knowledge-based protocols. Knowledge-based programs are syntactic objects: programs with tests for knowledge. The second notion is contexts, which capture the setting in which a program is executed. In a given context, a standard program (one without tests for knowledge) is represented by (i.e., corresponds in a precise sense to) a unique system. A knowledge-based program, on the other hand, may be represented by no system, one system, or many systems. We provide a condition that is sufficient to guarantee that a knowledge-based program is represented by a unique system, and covers many of the knowledge-based programs considered in the literature. We also characterize the complexity of determining whether a given knowledge-based program has a unique representation, or any representation at all, in a finite-state context.
In Distributed Computing 10:4, 1997, pp. 199-225. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in Proceedings of the Fourteenth Annual ACM Symposium on Principles of Distributed Computing, 1995, pp. 153-163. There is significant overlap between this paper and Chapters 4, 5, and 7 of our book, although the paper has some new material.
Modeling belief in dynamic systems. Part I: Foundations
Nir Friedman and Joseph Y. Halpern
Belief change is a fundamental problem in AI: Agents constantly have to update their beliefs to accommodate new observations. In recent years, there has been much work on axiomatic characterizations of belief change. We claim that a better understanding of belief change can be gained from examining appropriate semantic models. In this paper we propose a general framework in which to model belief change. We begin by defining belief in terms of knowledge and plausibility: an agent believes p if he knows that p is more plausible than not-p. We then consider some properties defining the interaction between knowledge and plausibility, and show how these properties affect the properties of belief. In particular, we show that by assuming two of the most natural properties, belief becomes a KD45 operator. Finally, we add time to the picture. This gives us a framework in which we can talk about knowledge, plausibility (and hence belief), and time, which extends the framework of Halpern and Fagin for modeling knowledge in multi-agent systems. We then examine the problem of ``minimal change''. This notion can be captured by using prior plausibilities, an analogue to prior probabilities, which can be updated by ``conditioning''. We show by example that conditioning on a plausibility measure can capture many scenarios of interest. In a companion paper, we show how the two best-studied scenarios of belief change, belief revision and belief update, fit into our framework.
In Artificial Intelligence 95:2, 1997, pp. 257-316. A version of the paper similar to the published version is available in postscript and pdf. An earlier (and much different) version of the paper appeared under the title "A knowledge-based framework for belief change, Part I: Foundations'', in Proceedings of the 5th Conference on Theoretical Aspects of Reasoning About Knowledge, 1994, pp. 44-64.
Defining relative likelihood in partially-ordered preferential structures
Joseph Y. Halpern
Starting with a likelihood or preference order on worlds, we extend it to a likelihood ordering on sets of worlds in a natural way, and examine the resulting logic. Lewis earlier considered such a notion of relative likelihood in the context of studying counterfactuals, but he assumed a total preference order on worlds. Complications arise when examining partial orders that are not present for total orders. There are subtleties involving the exact approach to lifting the order on worlds to an order on sets of worlds. In addition, the axiomatization of the logic of relative likelihood in the case of partial orders gives insight into the connection between relative likelihood and default reasoning.
In Journal of AI Research 7, 1997, pp. 1-24. A preliminary version appears in Proceedings of the Twelfth Conference on Uncertainty in AI, 1996, pp. 299-306. The paper is available in postscript and pdf.
Plausibility measures and default reasoning
Nir Friedman and Joseph Y. Halpern
We introduce a new approach to modeling uncertainty based on plausibility measures. This approach is easily seen to generalize other approaches to modeling uncertainty, such as probability measures, belief functions, and possibility measures. We focus on one application of plausibility measures in this paper: default reasoning. In recent years, a number of different semantics for defaults have been proposed, such as preferential structures, epsilon-semantics, possibilistic structures, and kappa-rankings, that have been shown to be characterized by the same set of axioms, known as the KLM properties. While this was viewed as a surprise, we show here that it is almost inevitable. In the framework of plausibility measures, we can give a necessary condition for the KLM axioms to be sound, and an additional condition necessary and sufficient to ensure that the KLM axioms are complete. This additional condition is so weak that it is almost always met whenever the axioms are sound. In particular, it is easily seen to hold for all the proposals made in the literature.
Accepted for publication, Journal of the ACM, March, 1997. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version appears in AAAI-96 (Proceedings of the Thirteenth National Conference on Artificial Intelligence), 1996, pp. 1297-1304.
On the knowledge requirements of tasks
Ronen I. Brafman, Joseph Y. Halpern, and Yoav Shoham
In order to successfully perform a task, a situated system requires some information about its domain. If we can understand what information the system requires, we may be able to equip it with more suitable sensors or make better use of the information available to it. These considerations have motivated roboticists to examine the issue of sensor design, and in particular, the minimal information required to perform a task. We show here that reasoning in terms of what the robot knows and needs to know to perform a task is a useful approach for analyzing these issues. We extend the formal framework for reasoning about knowledge, already used in AI and distributed computing, by developing a set of concepts basic and tools for modeling and analyzing the knowledge requirements of tasks. We investigate properties of the resulting framework, and show how it can be applied to robotics tasks.
In Artificial Intelligence, 98:1-2, 1998, pp. 317-349. A version of the paper similar to the published version is available in postscript and pdf.
A counterexample to theorems of Cox and Fine
Joseph Y. Halpern
Cox's well-known theorem justifying the use of probability is shown not to hold in finite domains. The counterexample also suggests that Cox's assumptions are insufficient to prove the result even in infinite domains. The same counterexample is used to disprove a result of Fine on comparative conditional probability.
In Journal of AI Research, 10, 1999, pp. 67-85. A preliminary version appears in AAAI-96 (Proceedings of the Thirteenth National Conference on Artificial Intelligence), 1996, pp. 1313-1319. The paper is available in postscript and pdf. Further discussion of Cox's Theorem can be found in Cox's Theorem revisited.
The hierarchical approach to modeling knowledge and common knowledge
Ronald Fagin, Joseph Y. Halpern, J. Geanakoplos, and Moshe Y. Vardi
One approach to representing knowledge or belief of agents, which has been explored independently by economists (Boge and Eisele; Mertens and Zamir; Brandenburger and Dekel; Tan and Werlang) and by computer scientists (Fagin, Halpern, and Vardi) involves an infinite hierarchy of beliefs. Such a hierarchy consists of an agent's beliefs about the state of the world, his beliefs about other agents' beliefs about the worlds, his beliefs about other agents' beliefs about other agents' beliefs about the worlds, etc. Economists and computer scientists differ, however, in the way they model beliefs. Economists prefer a probability-based framework, where belief is modeled as a probability distribution on the uncertainty space. In contrast, computer scientists prefer an information-based framework, where belief is modeled as a subset of the underlying space. The idea is that whatever is in the subset is believed to be possible, and whatever is not in the subset is believed to be impossible. We consider the question of when such an infinite hierarchy completely describes the uncertainty of the agents. We provide various necessary and sufficient conditions for this property. It turns out that the probability-based approach can be viewed as satisfying one of these conditions, which explains why the infinite hierarchy always completely describes the uncertainty of the agents in the probability-based approach. An interesting consequence of our conditions is that adequacy of an infinite hierarchy may depend on the ``richness'' of the states in the underlying state space. We also consider the question of whether an infinite hierarchy completely describes the uncertainty of the agents with respect to ``interesting'' sets of events and show that the answers depends on the definition of ``interesting''.
International Journal of Game Theory 28:3, 1999, pp. 331-365. A version of the paper similar to the published version is available in postscript and pdf. A preliminary version with the title ``The expressive power of the hierarchical approach to modeling knowledge and common knowledge'' appears in Proceedings of the 4th Conference on Theoretical Aspects of Reasoning About Knowledge, 1992, pp. 229-244
Hypothetical knowledge and counterfactual reasoning
Joseph Y. Halpern
Samet introduced a notion of hypothetical knowledge and showed how it could be used to capture the type of counterfactual reasoning necessary to force the backwards induction solution in a game of perfect information. He argued that while hypothetical knowledge and the extended information structures used to model it bear some resemblance to the way philosophers have used conditional logic to model counterfactuals, hypothetical knowledge cannot be reduced to conditional logic together with epistemic logic. Here it is shown that in fact hypothetical knowledge can be captured using the standard counterfactual operator and knowledge operator, provided that some assumptions are made regarding the interaction between the two. It is argued, however, that these assumptions are unreasonable in general, as are the axioms that follow from them. Some implications for game theory are discussed.
Accepted for publication, International Journal of Game Theory, 1998. A version of the paper similar to version to be published is available in postscript and pdf. A preliminary version appears in Proceedings of the Seventh Conference on Theoretical Aspects of Rationality and Knowledge, 1998, pp.~83-96.
Modeling belief in dynamic systems. Part II: Revision and update
Nir Friedman and Joseph Y. Halpern
The study of belief change has been an active area in philosophy and AI. In recent years two special cases of belief change, belief revision and belief update, have been studied in detail. In a companion paper we introduced a new framework to model belief change. This framework combines temporal and epistemic modalities with a notion of plausibility, allowing us to examine the changes of beliefs over time. In this paper we show how belief revision and belief update can be captured in our framework. This allows us to compare the assumptions made by each method and to better understand the principles underlying them. In particular, it allows us to understand the source of Gardenfors' triviality result for belief revision and suggests a way of mitigating the problem. It also shows that Katsuno and Mendelzon's notion of belief update depends on several strong assumptions that may limit its applicability in AI.
Journal of AI Research 10, 1999, pp. 117-167. A preliminary version, with the title ``A knowledge-based framework for belief change. Part II: Revision and Update'' appears in Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning, 1994, pp. 190-201. The full paper is available in postscript and pdf.
Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi
We consider the common-knowledge paradox raised in Knowledge and common knowledge in a distributed environment common knowledge is necessary for coordination, but common knowledge is unattainable in the real world because of temporal imprecision. We discuss two solutions to this paradox: (1) modeling the world with a coarser granularity, and (2) relaxing the requirements for coordination.
In Annals of Pure and Applied Logic 96, 1999, pp. 89-105. A preliminary version appears in Proceedings of the Sixth Conference on Theoretical Aspects of Rationality and Knowledge, 1996, pp. 283-298. This material is largely taken from Chapter 11 of our book. The paper is available in postscript and pdf.
Nir Friedman and Joseph Y. HalpernWe examine carefully the rationale underlying the approaches to belief change taken in the literature, and highlight what we view as methodological problems. We argue that to study belief change carefully, we must be quite explicit about the ``ontology'' or scenario underlying the belief change process. This is something that has been missing in previous work, with its focus on postulates. Our analysis shows that we must pay particular attention to two issues that have often been taken for granted: The first is how we model the agent's epistemic state. (Do we use a set of beliefs, or a richer structure, such as an ordering on worlds? And if we use a set of beliefs, in what language are these beliefs are expressed?) We show that even postulates that have been called ``beyond controversy'' are unreasonable when the agent's beliefs include beliefs about her own epistemic state as well as the external world. The second is the status of observations. (Are observations known to be true, or just believed? In the latter case, how firm is the belief?) Issues regarding the status of observations arise particularly when we consider iterated belief revision, and we must confront the possibility of revising by p and then by p.
In Journal of Logic, Language, and Information 8, 1999, pp. 401-420. A preliminary version appeared in Proceedings of the Fifth Internal Conference on Principles of Knowledge Representation and Reasoning (KR '96), 1996, pp. 421-431. The paper is available in postscript and pdf.
Joseph Y. Halpern
The assumptions needed to prove Cox's Theorem are discussed and examined. Various sets of assumptions under which a Cox-style theorem can be proved are provided, although all are rather strong and, arguably, not natural. This paper provides further discussion of the issues raised in A counterexample to theorems of Cox and Fine.
In Journal of AI Research 11, 1999, pp. 429-435. This is really a short note expanding on the issues raised in A counterexample to theorems of Cox and Fine. The paper is available in postscript and pdf.
Set-theoretic completeness for epistemic and conditional logic
Joseph Y. Halpern
The standard approach to logic in the literature in philosophy and mathematics, which has also been adopted in computer science, is to define a language (the syntax), an appropriate class of models together with an interpretation of formulas in the language (the semantics), a collection of axioms and rules of inference characterizing reasoning (the proof theory), and then relate the proof theory to the semantics via soundness and completeness results. Here we consider an approach that is more common in the economics literature, which works purely at the semantic, set-theoretic level. We provide set-theoretic completeness results for a number of epistemic and conditional logics, and contrast the expressive power of the syntactic and set-theoretic approaches.
In Annals of Mathematics and Artificial Intelligence 26, 1999, pp. 1-27. A preliminary version appears in Proceedings of the Fifth International Symposium on Artificial Intelligence and Mathematics, 1998. The paper is available in postscript and pdf.
Reasoning about noisy sensors in the situation calculus
Fahiem Bacchus, Joseph Y. Halpern, and Hector J. Levesque,
Agents interacting with an incompletely known dynamic world need to be able to reason about the effects of their actions, and to gain further information about that world using sensors of some sort. Unfortunately, sensor information is inherently noisy, and in general serves only to increase the agent's degree of confidence in various propositions. Building on a general logical theory of action formalized in the situation calculus developed by Reiter and others, we propose a simple axiomatization of the effect on an agent's state of belief of taking a reading from a noisy sensor. By exploiting Reiter's solution to the frame problem, we automatically obtain that these sensor actions leave the rest of the world unaffected, and further, that non-sensor actions change the state of belief of the agent in appropriate ways.
In Artificial Intelligence, 1999, pp. 131-169. A previous version appears in Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI 95), 1995, pp. 1933-1940. Available in postscript and pdf.
A note on knowledge-based programs and specifications
Joseph Y. Halpern
We view a knowledge-based protocol as specifying a set of systems (where a system is a set of runs), in contrast to a standard protocol, which specifies a set of runs. This point of view helps clarify the relationship between standard and knowledge-based protocols. It also leads naturally to a useful notion of knowledge-based specification, a specification that, like a knowledge-based protocol, can be identified with a set of systems.
In Distributed Computing 13:3, 2000, pp. 145-153. The paper is available in postscript and pdf.
A logic for SDSI's linked local named spaces
Joseph Y. Halpern and Ronald van der Meyden
Abadi has introduced a logic to explicate the meaning of local names in SDSI, the Simple Distributed Security Infrastructure proposed by Rivest and Lampson. Abadi's logic does not correspond precisely to SDSI, however; it draws conclusions about local names that do not follow from SDSI's name resolution algorithm. Moreover, its semantics is somewhat unintuitive. This paper presents the Logic of Local Name Containment, which does not suffer from these deficiencies. It has a clear semantics and provides a tight characterization of SDSI name resolution. The semantics is shown to be closely related to that of logic programs, leading to an approach to the efficient implementation of queries concerning local names. A complete axiomatization of the logic is also provided.
In Journal of Computer Security 9:1,2, 2001, pp. 47-74. A preliminary version appears in Proceedings of the 12th IEEE Computer Security Foundations Workshop, 1999, pp. 111-122. The paper is available in postscript and pdf.
CoRR: A Computing Research Repository (with commentary)
Joseph Y. Halpern
I describe how CoRR was set up and discuss some policy issues.
In ACM Journal of Computer Documentation, 24:2, 2000, pp. 41-48. There were also commentators who wrote a response to the artilce; my response to the commentators is on pp. 72-77. This article is based on (and borrows liberally from) two earlier articles: A Computing Research Repository, D-Lib Magazine, November 1998 and The Computing Research Repository: Promoting the Rapid Dissemination of Computer Science Research. The paper is available in postscript and pdf. My response to the commentators (which is fairly self-contained) is available in postscript and pdf.
Substantive rationality and backward induction
Joseph Y. Halpern
Aumann has proved that common knowledge of substantive rationality implies the backwards induction solution in games of perfect information. Stalnaker has proved that it does not. Roughly speaking, a player is substantively rational if, for all vertices v, if the player were to reach vertex v, then the player would be rational at vertex v. It is shown here that the key difference between Aumann and Stalnaker lies in how they interpret this counterfactual. A formal model is presented that lets us capture this difference, in which both Aumann's result and Stalnaker's result are true (under appropriate assumptions).
In Games and Economic Behavior 37, 2001, pp. 425-435. The paper is available in postscript and pdf.
Alternative semantics for unawareness
Joseph Y. Halpern
Modica and Rustichini [1994] provided a logic for reasoning about knowledge where agents may be unaware of certain propositions. However, their original approach had the unpleasant property that nontrivial unawareness was incompatible with partitional information structures. More recently, Modica and Rustichini [1999] have provided an approach that allows for nontrivial unawareness in partitional information structures. Here it is shown that their approach can be viewed as a special case of a general approach to unawareness considered in Belief, awareness, and limited reasoning.
In Games and Economic Behavior 37, 2001, pp. 321-339. The paper is available in postscript and pdf.
Joseph Y. Halpern
Causal models defined in terms of a collection of equations, as defined by Pearl, are axiomatized here. Axiomatizations are provided for three successively more general classes of causal models: (1) the class of recursive theories (those without feedback), (2) the class of theories where the solutions to the equations are unique, (3) arbitrary theories (where the equations may not have solutions and, if they do, they are not necessarily unique). It is shown that to reason about causality in the most general third class, we must extend the language used by Galles and Pearl. In addition, the complexity of the decision procedures is examined for all the languages and classes of models considered.
In Journal of AI Research 12, 2000, pp. 317-337. A preliminary version appears in Proceedings of the Fourteenth Conference on Uncertainty in AI, 1998, pp. 202-210. The paper is available in postscript and pdf.
First-order conditional logic for default reasoning revisited
Nir Friedman, Joseph Y. Halpern, and Daphne KollerConditional logics play an important role in recent attempts to investigate default reasoning. This paper investigates first-order conditional logic. We show that, as for first-order probabilistic logic, it is important not to confound statistical conditionals over the domain (such as ``most birds fly''), and subjective conditionals over possible worlds (such as ``I believe that Tweety is unlikely to fly''). We then address the issue of ascribing semantics to first-order conditional logic. As in the propositional case, there are many possible semantics. To study the problem in a coherent way, we use plausibility structures. These provide us with a general framework in which many of the standard approaches can be embedded. We show that while these standard approaches are all the same at the propositional level, they are significantly different in the context of a first-order language. We show that plausibilities provide the most natural extension of conditional logic to the first-order case: We provide a sound and complete axiomatization that contains only the KLM properties and standard axioms of first-order modal logic. We show that most of the other approaches have additional properties, which result in an inappropriate treatment of an infinitary version of the lottery paradox.
In ACM Transactions on Computational Logic 1:2, 2000, pp. 175-207. A preliminary version, with the title "First-order conditional logic revisited" appears in AAAI-96 (Proceedings of the Thirteenth National Conference on Artificial Intelligence), 1996, pp. 1305-1312. The full paper is available in postscript and pdf.
A decision-theoretic approach to reliable message delivery
Francis C. Chu and Joseph Y. Halpern
We argue that the tools of decision theory need to be taken more seriously in the specification and analysis of systems. We illustrate this by considering a simple problem involving reliable communication, showing how considerations of utility and probability can be used to decide when it is worth sending heartbeat messages and, if they are sent, how often they should be sent.
In Distributed Computing 14, 2001, pp. 1-16. A preliminary version appears in Proceedings of the 12th International Symposium on Distributed Computing, 1998, pp. 89-103. The full paper is available in postscript and pdf.
Joseph Y. Halpern and Gerhard Lakemeyer
Levesque introduced a notion of ``only knowing'', with the goal of capturing certain types of nonmonotonic reasoning. Levesque's logic dealt with only the case of a single agent. Recently, both Halpern and Lakemeyer independently attempted to extend Levesque's logic to the multi-agent case. Although there are a number of similarities in their approaches, there are some significant differences. In this paper, we reexamine the notion of only knowing, going back to first principles. In the process, we simplify Levesque's completeness proof, and point out some problems with the earlier definitions. This leads us to reconsider what the properties of only knowing ought to be. We provide an axiom system that captures our desiderata, and show that it has a semantics that corresponds to it. The axiom system has an added feature of interest: it includes a modal operator for satisfiability, and thus provides a complete axiomatization for satisfiability in the logic K45.
In Journal of Logic and Computation 11:1, 2001, pp. 41-70. A preliminary version appears in Proceedings of the Sixth Conference on Theoretical Aspects of Rationality and Knowledge, 1996, pp. 251-266. The paper is available in postscript and pdf.
Conditional plausibility measures and Bayesian networks
Joseph Y. Halpern
A general notion of algebraic conditional plausibility measures is defined. Probability measures, ranking functions, possibility measures, and (under the appropriate definitions) sets of probability measures can all be viewed as defining algebraic conditional plausibility measures. It is shown that the technology of Bayesian networks can be applied to algebraic conditional plausibility measures.
In Journal of AI Research 14, 2001, pp. 359-389. A preliminary version appears in Proceedings of the Sixteenth Conference on Uncertainty in AI, 2000, pp. 247-255. The full paper is available in postscript and pdf.
On the NP-completeness of finding an optimal strategy in games with common payoffs
Francis C. Chu and Joseph Y. Halpern
Given a finite game with common payoffs (i.e, the players have completely common interests), we show that the problem of determining whether there exists a joint strategy where each player nets at least k is NP-complete.
In International Journal of Game Theory 30:1, 2001, pp. 99-106. The paper is available in postscript and pdf.
A characterization of eventual Byzantine agreement
Joseph Y. Halpern, Yoram Moses, and Orli Waarts
We investigate eventual Byzantine agreement (EBA) in the crash and omission failure models. The emphasis is on characterizing optimal EBA protocols in terms of the states of knowledge required by the processors in order to attain EBA. It is well known that common knowledge among the nonfaulty processors is a necessary and sufficient condition for attaining simultaneous Byzantine agreement (SBA). We define a new variant that we call continual common knowledge, and use it to provide necessary and sufficient conditions for attaining E