Dexter Kozen. Lexicographic flow. Manuscript, July 2008. Draft.
[top]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[top]
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. A survey of language-based techniques for secure mobile processes.
[top]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text]
[bibtex]
[top]
Dexter Kozen and Alexa Sharp. On distance coloring. Technical Report TR2007-2084, Computing and Information Science, Cornell University, June 2007. 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]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen. Theory of Computation. Springer, 2006. A graduate-level text on theory of computation.
[top]
[table of contents (.pdf)]
[bibtex]
[top]
Dexter Kozen and Ganesh Ramanarayanan. Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge Management. Technical Report TR2005-1985, Computer Science Department, Cornell University, March 2005. 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]
[full text (.pdf)]
[bibtex]
[top]
Lucja Kot and Dexter Kozen. Kleene Algebra and Bytecode Verification. Proc. 1st Workshop Bytecode Semantics, Verification, Analysis, and Transformation (Bytecode'05), ed. Fausto Spoto, Edinburgh, April 2005, 201-215. 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]
[full text (.pdf)]
[bibtex]
[top]
Chavdar Botev, Hubert Chao, Theodore Chao, Yim Cheng, Raymond Doyle, Sergey Grankin, Jon Guarino, Saikat Guha, Pei-Chen 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. Technical Symposium on Computer Science Education (SIGCSE 2005). ACM SIGCSE, February 2005, pages 262-266. 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]
[full text (.pdf)]
[bibtex]
[top]
Lucja Kot and Dexter Kozen. Second-Order Abstract Interpretation via Kleene Algebra. Technical Report TR2004-1971, Computer Science Department, Cornell University, December 2004. 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen and Bernhard Möller. Separability in Domain Semirings. Technical Report 2004-16, Universität Augsburg, Institut für Informatik, December 2004. 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen. Toward the Automation of Category Theory. Technical Report TR2004-1964, Computer Science Department, Cornell University, September 2004. 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen. Natural transformations as rewrite rules and monad composition. Technical Report TR2004-1942, Computer Science Department, Cornell University, July 2004. 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen. Some Results in Dynamic Model Theory. Science of Computer Programming 51:1-2, May 2004, 3-22. Special issue, Mathematics of Program Construction (MPC 2002). Ed. E. Boiten and B. Moller. 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 TrU 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 RelU is not universal for the equational theory of relation algebras of Tarskian frames, but it is so modulo observational equivalence.
[top]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen. Computational Inductive Definability. Annals of Pure and Applied Logic 126:1-3, April 2004, 139-148. Special issue: Provinces of logic determined. Essays in the memory of Alfred Tarski. Ed. Z. Adamowicz, S. Artemov, D. Niwinski, E. Orlowska, A. Romanowska, J. Wolenski. 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen. Kleene Algebra with Tests and the Static Analysis of Programs. Technical Report TR2003-1915, Computer Science Department, Cornell University, November 2003. 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen. Automata on Guarded Strings and Applications. Matématica Contemporânea 24 (2003), 117-139. 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]
[full text (.pdf)]
[bibtex]
[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. We show that the universal Horn theory of relational Kleene algebras is Pi-1-1-complete.
[top]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen and Jerzy Tiuryn. Substructural Logic and Partial Correctness. Trans. Computational Logic, 4(3), July 2003, 355-378. (Subsumes Dexter Kozen and Jerzy Tiuryn. Intuitionistic Linear Logic and Partial Correctness. In Proc. 16th IEEE Symp. Logic in Comput. Sci. (LICS'01), June 2001, 259-268.) 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen. On Hoare Logic, Kleene Algebra, and Types. In P. Gärdenfors, J. Wolenski, 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. 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]
[full text (.pdf)]
[bibtex]
[top]
Robert Givan, David McAllester, Carl Witty and Dexter Kozen. Tarskian Set Constraints. Information and Computation, 174(2):105-131, May 2002. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen. On the Complexity of Reasoning in Kleene Algebra. Information and Computation 179, 152-162, 2002. 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,
[full text (.pdf)]
[bibtex]
[top]
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. 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 t1,...,tn, does p halt on input t1,...,tn 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]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[top]
Frank Adelstein, Dexter Kozen and Matt Stillerman. Malicious Code Detection for Open Firmware. In Proc. 18th Computer Security Applications Conf. (ACSAC'02), Las Vegas, December 2002, pages 403-412. 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]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen. On Two Letters versus Three. Technical Report 2002-1860, Computer Science Department, Cornell University, February 2002. 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]
[full text (.pdf)]
[bibtex]
[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. 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]
[full text (.pdf)]
[bibtex]
[top]
Allegra Angus and Dexter Kozen. Kleene Algebra with Tests and Program Schematology. Technical Report TR2001-1844, Computer Science Department, Cornell University, July 2001. 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen and Jerzy Tiuryn. On the completeness of propositional Hoare logic. Information Sciences, 139 (2001), 187-195. 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
[full text (.pdf)]
[bibtex]
[top]
----------------------------
{b}p{c}
are derivable in PHL, provided the propositional expressiveness conditions are met. Moreover, if the programs pi 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, eds., Proc. 18th Symp. Theoretical Aspects of Computer Science (STACS'01), Dresden, Germany, February 2001. Springer-Verlag, Lecture Notes in Computer Science 2010, 27-38. 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]
[full text (.pdf)]
[bibtex]
[top]
Ernie Cohen and Dexter Kozen. A Note on the Complexity of Propositional Hoare Logic. Trans. Computational Logic 1:1 (July 2000), 171-174. We provide a simpler alternative proof of the PSPACE-hardness of propositional Hoare logic.
[top]
[full text (.pdf)]
[bibtex]
[top]
David Harel, Dexter Kozen and Jerzy Tiuryn. Dynamic Logic. MIT Press, 2000. ISBN 0-262-08289-6. 459 pages. A graduate-level textbook on Dynamic Logic.
[top]
[table of contents (.ps)]
[bibtex]
[top]
Dexter Kozen and Maria-Cristina Patron. Certification of compiler optimizations using Kleene algebra with tests. In J. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palamidessi, L.~M. Pereira, Y. Sagiv, and P.~J. Stuckey, eds, Proc. 1st Int. Conf. Computational Logic (CL2000), volume 1861 of Lecture Notes in Artificial Intelligence, Springer-Verlag, London, July 2000, 568-582. 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen. On Hoare logic and Kleene algebra with tests. Proc. IEEE Conf. Logic in Computer Science (LICS'99), IEEE, July 1999, 167-172. Trans. Computational Logic 1:1 (July 2000), 60-76. 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen. Language-Based Security. In M. Kutylowski, 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. 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]
[full text (.pdf)]
[bibtex]
[top]
Mark Hopkins and Dexter Kozen. Parikh's theorem in commutative Kleene algebra. Proc. 14th Conf. Logic in Computer Science (LICS'99), IEEE, July 1999, 394-401. 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 fi(x1,...,xn) <= xi, 1 <= i <= n, over a commutative Kleene algebra K has a unique least solution in Kn; moreover, the components of the solution are given by polynomials in the coefficients of the fi. We also give a closed-form solution in terms of the Jacobian matrix.
[top]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen. Set Constraints and Logic Programming. Information and Computation 142:1 (April 1998), 2-25. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen, Yaron Minsky, and Brian Smith. Efficient algorithms for optimal video transmission. In: Proc. IEEE Data Compression Conference (DCC'98), ed. James A. Storer and Martin Cohn, Snowbird, Utah, March 1998, 229-238. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen. Typed Kleene algebra. Technical Report TR98-1669, Computer Science Department, Cornell University, March 1998. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen. Efficient Code Certification. Technical report TR98-1661, Computer Science Department, Cornell University, January 1998. 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]
[full text (.pdf)]
[bibtex]
[top]
Kenneth Andrews, Chris Heegard, and Dexter Kozen. A theory of interleavers. Technical report TR97-1634, Computer Science Department, Cornell University, June 1997. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen. Kleene algebra with tests. Transactions on Programming Languages and Systems, May 1997, 427-443. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen. Automata and Computability. Springer, 1997. ISBN 0-387-94907-0. 400 pages. (table of contents and a few sample chapters) An undergraduate text on automata and computability theory.
[top]
[table of contents (.ps)]
[bibtex]
[top]
Dexter Kozen and Kjartan Stefansson. Computing the Newtonian graph. J. Symbolic Computation 24 (1997), 125-136.
[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 Nf(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]
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. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen and Frederick Smith. Kleene algebra with tests: completeness and decidability. Proc. 10th Int. Workshop on Computer Science Logic (CSL'96), ed. D. van Dalen and M. Bezem, Utrecht, The Netherlands, Springer-Verlag Lecture Notes in Computer Science volume 1258, September 1996, 244-259. 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]
[full text (.ps)]
[bibtex]
[top]
Allan Cheng and Dexter Kozen. Some notes on rational spaces. Technical Report TR96-1576, Computer Science Department, Cornell University, March 1996. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen. Rational Spaces and Set Constraints. Theoretical Computer Science 167 (1996), 73-94. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen. On regularity-preserving functions. Bull. Europ. Assoc. Theor. Comput. Sci. 58, February, 1996, 131-138. A characterization of numeric functions that preserve regularity.
[top]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen, Susan Landau, and Richard Zippel. Decomposition of algebraic functions. J. Symbolic Computation, 22:3 (Sept. 1996), 235-246. 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]
[full text (.ps)]
[bibtex]
[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 International Colloquium, ICALP '96, volume 1099 of Lect. Notes in Comput. Sci., pages 134-145. Eur. Assoc. for Theoretical Comput. Sci., Springer, July 1996. 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]
[full text (.ps)]
[bibtex]
[top]
Nils Klarlund and Dexter Kozen. Rabin measures. Chicago Journal of Theoretical Computer Science, 1995(3), September 1995. 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]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science 5 (1995), 1-13. 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(n2) 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]
[full text (.ps)]
[bibtex]
[top]
Alexander Aiken, Dexter Kozen, and Edward Wimmers. Decidability of systems of set constraints with negative constraints. Infor. and Comput. 122:1, October 1995, 30-44. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient inference of partial types. J. Comput. Syst. Sci. 49:2 (October 1994), 306-324. 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(n3) 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]
[full text (.ps)]
[bibtex]
[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, Springer-Verlag Lect. Notes in Comput. Sci. 880, 1-11, December 1994. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Infor. and Comput., 110:366-390, May 1994. 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]
[full text (.ps)]
[bibtex]
[top]
Jin-Yi Cai, Wolfgang Fuchs, Dexter Kozen, and Zicheng Liu. Efficient Average-Case Algorithms for the Modular Group. In Proc. 35th IEEE Symp. Foundations of Computer Science, November 1994, 143-152. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen and Shmuel Zaks. Optimal bounds for the change-making problem. Theor. Comput. Sci., 123:377-388, 1994. 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 = c1 < c2 < ... < cm. Chang and Gill show that if the greedy algorithm is not always optimal, then there exists a counterexample x in the range
[full text (.ps)]
[bibtex]
[top]
c3 <= x < (cm(cmcm-1 + cm - 3c{m-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 ,
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. On action algebras. In J. van Eijck and A. Visser, editors, Logic and Information Flow, pages 78-88. MIT Press, 1994. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen. Logical aspects of set constraints. In Proc. 1993 Conf. Computer Science Logic (CSL'93). Eur. Assoc. Comput. Sci. Logic, Swansea, UK, September 1993. Ed. E. B"orger, Y. Gurevich, and K. Meinke, Springer-Verlag Lect. Notes in Comput. Sci. 832, 175-188. 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]
[full text (.ps)]
[bibtex]
[top]
Doug Ierardi and Dexter Kozen. Parallel resultant computation. In J. Reif, editor, Synthesis of Parallel Algorithms, pages 679-720. Morgan Kaufmann, 1993. 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]
[full text (.ps)]
[bibtex]
[top]
Alexander Aiken, Dexter Kozen, Moshe Vardi, and Edward Wimmers. The complexity of set constraints. In Proc. 1993 Conf. Computer Science Logic (CSL'93). Eur. Assoc. Comput. Sci. Logic, Ed. E. B"orger, Y. Gurevich, and K. Meinke, Swansea, UK, September 1993, Springer-Verlag Lect. Notes in Comput. Sci. 832, 1-17. 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]
[full text (.ps)]
[bibtex]
[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, 1993. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen. On the Myhill-Nerode theorem for trees. Bull. Europ. Assoc. Theor. Comput. Sci., 47:170-173, June 1992. We present an elementary proof of the Myhill-Nerode Theorem for term automata.
[top]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen. The Design and Analysis of Algorithms. Springer-Verlag, 1991. ISBN 0-387-97687-6. 322 pages. A graduate-level textbook on algorithms.
[top]
[table of contents (.ps)]
[bibtex]
[top]
Dexter Kozen. On Kleene algebras and closed semirings. In Rovan, editor, Proc. Math. Found. Comput. Sci., volume 452 of Lect. Notes in Comput. Sci., pages 26-47. Springer, 1990. 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]
[full text (.ps)]
[bibtex]
[top]
Neil Immerman and Dexter Kozen. Definability with bounded number of bound variables. Infor. and Comp. 83:2 (November 1989), 121-139. 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]
[full text (.ps)]
[bibtex]
[top]
Dexter Kozen and Susan Landau. Polynomial decomposition algorithms. J. Symbolic Computation 7 (1989), 445-456. 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(n2)-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]
[full text (.ps)]
[bibtex]
[top]
Michael Ben-Or, Ephraim Feig, Dexter Kozen, and Prasoon Tiwari. A fast parallel algorithm for determining all roots of a polynomial with real roots. SIAM J. Computing 17:6, 1081-1092, 1988. Given a polynomial p(z) of degree n with m bit integer coefficients and an integer mu, the problem of determining all its roots with error less than 2mu 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]
[full text]
[bibtex]
[top]
Dexter Kozen. A finite model theorem for the propositional mu-calculus. Studia Logica 47(3):233-241, 1988. We prove a finite model theorem and infinitary completeness result for the propositional $\mu$-calculus. The construction establishes a link between finite model theorems for propositional program logics and the theory of well-quasi-orders.
[top]
[full text (.pdf)]
[bibtex]
[top]
Krzysztof Apt and Dexter Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22:307-309, 1986. We show that some very simple temporal properties of schematic finite-state programs are not semi-decidable.
[top]
[full text (.pdf)]
[bibtex]
[top]
Dexter Kozen, Umesh Vazirani, and Vijay Vazirani. NC algorithms for comparability graphs, interval graphs, and unique perfect matching. 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]
[full text (.ps)]
[bibtex]
[top]
