The logic and computation group is composed of faculty and graduate students from the computer and information science, mathematics, and philosophy departments, and participates in the Institute for Research in the Cognitive Sciences.
The logic and computation group runs a weekly seminar.
The seminar meets regularly during the school year
on Mondays at 4:30 p.m.
in room DRL 4C8 in the DRL Building
at the University of Pennsylvania.
Any changes to this schedule will be specifically noted.
The seminar is open to the public and all are welcome.
To subscribe to the mailing list, send mail to majordomo@cis.upenn.edu
with the following in the message text: "subscribe lcs".
(Don't include quotes! The message should be in the message text, NOT the
subject)
In this talk we consider a natural extension of Linear-time Temporal Logic (LTL) with constraints interpreted over a concrete domain like the integers Z, with the relations < and =. While the model-checking problem for the logic reduces easily to that of LTL, the satisfiability problem is non-trivial even for common domains like (Z,<,=). We use a new automata-theoretic technique to show PSPACE decidability of the satisfiability problem of the logic for the constraint systems (Z,<,=) and (N,<,=).
This is joint work with Stephane Demri, LSV ENS-Cachan.
Kurt Goedel and Rudolf Carnap had significant interaction in the period 1928-1932; indeed Carnap's 1928 lectures at the University of Vienna played a crucial role in stimulating Goedel's interest in logic and the foundations and of mathematics, and specifically in questions of completeness. I survey their interaction, and the consequent nature of their influence on each other. I then discuss their profound philosophical differences, focusing particularly on an issue that has been little discussed in conntection with Goedel's Platonism, namely, how the applications of mathematics to the empirical world are to be accounted for.
A modal accessibility relation is just a transition relation, and so can be represented by a transition matrix. As a matter of fact, multimodal logics can also be represented by generalized transition matrices provided matrix entries are taken to be in a more complex Boolean algebra than the standard two-valued one. Starting from this point, I show that bisimulations have a rather elegant theory when expressed in terms of transformations on Boolean vector spaces. The resulting work is a curious hybrid, fitting between conventional modal semantics and conventional linear algebra. I don't know where the investigations begun here will ultimately wind up, but in the meantime the approach has a kind of curious charm that others may find appealing.
According to Brouwer, the truth in intuitionistic logic means provability. On this basis Heyting and Kolmogorov introduced what is now known as Brouwer-Heyting-Kolmogorov (BHK) semantics for intuitionistic logic and is generally recognized as the intended semantics for the latter. Since then, various mathematical models for intuitionistic logic have been found. However, despite many efforts the original BHK semantics of intuitionistic logic as logic of proofs did not meet, until recently, an exact mathematical formulation.
Goedel in 1933 suggested a mechanism based on modal logic S4 connecting classical provability (represented as S4-modality) to intuitionistic logic. This did not solve the BHK problem, since S4 itself was left without an exact provability model, but made an important reduction which later became an integral part of the solution. In 1938 Goedel suggested using the original BHK format of proof carrying formulas to build a provability model of S4. This Goedel's program was accomplished in a recently found Logic of Proofs (LP) which enjoys a natural provability semantics, is complete, and able to realize the whole of S4.
The Logic of Proofs is becoming a working tool in Computer Science addressing problems which lie outside the scope of the traditional logical machinery. In this talk we will discuss several applications of the Logic of Proofs. In the areas of lambda-calculi and typed theories, LP brings in a much richer system of types capable of iterating the type assignment, in particular, self-referential types. In the context of typed programming languages LP provides a theory of data types containing programs. In the area of knowledge representation LP allows us to approach classical logical omniscience problem, which addresses a failure of the traditional logic of knowledge to distinguish between given facts, like logical axioms on one hand and knowledge which can be only obtained after a long derivation process. The proof carrying formulas of LP naturally make this distinction.
The underlying question of propositional proof complexity is amazingly simple: when interesting propositional tautologies possess efficient proofs in a given (propositional) proof system? This theory makes an integral part of more general theory of feasible provability (not necessarily propositional), the latter being widely considered as the proof theory for the world of efficiently computable objects. Other motivations for studying complexity of propositional proofs come from algebra, automated theorem proving and, of course, computational (especially circuit) complexity.
Given its mixed origin, the methods currently employed in this area are also very diverse. In this introductory talk I will try to illustrate some of them and give the audience at least some feeling of the current state of the art in the area.
``Briareus was a hundred-handed creature with fifty heads. During the battle against the Titans, Briareus took advantage of his one hundred hands by throwing rocks at the Titans.'' Whereas, the problems like ``take $N$ balls from one room to another by means of a robot with $k$ grips'', are typical combinatorially exploded examples for AIPS Planning Competitions.
Since the typical AI problem of making a plan of the actions to be performed by a robot so that it could get into a set of final situations, if it started with a certain initial situation, is generally exponential (it is even EXPTIME-complete in the case of games `Robot against Nature'), the AI planners are very sensitive to the number of variables, the inherent symmetry of the problem, and the nature of the logic formalisms being used.
We have established a clear and easy-to-check syntactical criterion for detecting symmetry in planning domains, and developed techniques to break the extreme combinatorial explosion caused by the symmetry by reducing the unbounded number of `real' objects to a single `generic' object, and contracting thereby the exponential search space over `real' objects to a small polynomial search space but over the `generic' one, with providing a more abstract formulation whose solutions are proved to be directly translatable into polytime solutions to the original problem.
From the technical point of view, we take advantage of linear logic formalism, where the fact that ``one copy of $b$ has property $P$, and another has property $Q$'' can be recorded as a formula of the form $(P(b)\otimes Q(b))$. Notice that the situation is generally more subtle and messy, in particular, $(P(b)\otimes Q(b))$ can be interpreted (and used!) as ``one and the same copy of $b$ has both properties $P$ and $Q$''.
In closing, I would speculatively explain that Briareus won because he took advantage of his `multiset' logic (fifty heads!), as well.
This is a joint paper with Jacqueline Vauzeilles (U. Paris-Nord).
Reactive systems are systems that continuously and dynamically interact with their environment. The system and the environment can be viewed as two players playing a game. While the environment tries to give adversarial inputs to the system, the system tries to "play" in such a way so as to meet its requirement specification. Viewing reactive systems as games has met with success in various problems in formal methods. In this talk, we present two recent results that exploit this connection.
In the first part of the talk, we look at games on recursive state machines. Recursive state machines (RSMs) naturally model the control-flow of software modules with procedure calls and returns. We consider the problem of solving multi-player games on RSMs, which has applications to verifying compatibility of software modules and can be used to formalize interfaces. The main result is that the problem of solving this game is decidable for various specification mechanisms such as reachability, safety and LTL specifications. The complexity of the procedure is linear in the the size of the RSM and exponential in the total number of exits.
In the second half of the talk, we address the synthesis problem for distributed systems. Consider n agents that interact with the environment at different speeds, and communicate with each other at various points in time. We want to automatically design strategies for each agent so that they meet a common goal. Solving such a problem has applications in distributed control (the strategies are the controllers) and in synthesizing communication protocols. The problem is in general undecidable and notoriously hard to tame to decidability. We identify three restrictions under which the problem becomes decidable. Furthermore, if any of these restrictions are dropped, we show that the problem becomes undecidable.
We conclude with some results in ongoing work on implementing game-solvers using methods that have been effective in model-checking, such as symbolic exploration using BDDs and SAT-solvers.
In this talk we discuss Goedel sentences for bounded arithmetic.
Descriptive complexity studies the asymptotic computational effort required to evaluate logical queries on finite databases, with a focus on queries expressed by first-order or fixed-point formulas. In general, these queries require a polynomial amount of time with respect to the size of the structure. We illustrate the special case of how monadic first-order formulas can be evaluated in linear-time on ordinary data structures. We even extend this to monadic fixed-point formulas, leading to the possibility of providing a logical characterization of linear-time computability.
In this paper, we develop a new substructural logic that can encode invariants necessary for reasoning about hierarchical storage. We show how the logic can be used to describe the layout of bits in a memory word, the layout of memory words in a region, the layout of regions in an address space, or even the layout of address spaces in a multiprocessing environment. We provide a semantics for our formulas and then apply the semantics and logic to the task of developing a type system for Mini-KAM, a simplified version of the abstract machine used in the ML Kit with regions.
A survey of attempts to repair Frege's inconsistent system, with emphasis on recent ideas of Harvey Friedman.
Categorical investigations have disclosed an algebraic theory for ``interval algebras'' which looks like it will allow a good part of real analysis to be subsumed in an equational theory. Its intended model is the closed real interval, identifiable in many categories as -- ironically -- a final co-algebra. This later characterization (sometimes referred to as a "coinductive definition") forces the algorithms for much of the structure.
There are a number of completeness theorems, the most interesting of which is a consequence of the remarkable fact that every non-trivial algebra of this finitely presented equational theory has a simple quotient and that any simple algebra appears uniquely as a subalgebra of the intended model. This provides purely algebraic proofs of things such as the Dedekind completion for the reals.
Lamport diagrams are partial orders which depict computations of message passing systems. It is natural to consider generalizations of linear time temporal logics over such diagrams. In our earlier work, we presented a decidable temporal logic with local temporal modalities and a global `previous' modality to talk of message receipts.
It seems reasonable to extend the logic with a global `next' modality as well, so that sending of messages may also be easily specified, but this (or other similar attempts) lead to undecidability. Hence we consider ways of restricting the models so as to obtain decidability, while retaining the expressiveness of global `next' and global `previous' modalities. For this, we consider Lamport diagrams presented as a sequence of {\em layers}. The layers themselves describe finite communication patterns and a diagram is obtained by sequential composition of such parallel processes. The logic is defined appropriately, with layer formulas describing processes within a layer, and temporal formulas describing the sequence of layers in the computation. When the number of events in layers is uniformly bounded and each layer is communication closed, we get decidability. Alternatively, a stronger uniform bound on what we term channel capacity also yields decidability. We present an example of system specification in the logic.
Scenario-based specifications such as message sequence charts offer an intuitive and visual way of describing design requirements. Such specifications focus on message exchanges among communicating entities in distributed software systems, and form an integral part of modern software design environments such as UML. Requirements expressed using MSCs have been given formal semantics, and hence, can be subjected to analysis to reveal inconsistencies. This talk surveys algorithms for a variety of such analyses including detecting race conditions, inferring implied scenarios, and model checking with respect to temporal logic requirements.
This talk reports on recent work in what has been called ``Mac Lane set theory'', a categorical set theory with a global membership relation among the objects. In contrast to elementary topos theory, such categories of sets model elementary set theory directly. We use the methods developed by Joyal and Moerdijk, employing an axiomatic notion of a system of small maps in a category of classes, which serve to limit comprehension in a new and flexible way. We show that *every* elementary topos arises as such a category of sets, and that (a certain) elementary set theory is deductively complete with respect to such topos models. An further new result in this connection is that the axiom scheme of full Replacement is conservative over bounded intuitionistic Zermelo set theory.
To investigate computability is to analyze symbolic processes that can, in principle, be carried out by calculators. This is a philosophical lesson we owe to Turing. Drawing on and recasting work of Alan Turing and Robin Gandy, I formulate finiteness and locality conditions for two types of calculators, human computing agents and mechanical computing devices; the distinctive feature of the latter is that they operate in parallel.
Church's and Turing's Theses assert, dogmatically, that an informal notion of computability (or effective calculability) is captured by a particular precise mathematical concept. I will present a conceptual analysis of computations, which dispenses with theses. The analysis leads instead to axioms for discrete dynamical systems (representing human and machine computations) and allows the reduction of models of these axioms to Turing machines.
In this talk, we will introduce the concept of a compositional analysis and System I, an intersection type system, that provides such an analysis. Compositional analyses allow for, among other things, efficient incremental analysis and separate compilation. Compositionality in System I is made possible by introducing the notion of expansions and expansion variables. We will conclude with a discussion of work in progress on different proposals for extending System I with with sum types.
A process terminates if it does not have an infinite sequence of reductions P -> P_1 -> P_2 ...
Termination is a useful property in concurrency. For instance, termination may be useful to show that when a given service is interrogated, it will eventually produce an answer. Similarly, a terminating applet, when loaded on a machine, will not run for ever on the machine, possibly absorbing all computing resources (a `denial of service' attack).
We ensure termination of a non-trivial subset of the pi-calculus by a combination of conditions based on types and on the syntax.
The proof of termination is in two parts. The first uses the technique of logical relation -- a well-know technique of lambda-calculi -- on a small set of `functional' processes. The second part of the proof uses techniques of process calculi, in particular techniques of behavioural preorders.