@book(Con71,
 author       = "J. H. Conway",
 year         = "1971",
 title        = "Regular Algebra and Finite Machines",
 publisher    = "Chapman and Hall, Mathematics series",
)
@article(Den07a,
 author       = "Y. Deng and R. J. van Glabbeek and M. Hennessy and C. Morgan and C. Zhang",
 year         = "2007",
 title        = "Remarks on Testing Probabilistic Processes",
 journal      = "Electr. Notes Theor. Comput. Sci.",
 volume       = "172",
 pages        = "359--397",
 doi          = "10.1016/j.entcs.2007.02.013",
)
@inproceedings(Den07b,
 author       = "Y. Deng and R. Van Glabbeek",
 year         = "2007",
 title        = "Characterising testing preorders for finite probabilistic processes",
 booktitle    = "In LICS’07: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA",
 pages        = "313--325",
 doi          = "10.1109/LICS.2007.15",
)
@article(Des06,
 author       = "J. Desharnais and B. M\"{o}ller and G. Struth",
 year         = "2006",
 title        = "{K}leene algebra with domain",
 journal      = "ACM Trans. Comput. Logic",
 volume       = "7",
 pages        = "798--833",
 doi          = "10.1145/1183278.1183285",
)
@inproceedings(Hoa09,
 author       = "C. A. R. Hoare and B. M\"{o}ller and G. Struth and I. Wehrman",
 year         = "2011",
 title        = "Concurrent {K}leene Algebra and its Foundations",
 series       = "Journal of Logic and Algebraic Programming 80",
 pages        = "266--296",
 doi          = "10.1016/j.jlap.2011.04.005",
)
@book(Jon81,
 author       = "C. B. Jones",
 year         = "1981",
 title        = "Development methods for computer programs including a notion of interference",
 series       = "Technical Monograph. Programming Research Group, Oxford University Computing Laboratory",
 url          = "http://books.google.com.au/books?id=zjguSwAACAAJ",
)
@article(Kle51,
 author       = "S. C. Kleene",
 year         = "1951",
 title        = "Representation of Events in Nerve Nets and Finite Automata",
 journal      = "Automata Studies",
)
@article(Kom12,
 author       = "A. Komuravelli and C. S. Pasareanu and E. M. Clarke",
 year         = "2012",
 title        = "Assume-Guarantee Abstraction Refinement for Probabilistic Systems",
 journal      = "CoRR",
 volume       = "abs/1207.5086",
 url          = "http://arxiv.org/abs/1207.5086",
 doi          = "10.1007/978-3-642-31424-7\_25",
)
@article(Koz94,
 author       = "D. Kozen",
 year         = "1994",
 title        = "A completeness theorem for {K}leene algebras and the algebra of regular events",
 journal      = "Infor. and Comput.",
 volume       = "110",
 number       = "2",
 pages        = "366--390",
 doi          = "10.1006/inco.1994.1037",
)
@article(Koz97,
 author       = "D. Kozen",
 year         = "1997",
 title        = "{K}leene algebra with tests",
 journal      = "ACM Trans. Program. Lang. Syst.",
 volume       = "19",
 pages        = "427--443",
 doi          = "10.1145/256167.256195",
)
@article(Koz00a,
 author       = "D. Kozen",
 year         = "2000",
 title        = "On {H}oare logic and {K}leene algebra with tests",
 journal      = "Trans. Computational Logic",
 volume       = "1",
 number       = "1",
 pages        = "60--76",
 doi          = "10.1145/343369.343378",
)
@techreport(Koz03,
 author       = "D. Kozen",
 year         = "2003",
 title        = "Kleene Algebras with Tests and the Static Analysis of Programs",
 type         = "Technical Report",
 number       = "TR2003-1915",
 institution  = "Computer Science Department, Cornell University",
)
@inproceedings(Kwi10,
 author       = "M. Kwiatkowska and G. Norman and D. Parker and H. Qu",
 year         = "2010",
 title        = "Assume-Guarantee verification for probabilistic systems",
 booktitle    = "Proceedings of the 16th international conference on Tools and Algorithms for the Construction and Analysis of Systems",
 series       = "TACAS'10",
 publisher    = "Springer-Verlag",
 address      = "Berlin, Heidelberg",
 pages        = "23--37",
 doi          = "10.1007/978-3-642-12002-2\_3",
)
@inproceedings(Seg03,
 author       = "N. A. Lynch and R. Segala and F. W. Vaandrager",
 year         = "2003",
 title        = "Compositionality for Probabilistic Automata",
 booktitle    = "CONCUR",
 pages        = "204--222",
 doi          = "10.1007/978-3-540-45187-7\_14",
)
@inproceedings(Rab11,
 author       = "A. McIver and T. M. Rabehaja and G. Struth",
 year         = "2011",
 title        = "On probabilistic {K}leene algebras, automata and simulations",
 booktitle    = "Proceedings of the 12th international conference on Relational and algebraic methods in computer science",
 series       = "RAMICS'11",
 publisher    = "Springer-Verlag",
 address      = "Berlin, Heidelberg",
 pages        = "264--279",
 url          = "http://dl.acm.org/citation.cfm?id=2018285.2018305",
 doi          = "10.1007/978-3-642-21070-9\_20",
)
@book(Mci04,
 author       = "A. K. McIver and C. C. Morgan",
 year         = "2004",
 title        = "Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science)",
 publisher    = "SpringerVerlag",
)
@article(Mo07,
 author       = "B. M\"{o}ller",
 year         = "2007",
 title        = "Kleene getting lazy",
 journal      = "Sci. Comput. Program.",
 volume       = "65",
 pages        = "195--214",
 doi          = "10.1016/j.scico.2006.01.010",
 url          = "http://dl.acm.org/citation.cfm?id=1225317.1225705",
)
@techreport(Rab76,
 author       = "M. O. Rabin",
 year         = "1976",
 title        = "{Probabilistic Algorithms}",
 type         = "Technical Report",
 number       = "RC 6164 (\#26545)",
 institution  = "IBM Research Division",
 address      = "San Jose, Yorktown, Zurich",
)
@article(Sal66,
 author       = "A. Salomaa",
 year         = "1966",
 title        = "Two Complete Axiom Systems for the Algebra of Regular Events",
 journal      = "J. ACM",
 volume       = "13",
 pages        = "158--169",
 doi          = "10.1145/321312.321326",
)
@misc(Ste12,
 author       = "S. Schneider",
 year         = "2012",
 title        = "Incorporating time to an integrated formal method",
 url          = "http://www.nii.ac.jp/shonan/seminar017/files/2012/06/Slides1.pdf",
)
@inproceedings(Seg95,
 author       = "R. Segala",
 year         = "1995",
 title        = "A Compositional Trace-Based Semantics for Probabilistic Automata",
 booktitle    = "CONCUR",
 pages        = "234--248",
 doi          = "10.1007/3-540-60218-6\_17",
)
@inproceedings(Seg96,
 author       = "R. Segala",
 year         = "1996",
 title        = "Testing Probabilistic Automata",
 booktitle    = "CONCUR",
 pages        = "299--314",
 doi          = "10.1007/3-540-61604-7\_62",
)
@article(Sil11,
 author       = "A. Silva and F. Bonchi and M. Bonsangue and J. Rutten",
 year         = "2011",
 title        = "Quantitative Kleene coalgebras",
 journal      = "Inf. Comput.",
 volume       = "209",
 number       = "5",
 pages        = "822--849",
 doi          = "10.1016/j.ic.2010.09.007",
)
@inproceedings(Sta96,
 author       = "E. W. Stark and S. A. Smolka",
 year         = "1996",
 title        = "A Complete Axiom System for Finite-State Probabilistic Processes",
 booktitle    = "In Proof, Language, and Interaction: Essays in Honour of Robin Milner",
 publisher    = "MIT Press",
 pages        = "571--595",
)