Logic and Program Semantics

We show that there is no finitely axiomatizable class of algebras that would serve as an analogue to Kozen’s class of Kleene algebras if we include the residuals of composition in the similarity type of relation algebras.

We give a new presentation of Brzozowski’s algorithm to minimize finite automata, using elementary facts from universal algebra and coalgebra, and building on earlier work by Arbib and Manes on the duality between reachability and observability. This leads to a simple proof of its correctness and opens the door to further generalizations.

We describe our development and use of DescriptiveEnvironment (DE). This is a program to aid researchers in Finite Model Theory and students of logic to automatically generate examples, counter- examples of conjectures, reductions between problems, and visualizations of structures and queries.

DescriptiveEnvironment is available for free use under an ISC license at

http://www.cs.umass.edu/~immerman/de

. We encourage researchers and students at all levels to experiment with it. Please tell us of your insights, progress, suggestions, or extensions of DE.

The quantified constraint satisfaction problem (QCSP) is the problem of deciding, given a structure and a first-order prenex sentence whose quantifier-free part is the conjunction of atoms, whether or not the sentence holds on the structure. One obtains a family of problems by defining, for each structure

B

, the problem

QCSP

(

B

) to be the QCSP where the structure is fixed to be

B

. In this article, we offer a viewpoint on the research program of understanding the complexity of the problems

QCSP

(

B

) on finite structures. In particular, we propose and discuss a group of conjectures; throughout, we attempt to place the conjectures in relation to existing results and to emphasize open issues and potential research directions.

Robotics researchers will be aware of Dexter Kozen’s contributions to algebraic algorithms, which have enabled the widespread use of the theory of real closed fields and polynomial arithmetic for motion planning. However, Dexter has also made several important contributions to the theory of information invariants, and produced some of the most profound results in this field. These are first embodied in his 1978 paper

On the Power of the Compass

, with Manuel Blum. This work has had a wide impact in robotics and nanoscience.

Starting with Dexter’s insights, robotics researchers have explored the problem of determining the information requirements to perform robot tasks, using the concept of

information invariants.

This represents an attempt to characterize a family of complicated and subtle issues concerned with measuring robot task complexity.

In this vein, several measures have been proposed [14] to measure the information complexity of a task: (a) How much internal state should the robot retain? (b) How many cooperating robots are required, and how much communication between them is necessary? (c) How can the robot change (side-effect) the environment in order to record state or sensory information to perform a task? (d) How much information is provided by sensors? and (e) How much computation is required by the robot? We have considered how one might develop a kind of “calculus” on (a) – (e) in order to compare the power of sensor systems analytically. To this end, information invariants is a theory whereby one sensor can be “reduced” to another (much in the spirit of computation-theoretic reductions), by adding, deleting, and reallocating (a) – (e) among collaborating autonomous robots. As we show below, this work steers using Dexter’s compass.

Equirecursive types

consider a recursive type to be equal to its unrolling and have no explicit term-level coercions to change a term’s type from the former to the latter or vice versa. This equality makes deciding type equality and subtyping more difficult than the other approach—

isorecursive types

, in which the types are not equal, but isomorphic, witnessed by explicit term-level coercions. Previous work has built intuition, rules, and polynomial-time decision procedures for equirecursive types for first-order type systems. Some work has been done for type systems with parametric polymorphism, but that work is incomplete (see below). This chapter will give an intuitive theory of equirecursive types for second-order type systems, sound and complete rules, and a decision procedure for subtyping.

An H-tree is a formal model of evolutionary scenario. It can be used to represent any processes with gene duplication and loss, horizontal gene transfer (HGT) and speciation events. The model of H-trees, introduced in [26], is an extension of the duplication-loss model (DL-model). Similarly to its ancestor, it has a number of interesting mathematical and biological properties. It is, however, more computationally complex than the DL-model. In this paper, we primarily address the problem of inferring H-trees that are compatible with a given gene tree and a given phylogeny of species with HGTs. These results create a mathematical and computational foundation for a more general and practical problem of inferring HGTs from given gene and species trees with HGTs. We also demonstrate how our model can be used to support HGT hypotheses based on empirical data sets.

We present a side by side comparison of

Capsules

and

Closures

, including a proof of bisimilarity, using small-step semantics. A similar proof was presented in [8], using big-step semantics. However, while big-step semantics only allow to talk about final results of terminating computations, the use of small-step semantics allows to prove a stronger bisimilarity involving every step of the computation and thus also applicable to infinite computations.

We describe the construction of a semi-automated proof system for elementary category theory using the Nuprl proof development system as logical framework. We have used Nuprl’s display mechanism to implement the basic vocabulary and Nuprl’s rule compiler to implemented a first-order proof calculus for reasoning about categories, functors and natural transformations. To automate proofs we have formalized both standard techniques from automated theorem proving and reasoning patterns that are specific to category theory and used Nuprl’s tactic mechanism for the actual implementation. We illustrate our approach by automating proofs of natural isomorphisms between categories.

Streams are omnipresent in both mathematics and theoretical computer science. Automatic sequences form a particularly interesting class of streams that live in both worlds at the same time: they are defined in terms of finite automata, which are basic computational structures in computer science; and they appear in mathematics in many different ways, for instance in number theory. Examples of automatic sequences include the celebrated Thue-Morse sequence and the Rudin-Shapiro sequence. In this paper, we apply the coalgebraic perspective on streams to automatic sequences. We show that the set of automatic sequences carries a final coalgebra structure, consisting of the operations of head, even, and odd. This will allow us to show that automatic sequences are to (general) streams what rational languages are to (arbitrary) languages.

We identify the class of

${\bf\Sigma}^{1}_{1}$

–inductive sets studied by Moschovakis as a set theoretical generalization of the class (1,3) of the Rabin-Mostowski index hierarchy of alternating automata on infinite trees. That is, we show that every tree language recognized by an alternating automaton of index (1,3) is

${\bf\Sigma}^{1}_{1}$

–inductive, and exhibit an automaton whose language is complete in this class w.r.t. continuous reductions.

This paper presents a sound and complete logical system whose atomic sentences are the equalities of recursive terms involving sets. There are two interpretations of this language: one makes use of non-wellfounded sets with finite transitive closure, and the other uses pointed finite graphs modulo bisimulation. Our logical system is a sequent-style deduction system. The main axioms and inference rules come from the

$\mbox{{\it FLR}$_0$}$

-proof system from [6], including the Recursion Inference Rule (but an additional axiom is needed), and also axioms corresponding to the extensionality axiom of set theory.

We show that overloading is NP-complete. This solves exercise 6.25 in the 1986 version of the Dragon book.

We define an epistemic logic for labelled transition systems by introducing equivalence relations for the agents on the states of the labelled transition system. The idea is that agents observe the dynamics of the system modulo their ability to distinguish states and in the process learn about the current state and past history of the execution. This is in the spirit of dynamic epistemic logic but is a direct combination of Hennessy-Milner logic and epistemic logic. We give an axiomatization for the logic and prove a completeness theorem with respect to the class of models obtained by unfolding labelled transition systems.

We consider an agent choosing between two acts

A

,

B

, whose outcomes are uncertain and depend on factors which the agent does not fully know. But for each pair of possible outcomes the agent does know how she would choose. Does the agent then have a way of choosing between the acts which will work at least some of the time?

It is shown that the inhabitation problem for intersection types without the intersection introduction rule is

Expspace

-complete and that the further restriction without subtyping is

Pspace

-complete.

The paper investigates sequences generated by

reaction systems

. Arbitrary sequences can be generated if the cardinalities of the sets of

reactants

and

inhibitors

are unbounded. Most of the paper investigates systems where both of these cardinalities equal 1. A general result is obtained concerning sequences generated by systems with

interaction

. New estimates are obtained for lengths of sequences in the non-interactive case.

An undirected graph

G

 = (

V

,

E

) is (

d

,

k

)

-colorable

if there is a vertex coloring using at most

k

colors such that no two vertices within distance

d

have the same color. It is well known that (1,2)-colorability is decidable in linear time, and that (1,

k

)-colorability is

NP

-complete for

k

 ≥ 3. This paper presents the complexity of (

d

,

k

)-coloring for general

d

and

k

, and enumerates some interesting properties of (

d

,

k

)-colorable graphs. The main result is the dichotomy between polynomial and

NP

-hard instances: for fixed

d

 ≥ 2, the distance coloring problem is polynomial time for

$k \leq \lfloor \frac{3d}{2} \rfloor$

and NP-hard for

$k > \lfloor \frac{3d}{2} \rfloor$

. We present a reduction in the latter case, as well as an algorithm in the former. The algorithm entails several innovations that may be of independent interest: a generalization of tree decompositions to overlay graphs other than trees; a general construction that obtains such decompositions from certain classes of edge partitions; and the use of homology to analyze the cycle structure of colorable graphs. This paper is both a combining and reworking of the papers of Sharp and Kozen [14, 10].

Nondeterministic concurrent strategies—those strategies compatible with copy-cat behaving as identity w.r.t. composition—have been characterised as certain maps of event structures. This leads to a bicategory of general concurrent games in which the maps are nondeterministic concurrent strategies. This paper explores the consequences of extending concurrent games with (1) winning, losing and, implicitly, neutral configurations, and (2) access levels, to address situations where Player or Opponent have imperfect information as to what has occurred in the game. In both cases winning strategies are shown to form bicategories of games. The bicategories become equivalent to order-enriched categories when restricted to deterministic strategies.

“Choose as an advisor someone you can see yourself being in ten years.” Those were the words spoken to me by a fellow graduate student at Cornell University. It is a task that is easier said than done. How do I know who I want to be in ten years, let alone find someone who embodies those qualities? Through an incredible set of circumstances, I ended up working with an advisor who represented the person I wanted to be in ten years, Dexter Kozen. In the four and a half years I had the privilege of working with Dexter, I learned many lessons I have carried with me through graduate school and beyond to my life as a software engineer and manager.

Dexter was my manager during the first 8 months or so of my one year stay at the IBM Research Center at Yorktown Heights in the mid eighties. Our interaction in terms of scientific output was very slim — it consisted of just a single paper, titled “Limits for automatic verification of finite-state concurrent systems.” The paper appeared in 1986 in

Information Processing Letters

and had just 3 pages. Still, it has 275 citations on Google scholar, so more than 90 citations per page. I believe it is the best per page citation ratio for both of us.

Dexter has played music for most of his life and playing music is something that gives him great enjoyment. As a member of the band, Dexter has always been the organizer and musical director. Dexter is multitalented. He can play guitar, piano, and sing, all well enough to be done in public. As fellow band members we know when things are going well during a set because Dexter will have a huge grin on his face. Recently, Dexter has added Rapping to his repertoire. He has a really stellar performance that has yet to be presented to an audience!

Dexter is unabashedly and unequivocally exuberant for music. His kid like charm and enthusiasm has always been an inspiration to both his fellow band members and the audience. Dexter’s enthusiasm for music makes it a blast to get together for practice and gigs. In addition to playing in the band, Dexter’s enthusiasm stretches to acting as chief ‘roadie’. Dexter trucks all of our equipment around in his van. This is a real effort as he has to load the van before the gig and then unload it when he gets home. For anyone who has ever wondered what that it is like - let me tell you it’s a lot of work. Most guitar amps weigh at least 50-60 lb so loading and unloading is hard manual labor. From all of us in the band, Happy 60th birthday Dexter. I think that I speak for all the members of the current band and past bands in saying that it is a total blast to play music with you! Here’s a toast to you and to playing music with you for many more years.

I have known Dexter for 30 years, which, of course, means that I was 9 when I first met him. At that time, Dexter was already “the man”. Although he was only a few years ahead of me, he had already made his name by independently defining the notion of alternating Turing machines, a deep contribution to complexity theory that made it possible to connect time and space complexity. The results were viewed as so significant that it was already being taught in a graduate course on complexity theory that I attended. Of even more interest to me at the time was Dexter’s work on modal logic, since a large part of my thesis was on dynamic logic. Finding a sound and complete axiomatization for dynamic logic had been an open problem for many years. Krister Segerberg had suggested an obviously sound axiomatization, but couldn’t prove it complete. Rohit Parikh [7] showed that it was indeed complete, but his proof was rather complicated. Dexter then came up with a much simpler proof, one that got at the essence of Rohit’s ideas; this version was published as [6]. The proof is truly beautiful. I have taught it often, and used the ideas in a number of subsequent papers (e.g., [3,4]).

This is a somewhat non-standard piece about Dexter Kozen, longtime colleague and friend. I am sure that the praise of Dexter’s research will have been sung by many of the people contributing to this volume. I could probably have added my own perspective, talking at length about the enormous impact of his most profound work. For example, the wonderful paper on alternation influenced my work on seemingly unrelated topics years later, in many unexpected ways.

The papers in this book detail Dexters research contributions, which are profound. I would like to highlight another contribution Dexter has made that affects us all in the department every day

My husband Neil Immerman returned from the 1986 STOC meeting with an interesting proposition. Juris Hartmanis and Dexter Kozen had a small pocket of funds, and they proposed that the two of us visit the Cornell Computer Science Department for a week.

I have known and admired Dexter since the time long ago when Juris Hartmanis was chairman of his PhD committee and I was a member. Shortly after he came back to Cornell as a professor an occasion arose when he thought to ask why I had not attended his qualifying exam. I told him that Juris had to because he was chair, but that I avoided exams that were superfluous. I am not much on “rites of passage”.

In the Fall of 1985 Dexter and I both started at Cornell as new faculty members in the celebrated Computer Science Department, home to luminaries such as Juris Hartmanis, John Hopcroft, David Gries and Robert Constable. I was a very new assistant professor but Dexter was already an acknowledged star with celebrated contributions to several areas: algebra and complexity, decision procedures for real-closed fields [1], dynamic logic [2-4] and many other areas across both tracks of theoretical computer science. I had no doctorate in computer science, hardly any publications and no clearly defined research area. Early in the term Dexter summoned me to his office and grilled me about work I was doing on nondeterministic dataflow. After that meeting I needed several glasses of beer to recover but a lasting friendship was sealed.

I met Dexter Kozen in October 1979 at the FOCS meeting in Puerto Rico where he gave a paper on the semantics of probabilistic programs. The main reason for our discussion at that meeting was the fact that he was the referee of a paper which I had submitted to

Theoretical Computer Science - TCS

with Albert Meyer as editor.

At Aarhus University, we consider Dexter to be one of our oldest and best friends and colleagues. Dexter has visited our Department of Computer Science as a guest professor twice, first in 1981–1982 and again, exactly 10 years later, in 1991–1992. Both visits were immensely successful and laid the ground for continued cooperation during the following years. Dexter made numerous shorter visits to the department, and he served with great enthusiasm and competence on the advisory board for BRICS (Basic Research in Computer Science) Research Center and international PhD-School. BRICS covered both “Track A and B” activities (Algorithmics and Semantics), and as such Dexter was the ideal adviser. Looking back, we pay tribute to Dexter for his many contributions to computer science in Aarhus over a period of more than thirty years.

Aside from our shared interest in particular areas of Theoretical Computer Science, the experience I share with Dexter Kozen originates from the fact that we both belong to the not too large group of Theoreticiancs who during the late 1970-ies and early 1980-ies frequently crossed the Iron Curtain in order to interact with our colleagues from the Socialist part of Europe. This results into many appearances of Dexter in my collection of pictures from that period; a collection I like to share with the readers of this volume.

Dexter and I work in very different areas in Computer Science, so I cannot attest to his successes in Computer Science as I am sure others so eloquently will. However, I was Dexter’s first PhD graduate, and I can certainly attest to his skills as a PhD advisor. Dexter actually arrived at Cornell after I started my PhD program. He had a buzz of electricity about him and that quality above all others initially attracted my interest. At that time Dexter was already an accomplished theoretician. I know that he has considerably burnished that already formidable reputation in the intervening decades. My story is a different one though, and it winds through the area of graphical user interfaces.

I am not a student, colleague or co-author of Dexter’s, yet his person and his work have influenced and inspired me since my graduate student days, a time when Dexter already was a towering figure in the minds of students interested in theoretical computer science.