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

We identify the computational complexity of the satisfiability problem for FO 2 , the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO 2 has the finite-model property, which means that if an FO 2 -sentence is satisfiable, then it has a finite (...) model. Moreover, Mortimer showed that every satisfiable FO 2 -sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO 2 -sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO 2 is NEXPTIME-complete. (shrink)

Review of Joseph Y. Halpern (ed.), Theoretical Aspects of Reasoning About Knowledge: Proceedings of the 1986 Conference (Los Altos, CA: Morgan Kaufmann, 1986),.

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 $(\sigma \vdash_\mathrm{v} \varphi$ if for every substitution $\tau$, the validity of $\tau \lbrack\sigma\rbrack$ entails the validity of $\tau\lbrack\varphi\rbrack)$, and truth inference $(\sigma \vdash_\mathrm{t} \varphi$ if for every substitution $\tau$, the truth of $\tau\lbrack\sigma\rbrack$ entails the truth of $\tau\lbrack\varphi\rbrack)$. 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. (shrink)

We describe BDD-based decision procedures for the modal logic K. Our approach is inspired by the automata-theoretic approach, but we avoid explicit automata construction. Instead, we compute certain fixpoints of a set of types — which can be viewed as an on-the-fly emptiness of the automaton. We use BDDs to represent and manipulate such type sets, and investigate different kinds of representations as well as a “level-based” representation scheme. The latter turns out to speed up construction and reduce memory consumption (...) considerably. We also study the effect of formula simplification on our decision procedures. To prove the viability of our approach, we compare our approach with a representative selection of other approaches, including a translation of K to QBF. Our results indicate that the BDD-based approach dominates for modally heavy formulae, while search-based approaches dominate for propositionally heavy formulae. (shrink)

Vardi, M.Y., Verification of concurrent programs: the automata-theoretic framework, Annals of Pure and Applied Logic 51 79–98. We present an automata-theoretic framework to the verification of concurrent and nondeterministic programs. The basic idea is that to verify that a program P is correct one writes a program A that receives the computation of P as input and diverges only on incorrect computations of P. Now P is correct if and only if a program PA, obtained by combining P and A, (...) terminates. We formalize this idea in a framework of ω-automata with a recursive set of states. This unifies previous works on verification of fair termination and verification of temporal properties. (shrink)

In program synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. When the system is open, then at each moment it reads input signals and writes output signals, which depend on the input signals and the history of the computation so far. The specification considers all possible input sequences. Thus, if the specification is linear, it should hold in every computation generated by the interaction, and if the specification is branching, it should hold in (...) the tree that embodies all possible input sequences. Often, the system cannot read all the input signals generated by its environment. For example, in a distributed setting, it might be that each process can read input signals of only part of the underlying processes. Then, we should transform a specification into a system whose output depends only on the readable parts of the input signals and the history of the computation. This is called synthesis with incomplete information. In this work we solve the problem of synthesis with incomplete information in its full generality. We consider linear and branching settings with complete and incomplete information. We claim that alternation is a suitable and helpful mechanism for coping with incomplete information. Using alternating tree automata, we show that incomplete information does not make the synthesis problem more complex, in both the linear and the branching paradigm. In particular, we prove that independently of the presence of incomplete information, the synthesis problems for CTL and CTL * are complete for EXPTIME and 2EXPTIME, respectively. (shrink)

In the automata-theoretic approach to verification, we translate specifications to automata. Complexity considerations motivate the distinction between different types of automata. Already in the 60s, it was known that deterministic Büchi word automata are less expressive than nondeterministic Büchi word automata. The proof is easy and can be stated in a few lines. In the late 60s, Rabin proved that Büchi tree automata are less expressive than Rabin tree automata. This proof is much harder. In this work we relate the (...) expressiveness gap between deterministic and nondeterministic Büchi word automata and the expressiveness gap between Büchi and Rabin tree automata. We consider tree automata that recognize derived languages. For a word language L, the derived language of L, denoted L, is the set of all trees all of whose paths are in L. Since often we want to specify that all the computations of the program satisfy some property, the interest in derived languages is clear. Our main result shows that L is recognizable by a nondeterministic Büchi word automaton but not by a deterministic Büchi word automaton iff L is recognizable by a Rabin tree automaton and not by a Büchi tree automaton. Our result provides a simple explanation for the expressiveness gap between Büchi and Rabin tree automata. Since the gap between deterministic and nondeterministic Büchi word automata is well understood, our result also provides a characterization of derived languages that can be recognized by Büchi tree automata. Finally, it also provides an exponential determinization of Büchi tree automata that recognize derived languages. (shrink)