Dexter Kozen

CSL Conference 2025 Conference Paper

Classical Linear Logic in Perfect Banach Lattices

• Pedro H. Azevedo de Amorim
• Leon Witzman
• Dexter Kozen

In recent years, researchers have proposed various models of linear logic with strong connections to measure theory, with probabilistic coherence spaces (PCoh) being one of the most prominent. One of the main limitations of the PCoh model is that it cannot interpret continuous measures. To overcome this obstacle, Ehrhard has extended PCoh to a category of positive cones and linear Scott-continuous functions and shown that it is a model of intuitionistic linear logic. In this work we show that the category PBanLat₁ of perfect Banach lattices and positive linear functions of norm at most 1 can serve the same purpose, with some added benefits. We show that PBanLat₁ is a model of classical linear logic (without exponential) and that PCoh embeds fully and faithfully in PBanLat₁ while preserving the monoidal and *-autonomous structures. Finally, we show how PBanLat₁ can be used to give semantics to a higher-order probabilistic programming language.

Highlights Conference 2022 Conference Abstract

25 Years of KAT

• Dexter Kozen

Kleene algegra with tests (KAT) is a system for equational reasoning about imperative programs. The system is based on Kleene algebra, the algebra of regular expressions. In this talk I will trace the origins of the system and survey past and recent results on expressiveness, decision complexity, and deductive completeness, along with various applications, including correctness of compiler optimizations and verification of packet switching networks.

TCS Journal 2020 Journal Article

Left-handed completeness

• Dexter Kozen
• Alexandra Silva

We give a new proof of the completeness of the left-handed star rule of Kleene algebra. The proof is significantly shorter than previous proofs and exposes the rich interaction of algebra and coalgebra in the theory of Kleene algebra.

CSL Conference 2018 Conference Paper

The Ackermann Award 2018

• Dexter Kozen
• Thomas Schwentick

The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2018 edition of the award.

CSL Conference 2015 Conference Paper

The Ackermann Award 2015

• Anuj Dawar
• Dexter Kozen
• Simona Ronchi Della Rocca

The eleventh Ackermann Award is presented at CSL'15 in Berlin, Germany. This year, again, the EACSL Ackermann Award is generously sponsored by the Kurt Gödel Society. Besides providing financial support for the Ackermann Award, the Kurt Gödel Society has also committed to inviting the recipients of the Award for a special lecture to be given to the Society in Vienna.

CSL Conference 2013 Conference Paper

Kleene Algebra with Products and Iteration Theories

• Dexter Kozen
• Konstantinos Mamouras

We develop a typed equational system that subsumes both iteration theories and typed Kleene algebra in a common framework. Our approach is based on cartesian categories endowed with commutative strong monads to handle nondeterminism.

MFCS Conference 2013 Conference Paper

Strong Completeness for Markovian Logics

• Dexter Kozen
• Radu Mardare
• Prakash Panangaden

Abstract In this paper we present Hilbert-style axiomatizations for three logics for reasoning about continuous-space Markov processes (MPs): (i) a logic for MPs defined for probability distributions on measurable state spaces, (ii) a logic for MPs defined for sub-probability distributions and (iii) a logic defined for arbitrary distributions. These logics are not compact so one needs infinitary rules in order to obtain strong completeness results. We propose a new infinitary rule that replaces the so-called Countable Additivity Rule (CAR) currently used in the literature to address the problem of proving strong completeness for these and similar logics. Unlike the CAR, our rule has a countable set of instances; consequently it allows us to apply the Rasiowa-Sikorski lemma for establishing strong completeness. Our proof method is novel and it can be used for other logics as well.

ICML Conference 2009 Conference Paper

Learning prediction suffix trees with Winnow

• Nikolaos Karampatziakis
• Dexter Kozen

NeurIPS Conference 2007 Conference Paper

Collective Inference on Markov Models for Modeling Bird Migration

• M. a. Elmohamed
• Dexter Kozen
• Daniel Sheldon

We investigate a family of inference problems on Markov models, where many sample paths are drawn from a Markov chain and partial information is revealed to an observer who attempts to reconstruct the sample paths. We present algo- rithms and hardness results for several variants of this problem which arise by re- vealing different information to the observer and imposing different requirements for the reconstruction of sample paths. Our algorithms are analogous to the clas- sical Viterbi algorithm for Hidden Markov Models, which finds the single most probable sample path given a sequence of observations. Our work is motivated by an important application in ecology: inferring bird migration paths from a large database of observations.

TCS Journal 2006 Journal Article

Logic, Language, Information and Computation

• Ruy de Queiroz
• Dexter Kozen

MFCS Conference 2006 Invited Paper

On the Representation of Kleene Algebras with Tests

• Dexter Kozen

Abstract We investigate conditions under which a given Kleene algebra with tests is isomorphic to an algebra of binary relations. Two simple separation properties are identified that, along with star-continuity, are sufficient for nonstandard relational representation. An algebraic condition is identified that is necessary and sufficient for the construction to produce a standard representation.

I&C Journal 2002 Journal Article

On the Complexity of Reasoning in Kleene Algebra

• Dexter Kozen

We study the complexity of reasoning in Kleene algebra and *-continuous Kleene algebra in the presence of extra-equational assumptions E; that is, the complexity of deciding the validity of universal Horn formulas E→s=t, where E is a finite set of equations. We obtain various levels of complexity based on the form of the assumptions E. Our main results are as follows: for *-continuous Kleene algebra, (i) if E contains only commutativity assumptions pq=qp, the problem is Π1 0-complete; (ii) if E contains only monoid equations, the problem is Π2 0-complete; and (iii) for arbitrary equations E, the problem is Π1 1-complete. The last problem is the universal Horn theory of the *-continuous Kleene algebras. This resolves an open question of the author [D. Kozen, 1994, Inform. and Comput. 110, 366–390].

I&C Journal 2002 Journal Article

Tarskian Set Constraints

• Robert Givan
• David McAllester
• Carl Witty
• Dexter Kozen

We investigate set constraints over set expressions with Tarskian functional and relational operations. Unlike the Herbrand constructor symbols used in recent set constraint formalisms, the meaning of a Tarskian function symbol is interpreted in an arbitrary first order structure. We show that satisfiability of Tarskian set constraints is decidable in nondeterministic doubly exponential time. We also give complexity results and open problems for various extensions and restrictions of the language.

MFCS Conference 1999 Conference Paper

Language-Based Security

• Dexter Kozen

Abstract Security of mobile code is a major issue in today’s global computing environment. When you download a program from an untrusted source, how can you be sure it will not do something undesirable? In this paper I will discuss a particular approach to this problem called language-based security. In this approach, security information is derived from a program written in a high-level language during the compilation process and is included in the compiled object. This extra security information can take the form of a formal proof, a type annotation, or some other form of certificate or annotation. It can be downloaded along with the object code and automatically verified before running the code locally, giving some assurance against certain types of failure or unauthorized activity. The verifier must be trusted, but the compiler, code, and certificate need not be. Java bytecode verification is an example of this approach. I will give an overview of some recent work in this area, including a particular effort in which we are trying to make the production of certificates and the verification as efficient and invisible as possible.

I&C Journal 1998 Journal Article

Set Constraints and Logic Programming

• Dexter Kozen

Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are the main ingredient in set-based program analysis. In this paper we describe a constraint logic programming languageclp(sc) over set constraints in the style of J. Jaffar and J. -L. Lassez (1987, “Proc. Symp. Principles of Programming Languages 1987, ” pp. 111–119). The language subsumes ordinary logic programs over an Herbrand domain. We give an efficient unification algorithm and operational, declarative, and fixpoint semantics. We show how the language can be applied in set-based program analysis by deriving explicitly the monadic approximation of the collecting semantics of N. Heintze and J. Jaffar (1992, “Set Based Program Analysis”; 1990, “Proc. 17th Symp. Principles of Programming Languages, ” pp. 197–209).

CSL Conference 1997 Conference Paper

Kleene Algebra with Tests: Completeness and Decidability

• Dexter Kozen
• Frederick Smith

Abstract Kleene algebras with tests provide a rigorous framework for equational specification and verification. They have been used successfully in basic safety analysis, source-to-source program transformation, and concurrency control. We prove the completeness of the equational theory of Kleene algebra with tests and-continuous Kleene algebra with tests over language-theoretic and relational models. We also show decidability. Cohen's reduction of Kleene algebra with hypotheses of the form r =0 to Kleene algebra without hypotheses is simplified and extended to handle Kleene algebras with tests.

TCS Journal 1996 Journal Article

Rational spaces and set constraints

• Dexter Kozen

Set constraints are inclusions between expressions denoting sets of ground terms. They have been used extensively in program analysis and type inference. In this paper we investigate the topological structure of the spaces of solutions to systems of set constraints. We identify a family of topological spaces called rational spaces, which formalize the notion of a topological space with a regular or self-similar structure, such as the Cantor discontinuum or the space of runs of a finite automaton. We develop the basic theory of rational spaces and derive generalizations and proofs from topological principles of some results in the literature on set constraints.

FOCS Conference 1994 Conference Paper

Efficient Average-Case Algorithms for the Modular Group

• Jin-Yi Cai
• Wolfgang H. J. Fuchs
• Dexter Kozen
• Zicheng Liu 0001

The modular group occupies a central position in many branches of mathematical sciences. In this paper we give average polynomial-time algorithms for the unbounded and bounded membership problems for finitely generated subgroups of the modular group. The latter result affirms a conjecture of Y. Gurevich (1990). >

CSL Conference 1994 Conference Paper

Logical Aspects of Set Constraints

• Dexter Kozen

Abstract Set constraints are inclusion relations between sets of ground terms over a ranked alphabet. They have been used extensively in program analysis and type inference. Here we present an equational axiomatization of the algebra of set constraints. Models of these axioms are called termset algebras. They are related to the Boolean algebras with operators of Jónsson and Tarski. We also define a family of combinatorial models called topological term automata, which are essentially the term automata studied by Kozen, Palsberg, and Schwartzbach endowed with a topology such that all relevant operations are continuous. These models are similar to Kripke frames for modal or dynamic logic. We establish a Stone duality between termset algebras and topological term automata, and use this to derive a completeness theorem for a related multidimensional modal logic. Finally, we prove a small model property by filtration, and argue that this result contains the essence of several algorithms appearing in the literature on set constraints.

TCS Journal 1994 Journal Article

Optimal bounds for the change-making problem

• Dexter Kozen
• Shmuel Zaks

The change-making problem is the problem of representing a given value with the fewest coins possible. We investigate the problem of determining whether the greedy algorithm produces an optimal representation of all amounts for a given set of coin denominations 1=c 1<c 2<⋯<c m. Chang and Gill (1970) show that if the greedy algorithm is not always optimal, then there exists a counterexample x in the range c3≤x< cm(cmcm−1+cm−3cm−1) cm−cm−1. To test for the existence of such a counterexample, Chang and Gill propose computing and comparing the greedy and optimal representations of all x in this range. In this paper we show that if a counterexample exists, then the smallest one lies in the range c3+1 <x<cm+cm−1.

CSL Conference 1994 Conference Paper

The Complexity of Set Constraints

• Alexander Aiken
• Dexter Kozen
• Moshe Y. Vardi
• Edward L. Wimmers

Abstract Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. We present several results on the computational complexity of solving systems of set constraints. The systems we study form a natural complexity hierarchy depending on the form of the constraint language.

FOCS Conference 1992 Conference Paper

Efficient Inference of Partial Types

• Dexter Kozen
• Jens Palsberg
• Michael I. Schwartzbach

Partial types for the lambda -calculus were introduced by Thatte (1988) as a means of typing objects that are not typable with simple types, such as heterogeneous lists and persistent data. He showed that type inference for partial types was semidecidable. Decidability remained open until O'Keefe and Wand gave an exponential time algorithm for type inference. The authors give an O(n/sup 3/) algorithm. The algorithm constructs a certain finite automaton that represents a canonical solution to a given set of type constraints. Moreover, the construction works equally well for recursive types. >

MFCS Conference 1990 Invited Paper

On Kleene Algebras and Closed Semirings

• Dexter Kozen

Abstract Kleene algebras are an important class of algebraic structures that arise in diverse areas of computer science: program logic and semantics, relational algebra, automata theory, and the design and analysis of algorithms. The literature contains at several inequivalent definitions of Kleene algebras and related algebraic structures [2, 13, 14, 5, 6, 1, 9, 7]. In this paper we establish some new relationships among these structures. Our main results are: •There is a Kleene algebra in the sense of [6] that is not *-continuous. •The categories of *-continuous Kleene algebras [5, 6], closed semirings [1, 9] and S-algebras [2] are strongly related by adjunctions. •The axioms of Kleene algebra in the sense of [6] are not complete for the universal Horn theory of the regular events. This refutes a conjecture of Conway [2, p. 103]. •Right-handed Kleene algebras are not necessarily left-handed Kleene algebras. This verifies a weaker version of a conjecture of Pratt [14].

I&C Journal 1989 Journal Article

Definability with bounded number of bound variables

• Neil Immerman
• Dexter Kozen

A theory satisfies the k-variable property if every first-order formula is equivalent to a formula with at most k bound variables (possibly reused). Gabbay has shown that a model of temporal logic satisfies the k-variable property for some k if and only if there exists a finite basis for the temporal connectives over that model. We give a model-theoretic method for establishing the k-variable property, involving a restricted Ehrenfeucht-Fraisse game in which each player has only k pebbles. We use the method to unify and simplify results in the literature for linear orders. We also establish new k-variable properties for various theories of bounded-degree trees, and in each case obtain tight upper and lower bounds on k. This gives the first finite basis theorems for branching-time models of temporal logic.

FOCS Conference 1987 Conference Paper

Functional Decomposition of Polynomials

• Joachim von zur Gathen
• Dexter Kozen
• Susan Landau 0001

STOC Conference 1986 Conference Paper

A Fast Parallel Algorithm for Determining All Roots of a Polynomial with Real Roots

• Michael Ben-Or
• Ephraim Feig
• Dexter Kozen
• Prasoon Tiwari

FOCS Conference 1985 Conference Paper

Algebraic Cell Decomposition in NC (Preliminary Version)

• Dexter Kozen
• Chee-Keng Yap

We give an algorithm to construct a cell decomposition of Rd, including adjacency information, defined by any given set of rational polynomials in d variables. The algorithm runs in single exponential parallel time, and in NC for fixed d. The algorithm extends a recent algorithm of Ben-Or, Kozen, and Reif for deciding the theory of real closed fields.

STOC Conference 1984 Conference Paper

Pebblings, Edgings, and Equational Logic

• Dexter Kozen

STOC Conference 1984 Conference Paper

The Complexity of Elementary Algebra and Geometry (Preliminary Abstract)

• Michael Ben-Or
• Dexter Kozen
• John H. Reif

STOC Conference 1983 Conference Paper

A Probabilistic PDL

• Dexter Kozen

In this paper we give a probabilistic analog PPDL of Propositional Dynamic Logic. We prove a small model property and give a polynomial space decision procedure for formulas involving well-structured programs. We also give a deductive calculus and illustrate its use by calculating the expected running time of a simple random walk program.

TCS Journal 1983 Journal Article

Results on the propositional μ-calculus

• Dexter Kozen

In this paper we define and study a propositional μ-calculus Lμ, which consists essentially of propositional modal logic with a least fixpoint operator. Lμ is syntactically simpler yet strictly more expressive than Propositional Dynamic Logic (PDL). For a restricted version we give an exponential-time decision procedure, small model property, and complete deductive system, theory subsuming the corresponding results for PDL.

TCS Journal 1981 Journal Article

An elementary proof of the completeness of PDL

• Dexter Kozen
• Rohit Parikh

We give an elementary proof of the completeness of the Segerberg axions for Propositional Dynamic Logic.

TCS Journal 1980 Journal Article

Complexity of Boolean algebras

• Dexter Kozen

We show that the elementary theory of Boolean algebras is ⩽log-complete for the Berman complexity class ⋃c<ω STA(∗, 2 cn, n), the class of sets accepted by alternating Turing machines running in time 2 cn for some constant c and making at most n alternations on inputs of length n; thus the theory is computationally equivalent to the theory of real addition with order. We extend the completeness results to various subclasses of Boolean algebras, including the finite, free, atomic, atomless, and complete Boolean algebras. Finally we show that the theory of any finite collection of finite Boolean algebras is complete for PSPACE, while the theory of any other collection is ⩽log-hard for ⋃c<ω STA(∗, 2 cn, n).

TCS Journal 1980 Journal Article

Indexings of subrecursive classes

• Dexter Kozen

A subrecursive indexing is a programming language or Gödel numbering for a class of total recursive functions. Several properties of subrecursive indexings, such as effective composition and generation of constant functions, are investigated from an axiomatic point of view. The result is a theory akin to the axiomatic treatment of recursive function theory of Strong and Wagner. Using this formalism, we prove results relating the complexity of uniform simulation, diagonalization, deciding membership, and deciding halting; we give a subrecursive analog of Rice's theorem; we give a characterization of the combinatorial power of subrecursive indexings analogous to the combinatorial completeness of the lambda calculus; finally, we give a characterization the power of diagonalization over subrecursive classes and show that if P≠NP is provable at all, then it is provable by diagonalization.

FOCS Conference 1980 Conference Paper

Process Logic: Expressiveness, Decidability, Completeness

• David Harel
• Dexter Kozen
• Rohit Parikh

We define a process logic PL that subsumes Pratt's process logic, Parikh's SOAPL, Nishimura's process logic, and Pnueli's Temporal Logic in expressiveness. The language of PL is an extension of the language of Propositional Dynamic Logic (PDL). We give a deductive system for PL which includes the Segerberg axioms for PDL and prove that it is complete. We also show that PL is decidable.

FOCS Conference 1979 Conference Paper

Semantics of Probabilistic Programs

• Dexter Kozen

Two complementary but equivalent semantic interpretations of a high level probabilistic programming language are given. One of these interprets programs as partial measurable functions on a measurable space. The other interprets programs as continuous linear operators on a Banach space of measures. It is shown how the ordered domains of Scott and others are embedded naturally into these spaces. Two general results about probabilistic programs are proved.

STOC Conference 1978 Conference Paper

Indexing of Subrecursive Classes

• Dexter Kozen

A theory of subrecursive indexings is developed, with emphasis on relationships between reducibilities, uniform simulation, and diagonalization.

FOCS Conference 1978 Conference Paper

On the Power of the Compass (or, Why Mazes Are Easier to Search than Graphs)

• Manuel Blum 0001
• Dexter Kozen

STOC Conference 1977 Conference Paper

Complexity of Finitely Presented Algebras

• Dexter Kozen

An algebra A is finitely presented if there is a finite set G of generator symbols, a finite set O of operator symbols, and a finite set Γ of defining relations xΞy where x and y are well-formed terms over G and O, such that A is isomorphic to the free algebra on G and O modulo the congruence induced by Γ.

FOCS Conference 1977 Conference Paper

Lower Bounds for Natural Proof Systems

• Dexter Kozen

Two decidable logical theories are presented, one complete for deterministic polynomial time, one complete for polynomial space. Both have natural proof systems. A lower space bound of n/log(n) is shown for the proof system for the PTIME complete theory and a lower length bound of 2cn/log(n) is shown for the proof system for the PSPACE complete theory.

FOCS Conference 1976 Conference Paper

On Parallelism in Turing Machines

• Dexter Kozen

A model of parallel computation based on a generalization of nondeterminism in Turing machines is introduced. Complexity classes //T(n)-TIME, //L(n)-SPACE, //LOGSPACE, //PTIME, etc. are defined for these machines in a way analogous to T(n)-TIME, L(n)-SPACE, LOGSPACE, PTIME, etc. for deterministic machines. It is shown that, given appropriate honesty conditions, L(n)-SPACE ⊆ //L(n)2-TIME T(n)-TIME ⊆ //log T(n)-SPACE //L(n)-SPACE ⊆ exp L(n)-TIME //T(n)-TIME ⊆ T(n)2-SPACE thus · · //EXPTIME = EXPSPACE //PSPACE = EXPTIME //PTIME = PSPACE //LOGSPACE = PTIME? = LOGSPACE That is, the deterministic hierarchy LOGSPACE ⊆ PTIME ⊆ PSPACE ⊆ EXPTIME ⊆. .. shifts by exactly one level when parallelism is introduced. We give a natural characterization of the polynomial time hierarchy of Stockmeyer and Meyer in terms of parallel machines. Analogous space hierarchies are defined and explored, and a generalization of Saviten's result NONDET-L(n)-SPACE ⊆ L(n)2-SPACE is given. Parallel finite automata are defined, and it is shown that, although they accept only regular sets, in general 22k states are necessary and sufficient to simulate a k-state parallel finite automaton deterministically.