Dexter Kozen's Online Publications

Kleene Algebra & Logic

Dexter Kozen. New. Technical Report http://hdl.handle.net/1813/28632, Computing and Information Science, Cornell University, March 2012. Conf. Mathematical Foundations of Programming Semantics (MFPS XXVIII), Bath, UK, June 2012, to appear.
[full text (.pdf)] [bibtex] [top]
We propose a theoretical device for modeling the creation of new indiscernible semantic objects during program execution. The method fits well with the semantics of imperative, functional, and object-oriented languages and promotes equational reasoning about higher-order state. [top]
Jean-Baptiste Jeannin and Dexter Kozen. Capsules and separation. Technical Report http://hdl.handle.net/1813/28284, Computing and Information Science, Cornell University, January 2012. Conf. Logic in Computer Science (LICS12), Dubrovnik, Croatia, June 2012, to appear.
[full text (.pdf)] [bibtex] [top]
We study a formulation of separation logic using capsules, a representation of the state of a computation in higher-order programming languages with mutable variables. We prove soundness of the frame rule in this context and investigate alternative formulations with weaker side conditions. [top]
Dexter Kozen and Alexandra Silva. Left-handed completeness. Technical Report http://hdl.handle.net/1813/23556, Computing and Information Science, Cornell University, August 2011.
[full text (.pdf)] [bibtex] [top]
We give a new, significantly shorter proof of the completeness of the left-handed star rule of Kleene algebra. The proof reveals the rich interaction of algebra and coalgebra in the theory. [top]
Dexter Kozen and Ganesh Ramanarayanan. Publication/citation: A proof-theoretic approach to mathematical knowledge management. In Johan van Benthem, Amitabha Gupta, and Eric Pacuit, editors, Games, Norms, and Reasons: Logic at the Crossroads, volume 353 of Synthese Library, pages 151-161. Dordrecht, Springer Science and Business Media, 2011.
[full text (.pdf)] [bibtex] [top]
There are many real-life examples of formal systems that support constructions or proofs, but that do not provide direct support for remembering them so that they can be recalled and reused in the future. In this paper we examine the operations of publication (remembering a proof) and citation (recalling a proof for reuse), regarding them as forms of common subexpression elimination on proof terms. We then develop this idea from a proof theoretic perspective, describing a simple complete proof system for universal Horn equational logic using three new proof rules, publish, cite and forget. These rules can provide a proof-theoretic infrastructure for proof reuse in any system. [top]
Dexter Kozen. Halting and equivalence of program schemes in models of arbitrary theories. In Andreas Blass, Nachum Dershowitz, and Wolfgang Reisig, editors, Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, volume 6300 of Lecture Notes in Computer Science, pages 463-469. Springer-Verlag, August 2010.
[full text (.pdf)] [bibtex] [top]
In this note we consider the following decision problems. Let Σ be a fixed first-order signature.

(i) Given a first-order theory or ground theory T over Σ of Turing degree α, a program scheme p over Σ, and input values specified by ground terms t₁,...,t_n, does p halt on input t₁,...,t_n in all models of T?

(ii) Given a first-order theory or ground theory T over Σ of Turing degree α and two program schemes p and q over Σ, are p and q equivalent in all models of T?

When T is empty, these two problems are the classical halting and equivalence problems for program schemes, respectively. We show that problem (i) is Σ^α₁-complete and problem (ii) is Π^α₂-complete. Both problems remain hard for their respective complexity classes even if Σ is restricted to contain only a single constant, a single unary function symbol, and a single monadic predicate. It follows from (ii) that there can exist no relatively complete deductive system for scheme equivalence over models of theories of any Turing degree. [top]
Dexter Kozen. Church-Rosser made easy. Fundamenta Informaticae, 103:129-136, 2010.
[full text (.pdf)] [bibtex] [top]
The Church–Rosser theorem states that the λ-calculus is confluent under β-reductions. The standard proof of this result is due to Tait and Martin-Löf. In this note, we present an alternative proof based on the notion of acceptable orderings. The technique is easily modified to give confluence of the βη-calculus. [top]
Dexter Kozen. Nonlocal flow of control and Kleene algebra with tests. In Proc. 23rd IEEE Symp. Logic in Computer Science (LICS'08), pages 105-117, June 2008.
[full text] [bibtex] [top]
Kleene algebra with tests (KAT) is an equational system for program verification that combines Kleene algebra (KA), or the algebra of regular expressions, with Boolean algebra. It can model basic programming and verification constructs such as conditional tests, while loops, and Hoare triples, thus providing a relatively simple equational approach to program equivalence and partial correctness. In this paper we show how KAT can be used to give a rigorous equational treatment of control constructs involving nonlocal transfer of control such as unconditional jumps, loop statements with multi-level breaks, and exception handlers. We develop a compositional semantics and a complete equational axiomatization. The approach has some novel technical features, including a treatment of multi-level break statements that is reminiscent of de Bruijn indices in the variable-free lambda calculus. We illustrate the use of the system by giving a purely calculational proof that every deterministic flowchart is equivalent to a loop program with multi-level breaks. [top]
Dexter Kozen. On the coalgebraic theory of Kleene algebra with tests. Technical Report http://hdl.handle.net/1813/10173, Computing and Information Science, Cornell University, March 2008.
[full text (.pdf)] [bibtex] [top]
We develop a coalgebraic theory of Kleene algebra with tests (KAT) along the lines of Rutten (1998) for Kleene algebra (KA) and Chen and Pucella (2003) for a limited version of KAT, resolving some technical issues raised by Chen and Pucella. Our treatment includes a simple definition of the Brzozowski derivative for KAT expressions and an automata-theoretic interpretation involving automata on guarded strings. We also give a complexity analysis, showing that an efficient implementation of coinductive equivalence proofs in this setting is tantamount to a standard automata-theoretic construction. It follows that coinductive equivalence proofs can be generated automatically in PSPACE. This matches the bound of Worthington (2008) for the automatic generation of equational proofs in KAT. [top]
Dexter Kozen and Wei-Lung (Dustin) Tseng. The Böhm-Jacopini theorem is false, propositionally. In P. Audebaud and C. Paulin-Mohring, editors, Proc. 9th Int. Conf. Mathematics of Program Construction (MPC'08), volume 5133 of Lect. Notes in Comput. Sci., pages 177-192. Springer, July 2008.
[full text (.pdf)] [bibtex] [top]
The Böhm-Jacopini theorem (Böhm and Jacopini, 1966) is a classical result of program schematology. It states that any deterministic flowchart program is equivalent to a while program. The theorem is usually formulated at the first-order interpreted or first-order uninterpreted (schematic) level, because the construction requires the introduction of auxiliary variables. Ashcroft and Manna (1972) and Kosaraju (1973) showed that this is unavoidable. As observed by a number of authors, a slightly more powerful structured programming construct, namely loop programs with multi-level breaks, is sufficient to represent all deterministic flowcharts without introducing auxiliary variables. Kosaraju (1973) established a strict hierarchy determined by the maximum level of the multi-level breaks that are allowed. In this paper we give purely propositional account of these results. We reformulate the problems at the propositional level in terms of automata on guarded strings, the automata-theoretic counterpart to Kleene algebra with tests. Whereas the classical approaches do not distinguish the first-order and propositional level of abstraction, we find that the purely propositional formulation allows a more streamlined mathematical treatment, using algebraic and topological concepts such as bisimulation and coinduction. Using these tools, we can give more mathematically rigorous formulations and simpler and more revealing proofs. [top]
Kamal Aboul-Hosn and Dexter Kozen. Local variable scoping and Kleene algebra with tests. J. Log. Algebr. Program., 2007. DOI: 10.1016/j.jlap.2007.10.007.
[full text (.pdf)] [bibtex] [top]
Most previous work on the semantics of programs with local state involves complex storage modeling with pointers and memory cells, complicated categorical constructions, or reasoning in the presence of context. In this paper, we explore the extent to which relational semantics and axiomatic reasoning in the style of Kleene algebra can be used to avoid these complications. We provide (i) a fully compositional relational semantics for a first-order programming language with a construct for local variable scoping; and (ii) an equational proof system based on Kleene algebra with tests for proving equivalence of programs in this language. We show that the proof system is sound and complete relative to the underlying equational theory without local scoping. We illustrate the use of the system with several examples. [top]
Dexter Kozen. Coinductive proof principles for stochastic processes. Logical Methods in Computer Science, 3(4:8), 2007. DOI: 10.2168/LMCS-3 (4:8) 2007.
[full text (.pdf)] [bibtex] [top]
We give an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique. The rule encapsulates low-level analytic arguments, allowing reasoning about such processes at a higher algebraic level. We illustrate the use of the rule in deriving properties of a simple coin-flip process. [top]
Dexter Kozen and Marc Timme. Indefinite summation and the Kronecker delta. Technical Report http://hdl.handle.net/1813/8352, Computing and Information Science, Cornell University, October 2007.
[full text] [bibtex] [top]
Indefinite summation, together with a generalized version of the Kronecker delta, provide a calculus for reasoning about various polynomial functions that arise in combinatorics, such as the Tutte, chromatic, flow, and reliability polynomials. In this paper we develop the algebraic properties of the indefinite summation operator and the generalized Kronecker delta from an axiomatic viewpoint. Our main result is that the axioms are equationally complete; that is, all equations that hold under the intended interpretations are derivable in the calculus. [top]
Dexter Kozen and Nicholas Ruozzi. Applications of metric coinduction. In T. Mossakowski et al., editor, Proc. 2nd Conf. Algebra and Coalgebra in Computer Science (CALCO 2007), volume 4624 of Lecture Notes in Computer Science, pages 327-341. Springer, August 2007.
[full text (.pdf)] [bibtex] [top]
Metric coinduction is a form of coinduction that can be used to establish properties of objects constructed as a limit of finite approximations. One can prove a coinduction step showing that some property is preserved by one step of the approximation process, then automatically infer by the coinduction principle that the property holds of the limit object. This can often be used to avoid complicated analytic arguments involving limits and convergence, replacing them with simpler algebraic arguments. This paper examines the application of this principle in a variety of areas, including infinite streams, Markov chains, Markov decision processes, and non-well-founded sets. These results point to the usefulness of coinduction as a general proof technique. [top]
Dexter Kozen. On the representation of Kleene algebras with tests. In R. Královic and P. Urzyczyn, editors, Proc. Conf. Mathematical Foundations of Computer Science (MFCS'06), volume 4162 of Lecture Notes in Computer Science, pages 73-83. Springer, August 2006.
[full text (.pdf)] [bibtex] [top]
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. [top]
Kamal Aboul-Hosn and Dexter Kozen. Relational semantics for higher-order programs. In Tarmo Uustalu, editor, Proc. 8th Int. Conf. Mathematics of Program Construction (MPC'06), volume 4014 of Lecture Notes in Computer Science, pages 29-48. Springer, July 2006.
[full text (.pdf)] [bibtex] [top]
Most previous work on the semantics of higher-order programs with local state involves complex storage modeling with pointers and memory cells, complicated categorical constructions, or reasoning in the presence of context. In this paper we show how a relatively simple relational semantics can be used to avoid these complications. We provide a natural relational semantics for a programming language with higher-order functions. The semantics is purely compositional, with all contextual considerations completely encapsulated in the state. We show several equivalence proofs using this semantics based on examples of Meyer and Sieber (1988). [top]
Dexter Kozen, Christoph Kreitz, and Eva Richter. Automating proofs in category theory. In Proc. 3rd Int. Joint Conf. Automated Reasoning (IJCAR'06), number 4130 in Lecture Notes in AI, pages 392-407. Springer, August 2006.
[full text (.pdf)] [bibtex] [top]
We introduce a semi-automated proof system for basic category-theoretic reasoning. It is based on a first-order sequent calculus that captures the basic properties of categories, functors and natural transformations as well as a small set of proof tactics that automate proof search in this calculus. We demonstrate our approach by automating the proof that the functor categories Fun[CxD,E] and Fun[C,Fun[D,E]] are naturally isomorphic. [top]
Kamal Aboul-Hosn and Dexter Kozen. KAT-ML: An interactive theorem prover for Kleene algebra with tests. Journal of Applied Non-Classical Logics, 16(1-2):9-33, 2006.
[full text (.pdf)] [bibtex] [top]
We describe KAT-ML, an implementation of an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. One can also use the system to reason about properties of simple imperative programs using schematic KAT (SKAT). We explain how the system works and illustrate its use with some examples, including an extensive scheme equivalence proof. [top]
Dexter Kozen and Bernhard Möller. Separability in domain semirings. Technical Report 2004-16, Universität Augsburg, Institut für Informatik, December 2004.
[full text (.pdf)] [bibtex] [top]
First, we show with two examples that in test semirings with an incomplete test algebra a domain operation may or may not exist. Second, we show that two notions of separability in test semirings coincide, respectively, with locality of composition and with extensionality of the diamond operators in domain semirings. We conclude with a brief comparison of dynamic algebras and modal Kleene algebras. [top]
Dexter Kozen. Toward the automation of category theory. Technical Report TR2004-1964, Computer Science Department, Cornell University, September 2004.
[full text (.pdf)] [bibtex] [top]
We introduce a sequent system for basic category-theoretic reasoning suitable for computer implementation. We illustrate its use by giving a complete formal proof that the functor categories Fun[CxD,E] and Fun[C,Fun[D,E]] are naturally isomorphic. [top]
Dexter Kozen. Natural transformations as rewrite rules and monad composition. Technical Report TR2004-1942, Computer Science Department, Cornell University, July 2004.
[full text (.pdf)] [bibtex] [top]
Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a different approach involving string rewriting. We show that a given tuple (T,mu,eta) is a monad if and only if T is a terminal object in a certain category of functors and natural transformations, and that this fact can be established by proving confluence of a certain string rewriting system. We illustrate the technique on the monad composition problem of Eklund et al. [top]
Dexter Kozen. Some results in dynamic model theory. Science of Computer Programming, 51(1-2):3-22, May 2004. Special issue: Mathematics of Program Construction (MPC 2002). Eerke Boiten and Bernhard Möller (eds.).
[full text (.pdf)] [bibtex] [top]
First-order structures over a fixed signature Sgive rise to a family of trace-based and relational Kleene algebras with tests defined in terms of Tarskian frames. A Tarskian frame is a Kripke frame whose states are valuations of program variables and whose atomic actions are state changes effected by variable assignments x := e, where e is a S-term. The Kleene algebras with tests that arise in this way play a role in dynamic model theory akin to the role played by Lindenbaum algebras in classical first-order model theory. Given a first-order theory T over S, we exhibit a Kripke frame U whose trace algebra Tr_U is universal for the equational theory of Tarskian trace algebras over Ssatisfying T, although U itself is not Tarskian in general. The corresponding relation algebra Rel_U is not universal for the equational theory of relation algebras of Tarskian frames, but it is so modulo observational equivalence. [top]
Dexter Kozen. Computational inductive definability. Annals of Pure and Applied Logic, 126(1-3):139-148, April 2004. Special issue: Provinces of logic determined. Essays in the memory of Alfred Tarski. Zofia Adamowicz, Sergei Artemov, Damian Niwinski, Ewa Orlowska, Anna Romanowska, and Jan Wolenski (eds.).
[full text (.pdf)] [bibtex] [top]
It is shown that over any countable first-order structure, IND programs with dictionaries accept exactly the Pi-1-1 relations. This extends a result of Harel and Kozen (1984) relating IND and Pi-1-1 over countable structures with some coding power, and provides a computational analog of a result of Barwise, Gandy, and Moschovakis (1971) relating the Pi-1-1 relations on a countable structure to a certain family of inductively definable relations on the hereditarily finite sets over that structure. [top]
Chris Hardin and Dexter Kozen. On the complexity of the Horn theory of REL. Technical Report TR2003-1896, Computer Science Department, Cornell University, May 2003.
[full text (.pdf)] [bibtex] [top]
We show that the universal Horn theory of relational Kleene algebras is Pi-1-1-complete. [top]
Dexter Kozen and Jerzy Tiuryn. Substructural logic and partial correctness. Trans. Computational Logic, 4(3):355-378, July 2003.
[full text (.pdf)] [bibtex] [top]
We formulate a noncommutative sequent calculus for partial correctness that subsumes propositional Hoare Logic. Partial correctness assertions are represented by intuitionistic linear implication. We prove soundness and completeness over relational and trace models. As a corollary we obtain a complete sequent calculus for inclusion and equivalence of regular expressions. [top]
Dexter Kozen. On Hoare logic, Kleene algebra, and types. In P. Gärdenfors, J. Wole\'nski, and K. Kijania-Placek, editors, In the Scope of Logic, Methodology, and Philosophy of Science: Volume 1 of the 11th Int. Congress Logic, Methodology and Philosophy of Science, Cracow, August 1999, volume 315 of Studies in Epistemology, Logic, Methodology, and Philosophy of Science, pages 119-133. Kluwer, 2002.
[full text (.pdf)] [bibtex] [top]
We show that propositional Hoare logic is subsumed by the type calculus of typed Kleene algebra augmented with subtypes and typecasting. Assertions are interpreted as typecast operators. Thus Hoare-style reasoning with partial correctness assertions reduces to typechecking in this system. [top]
Dexter Kozen. On the complexity of reasoning in Kleene algebra. Information and Computation, 179:152-162, 2002.
[full text (.pdf)] [bibtex] [top]
We study the complexity of reasoning in Kleene algebra and *-continuous Kleene algebra in the presence of extra assumptions; i.e., 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: for *-continuous Kleene algebra,

1. if E contains only commutativity assumptions pq=qp, the problem is Pi-0-1-complete (co-r.e. complete);
2. if E contains only monoid equations, the problem is Pi-0-2-complete;
3. for arbitrary equations E, the problem is Pi-1-1-complete.

The last problem is the universal Horn theory of the *-continuous Kleene algebras. This resolves an open question of [Kozen, LICS 1991]. [top]
Dexter Kozen. Halting and equivalence of schemes over recursive theories. Technical Report TR2002-1881, Computer Science Department, Cornell University, October 2002.
[full text (.pdf)] [bibtex] [top]
Let S be a fixed first-order signature. In this note we consider the following decision problems. (i) Given a recursive ground theory T over S, a program scheme p over S, and input values specified by ground terms t₁,...,t_n, does p halt on input t₁,...,t_n in all models of T? (ii) Given a recursive ground theory T over S and two program schemes p and q over S, are p and q equivalent in all models of T? When T is empty, these two problems are the classical halting and equivalence problems for program schemes, respectively. We show that problem (i) is r.e.-complete and problem (ii) is Pi-0-2-complete. Both these problems remain hard for their respective complexity classes even if T is empty and S is restricted to contain only a single constant, a single unary function symbol, and a single monadic predicate. It follows from (ii) that there can exist no relatively complete deductive system for scheme equivalence. [top]
Chris Hardin and Dexter Kozen. On the elimination of hypotheses in Kleene algebra with tests. Technical Report TR2002-1879, Computer Science Department, Cornell University, October 2002.
[full text (.pdf)] [bibtex] [top]
The validity problem for certain universal Horn formulas of Kleene algebra with tests (KAT) can be efficiently reduced to the equational theory. This reduction is known as elimination of hypotheses. Hypotheses are used to describe the interaction of atomic programs and tests and are an essential component of practical program verification with KAT. The ability to eliminate hypotheses of a certain form means that the Horn theory with premises of that form remains decidable in PSPACE. It was known (Cohen 1994, Kozen and Smith 1996, Kozen 1997) how to eliminate hypotheses of the form q=0. In this paper we show how to eliminate hypotheses of the form cp=c for atomic p. Hypotheses of this form are useful in eliminating redundant code and arise quite often in the verification of compiler optimizations (Kozen and Patron 2000). [top]
Adam Barth and Dexter Kozen. Equational verification of cache blocking in LU decomposition using Kleene algebra with tests. Technical Report TR2002-1865, Computer Science Department, Cornell University, June 2002.
[full text (.pdf)] [bibtex] [top]
In a recent paper of Mateev et al. (2001), a new technique for program analysis called fractal symbolic analysis was introduced and applied to verify the correctness of a series of source-level transformations for cache blocking in LU decomposition with partial pivoting. It was argued in that paper that traditional techniques are inadequate because the transformations break definition-use dependencies. We show how the task can be accomplished purely equationally using Kleene algebra with tests. [top]
Allegra Angus and Dexter Kozen. Kleene algebra with tests and program schematology. Technical Report TR2001-1844, Computer Science Department, Cornell University, July 2001.
[full text (.pdf)] [bibtex] [top]
The theory of flowchart schemes has a rich history going back to Ianov (1960); see Manna (1974) for an elementary exposition. A central question in the theory of program schemes is scheme equivalence. Manna presents several examples of equivalence proofs that work by simplifying the schemes using various combinatorial transformation rules. In this paper we present a purely algebraic approach to this problem using Kleene algebra with tests (KAT). Instead of transforming schemes directly using combinatorial graph manipulation, we regard them as a certain kind of automaton on abstract traces. We prove a generalization of Kleene's theorem and use it to construct equivalent expressions in the language of KAT. We can then give a purely equational proof of the equivalence of the resulting expressions. We prove soundness of the method and give a detailed example of its use. [top]
Dexter Kozen and Jerzy Tiuryn. On the completeness of propositional Hoare logic. Information Sciences, 139(3-4):187-195, 2001.
[full text (.pdf)] [bibtex] [top]
We investigate the completeness of Hoare Logic on the propositional level. In particular, the expressiveness requirements of Cook's proof are characterized propositionally. We give a completeness result for Propositional Hoare Logic (PHL): all relationally valid rules
{b₁}p₁{c₁}, ..., {b_n}p_n{c_n}
----------------------------
{b}p{c}
are derivable in PHL, provided the propositional expressiveness conditions are met. Moreover, if the programs p_i in the premises are atomic, no expressiveness assumptions are needed. [top]
Dexter Kozen. Myhill-Nerode relations on automatic systems and the completeness of Kleene algebra. In Afonso Ferreira and Horst Reichel, editors, Proc. 18th Symp. Theoretical Aspects of Computer Science (STACS'01), volume 2010 of Lecture Notes in Computer Science, pages 27-38, Dresden, Germany, February 2001. Springer-Verlag.
[full text (.pdf)] [bibtex] [top]
It is well known that finite square matrices over a Kleene algebra again form a Kleene algebra. This is also true for infinite matrices under suitable restrictions. One can use this fact to solve certain infinite systems of inequalities over a Kleene algebra. Automatic systems are a special class of infinite systems that can be viewed as infinite-state automata. Automatic systems can be collapsed using Myhill-Nerode relations in much the same way that finite automata can. The Brzozowski derivative on an algebra of polynomials over a Kleene algebra gives rise to a triangular automatic system that can be solved using these methods. This provides an alternative method for proving the completeness of Kleene algebra. [top]
Ernie Cohen and Dexter Kozen. A note on the complexity of propositional Hoare logic. Trans. Computational Logic, 1(1):171-174, July 2000.
[full text (.pdf)] [bibtex] [top]
We provide a simpler alternative proof of the PSPACE-hardness of propositional Hoare logic. [top]
David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. MIT Press, Cambridge, MA, 2000.
[table of contents (.ps)] [bibtex] [top]
A graduate-level textbook on Dynamic Logic. [top]
Dexter Kozen and Maria-Cristina Patron. Certification of compiler optimizations using Kleene algebra with tests. In John Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luis Moniz Pereira, Yehoshua Sagiv, and Peter J. Stuckey, editors, Proc. 1st Int. Conf. Computational Logic (CL2000), volume 1861 of Lecture Notes in Artificial Intelligence, pages 568-582, London, July 2000. Springer-Verlag.
[full text (.pdf)] [bibtex] [top]
We use Kleene algebra with tests to verify a wide assortment of common compiler optimizations, including dead code elimination, common subexpression elimination, copy propagation, loop hoisting, induction variable elimination, instruction scheduling, algebraic simplification, loop unrolling, elimination of redundant instructions, array bounds check elimination, and introduction of sentinels. In each of these cases, we give a formal equational proof of the correctness of the optimizing transformation. [top]
Dexter Kozen. On Hoare logic and Kleene algebra with tests. Trans. Computational Logic, 1(1):60-76, July 2000.
[full text (.pdf)] [bibtex] [top]
We show that Kleene algebra with tests (KAT) subsumes propositional Hoare logic (PHL). Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by simple equational reasoning. In addition, we show that all relationally valid inference rules are derivable in KAT and that deciding the relational validity of such rules is PSPACE-complete. [top]
Mark Hopkins and Dexter Kozen. Parikh's theorem in commutative Kleene algebra. In Proc. 14th Conf. Logic in Computer Science (LICS'99), pages 394-401. IEEE, July 1999.
[full text (.ps)] [bibtex] [top]
Parikh's Theorem says that the commutative image of every context free language is the commutative image of some regular set. Pilling has shown that this theorem is essentially a statement about least solutions of polynomial inequalities. We prove the following general theorem of commutative Kleene algebra, of which Parikh's and Pilling's theorems are special cases: Every system of polynomial inequalities f_i(x₁,...,x_n) <= x_i, 1 <= i <= n, over a commutative Kleene algebra K has a unique least solution in Kⁿ; moreover, the components of the solution are given by polynomials in the coefficients of the f_i. We also give a closed-form solution in terms of the Jacobian matrix. [top]
Dexter Kozen. Typed Kleene algebra. Technical Report TR98-1669, Computer Science Department, Cornell University, March 1998.
[full text (.ps)] [bibtex] [top]
In previous work we have found it necessary to argue that certain theorems of Kleene algebra hold even when the symbols are interpreted as nonsquare matrices. In this note we define and investigate typed Kleene algebra, a typed version of Kleene algebra in which objects have types s -> t. Although nonsquare matrices are the principal motivation, there are many other useful interpretations: traces, binary relations, Kleene algebra with tests. We give a set of typing rules and show that every expression has a unique most general typing (mgt). Then we prove the following metatheorem that incorporates the abovementioned results for nonsquare matrices as special cases. Call an expression 1-freeif it contains only the Kleene algebra operators (binary) +, (unary) ⁺, 0, and ·, but no occurrence of 1 or *. Then every universal 1-free formula that is a theorem of Kleene algebra is also a theorem of typed Kleene algebra under its most general typing. The metatheorem is false without the restriction to 1-free formulas. [top]
Dexter Kozen. Kleene algebra with tests. Transactions on Programming Languages and Systems, 19(3):427-443, May 1997.
[full text (.ps)] [bibtex] [top]
We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program with at most one while loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs. We also show that the universal Horn theory of *-continuous Kleene algebras is not finitely axiomatizable. [top]
Ernie Cohen, Dexter Kozen, and Frederick Smith. The complexity of Kleene algebra with tests. Technical Report TR96-1598, Computer Science Department, Cornell University, July 1996.
[full text (.ps)] [bibtex] [top]
The equational theory of Kleene algebras with tests (KAT) has been shown to be decidable in at most exponential time by an efficient reduction to Propositional Dynamic Logic. We show that the theory is PSPACE-complete. Thus KAT, while considerably more expressive than Kleene algebra, is no more difficult to decide. [top]
Dexter Kozen and Frederick Smith. Kleene algebra with tests: Completeness and decidability. In D. van Dalen and M. Bezem, editors, Proc. 10th Int. Workshop Computer Science Logic (CSL'96), volume 1258 of Lecture Notes in Computer Science, pages 244-259, Utrecht, The Netherlands, September 1996. Springer-Verlag.
[full text (.ps)] [bibtex] [top]
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. [top]
Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Infor. and Comput., 110(2):366-390, May 1994.
[full text (.ps)] [bibtex] [top]
We give a finitary axiomatization of the algebra of regular events involving only equations and equational implications. Unlike Salomaa's axiomatizations, the axiomatization given here is sound for all interpretations over Kleene algebras. [top]
Dexter Kozen. On action algebras. In J. van Eijck and A. Visser, editors, Logic and Information Flow, pages 78-88. MIT Press, 1994.
[full text (.ps)] [bibtex] [top]
Action algebras have been proposed by Pratt as an alternative to Kleene algebras. Their chief advantage over Kleene algebras is that they form a finitely-based equational variety, so the essential properties of * (iteration) are captured purely equationally. However, unlike Kleene algebras, they are not closed under the formation of matrices, which renders them inapplicable in certain constructions in automata theory and the design and analysis of algorithms. In this paper we consider a class of action algebras called action lattices. An action lattice is simply an action algebra that forms a lattice under its natural order. Action lattices combine the best features of Kleene algebras and action algebras: like action algebras, they form a finitely-based equational variety; like Kleene algebras, they are closed under the formation of matrices. Moreover, they form the largest subvariety of action algebras for which this is true. All common examples of Kleene algebras appearing in automata theory, logics of programs, relational algebra, and the design and analysis of algorithms are action lattices. [top]
Dexter Kozen. On Kleene algebras and closed semirings. In Rovan, editor, Proc. Math. Found. Comput. Sci., volume 452 of Lecture Notes in Computer Science, pages 26-47, Banska-Bystrica, Slovakia, 1990. Springer-Verlag.
[full text (.ps)] [bibtex] [top]
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 several inequivalent definitions of Kleene algebras and related algebraic structures. In this paper we establish some new relationships among these structures. Our main results are: (i) There is a Kleene algebra that is not *-continuous. (ii) The categories of *-continuous Kleene algebras, closed semirings, and S-algebras are strongly related by adjunctions. (iii) The axioms of Kleene algebra are not complete for the universal Horn theory of the regular events. This refutes a conjecture of Conway. (iv) Right-handed Kleene algebras are not necessarily left-handed Kleene algebras. This verifies a weaker version of a conjecture of Pratt. [top]
Neil Immerman and Dexter Kozen. Definability with bounded number of bound variables. Infor. and Comp., 83(2):121-139, November 1989.
[full text (.ps)] [bibtex] [top]
A theory satisfies the k-variable propertyif 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. [top]
Dexter Kozen. A finite model theorem for the propositional μ-calculus. Studia Logica, 47(3):233-241, 1988.
[full text (.pdf)] [bibtex] [top]
We prove a finite model theorem and infinitary completeness result for the propositional μ-calculus. The construction establishes a link between finite model theorems for propositional program logics and the theory of well-quasi-orders. [top]
Krzysztof Apt and Dexter Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22:307-309, 1986.
[full text (.pdf)] [bibtex] [top]
We show that some very simple temporal properties of schematic finite-state programs are not semi-decidable. [top]
Dexter Kozen. A probabilistic PDL. J. Comput. Syst. Sci., 30(2):162-178, April 1985.
[full text (.pdf)] [bibtex] [top]
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. [top]
Dexter Kozen. Results on the propositional μ-calculus. Theor. Comput. Sci., 27:333-354, 1983.
[full text (.pdf)] [bibtex] [top]
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, thereby subsuming the corresponding results for PDL. [top]
Dexter Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22:328-350, 1981.
[full text (.pdf)] [bibtex] [top]
This paper presents two complementary but equivalent semantics for a high level probabilistic programming language. 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. We use the semantics to prove a general result about probabilistic programs, namely that a program's behavior is completely determined by its action on fixed inputs. [top]

Programming Languages & Program Analysis

Dexter Kozen. Realization of coinductive types. In Michael Mislove and Joël Ouaknine, editors, Proc. 27th Conf. Math. Found. Programming Semantics (MFPS XXVII), pages 148-155, Pittsburgh, PA, May 2011. Elsevier Electronic Notes in Theoretical Computer Science.
[full text (.pdf)] [bibtex] [top]
We give an explicit combinatorial construction of final coalgebras for a modest generalization of polynomial functors on Set. Type signatures are modeled as directed multigraphs instead of endofunctors. The final coalgebra for a type signature F involves the notion of Brzozowski derivative on sets of paths in F. [top]
Jean-Baptiste Jeannin and Dexter Kozen. Computing with capsules. Technical Report http://hdl.handle.net/1813/22082, Computing and Information Science, Cornell University, January 2011. Proc. Conf. Descriptional Complexity of Formal Systems (DCFS 2012), Braga, Portugal, July 2012, to appear.
[full text (.pdf)] [bibtex] [top]
Capsules provide a clean algebraic representation of the state of a computation in higher-order functional and imperative languages. They play the same role as closures or heap- or stack-allocated environments but are much simpler. A capsule is essentially a finite coalgebraic representation of a regular closed λ-coterm. One can give an operational semantics based on capsules for a higher-order programming language with functional and imperative features, including mutable bindings. Lexical scoping is captured purely algebraically without stacks, heaps, or closures. All operations of interest are typable with simple types, yet the language is Turing complete. Recursive functions are represented directly as capsules without the need for unnatural and untypable fixpoint combinators. [top]
Łucja Kot and Dexter Kozen. Kleene algebra and bytecode verification. In Fausto Spoto, editor, Proc. 1st Workshop Bytecode Semantics, Verification, Analysis, and Transformation (Bytecode'05), pages 201-215, April 2005.
[full text (.pdf)] [bibtex] [top]
In this paper we show how the general framework introduced in the paper "Second-Order Abstract Interpretation via Kleene Algebra" applies to the problem of Java bytecode verification. We show how to specify transfer functions arising in Java bytecode verification in such a way that the Kleene algebra operations (join, composition, star) can be computed efficiently. We also give a hybrid dataflow analysis algorithm that computes the closure of a matrix on a cutset of the control flow graph, thereby avoiding the recalculation of dataflow information along long paths. This method could potentially improve the performance over the standard worklist algorithm when a small cutset can be found. [top]
Łucja Kot and Dexter Kozen. Second-order abstract interpretation via Kleene algebra. Technical Report TR2004-1971, Computer Science Department, Cornell University, December 2004.
[full text (.pdf)] [bibtex] [top]
Most standard approaches to the static analysis of programs, such as the popular worklist method, are first-order methods that inductively annotate program points with abstract values. In this paper we introduce a second-order approach based on Kleene algebra. In this approach, the primary objects of interest are not the abstract data values, but the transfer functions that manipulate them. These elements form a Kleene algebra. The dataflow labeling is not achieved by inductively labeling the program with abstract values, but rather by computing the star (Kleene closure) of a matrix of transfer functions. In this paper we introduce the method and prove soundness and completeness with respect to the standard worklist algorithm. [top]
Dexter Kozen. Kleene algebras with tests and the static analysis of programs. Technical Report TR2003-1915, Computer Science Department, Cornell University, November 2003.
[full text (.pdf)] [bibtex] [top]
We propose a general framework for the static analysis of programs based on Kleene algebra with tests (KAT). We show how KAT can be used to statically verify compliance with safety policies specified by security automata. We prove soundness and completeness over relational interpretations. We illustrate the method on an example involving the correctness of a device driver. [top]
Robert Givan, David McAllester, Carl Witty, and Dexter Kozen. Tarskian set constraints. Information and Computation, 174(2):105-131, May 2002.
[full text (.ps)] [bibtex] [top]
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. [top]
Dexter Kozen and Matt Stillerman. Eager class initialization for Java. In W. Damm and E.R. Olderog, editors, Proc. 7th Int. Symp. Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), volume 2469 of Lecture Notes in Computer Science, pages 71-80. IFIP, Springer-Verlag, Sept. 2002.
[full text (.pdf)] [bibtex] [top]
We describe a static analysis method on Java bytecode to determine class initialization dependencies. This method can be used for eager class loading and initialization. It catches many initialization circularities that are missed by the standard lazy implementation. Except for contrived examples, the computed initialization order gives the same results as standard lazy initialization. [top]
Dexter Kozen. Set constraints and logic programming. Information and Computation, 142(1):2-25, April 1998.
[full text (.ps)] [bibtex] [top]
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 language CLP(SC) over set constraints in the style of Jaffar and Lassez. 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 Heintze and Jaffar. [top]
Allan Cheng and Dexter Kozen. Some notes on rational spaces. Technical Report TR96-1576, Computer Science Department, Cornell University, March 1996.
[full text (.ps)] [bibtex] [top]
Set constraints are inclusions between expressions denoting set of ground terms over a finitely ranked alphabet. Rational spaces are topological spaces obtained as spaces of runs of topological hypergraphs. They were introduced by Kozen, who described the topological structure of spaces of solutions to systems of set constraints in terms of rational spaces. In this paper we continue the investigation of rational spaces. We give a Myhill-Nerode like characterization of rational points, which in turn is used to rederive results about the rational points of finitary rational spaces. We define congruences on hypergraphs and investigate their interplay with the Myhill-Nerode characterization, and determine the computational complexity of some decision problems related to rational spaces. [top]
Dexter Kozen. Rational spaces and set constraints. Theoretical Computer Science, 167:73-94, 1996.
[full text (.ps)] [bibtex] [top]
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. [top]
Allan Cheng and Dexter Kozen. A complete Gentzen-style axiomatization for set constraints. In F. Meyer auf der Heide and B. Monien, editors, Proc. 23rd Int. Colloq. Automata, Languages, and Programming (ICALP'96), volume 1099 of Lecture Notes in Computer Science, pages 134-145, Paderborn, Germany, July 1996. Eur. Assoc. for Theoretical Comput. Sci., Springer-Verlag.
[full text (.ps)] [bibtex] [top]
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 provide a Gentzen-style axiomatization for sequents P |- Q, where P and Q are finite sets of set constraints, based on the axioms of termset algebra. Sequents of the restricted form P |- false correspond to positive set constraints, and those of the more general form P |- Q correspond to systems of mixed positive and negative set constraints. We show that the deductive system is (i) complete for the restricted sequents P |- falseover standard models, (ii) incomplete for general sequents P |- Q over standard models, but (iii) complete for general sequents over set-theoretic termset algebras. [top]
Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5:113-125, 1995.
[full text (.ps)] [bibtex] [top]
Subtyping in the presence of recursive types for the lambda-calculus was studied by Amadio and Cardelli in 1991. In that paper they showed that the problem of deciding whether one recursive type is a subtype of another is decidable in exponential time. In this paper we give an O(n²) algorithm. Our algorithm is based on a simplification of the definition of the subtype relation, which allows us to reduce the problem to the emptiness problem for a certain finite automaton with quadratically many states. It is known that equality of recursive types and the covariant Böhm order can be decided efficiently by means of finite automata, since they are just language equality and language inclusion, respectively. Our results extend the automata-theoretic approach to handle orderings based on contravariance. [top]
Alexander Aiken, Dexter Kozen, and Edward Wimmers. Decidability of systems of set constraints with negative constraints. Infor. and Comput., 122(1):30-44, October 1995.
[full text (.ps)] [bibtex] [top]
Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. Recently, several algorithms for solving general systems of positive set constraints have appeared. In this paper we consider systems of mixed positive and negative constraints, which are considerably more expressive than positive constraints alone. We show that it is decidable whether a given such system has a solution. The proof involves a reduction to a number-theoretic decision problem that may be of independent interest. [top]
Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient inference of partial types. J. Comput. Syst. Sci., 49(2):306-324, October 1994.
[full text (.ps)] [bibtex] [top]
Partial types for the lambda-calculus were introduced by Thatte in 1988 as a means of typing objects that are not typable with simple types, such as heterogeneous lists and persistent data. In that paper he showed that type inference for partial types was semidecidable. Decidability remained open until quite recently, when O'Keefe and Wand gave an exponential time algorithm for type inference. In this paper we give an O(n³) algorithm. Our 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; this solves an open problem of O'Keefe and Wand. [top]
Dexter Kozen. Logical aspects of set constraints. In E. Börger, Y. Gurevich, and K. Meinke, editors, Proc. 1993 Conf. Computer Science Logic (CSL'93), volume 832 of Lecture Notes in Computer Science, pages 175-188, Swansea, U. K., September 1993. Eur. Assoc. Comput. Sci. Logic, Springer-Verlag.
[full text (.ps)] [bibtex] [top]
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 Jonsson 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. [top]
Alexander Aiken, Dexter Kozen, Moshe Vardi, and Edward Wimmers. The complexity of set constraints. In E. Börger, Y. Gurevich, and K. Meinke, editors, Proc. 1993 Conf. Computer Science Logic (CSL'93), volume 832 of Lecture Notes in Computer Science, pages 1-17, Swansea, U. K., September 1993. Eur. Assoc. Comput. Sci. Logic, Springer-Verlag.
[full text (.ps)] [bibtex] [top]
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. [top]

Computational Algebra

Dexter Kozen and Alexandra Silva. On Moessner's theorem. Technical Report http://hdl.handle.net/1813/22959, Computing and Information Science, Cornell University, June 2011. American Mathematical Monthly, to appear.
[full text (.pdf)] [bibtex] [top]
Moessner's theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers 1ⁿ, 2ⁿ, 3ⁿ, ... Paasche's theorem is a generalization of Moessner's; by varying the parameters of the procedure, one can obtain the sequence of factorials 1!, 2!, 3!, ... or the sequence of superfactorials 1!!, 2!!, 3!!, ... Long's theorem generalizes Moessner's in another direction, providing a procedure to generate the sequence a1^n-1, (a+d)2^n-1, (a+2d)3^n-1, ... Proofs of these results in the literature are typically based on combinatorics of binomial coefficients or calculational scans. In this note we give a short and revealing algebraic proof of a general theorem that contains Moessner's, Paasche's, and Long's as special cases. We also prove a generalization that gives new Moessner-type theorems. [top]
Dexter Kozen and Kjartan Stefansson. Computing the Newtonian graph. Journal of Symbolic Computation, 24:125-136, 1997.
[full text (.ps)] [bibtex] [top]
In his study of Newton's root approximation method, Smale defined the Newtonian graph of a complex univariate polynomial f. The vertices of this graph are the roots of f and f' and the edges are the degenerate curves of flow of the Newtonian vector field N_f(z) = -f(z)/f'(z). The embedded edges of this graph form the boundaries of root basins in Newton's root approximation method. The graph defines a treelike relation on the roots of f and f', similar to the linear order when f has only real roots. We give an efficient algebraic algorithm based on cell decomposition to compute the Newtonian graph. The resulting structure can be used to query whether two complex points are in the same basin. This suggests a modified version of Newton's method in which one can test whether a step has crossed a basin boundary. We show that this modified version does not necessarily converge to a root. Stefansson has recently extended this algorithm to handle rational and algebraic functions without significant increase in complexity. He has shown that the Newtonian graph tesselates the associated Riemann surface and can be used in conjunction with Euler's formula to give an NC algorithm to calculate the genus of an algebraic curve. [top]
Dexter Kozen, Susan Landau, and Richard Zippel. Decomposition of algebraic functions. Journal of Symbolic Computation, 22(3):235-246, September 1996.
[full text (.ps)] [bibtex] [top]
Functional decomposition---whether a function f(x) can be written as a composition of functions g(h(x)) in a nontrivial way---is an important primitive in symbolic computation systems. The problem of univariate polynomial decomposition was shown to have an efficient solution by Kozen and Landau. Dickerson and von zur Gathen gave algorithms for certain multivariate cases. Zippel showed how to decompose rational functions. In this paper, we address the issue of decomposition of algebraic functions. We show that the problem is related to univariate resultants in algebraic function fields, and in fact can be reformulated as a problem of resultant decomposition. We characterize all decompositions of a given algebraic function up to isomorphism, and give an exponential time algorithm for finding a nontrivial one if it exists. The algorithm involves genus calculations and constructing transcendental generators of fields of genus zero. [top]
Dexter Kozen. Efficient resolution of singularities of plane curves. In P. S. Thiagarajan, editor, Proc. 14th Conf. Foundations of Software Technology and Theoretical Computer Science, volume 880 of Lecture Notes in Computer Science, pages 1-11, Madras, India, December 1994. Springer-Verlag.
[full text (.ps)] [bibtex] [top]
We give a new algorithm for resolving singularities of plane curves. The algorithm is polynomial time in the bit complexity model, does not require factorization, and works over the rationals or finite fields. [top]
Jin-Yi Cai, W. H. J. Fuchs, Dexter Kozen, and Zicheng Liu. Efficient average-case algorithms for the modular group. In Proc. 35th Symp. Found. Comput. Sci., pages 143-152. IEEE, November 1994.
[full text (.ps)] [bibtex] [top]
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 Gurevich. [top]
Doug Ierardi and Dexter Kozen. Parallel resultant computation. In J. Reif, editor, Synthesis of Parallel Algorithms, pages 679-720. Morgan Kaufmann, 1993.
[full text (.ps)] [bibtex] [top]
This is a survey paper on resultants. From the introduction: A resultant is a purely algebraic criterion for determining whether a finite collection of polynomials have a common zero. It has been shown to be a useful tool in the design of efficient parallel and sequential algorithms in symbolic algebra, computational geometry, computational number theory, and robotics. We begin with a brief history of resultants and a discussion of some of their important applications. Next we review some of the mathematical background in commutative algebra that will be used in subsequent sections. The Nullstellensatz of Hilbert is presented in both its strong and weak forms. We also discuss briefly the necessary background on graded algebras, and define affine and projective spaces over arbitrary fields. We next present a detailed account of the resultant of a pair of univariate polynomials, and present efficient parallel algorithms for its computation. The theory of subresultants is developed in detail, and the computation of polynomial remainder sequences is derived. A resultant system for several univariate polynomials and algorithms for the gcd of several polynomials are given. Finally, we develop the theory of multivariate resultants as a natural extension of the univariate case. Here we treat both classical results on the projective (homogeneous) case, as well as more recent results on the affine (inhomogeneous) case. The u-resultantof a set of multivariate polynomials is defined and a parallel algorithm is presented. We discuss the computation of generalized characteristic polynomials and relate them to the decision problem for the theories of real closed and algebraically closed fields. [top]
Dexter Kozen and Susan Landau. Polynomial decomposition algorithms. J. Symb. Comput., 7:445-456, 1989.
[full text (.ps)] [bibtex] [top]
We examine the question of when a polynomial f over a commutative ring has a nontrivial functional decomposition f(x) = g(h(x)). Previous algorithms (Barton and Zippel 76, Barton and Zippel 85, Alagar and Thahn 85) are exponential-time in the worst case, require polynomial factorization, and only work over fields of characteristic 0. We present an O(n²)-time algorithm. We also show that the problem is in NC. The algorithm does not use polynomial factorization, and works over any commutative ring containing a multiplicative inverse of r. Finally, we give a new structure theorem that leads to necessary and sufficient algebraic conditions for decomposibility over any field. We apply this theorem to obtain an NC algorithm for decomposing irreducible polynomials over finite fields, and a subexponential algorithm for decomposing irreducible polynomials over any field admitting efficient polynomial factorization. [top]
Michael Ben-Or, Ephraim Feig, Dexter Kozen, and Prasoon Tiwari. Fast parallel algorithms for finding the roots of a polynomial with all real roots. SIAM J. Comput., 17(6):1081-1092, 1988.
[full text] [bibtex] [top]
Given a polynomial p(z) of degree n with m bit integer coefficients and an integer μ, the problem of determining all its roots with error less than 2^μ is considered. It is shown that this problem is in the class NC if p(z) has all real roots. Some very interesting properties of a Sturm sequence of a polynomial with distinct real roots are proved and used in the design of a fast parallel algorithm for this problem. Using Newton identities and a novel numerical integration scheme for evaluating a contour integral to high precision, this algorithm determines good approximations to the linear factors of p(z). [top]

Automata & Formal Languages

Dexter Kozen. Theory of Computation. Springer, New York, 2006.
[table of contents (.pdf)] [bibtex] [top]
A graduate-level text on theory of computation. [top]
Dexter Kozen. Automata on guarded strings and applications. Matématica Contemporânea, 24:117-139, 2003.
[full text (.pdf)] [bibtex] [top]
Guarded strings are like ordinary strings over a finite alphabet P, except that atoms of the free Boolean algebra on a set of atomic tests B alternate with the symbols of P. The regular sets of guarded strings play the same role in Kleene algebra with tests as the regular sets of ordinary strings do in Kleene algebra. In this paper we develop the elementary theory of finite automata on guarded strings, a generalization of the theory of finite automata on ordinary strings. We give several basic constructions, including determinization, state minimization, and an analog of Kleene's theorem. We then use these results to verify a conjecture on the complexity of a complete Gentzen-style sequent calculus for partial correctness. We also show that a basic result of the theory of Boolean decision diagrams (BDDs), namely that minimal ordered BDDs are unique, is a special case of the Myhill-Nerode theorem for a class of automata on guarded strings. [top]
Dexter Kozen. On two letters versus three. In Zoltán Ésik and Anna Ingólfsdóttir, editors, Proc. Workshop on Fixed Points in Computer Science (FICS'02), pages 44-50, July 2002.
[full text (.pdf)] [bibtex] [top]
If A is a context-free language over a two-letter alphabet, then the set of all words obtained by sorting words in A and the set of all permutations of words in A are context-free. This is false over alphabets of three or more letters. Thus these problems illustrate a difference in behavior between two- and three-letter alphabets. [top]
Dexter Kozen. Automata and Computability. Springer-Verlag, New York, 1997.
[table of contents (.ps)] [bibtex] [top]
An undergraduate text on automata and computability theory. [top]
Dexter Kozen. On regularity-preserving functions. Bull. Europ. Assoc. Theor. Comput. Sci., 58:131-138, February 1996.
[full text (.ps)] [bibtex] [top]
A characterization of numeric functions that preserve regularity. [top]
Nils Klarlund and Dexter Kozen. Rabin measures. Chicago Journal of Theoretical Computer Science, 1995(3), September 1995.
[full text (.pdf)] [bibtex] [top]
Rabin conditions are a general class of properties of infinite sequences that encompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper, we introduce a concept, called a Rabin measure, which in a precise sense expresses progress for each transition towards satisfaction of the Rabin condition. We show that these measures of progress are linked to the Kleene-Brouwer ordering of recursion theory. Klarlund uses this property to establish an exponential upper bound for the complementation of automata on infinite trees. When applied to termination problems under fairness constraints, Rabin measures eliminate the need for syntax-dependent, recursive applications of proof rules. [top]
Dexter Kozen. Partial automata and finitely generated congruences: An extension of Nerode's theorem. In J. N. Crossley, J. B. Remmel, R. A. Shore, and M. E. Sweedler, editors, Logical Methods: In Honor of Anil Nerode's Sixtieth Birthday, pages 490-511. Birkhäuser, Ithaca, New York, 1993.
[full text (.ps)] [bibtex] [top]
Let T be the set of ground terms over a finite ranked alphabet. We define partial automata on T and prove that the finitely generated congruences on T are in one-to-one correspondence (up to isomorphism) with the finite partial automata on T with no inaccessible and no inessential states. We give an application in term rewriting: every ground term rewrite system has a canonical equivalent system that can be constructed in polynomial time. [top]
Dexter Kozen. On the Myhill-Nerode theorem for trees. Bull. Europ. Assoc. Theor. Comput. Sci., 47:170-173, June 1992.
[full text (.ps)] [bibtex] [top]
We present an elementary proof of the Myhill-Nerode Theorem for term automata. [top]

Algorithms & Complexity

Nikos Karampatziakis and Dexter Kozen. Learning prediction suffix trees with Winnow. In Léon Bottou and Michael Littman, editors, Proc. 26th Int. Conf. Machine Learning (ICML'09), pages 489-496, Montreal, Canada, June 2009. Omnipress.
[full text (.pdf)] [bibtex] [top]
Prediction suffix trees (PSTs) are a popular tool for modeling sequences and have been successfully applied in many domains such as compression and language modeling. In this work we adapt the well studied Winnow algorithm to the task of learning PSTs. The proposed algorithm automatically grows the tree, so that it provably remains competitive with any fixed PST determined in hindsight. At the same time we prove that the depth of the tree grows only logarithmically with the number of mistakes made by the algorithm. Finally, we empirically demonstrate its effectiveness in two different tasks. [top]
Dexter Kozen. Lexicographic flow. Technical Report http://hdl.handle.net/1813/13018, Computing and Information Science, Cornell University, June 2009.
[full text (.pdf)] [bibtex] [top]
The lexicographic flow problem is a flow problem in which the edges are assigned priorities, and we wish to find a flow that is lexicographically maximum with respect to the priority assignment. The problem is reducible to a weighted flow problem, but we show that exponentially large weights are necessary in general. We then give an efficient direct algorithm that does not use weights. [top]
Dexter Kozen. Optimal coin flipping. Technical Report http://hdl.handle.net/1813/12869, Computing and Information Science, Cornell University, June 2009.
[full text (.pdf)] [bibtex] [top]
This paper studies the problem of simulating a coin of arbitrary real bias q with a coin of arbitrary real bias p with minimum loss of entropy. We establish a lower bound that is strictly greater than the information-theoretic bound. We show that as a function of q, it is an everywhere-discontinuous self-similar fractal. We provide efficient protocols that achieve the lower bound to within any desired accuracy for (3-sqrt(5))/2 < p < 1/2 and achieve it exactly for p=1/2. [top]
Dexter Kozen and Alexa Sharp. On distance coloring. Technical Report TR2007-2084, Computing and Information Science, Cornell University, June 2007.
[full text (.pdf)] [bibtex] [top]
Call a connected undirected graph (d,c)-colorable if there is a vertex coloring using at most c colors such that no two vertices of distance d or less have the same color. It is well known that (1,2)-colorability is decidable in linear time, but (1,c)-colorability for c >= 3 is NP-complete. Sharp (2007) shows that for fixed d >= 2, the (d,c)-colorability problem is solvable in linear time for c <= 3d/2 and NP-complete otherwise. In this note we give an alternative construction that improves the upper time bound as a function of d for the case c <= 3d/2. The construction entails a generalization of the notion of tree ecomposition and bounded treewidth (Robertson and Seymour 1986) to arbitrary overlay graphs, not just trees, which may be of independent interest. [top]
Daniel Sheldon, M. A. Saleh Elmohamed, and Dexter Kozen. Collective inference on Markov models for modeling bird migration. In J. Platt, D. Koller, Y. Singer, and S. Roweis, editors, Advances in Neural Information Processing Systems (NIPS'07), volume 20, December 2007.
[full text (.pdf)] [bibtex] [top]
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 algorithms and hardness results for several variants of this problem which arise by revealing different information to the observer and imposing different requirements for the reconstruction of sample paths. Our algorithms are analogous to the classical Viterbi algorithm for Hidden Markov Models, which finds 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. [top]
Dexter Kozen, Yaron Minsky, and Brian Smith. Efficient algorithms for optimal video transmission. In James A. Storer and Martin Cohn, editors, Proc. Data Compression Conference (DCC'98), pages 229-238, Snowbird, Utah, March 1998. IEEE.
[full text (.ps)] [bibtex] [top]
This paper addresses the problem of sending an encoded video stream over a channel of limited bandwidth. When there is insufficient bandwidth available, some data must be dropped. For many video encodings, some data are more important that others, leading to a natural prioritization of the data. In this paper we give fast algorithms to determine a prioritization which optimizes the visual quality of the received data. By optimized visual quality, we mean that the expected maximum interval of unplayable frames is minimized. Our results are obtained in a model of encoded video data that is applicable to many encoding technologies. The highlight of the model is an interesting relationship between the play order and dependence order of frames. The property allows fast determination of optimal send orders by dynamic programming and is satisfied by all MPEG sequences. [top]
Dexter Kozen and Shmuel Zaks. Optimal bounds for the change-making problem. Theor. Comput. Sci., 123:377-388, 1994.
[full text (.ps)] [bibtex] [top]
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₁ < c₂ < ... < c_m. Chang and Gill show that if the greedy algorithm is not always optimal, then there exists a counterexample x in the range

c₃ <= x < (c_m(c_mc_m-1 + c_m - 3c_{m-1}) / (c_m - c_m-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

c₃ + 1 < x < c_m + c_m-1 ,

and these bounds are tight. Moreover, we give a simple test for the existence of a counterexample that does not require the calculation of optimal representations. In addition, we give a complete characterization of three-coin systems and an efficient algorithm for all systems with a fixed number of coins. Finally, we show that a related problem is coNP-complete. [top]
Dexter Kozen. The Design and Analysis of Algorithms. Springer-Verlag, New York, 1991.
[table of contents (.ps)] [bibtex] [top]
A graduate-level textbook on algorithms. [top]
Dexter Kozen, Umesh Vazirani, and Vijay Vazirani. NC algorithms for comparability graphs, interval graphs, and unique perfect matching. In Maheshwari, editor, Proc. 5th Conf. Found. Software Technology and Theor. Comput. Sci., volume 206 of Lecture Notes in Computer Science, pages 496-503, New Delhi, December 1985. Springer-Verlag.
[full text (.ps)] [bibtex] [top]
Laszlo Lovasz recently posed the following problem: ``Is there an NC algorithm for testing if a given graph has a unique perfect matching?'' We present such an algorithm for bipartite graphs. We also give NC algorithms for obtaining a transitive orientation of a comparability graph, and an interval representation of an interval graph. These enable us to obtain an NC algorithm for finding a maximum matching in an incomparability graph. [top]

Coding Theory

Kenneth Andrews, Chris Heegard, and Dexter Kozen. Interleaver design methods for turbo codes. In Proc. International Symposium on Information Theory (ISIT'98), page 420. IEEE, August 1998.
[full text (.pdf)] [bibtex] [top]
It is generally assumed that when a turbo decoder is operating at low bit error rates, error sequences have small Hamming weights. From this, and properties of turbo encoders, a mathematical structure is developed for interleaver design, permitting the identification of quantitatively optimal interleavers. Simulations show the math captures some but not all the essential characteristics of a successful interleaver. Modifying a random interleaver according to the mathematical ideas gives excellent simulation results. [top]
Kenneth Andrews, Chris Heegard, and Dexter Kozen. A theory of interleavers. Technical Report TR97-1634, Computer Science Department, Cornell University, June 1997.
[full text (.ps)] [bibtex] [top]
An interleaver is a hardware device commonly used in conjunction with error correcting codes to counteract the effect of burst errors. Interleavers are in widespread use and much is known about them from an engineering standpoint. In this paper we propose a mathematical model that provides a rigorous foundation for the theoretical study of interleavers. The model captures precisely such notions as block and convolutional interleavers, spread, periodicity, causality, latency, and memory usage. Using this model, we derive several optimality results on the latency and memory usage of interleavers. We describe a family of block interleavers and show that they are optimal with respect to latency among all block interleavers with a given spread. We also give tight upper and lower bounds on the memory requirements of interleavers. [top]

Security

Fred B. Schneider, Dexter Kozen, Greg Morrisett, and Andrew C. Myers. Language-based security for malicious mobile code. In Department of Defense Sponsored Information Security Research: New Methods for Protecting Against Cyber Threats, pages 477-494. Wiley, 2007.
[full text (.pdf)] [bibtex] [top]
A survey of language-based techniques for secure mobile processes. [top]
Frank Adelstein, Dexter Kozen, and Matt Stillerman. Malicious code detection for open firmware. In Proc. 18th Computer Security Applications Conf. (ACSAC'02), pages 403-412, December 2002.
[full text (.pdf)] [bibtex] [top]
Malicious boot firmware is a largely unrecognized but significant security risk to our global information infrastructure. Since boot firmware executes before the operating system is loaded, it can easily circumvent any operating system-based security mechanism. Boot firmware programs are typically written by third-party device manufacturers and may come from various suppliers of unknown origin. In this paper we describe an approach to this problem based on load-time verification of onboard device drivers against a standard security policy designed to limit access to system resources. We also describe our ongoing effort to construct a prototype of this technique for Open Firmware boot platforms. [top]
Dexter Kozen. Language-based security. In M. Kutyowski, L. Pacholski, and T. Wierzbicki, editors, Proc. Conf. Mathematical Foundations of Computer Science (MFCS'99), volume 1672 of Lecture Notes in Computer Science, pages 284-298. Springer-Verlag, September 1999.
[full text (.pdf)] [bibtex] [top]
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. [top]
Dexter Kozen. Efficient code certification. Technical Report TR98-1661, Computer Science Department, Cornell University, January 1998.
[full text (.pdf)] [bibtex] [top]
We introduce a simple and efficient approach to the certification of compiled code. We ensure a basic but nontrivial level of code safety, including control flow safety, memory safety, and stack safety. The system is designed to be simple, efficient, and (most importantly) relatively painless to incorporate into existing compilers. Although less expressive than the proof carrying code of Necula and Lee or typed assembly language of Morrisett et al., our certificates are by comparison extremely compact and relatively easy to produce and to verify. Unlike JAVA byte code, our system operates at the level of native code; it is not interpreted and no further compilation is necessary. [top]

Other

Chavdar Botev, Hubert Chao, Theodore Chao, Yim Cheng, Raymond Doyle, Sergey Grankin, Jon Guarino, Saikat Guha, PeiChen Lee, Dan Perry, Christopher Re, Ilya Rifkin, Tingyan Yuan, Dora Abdullah, Kathy Carpenter, David Gries, Dexter Kozen, Andrew Myers, David Schwartz, and Jayavel Shanmugasundaram. Supporting workflow in a course management system. In W. Dann et al., editor, Proc. 36th Technical Symposium on Computer Science Education (SIGCSE'05), pages 262-266. ACM SIGCSE, February 2005.
[full text (.pdf)] [bibtex] [top]
CMS is a secure and scalable web-based course management system developed by the Cornell University Computer Science Department. The system was designed to simplify, streamline, and automate many aspects of the workflow associated with running a large course, such as course creation, importing students, management of student workgroups, online submission of assignments, assignment of graders, grading, handling regrade requests, and preparation of final grades. In contrast, other course management systems of which we are aware provide only specialized solutions for specific components, such as grading. CMS is increasingly widely used for course management at Cornell University. In this paper we articulate the principles we followed in designing the system and describe the features that users found most useful. [top]
Dexter Kozen. On teaching left-handed children to write. Technical Report TR87-844, Computer Science Department, Cornell University, June 1987.
[full text] [bibtex] [top]
A treatise on how to teach left-handed children to write comfortably and without smearing. [top]

Publications Available Online Dexter Kozen

Kleene Algebra & Logic

Programming Languages & Program Analysis

Computational Algebra

Automata & Formal Languages

Algorithms & Complexity

Coding Theory

Security

Other

Publications Available Online
Dexter Kozen