KA.bib

   1 @InProceedings{KA-complexity,
   2   author =       "D. Kozen",
   3   title =        "On the Complexity of Reasoning in {Kleene} Algebra",
   4   pages =        "195--203",
   5   booktitle =    "12th Annual {IEEE} Symposium on Logic in Computer
   6                  Science ({LICS}'97)",
   7   ISBN =         "0-8186-7925-5",
   8   month =        jun,
   9   publisher =    "IEEE",
  10   address =      "Washington - Brussels - Tokyo",
  11   year =         "1997",
  12 }
  13
  14 @Article{KAT,
  15   author =       "Dexter Kozen",
  16   title =        "{Kleene} Algebra with Tests",
  17   journal =      "ACM Transactions on Programming Languages and
  18                  Systems",
  19   volume =       "19",
  20   number =       "3",
  21   pages =        "427--443",
  22   month =        may,
  23   year =         "1997",
  24   CODEN =        "ATPSDT",
  25   ISSN =         "0164-0925",
  26   bibdate =      "Thu Sep 11 18:32:35 MDT 1997",
  27   URL =          "http://www.acm.org/pubs/citations/journals/toplas/1997-19-3/p427-kozen/",
  28   abstract =     "We introduce Kleene algebra with tests, an equational
  29                  system for manipulating programs. We give a purely
  30                  equational proof, using Kleene algebra with tests and
  31                  commutativity conditions, of the following classical
  32                  result: every {\bf while} program can be simulated by a
  33                  while program can be simulated by a {\bf while} program
  34                  with at most one {\bf while} loop. The proof
  35                  illustrates the use of Kleene algebra with tests and
  36                  commutativity conditions in program equivalence
  37                  proofs.",
  38   acknowledgement = ack-nhfb,
  39   keywords =     "design; languages; theory; verification",
  40   subject =      "{\bf D.2.2} Software, SOFTWARE ENGINEERING, Tools and
  41                  Techniques, Structured programming. {\bf D.2.4}
  42                  Software, SOFTWARE ENGINEERING, Program Verification,
  43                  Correctness proofs. {\bf D.3.3} Software, PROGRAMMING
  44                  LANGUAGES, Language Constructs and Features, Control
  45                  structures. {\bf F.3.1} Theory of Computation, LOGICS
  46                  AND MEANINGS OF PROGRAMS, Specifying and Verifying and
  47                  Reasoning about Programs, Assertions. {\bf F.3.1}
  48                  Theory of Computation, LOGICS AND MEANINGS OF PROGRAMS,
  49                  Specifying and Verifying and Reasoning about Programs,
  50                  Invariants. {\bf F.3.1} Theory of Computation, LOGICS
  51                  AND MEANINGS OF PROGRAMS, Specifying and Verifying and
  52                  Reasoning about Programs, Logics of programs. {\bf
  53                  F.3.1} Theory of Computation, LOGICS AND MEANINGS OF
  54                  PROGRAMS, Specifying and Verifying and Reasoning about
  55                  Programs, Mechanical verification. {\bf F.3.1} Theory
  56                  of Computation, LOGICS AND MEANINGS OF PROGRAMS,
  57                  Specifying and Verifying and Reasoning about Programs,
  58                  Pre- and post-conditions. {\bf F.3.1} Theory of
  59                  Computation, LOGICS AND MEANINGS OF PROGRAMS,
  60                  Specifying and Verifying and Reasoning about Programs,
  61                  Specification techniques. {\bf F.3.2} Theory of
  62                  Computation, LOGICS AND MEANINGS OF PROGRAMS, Semantics
  63                  of Programming Languages, Algebraic approaches to
  64                  semantics. {\bf F.3.3} Theory of Computation, LOGICS
  65                  AND MEANINGS OF PROGRAMS, Studies of Program
  66                  Constructs, Control primitives. {\bf I.1.1} Computing
  67                  Methodologies, ALGEBRAIC MANIPULATION, Expressions and
  68                  Their Representation, Simplification of expressions.
  69                  {\bf I.1.3} Computing Methodologies, ALGEBRAIC
  70                  MANIPULATION, Languages and Systems, Special-purpose
  71                  algebraic systems. {\bf I.2.2} Computing Methodologies,
  72                  ARTIFICIAL INTELLIGENCE, Automatic Programming, Program
  73                  modification. {\bf I.2.2} Computing Methodologies,
  74                  ARTIFICIAL INTELLIGENCE, Automatic Programming, Program
  75                  synthesis; program transformation; program
  76                  verification",
  77 }
  78
  79 @InProceedings{KAT-Hoare,
  80   author =       "D. Kozen",
  81   title =        "On {Hoare} Logic and {Kleene} Algebra with Tests",
  82   pages =        "167--173",
  83   booktitle =    "14th Symposium on Logic in Computer Science
  84                  ({LICS}'99)",
  85   ISBN =         "0-7695-0158-3",
  86   month =        jul,
  87   publisher =    "IEEE",
  88   address =      "Washington - Brussels - Tokyo",
  89   year =         "1999",
  90 }
  91
  92 @article{KAT-Hoare-simpler,
  93  author = {Ernie Cohen and Dexter Kozen},
  94  title = {A note on the complexity of propositional {Hoare} logic},
  95  journal = {ACM Trans. Comput. Logic},
  96  volume = {1},
  97  number = {1},
  98  year = {2000},
  99  issn = {1529-3785},
 100  pages = {171--174},
 101  doi = {http://doi.acm.org/10.1145/343369.343404},
 102  publisher = {ACM Press},
 103  address = {New York, NY, USA},
 104  }
 105
 106 @Article{KAT-commutativity,
 107   author =       "D. Kozen",
 108   title =        "{Kleene} Algebra with Tests and Commutativity
 109                  Conditions",
 110   journal =      "Lecture Notes in Computer Science",
 111   volume =       "1055",
 112   pages =        "14--??",
 113   year =         "1996",
 114   CODEN =        "LNCSD9",
 115   ISSN =         "0302-9743",
 116   bibdate =      "Sat May 11 13:45:32 MDT 1996",
 117   acknowledgement = ack-nhfb,
 118 }
 119
 120
 121 @InProceedings{KAT-complete-decidable,
 122   author =       "Kozen and Smith",
 123   title =        "{Kleene} Algebra with Tests: Completeness and
 124                  Decidability",
 125   booktitle =    "CSL: 10th Workshop on Computer Science Logic",
 126   publisher =    "LNCS, Springer-Verlag",
 127   year =         "1996",
 128 }
 129
 130
 131 @Article{KA-regevents-complete,
 132   refkey =       "C1459",
 133   title =        "A Completeness Theorem for {Kleene} Algebras and the
 134                  Algebra of Regular Events",
 135   author =       "Dexter Kozen",
 136   pages =        "366--390",
 137   journal =      "Information and Computation",
 138   month =        "1~" # may,
 139   year =         "1994",
 140   volume =       "110",
 141   number =       "2",
 142   preliminary =  "LICS::Kozen1991:214",
 143   abstract =     "We give a finitary axiomatization of the algebra of
 144                  regular events involving only equations and equational
 145                  implications. Unlike Salomaa's axiomatizations, the
 146                  axiomatization given here is sound for all
 147                  interpretations over Kleene algebras.",
 148   xxx-references = "Immerman86, LICS::Kozen91, Leivant90, FOCS::Safra88,
 149                  JACM::Salomaa66, LICS::Walukiewicz93",
 150   references =   "\cite{IC::Immerman1986} \cite{LICS::Kozen1991}
 151                  \cite{IC::Leivant1990} \cite{FOCS::Safra1988}
 152                  \cite{JACM::Salomaa1966} \cite{LICS::Walukiewicz1993}",
 153 }
 154
 155 @Misc{KA-hypo,
 156   title =        "Hypotheses in {Kleene} Algebra",
 157   author =       "Ernie Cohen",
 158   year =         "1993",
 159   month =        feb # "~03",
 160   abstract =     "Kleene algebra (an Horn axiomatization of Kleene's
 161                  algebra of regular events) has proved to be an
 162                  effective tool for reasoning about programs. Within the
 163                  algebra, we can reason succinctly about both ordinary
 164                  safety properties and important program transformations
 165                  such as loop unwinding, change of data representation,
 166                  and refinement of atomicity. One of the nice properties
 167                  of Kleene algebra is that its equational theory has a
 168                  simple decision procedure. However, to use it for
 169                  programming applications, we need to reason in the
 170                  presence of hypotheses stating the equality of certain
 171                  programs; such hypotheses can, in general, render the
 172                  theory undecidable. In this note, we show that for
 173                  certain important cases, checking an equation under
 174                  hypotheses can be reduced to checking a related
 175                  equation without hypotheses. 1 Introduction A Kleene
 176                  algebra (KA) is an algebraic structure (K; +; ; ; ; 0;
 177                  1) satisfying the following axioms (we use infix
 178                  notation for + and ;, and postfix notation for ,
 179                  an...",
 180   citeseer-references = "oai:CiteSeerPSU:111064",
 181   annote =       "The Pennsylvania State University CiteSeer Archives",
 182   language =     "en",
 183   oai =          "oai:CiteSeerPSU:1688",
 184   rights =       "unrestricted",
 185   subject =      "Ernie Cohen Hypotheses in {Kleene} Algebra",
 186   URL =          "http://citeseer.ist.psu.edu/1688.html;
 187                  ftp://thumper.bellcore.com/pub/ernie/research/kozen.ps.gz",
 188 }
 189
 190 @Misc{KAT-complexity,
 191   title =        "The Complexity of {Kleene} Algebra with Tests",
 192   author =       "Dexter Kozen and Ernie Cohen and Frederick Smith",
 193   year =         "1996",
 194   month =        oct # "~11",
 195   abstract =     "Kleene algebras with tests provide a natural framework
 196                  for equational specification and verification. Kleene
 197                  algebras with tests and related systems have been used
 198                  successfully in basic safety analysis, source-to-source
 199                  program transformation, and concurrency control. The
 200                  equational theory of Kleene algebras with tests has
 201                  been shown to be decidable in at most exponential time
 202                  by an efficient reduction to Propositional Dynamic
 203                  Logic. In this paper we prove that the theory is
 204                  PSPACE-complete. 1 Introduction Kleene algebra with
 205                  tests (KAT) [15] is an algebraic system intermediate to
 206                  Kleene algebra (KA) and Propositional Dynamic Logic
 207                  (PDL) in expressive power. One can use KAT for a range
 208                  of common verification tasks without resorting to the
 209                  full power of PDL. KAT and related systems have been
 210                  applied successfully to real problems in basic safety
 211                  analysis, source-to-source 1 Bell Communications
 212                  Research Inc., 445 South St., Morristown, NJ 07960, USA
 213                  2 Computer Science Department, Cor...",
 214   citeseer-references = "oai:CiteSeerPSU:62200; oai:CiteSeerPSU:188632",
 215   annote =       "The Pennsylvania State University CiteSeer Archives",
 216   language =     "en",
 217   oai =          "oai:CiteSeerPSU:85616",
 218   rights =       "unrestricted",
 219   subject =      "Dexter Kozen,Ernie Cohen,Frederick Smith The
 220                  Complexity of Kleene Algebra with Tests",
 221   URL =          "http://citeseer.ist.psu.edu/85616.html;
 222                  http://www.cs.cornell.edu/kozen/papers/ckat.ps",
 223 }
 224
 225 @techreport{KA-lect04,
 226   author =       {Dexter Kozen},
 227   title =        {Introduction to {Kleene} Algebra},
 228   howpublished = {\url!http://www.cs.cornell.edu/Courses/cs786/2004sp/Lectures/lectures.htm!},
 229   year =         {2004},
 230   note =         {\url!http://www.cs.cornell.edu/Courses/cs786/2004sp/Lectures/lectures.htm!},
 231   institution =  {Cornell University},
 232  address = {Ithaca, NY, USA},
 233   type =         {Course notes},
 234 }
 235
 236 @techreport{KA-lect02,
 237   author =       {Dexter Kozen},
 238   title =        {Introduction to {Kleene} Algebra},
 239   howpublished = {\url!http://www.cs.cornell.edu/Courses/cs786/2002sp/Lectures/lectures.htm!},
 240   year =         {2002},
 241   note =         {\url!http://www.cs.cornell.edu/Courses/cs786/2002sp/Lectures/lectures.htm!},
 242   institution =  {Cornell University},
 243  address = {Ithaca, NY, USA},
 244   type =         {Course notes},
 245 }
 246
 247 @techreport{lectAK,
 248   editor =       {Jules Desharnais},
 249   author =       {H. Bherer and C. Bolduc and V. Mathieu},
 250   title =        {Alg\`{e}bres de {Kleene}},
 251   howpublished = {\url!www.ift.ulaval.ca/~desharnais/ Recherche/AutresPubs/LectureDirigee2003.pdf!},
 252   year =         {2003},
 253   note =         {Useful index.},
 254   type =         {Rapport de lecture dirig\'{e}e},
 255   institution =  {Universit\'{e} Laval},
 256 }
 257
 258 @techreport{AGS,
 259  author = {Dexter Kozen},
 260  title = {Automata on Guarded Strings and Applications},
 261  year = {2001},
 262  source = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Acornellcs%3ACORNELLCS%3ATR2001-1833},
 263  publisher = {Cornell University},
 264  address = {Ithaca, NY, USA},
 265   institution =  {Cornell University},
 266  }
 267
 268
 269 @techreport{REL-Horn-complexity,
 270  author = {Chris Hardin and Dexter Kozen},
 271  title = {On the Complexity of the Horn Theory of REL},
 272  year = {2003},
 273   month =        {may},
 274  publisher = {Cornell University},
 275  address = {Ithaca, NY, USA},
 276   institution =  {Cornell University},
 277   note =         {\url!http://www.math.cornell.edu/~hardin/papers/hornrel.ps!},
 278  }
 279
 280 @techreport{KAT-elimination,
 281  author = {Chris Hardin and Dexter Kozen},
 282  title = {On the Elimination of Hypotheses in {Kleene} Algebra with Tests},
 283  year = {2002},
 284   month =        {oct},
 285  publisher = {Cornell University},
 286  address = {Ithaca, NY, USA},
 287   institution =  {Cornell University},
 288   note =         {\url!http://www.math.cornell.edu/~hardin/papers/hornrel.ps!},
 289  }
 290
 291 @Unpublished{Cohen-hypo,
 292   author =       {Ernie Cohen},
 293   title =        {Hypotheses in {Kleene} Algebra},
 294   year =         {1994},
 295 }
 296
 297 @InProceedings{Cohen-annihilating-annih,
 298   author =       {Ernie Cohen},
 299   title =        {Annihilating the annihilation axioms},
 300   year =         {2003},
 301   note =         {\url!http://www.informatik.uni-kiel.de/~relmics7/submitted/Cohen/annihilatorsAbstract.ps.gz!},
 302   booktitle =    {RelMiCS 7},
 303 }
 304
 305 @InProceedings{KA-proof-theory,
 306   author =       {Chris Hardin},
 307   title =        {Proof Theory for {Kleene} Algebra},
 308   year =         {2005},
 309   note =         {To be presented at LICS 2005. \url!http://www.math.cornell.edu/~hardin/papers/prooftheory.ps!},
 310   booktitle =    {LICS 2005 (Logic in Computer Science)},
 311 }
 312
 313 @InProceedings{KA-modular-elimination,
 314   author =       {Chris Hardin},
 315   title =        {Modularizing the Elimination of $r=0$ in {Kleene} Algebra},
 316   year =         {2005},
 317   note =         {Submitted to Logical Methods in Computer Science. \url!http://www.math.cornell.edu/~hardin/papers/rzeroelim.ps!},
 318   month =        {apr},
 319   booktitle =    {Submitted to Logical Methods in Computer Science},
 320 }
 321