SDRL
Systems Design Research Lab
 
 

Question or Comment
Contact: Valentina Sokolskaya
Last updated: January 31, 07

Seminars

 

We have seminars together with Logic and Computation Group
each Monday at 4:30PM
University of Pennsylvania, DRL 4C8

You can see the same list of seminars on Logic and Computation Group seminar page

Also we participate in the seminars of the hybrid systems group

Spring - Fall 2003

Fall 2002

Spring 2002

Fall 2001

Spring 2001

Fall 2000

Spring 2000

Fall 1999

Hardness assumptions in complexity theory

  Jan Krajicek
Mathematical Institute of the Czech Academy of Sciences and IAS

Monday, March 22, 2004,
4:30PM     DRL 4C8

I shall describe several main conjectures in complexity theory and discuss whether there is a common "hardness assumption" behind them (or few of such assumptions of a "similar" nature). I will look in some detail at proof complexity (i.e. the NP/coNP problem). The talk does not presuppose deeper knowledge of complexity theory than basic definitions.

Back to seminars list

Hilbert's Tenth Problem for function fields of complex surfaces

  Kirsten Eisentraeger
IAS

Monday, February 16, 2004,
4:30PM     DRL 4C8

Hilbert's Tenth Problem in its original form is the following: Is there an algorithm that determines, given a multivariate polynomial equation with integer coefficients, whether the equation has a solution over the integers?
Davis-Putnam-Robinson-Matiyasevich showed that there is no such algorithm, i.e., Hilbert's Tenth Problem is undecidable. Since then the analogue of this question has been studied for various rings. I will discuss the result by Kim and Roush that Hilbert's Tenth Problem for C(t,s) is undecidable, and show how their result can be generalized to finite extensions of C(t,s), i.e., to function fields of complex surfaces.

Back to seminars list

Diagonalization, language, and sentences that `speak about themselves'

  Haim Gaifman
Columbia University

Monday, February 2, 2004,
4:30PM     DRL 4C8

Goedel's 1931 proof of the incompleteness theorem is rooted in Cantor's 1891 discovery of diagonalization. The historical route reflects the train of ideas that, probably, led Goedel to his proof. It also leads naturally to the proof of the fixed point theorem, first stated by Carnap in 1934. There is an obvious further link to Kleene's 1938 recursion theorem. This kind of analysis can yield new insight, and a general theorem, of which the fixed point and recursion theorems are special cases. The setup is essentially linguistic, where "language" is conceived in a broad way. It suggests new ways of applying the diagonalization technique, in non-customary cases of "language".

Back to seminars list

Program Semantics and Quantum Mechanics

  Keye Martin
University of Oxford

Monday, January 26, 2004,
4:30PM     DRL 4C8

Domains were originally introduced by D. Scott and others as an appropriate mathematical universe for the semantics of programming languages. The original viewpoint was "higher order" in nature, e.g., a recursive algorithm was a least fixed point of a continous map on a domain -- in particular, an element of a domain. In the speaker's thesis, a "first order" view is taken, e.g., a recursive algorithm is now a function x on a domain satisfying a relation like x = a + b;x and domains are exactly the data types we program with (lists, natural numbers, booleans, etc).
The desire to analyze algorithms quantitatively (e.g., accuracy, complexity) in the first order view partly motivates the study of measurement: if a domain is a collection of informative objects, a measurement is a map on a domain that specifies the amount of information each object possesses. Measurement makes a number of things possible in domain theory that previously were not. One of these is the recent discovery that quantum mechanics has a natural domain theoretic structure, which is the focus of this talk.
The set of classical states form a domain with Shannon entropy as a measurement, and this order -- the Bayesian order -- extends to the set of quantum states in such a way that it too forms a domain with von Neumann entropy as a measurement. In the simplest of terms: `Entropy' is to quantum state as `length' is to list, or `domain' is to partial function. By taking domains and measurements as the basis for a form of kinematics, we will see that certain algorithms can be analyzed as though they were objects moving in space. In particular, Grover's algorithm for quantum searching is like a projectile fired into the air which reaches its zenith and then falls back to the ground -- the amount of time required for the projectile to reach its maximum height is the complexity of the algorithm.
We may as time permits also consider some uses for these domains within theoretical physics, and perhaps their connection to a certain type of Lie algebra.
http://web.comlab.ox.ac.uk/oucl/work/keye.martin

Back to seminars list

Bridging logic and combinatorics

  Max Kanovich
University of Pennsylvania

Monday, December 12, 2003,
4:30PM     DRL 4C8

The aim of this talk is to show how techniques from the formal logic world can sometimes be applied directly to specific mathematical problems studied completely independently in the world of combinatorics.
One basic activity in combinatorics is to establish combinatorial identities by so-called `bijective proofs,' which consist in constructing explicit bijections between two types of the combinatorial objects under consideration.
Based on the author's two-directional multiset rewriting technique and reasonably `restricted' two-directional strong normalization, recently I have fully characterized all equinumerous partition ideals whose complementary order filters are generated by pairwise disjoint minimal elements, with providing, in addition, the most `natural bijections' between the partition ideals.
Along the above transparent `geometrical' lines, I will show a much stronger bijection form of Andrews's and Subbarao's results on so-called `Euler pairs', and, moreover, I will fully characterize the class of all Euler-like partition identities, in which the number of repeated parts is variable and controlled by some function.
In the second, "overlapping", part of my talk, I discuss the challenges of the `overlapping' multiset rewriting systems. I will show the `bijective proofs' (based on the two-directional multiset rewriting technique indeed) of a new series of partition identities related to Fibonacci and Lucas numbers.
In closing, I will show a much stronger form of the above `bijective proofs' - that the related fine partition statistics have identical distribution functions.
No acquaintance with partitions, etc. is required.

Back to seminars list

Forcing in proof theory

  Jeremy Avigal
Carnegy Mellon University

Monday, November 24, 2003,
4:30PM     DRL 4C8

Paul Cohen's method of forcing, together with Saul Kripke's related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. In this talk, I will argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or combinatorial terms. I will discuss the aspects of forcing that are useful in this respect, and offer some examples, including constructivizing model-theoretic arguments, translating classical theories to constructive ones, and obtaining conservation results for subsystems of second-order arithmetic.

An associated paper is available online, http://www.andrew.cmu.edu/~avigad, under "surveys".

Back to seminars list

Responsiveness of Interoperating Components

  Joy Reed
Armstrong Atlantic State University

Monday, September 29, 2003,
4:30PM     DRL 4C8

I will discuss the issue of responsiveness of interoperating components: one not causing the other to deadlock. In CSP process algebra terms, responsiveness can be captured for deadlock-free processes by simply requiring their parallel composition to be deadlock-free. However, the issue becomes more subtle when dealing with processes which can non-deterministically block, either through graceful termination or unfortunate deadlock. Our contribution is to define appropriate properties which can be mechanically checked, and to demonstrate the suitability of these properties as a characterization of responsiveness. Our formulation is relational. Relational properties are not in general preserved by refinement, but significantly, our formulation is refinement-closed. Model-checking is provided by the FDR tool.

This is joint work with Jane Sinclair, Univ. of Warwick, England.

Back to seminars list

An automata-theoretic approach to Constraint LTL

  Deepak D'Souza
Indian Institute of Science

Monday, May 12, 2003,
4:30PM     DRL 4C8

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.

Back to seminars list

Goedel and Carnap: Influence and Opposition

  Warren Goldfarb
Harvard

Monday, April 28, 2003,
4:30PM     DRL 4C8

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.

Back to seminars list

Bisimulations and Boolean Matrices

  Melvin Fitting
Lehman College, CUNY

Monday, April 21, 2003,
4:30PM     DRL 4C8

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.

Back to seminars list

Proof carrying formulas and reflective lambda-calculus

  Sergei Artemov
Graduate Center, CUNY

Monday, April 14, 2003,
4:30PM     DRL 4C8

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.

Back to seminars list

Complexity of Propositional Proofs

  Alexander Razborov
Institute for Advanced Study, Princeton
and Steklov Mathematical Institute, Moscow

Monday, April 7, 2003,
4:30PM     DRL 4C8

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.

Back to seminars list

Why did Briareus succeed in doing what the modern planners fail,
or Coping polynomially with numerous but identical elements

  Max Kanovitch
University of Pennsylvania

Monday, March 17, 2003,
4:30PM     DRL 4C8

"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).

Back to seminars list

Games for Verification and Control of Reactive Systems

  P. Madhusudan
University of Pennsylvania

Monday, March 13, 2003,
4:30PM     DRL 4C8

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.

Back to seminars list

Goedel Sentence

  Gaisi Takeuti
University of Pennsylvania

Monday, March 3, 2003,
4:30PM     DRL 4C8

In this talk we discuss Goedel sentences for bounded arithmetic.

Back to seminars list

Linear-time algorithms for Monadic Logic

  Steven Lindell
Haverford College

Monday, February 24, 2003,
4:30PM     DRL 4C8

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.

Back to seminars list

Reasoning about Hierarchical Storage

  Amal Ahmed
Prinston University

Monday, February 10, 2003,
4:30PM     DRL 4C8

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.

Back to seminars list

Fixing Frege

  John Burgess
Prinston University

Monday, January 27, 2003,
4:30PM     DRL 4C8

A survey of attempts to repair Frege's inconsistent system, with emphasis on recent ideas of Harvey Friedman.

Back to seminars list

Algebraic Real Analysis

  Peter Freyd
University of Pennsylvania

Monday, January 13 and 20, 2003,
4:30PM     DRL 4C8

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.

Back to seminars list

Reasoning about layered message passing systems

  B. Meenakshi
Institute of Mathematical Sciences, Chennai, India

Monday, January 6, 2003,
4:30PM     DRL 4C8

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 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.

Back to seminars list