K
[Kai97] Roope Kaivola. Using Automata to Characterise Fixed Point Temporal Logics. PhD thesis, School of Informatics, University of Edinburgh, UK, July 1997. 
@phdthesis{phd-kaivola,
  author =              {Kaivola, Roope},
  title =               {Using Automata to Characterise Fixed Point Temporal
                         Logics},
  year =                {1997},
  month =               jul,
  school =              {School of Informatics, University of Edinburgh, UK},
  type =                {{PhD} thesis},
}
[Kam68] Johan Anthony Willem Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, Computer Science Department, University of California at Los Angeles, USA, 1968. 
@phdthesis{phd-kamp,
  author =              {Kamp, Johan Anthony Willem},
  title =               {Tense Logic and the Theory of Linear Order},
  year =                {1968},
  school =              {Computer Science Department, University of
                         California at Los~Angeles, USA},
  type =                {{PhD} thesis},
}
[Kam94] Michael Kaminski. A branching time logic with past operators. Journal of Computer and System Sciences 49(2):223-246. Academic Press, October 1994. 
@article{jcss49(2)-Kam,
  author =              {Kaminski, Michael},
  title =               {A branching time logic with past operators},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {49},
  number =              {2},
  pages =               {223-246},
  year =                {1994},
  month =               oct,
}
[Kar72] Richard M. Karp. Reducibility Among Combinatorial Problems. In CCC'72, IBM Research Symposia Series, pages 85-103. Plenum Press, March 1972. 
@inproceedings{ccc1972-Kar,
  author =              {Karp, Richard M.},
  title =               {Reducibility Among Combinatorial Problems},
  editor =              {Miller, Raymond E. and Thatcher, James W.},
  booktitle =           {{P}roceedings of a symposium on the Complexity of
                         Computer Computations ({CCC}'72)},
  acronym =             {{CCC}'72},
  publisher =           {Plenum Press},
  series =              {IBM Research Symposia Series},
  pages =               {85-103},
  year =                {1972},
  month =               mar,
}
[Kar78] Richard M. Karp. A characterization of the minimum cycle mean in a digraph. Discrete Mathematics 23(3):309-311. Elsevier, September 1978. 
@article{dm23(3)-Kar,
  author =              {Karp, Richard M.},
  title =               {A~characterization of the minimum cycle mean in a
                         digraph},
  publisher =           {Elsevier},
  journal =             {Discrete Mathematics},
  volume =              {23},
  number =              {3},
  pages =               {309-311},
  year =                {1978},
  month =               sep,
}
[Kar05] Jarkko Kari. Theory of Cellular Automata: A Survey. Theoretical Computer Science 334(1-3):3-33. Elsevier, April 2005. 
@article{tcs334(1-3)-Kar,
  author =              {Kari, Jarkko},
  title =               {Theory of Cellular Automata: A Survey},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {334},
  number =              {1-3},
  pages =               {3-33},
  year =                {2005},
  month =               apr,
}
[KBB+08] Leonid Khachiyan, Endre Boros, Konrad Borys, Khaled Elbassioni, Vladimir Gurvich, Gabor Rudolf, and Jihui Zhao. On short paths interdiction problems: Total and node-wise limited interdiction. Theory of Computing Systems 43(2):204-233. Springer-Verlag, August 2008. 
@article{tcsyst43(2)-KBBEGRZ,
  author =              {Khachiyan, Leonid and Boros, Endre and Borys, Konrad
                         and Elbassioni, Khaled and Gurvich, Vladimir and
                         Rudolf, Gabor and Zhao, Jihui},
  title =               {On short paths interdiction problems: Total and
                         node-wise limited interdiction},
  publisher =           {Springer-Verlag},
  journal =             {Theory of Computing Systems},
  volume =              {43},
  number =              {2},
  pages =               {204-233},
  year =                {2008},
  month =               aug,
  doi =                 {10.1007/s00224-007-9025-6},
}
[KBM13] Jean-François Kempf, Marius Bozga, and Oded Maler. As soon as probable: Optimal scheduling under stochastic uncertainty. In TACAS'13, Lecture Notes in Computer Science 7795, pages 385-400. Springer-Verlag, March 2013. 
@inproceedings{tacas2013-KBM,
  author =              {Kempf, Jean-Fran{\c c}ois and Bozga, Marius and
                         Maler, Oded},
  title =               {As soon as probable: Optimal scheduling under
                         stochastic uncertainty},
  editor =              {Piterman, Nir and Smolka, Scott A.},
  booktitle =           {{P}roceedings of the 19th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'13)},
  acronym =             {{TACAS}'13},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7795},
  pages =               {385-400},
  year =                {2013},
  month =               mar,
}
[KDH+07] Sebastian Kupferschmid, Klaus Dräger, Jörg Hoffmann, Bernd Finkbeiner, Henning Dierks, Andreas Podelski, and Gerd Behrmann. Uppaal/DMC – Abstraction-Based Heuristics for Directed Model Checking. In TACAS'07, Lecture Notes in Computer Science 4424, pages 679-682. Springer-Verlag, March 2007. 
@inproceedings{tacas2007-KDHFDPB,
  author =              {Kupferschmid, Sebastian and Dr{\"a}ger, Klaus and
                         Hoffmann, J{\"o}rg and Finkbeiner, Bernd and Dierks,
                         Henning and Podelski, Andreas and Behrmann, Gerd},
  title =               {{U}ppaal{\slash}{DMC}~-- Abstraction-Based
                         Heuristics for Directed Model Checking},
  editor =              {Grumberg, Orna and Huth, Michael},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'07)},
  acronym =             {{TACAS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4424},
  pages =               {679-682},
  year =                {2007},
  month =               mar,
}
[KF09] Lars Kuhtz and Bernd Finkbeiner. LTL Path Checking is Efficiently Parallelizable. In ICALP'09, Lecture Notes in Computer Science 5556, pages 235-246. Springer-Verlag, July 2009. 
@inproceedings{icalp2009-KF,
  author =              {Kuhtz, Lars and Finkbeiner, Bernd},
  title =               {{LTL} Path Checking is Efficiently Parallelizable},
  editor =              {Albers, Susanne and Marchetti{-}Spaccamela Alberto
                         and Matias, Yossi and Nikoletseas, Sotiris and
                         Thomas, Wolfgang},
  booktitle =           {{P}roceedings of the 36th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'09)~-- Part~{II}},
  acronym =             {{ICALP}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5556},
  pages =               {235-246},
  year =                {2009},
  month =               jul,
}
[KFS+09] Jeroen Kuipers, Janos Flesch, Gijs Schoenmakers, and Koos Vrieze. Pure subgame-perfect equilibria in free transition games. European Journal of Operational Research 199(2):442-447. Elsevier, December 2009. 
@article{ejor199(2)-KFS,
  author =              {Kuipers, Jeroen and Flesch, Janos and Schoenmakers,
                         Gijs and Vrieze, Koos},
  title =               {Pure subgame-perfect equilibria in free transition
                         games},
  publisher =           {Elsevier},
  journal =             {European Journal of Operational Research},
  volume =              {199},
  number =              {2},
  pages =               {442-447},
  year =                {2009},
  month =               dec,
}
[KG96] Orna Kupferman and Orna Grumberg. Buy One, Get One Free!!!. Journal of Logic and Computation 6(4):523-539. Oxford University Press, August 1996. 
@article{jlc6(4)-KG,
  author =              {Kupferman, Orna and Grumberg, Orna},
  title =               {Buy One, Get One Free!!!},
  publisher =           {Oxford University Press},
  journal =             {Journal of Logic and Computation},
  volume =              {6},
  number =              {4},
  pages =               {523-539},
  year =                {1996},
  month =               aug,
}
[KG96] Orna Kupferman and Orna Grumberg. Branching Time Temporal Logic and Tree Automata. Information and Computation 125(1):62-69. Academic Press, February 1996. 
@article{icomp125(1)-KG,
  author =              {Kupferman, Orna and Grumberg, Orna},
  title =               {Branching Time Temporal Logic and Tree Automata},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {125},
  number =              {1},
  pages =               {62-69},
  year =                {1996},
  month =               feb,
}
[Kha87] Oussama Khatib. A unified approach for motion and force control of robot manipulators: The operational space formulation. IEEE Journal of Robotics and Auomation 3(1):43-53. February 1987. 
@article{jra3(1)-Kha,
  author =              {Khatib, Oussama},
  title =               {A~unified approach for motion and force control of
                         robot manipulators: The operational space
                         formulation},
  journal =             {IEEE Journal of Robotics and Auomation},
  volume =              {3},
  number =              {1},
  pages =               {43-53},
  year =                {1987},
  month =               feb,
  doi =                 {10.1109/JRA.1987.1087068},
}
[KHL08] Sebastian Kupferschmid, Jörg Hoffmann, and Kim Guldstrand Larsen. Fast Directed Model Checking Via Russian Doll Abstraction. In TACAS'08, Lecture Notes in Computer Science 4963, pages 203-217. Springer-Verlag, March 2008. 
@inproceedings{tacas2008-KHL,
  author =              {Kupferschmid, Sebastian and Hoffmann, J{\"o}rg and
                         Larsen, Kim Guldstrand},
  title =               {Fast Directed Model Checking Via Russian Doll
                         Abstraction},
  editor =              {Ramakrishnan, C. R. and Rehof, Jakob},
  booktitle =           {{P}roceedings of the 14th {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'08)},
  acronym =             {{TACAS}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4963},
  pages =               {203-217},
  year =                {2008},
  month =               mar,
}
[KHM+94] Arjun Kapur, Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. Proving Safety Properties of Hybrid Systems. In FTRTFT'94, Lecture Notes in Computer Science 863, pages 431-454. Springer-Verlag, September 1994. 
@inproceedings{ftrtft1994-KHMP,
  author =              {Kapur, Arjun and Henzinger, Thomas A. and Manna,
                         Zohar and Pnueli, Amir},
  title =               {Proving Safety Properties of Hybrid Systems},
  editor =              {Langmaack, Hans and de Roever, Willem-Paul and
                         Vytopil, Jan},
  booktitle =           {{P}roceedings of the 3rd {F}ormal {T}echniques in
                         {R}eal-Time and {F}ault-Tolerant {S}ystems
                         ({FTRTFT}'94)},
  acronym =             {{FTRTFT}'94},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {863},
  pages =               {431-454},
  year =                {1994},
  month =               sep,
}
[Kir02] Daniel Kirsten. Alternating tree automata and parity games. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke (eds.), Automata, Logics, and Infinite Games, Lecture Notes in Computer Science 2500, pages 153-167. Springer-Verlag, 2002. 
@incollection{lncs2500-kirsten,
  author =              {Kirsten, Daniel},
  title =               {Alternating tree automata and parity games},
  editor =              {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke,
                         Thomas},
  booktitle =           {Automata, Logics, and Infinite Games},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2500},
  pages =               {153-167},
  year =                {2002},
}
[KJJ02] Andrei A. Krokhin, Peter Jeavons, and Peter Jonsson. The Complexity of Constraints on Intervals and Lengths. In STACS'02, Lecture Notes in Computer Science 2285, pages 443-454. Springer-Verlag, March 2002. 
@inproceedings{stacs2002-KJJ,
  author =              {Krokhin, Andrei A. and Jeavons, Peter and Jonsson,
                         Peter},
  title =               {The Complexity of Constraints on Intervals and
                         Lengths},
  editor =              {Alt, Helmut and Ferreira, Afonso},
  booktitle =           {{P}roceedings of the 19th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'02)},
  acronym =             {{STACS}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2285},
  pages =               {443-454},
  year =                {2002},
  month =               mar,
}
[KLL+97] Kåre J. Kristoffersen, François Laroussinie, Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. A Compositional Proof of a Real-Time Mutual Exclusion Protocol. In TAPSOFT'97, Lecture Notes in Computer Science 1214, pages 565-579. Springer-Verlag, April 1997. 
@inproceedings{tapsoft1997-KLLPY,
  author =              {Kristoffersen, K{\aa}re J. and Laroussinie, Fran{\c
                         c}ois and Larsen, Kim Guldstrand and Pettersson,
                         Paul and Yi, Wang},
  title =               {A Compositional Proof of a Real-Time Mutual
                         Exclusion Protocol},
  editor =              {Bidoit, Michel and Dauchet, Max},
  booktitle =           {{P}roceedings of the 7th {I}nternational {J}oint
                         {C}onference {CAAP}{\slash}{FASE} on {T}heory and
                         {P}ractice of {S}oftware {D}evelopment
                         ({TAPSOFT}'97)},
  acronym =             {{TAPSOFT}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1214},
  pages =               {565-579},
  year =                {1997},
  month =               apr,
}
[Klo94] Ton Kloks. Treewidth, Computations and Approximations. Lecture Notes in Computer Science 842. Springer-Verlag, 1994. 
@book{twca1994-Klo,
  author =              {Kloks, Ton},
  title =               {Treewidth, Computations and Approximations},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {842},
  year =                {1994},
  doi =                 {10.1007/BFb0045375},
}
[KLS+12] Miroslav Klimoš, Kim Guldstrand Larsen, Filip Štefaňák, and Jeppe Thaarup. Nash Equilibria in Concurrent Priced Games. In LATA'12, Lecture Notes in Computer Science 7183, pages 363-376. Springer-Verlag, May 2012. 
@inproceedings{lata2012-KLST,
  author =              {Klimo{\v{s}}, Miroslav and Larsen, Kim Guldstrand
                         and {\v{S}}tefa{\v{n}}{\'a}k, Filip and Thaarup,
                         Jeppe},
  title =               {{N}ash Equilibria in Concurrent Priced Games},
  editor =              {Dediu, Adrian Horia and Mart{\'\i}n-Vide, Carlos},
  booktitle =           {{P}roceedings of the 6th {I}nternational
                         {C}onference on {L}anguage and {A}utomata {T}heory
                         and {A}pplications ({LATA}'12)},
  acronym =             {{LATA}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7183},
  pages =               {363-376},
  year =                {2012},
  month =               may,
}
[KLV03] George Karakostas, Richard J. Lipton, and Anastasios Viglas. On the Complexity of Intersecting Finite State Automata and NL versus NP. Theoretical Computer Science 302(1-3):257-274. Elsevier, June 2003. 
@article{tcs302(1-3)-KLV,
  author =              {Karakostas, George and Lipton, Richard J. and
                         Viglas, Anastasios},
  title =               {On the Complexity of Intersecting Finite State
                         Automata and {NL} versus~{NP}},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {302},
  number =              {1-3},
  pages =               {257-274},
  year =                {2003},
  month =               jun,
}
[KM01] Jarkko Kari and Cristopher Moore. Rectangles and Squares Recognized by Two-dimensional Automata. In STACS'01, Lecture Notes in Computer Science 2010, pages 396-406. Springer-Verlag, February 2001. 
@inproceedings{stacs2001-KM,
  author =              {Kari, Jarkko and Moore, Cristopher},
  title =               {Rectangles and Squares Recognized by Two-dimensional
                         Automata},
  editor =              {Ferreira, Afonso and Reichel, Horst},
  booktitle =           {{P}roceedings of the 18th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'01)},
  acronym =             {{STACS}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2010},
  pages =               {396-406},
  year =                {2001},
  month =               feb,
}
[KM02] Antonín Kučera and Richard Mayr. Why is Simulation Harder than Bisimulation?. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 594-609. Springer-Verlag, August 2002. 
@inproceedings{concur2002-KM,
  author =              {Ku{\v c}era, Anton{\'\i}n and Mayr, Richard},
  title =               {Why is Simulation Harder than Bisimulation?},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {594-609},
  year =                {2002},
  month =               aug,
}
[KMM+93] Yonit Kesten, Zohar Manna, Hugh McGuire, and Amir Pnueli. A Decision Algorithm for Full Propositional Temporal Logic. In CAV'93, Lecture Notes in Computer Science 697, pages 97-109. Springer-Verlag, June 1993. 
@inproceedings{cav1993-KMMP,
  author =              {Kesten, Yonit and Manna, Zohar and McGuire, Hugh and
                         Pnueli, Amir},
  title =               {A Decision Algorithm for Full Propositional Temporal
                         Logic},
  editor =              {Courcoubetis, Costas},
  booktitle =           {{P}roceedings of the 5th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'93)},
  acronym =             {{CAV}'93},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {697},
  pages =               {97-109},
  year =                {1993},
  month =               jun,
}
[KMP00] Yonit Kesten, Zohar Manna, and Amir Pnueli. Verifying Clocked Transition Systems. Acta Informatica 36(11):837-912. Springer-Verlag, 2000. 
@article{acta36(11)-KMP,
  author =              {Kesten, Yonit and Manna, Zohar and Pnueli, Amir},
  title =               {Verifying Clocked Transition Systems},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {36},
  number =              {11},
  pages =               {837-912},
  year =                {2000},
}
[KMP16] Shankara Narayanan Krishna, Khushraj Madnani, and Paritosh K. Pandya. Metric Temporal Logic with Counting. In FoSSaCS'16, Lecture Notes in Computer Science 9634, pages 335-352. Springer-Verlag, April 2016. 
@inproceedings{fossacs2016-KMP,
  author =              {Krishna, Shankara Narayanan and Madnani, Khushraj
                         and Pandya, Paritosh K.},
  title =               {Metric Temporal Logic with Counting},
  editor =              {Jacobs, Bart and L{\"o}ding, Christof},
  booktitle =           {{P}roceedings of the 19th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'16)},
  acronym =             {{FoSSaCS}'16},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9634},
  pages =               {335-352},
  year =                {2016},
  month =               apr,
  doi =                 {10.1007/978-3-662-49630-5_20},
}
[KMS19] Sophia Knight, Bastien Maubert, and François Schwarzentruber. Reasoning about knowledge and messages in asynchronous multi-agent systems. Mathematical Structures in Computer Science 29(1):127-168. January 2019. 
@article{mscs29(1)-KMS,
  author =              {Knight, Sophia and Maubert, Bastien and
                         Schwarzentruber, Fran{\c c}ois},
  title =               {Reasoning about knowledge and messages in
                         asynchronous multi-agent systems},
  journal =             {Mathematical Structures in Computer Science},
  volume =              {29},
  number =              {1},
  pages =               {127-168},
  year =                {2019},
  month =               jan,
  doi =                 {10.1017/S0960129517000214},
}
[KMS+04] Daniel Král, Vladan Majerech, Jiří Sgall, Tomáš Tichý, and Gerhard J. Woeginger. It is Tough to be a Plumber. Theoretical Computer Science 313(3):473-484. Elsevier, February 2004. 
@article{tcs313(3)-KMSTW,
  author =              {Kr{\'a}l, Daniel and Majerech, Vladan and Sgall,
                         Ji{\v r}{\'\i} and Tich{\'y}, Tom{\'a}{\v s} and
                         Woeginger, Gerhard J.},
  title =               {It is Tough to be a Plumber},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {313},
  number =              {3},
  pages =               {473-484},
  year =                {2004},
  month =               feb,
}
[KMT+00] Orna Kupferman, Parthasarathy Madhusudan, P. S. Thiagarajan, and Moshe Y. Vardi. Open Systems in Reactive Environments: Control and Synthesis. In CONCUR'00, Lecture Notes in Computer Science 1877, pages 92-107. Springer-Verlag, August 2000. 
@inproceedings{concur2000-KMTV,
  author =              {Kupferman, Orna and Madhusudan, Parthasarathy and
                         Thiagarajan, P. S. and Vardi, Moshe Y.},
  title =               {Open Systems in Reactive Environments: Control and
                         Synthesis},
  editor =              {Palamidessi, Catuscia},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'00)},
  acronym =             {{CONCUR}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1877},
  pages =               {92-107},
  year =                {2000},
  month =               aug,
}
[KMT+04] Pavel Krčál, Leonid Mokrushin, P. S. Thiagarajan, and Wang Yi. Timed vs. Timed-Triggered Automata. In CONCUR'04, Lecture Notes in Computer Science 3170, pages 340-354. Springer-Verlag, August 2004. 
@inproceedings{concur2004-KMTY,
  author =              {Kr{\v{c}}{\'a}l, Pavel and Mokrushin, Leonid and
                         Thiagarajan, P. S. and Yi, Wang},
  title =               {Timed vs.{} Timed-Triggered Automata},
  editor =              {Gardner, {\relax Ph}ilippa and Yoshida, Nobuko},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'04)},
  acronym =             {{CONCUR}'04},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3170},
  pages =               {340-354},
  year =                {2004},
  month =               aug,
}
[Kna28] Bronisław Knaster. Un théorème sur les fonctions d'ensembles. Annales de la Société Polonaise de Mathématiques 6:133-134. Polish Mathematical Society, 1928. 
@article{aspm6()-Kna,
  author =              {Knaster, Bronis{\l}aw},
  title =               {Un th{\'e}or{\`e}me sur les fonctions d'ensembles},
  publisher =           {Polish Mathematical Society},
  journal =             {Annales de la Soci\'et\'e Polonaise de
                         Math\'ematiques},
  volume =              {6},
  pages =               {133-134},
  year =                {1928},
}
[KNP06] Marta Kwiatkowska, Gethin Norman, and David Parker. Symmetry Reduction for Probabilistic Model Checking. In CAV'06, Lecture Notes in Computer Science 4144, pages 234-248. Springer-Verlag, July 2006. 
@inproceedings{cav2006-KNP,
  author =              {Kwiatkowska, Marta and Norman, Gethin and Parker,
                         David},
  title =               {Symmetry Reduction for Probabilistic Model Checking},
  editor =              {Ball, Thomas and Jones, Robert},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'06)},
  acronym =             {{CAV}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4144},
  pages =               {234-248},
  year =                {2006},
  month =               jul,
  doi =                 {10.1007/11817963_23},
}
[KNS+02] Marta Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282(1):101-150. Elsevier, June 2002. 
@article{tcs282(1)-KNSS,
  author =              {Kwiatkowska, Marta and Norman, Gethin and Segala,
                         Roberto and Sproston, Jeremy},
  title =               {Automatic verification of real-time systems with
                         discrete probability distributions},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {282},
  number =              {1},
  pages =               {101-150},
  year =                {2002},
  month =               jun,
  doi =                 {10.1016/S0304-3975(01)00046-9},
}
[KO05] Ahmed Khoumsi and Lucien Ouedraogo. A New Method for Transforming Timed Automata. In SBMF'04, Electronic Notes in Theoretical Computer Science 130. Elsevier, 2005. 
@inproceedings{sbmf2004-KO,
  author =              {Khoumsi, Ahmed and Ouedraogo, Lucien},
  title =               {A New Method for Transforming Timed Automata},
  editor =              {Mota, Alexandre and Moura, Arnaldo V.},
  booktitle =           {{P}roceedings of the 7th {B}razilian {S}ymposium on
                         {F}ormal {M}ethods ({SBMF}'04)},
  acronym =             {{SBMF}'04},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {130},
  year =                {2005},
  confyear =            {2004},
  confmonth =           {11},
}
[Kon27] Dénes Kőnig. Über eine Schlussweise aus dem Endlichen ins Unendliche. Acta litt. sci. Reg. Univ. Hung. Francisco-Josephinae, Sect. sci. math. 3(2-3):121-130. János Bolyai Mathematical Institute, University of Szeged, June 1927. 
@article{actaszeged3(2-3)-Kon,
  author =              {K{\H o}nig, D{\'e}nes},
  title =               {{\"U}ber eine Schlussweise aus dem Endlichen ins
                         Unendliche},
  publisher =           {J{\'a}nos Bolyai Mathematical Institute, University
                         of Szeged},
  journal =             {Acta litt. sci. Reg. Univ. Hung.
                         Francisco-Josephinae, Sect. sci. math.},
  volume =              {3},
  number =              {2-3},
  pages =               {121-130},
  year =                {1927},
  month =               jun,
}
[Kop06] Eryk Kopczynski. Half-Positional Determinacy of Infinite Games. In ICALP'06, Lecture Notes in Computer Science 4052, pages 336-347. Springer-Verlag, July 2006. 
@inproceedings{icalp2006-Kop,
  author =              {Kopczynski, Eryk},
  title =               {Half-Positional Determinacy of Infinite Games},
  editor =              {Bugliesi, Michele and Preneel, Bart and Sassone,
                         Vladimiro and Wegener, Ingo},
  booktitle =           {{P}roceedings of the 33rd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'06))~-- Part~{II}},
  acronym =             {{ICALP}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4052},
  pages =               {336-347},
  year =                {2006},
  month =               jul,
  doi =                 {10.1007/11787006_29},
}
[Koy87] Ron Koymans. Specifying Message Passing and Real-Time Systems with Real-Time Temporal Logic. In ESPRIT'87. Elsevier, September 1987. 
@inproceedings{esprit1987-Koy,
  author =              {Koymans, Ron},
  title =               {Specifying Message Passing and Real-Time Systems
                         with Real-Time Temporal Logic},
  booktitle =           {{P}roceedings of the 4th {A}nnual {ESPRIT}
                         {C}onference ({ESPRIT}'87)},
  acronym =             {{ESPRIT}'87},
  publisher =           {Elsevier},
  year =                {1987},
  month =               sep,
}
[Koy90] Ron Koymans. Specifying Real-Time Properties with Metric Temporal Logic. Real-Time Systems 2(4):255-299. Kluwer Academic, 1990. 
@article{rts2(4)-Koy,
  author =              {Koymans, Ron},
  title =               {Specifying Real-Time Properties with Metric Temporal
                         Logic},
  publisher =           {Kluwer Academic},
  journal =             {Real-Time Systems},
  volume =              {2},
  number =              {4},
  pages =               {255-299},
  year =                {1990},
}
[Koz83] Dexter C. Kozen. Results on the Propositional μ-calculus. Theoretical Computer Science 27:333-354. Elsevier, 1983. 
@article{tcs27()-Koz,
  author =              {Kozen, Dexter C.},
  title =               {Results on the Propositional {\(\mu\)}-calculus},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {27},
  pages =               {333-354},
  year =                {1983},
}
[Koz92] Dexter C. Kozen. The design and analysis of algorithms. Springer-Verlag, 1992. 
@book{Koz92-daa,
  author =              {Kozen, Dexter C.},
  title =               {The design and analysis of algorithms},
  publisher =           {Springer-Verlag},
  year =                {1992},
  doi =                 {10.1007/978-1-4612-4400-4},
}
[Koz06] Dexter C. Kozen. Coinductive Proof Principles for Stochastic Processes. In LICS'06, pages 359-366. IEEE Comp. Soc. Press, July 2006. 
@inproceedings{lics2006-koz,
  author =              {Kozen, Dexter C.},
  title =               {Coinductive Proof Principles for Stochastic
                         Processes},
  booktitle =           {{P}roceedings of the 21st {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'06)},
  acronym =             {{LICS}'06},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {359-366},
  year =                {2006},
  month =               jul,
}
[KP95] Yonit Kesten and Amir Pnueli. A Complete Proof Systems for QPTL. In LICS'95, pages 2-12. IEEE Comp. Soc. Press, June 1995. 
@inproceedings{lics1995-KeP,
  author =              {Kesten, Yonit and Pnueli, Amir},
  title =               {A Complete Proof Systems for {QPTL}},
  booktitle =           {{P}roceedings of the 10th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'95)},
  acronym =             {{LICS}'95},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {2-12},
  year =                {1995},
  month =               jun,
}
[KP95] Orna Kupferman and Amir Pnueli. Once and For All. In LICS'95, pages 25-35. IEEE Comp. Soc. Press, June 1995. 
@inproceedings{lics1995-KuP,
  author =              {Kupferman, Orna and Pnueli, Amir},
  title =               {{\emph{Once}} and {\emph{For All}}},
  booktitle =           {{P}roceedings of the 10th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'95)},
  acronym =             {{LICS}'95},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {25-35},
  year =                {1995},
  month =               jun,
}
[KP99] Elias Koutsoupias and Christos H. Papadimitriou. Worst-case equilibria. In STACS'99, Lecture Notes in Computer Science 1563, pages 404-413. Springer-Verlag, March 1999. 
@inproceedings{stacs1999-KP,
  author =              {Koutsoupias, Elias and Papadimitriou, {\relax
                         Ch}ristos H.},
  title =               {Worst-case equilibria},
  editor =              {Meinel, {\relax Ch}ristoph and Tison, Sophie},
  booktitle =           {{P}roceedings of the 16th {S}ymposium on
                         {T}heoretical {A}spects of {C}omputer {S}cience
                         ({STACS}'99)},
  acronym =             {{STACS}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1563},
  pages =               {404-413},
  year =                {1999},
  month =               mar,
  doi =                 {10.1007/3-540-49116-3_38},
}
[KP02] Yonit Kesten and Amir Pnueli. Complete Proof System for QPTL. Journal of Logic and Computation 12(5):701-745. Oxford University Press, October 2002. 
@article{jlc12(5)-KP,
  author =              {Kesten, Yonit and Pnueli, Amir},
  title =               {Complete Proof System for~{QPTL}},
  publisher =           {Oxford University Press},
  journal =             {Journal of Logic and Computation},
  volume =              {12},
  number =              {5},
  pages =               {701-745},
  year =                {2002},
  month =               oct,
  doi =                 {10.1093/logcom/12.5.701},
}
[KP02] Beata Konikowska and Wojciech Penczek. Reducing Model Checking from Multi-Valued CTL* to CTL*. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 226-239. Springer-Verlag, August 2002. 
@inproceedings{concur2002-KP,
  author =              {Konikowska, Beata and Penczek, Wojciech},
  title =               {Reducing Model Checking from Multi-Valued
                         {CTL}{\(^*\)} to {CTL}{\(^*\)}},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {226-239},
  year =                {2002},
  month =               aug,
}
[KP04] Magdalena Kacprzak and Wojciech Penczek. Unbounded Model Checking for Alternating-Time Temporal Logic. In AAMAS'04, pages 646-653. IEEE Comp. Soc. Press, August 2004. 
@inproceedings{aamas2004-KP,
  author =              {Kacprzak, Magdalena and Penczek, Wojciech},
  title =               {Unbounded Model Checking for Alternating-Time
                         Temporal Logic},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {J}oint
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'04)},
  acronym =             {{AAMAS}'04},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {646-653},
  year =                {2004},
  month =               aug,
}
[KP05] Yonit Kesten and Amir Pnueli. A Compositional Approach to CTL* Verification. Theoretical Computer Science 331(2-3):397-428. Elsevier, February 2005. 
@article{tcs331(2-3)-KP,
  author =              {Kesten, Yonit and Pnueli, Amir},
  title =               {A Compositional Approach to {CTL}{\(^*\)}
                         Verification},
  publisher =           {Elsevier},
  journal =             {Theoretical Computer Science},
  volume =              {331},
  number =              {2-3},
  pages =               {397-428},
  year =                {2005},
  month =               feb,
}
[KP05] Pavel Krčál and Radek Pelánek. On Sampled Semantics of Timed Systems. In FSTTCS'05, Lecture Notes in Computer Science 3821, pages 310-321. Springer-Verlag, December 2005. 
@inproceedings{fsttcs2005-KP,
  author =              {Kr{\v{c}}{\'{a}}l, Pavel and Pel{\'{a}}nek, Radek},
  title =               {On Sampled Semantics of Timed Systems},
  editor =              {Ramanujam, R. and Sen, Sandeep},
  booktitle =           {{P}roceedings of the 25th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'05)},
  acronym =             {{FSTTCS}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3821},
  pages =               {310-321},
  year =                {2005},
  month =               dec,
}
[KP09] Elias Koutsoupias and Christos H. Papadimitriou. Worst-case equilibria. Computer Science Review 3(2):65-69. May 2009. 
@article{KP-csr09,
  author =              {Koutsoupias, Elias and Papadimitriou, {\relax
                         Ch}ristos H.},
  title =               {Worst-case equilibria},
  journal =             {Computer Science Review},
  volume =              {3},
  number =              {2},
  pages =               {65-69},
  year =                {2009},
  month =               may,
  doi =                 {10.1016/j.cosrev.2009.04.003},
}
[KP12] Elias Koutsoupias and Katia Papakonstantinopoulou. Contention Issues in Congestion Games. In ICALP'12, Lecture Notes in Computer Science 7392, pages 623-635. Springer-Verlag, July 2012. 
@inproceedings{icalp2012-KP,
  author =              {Koutsoupias, Elias and Papakonstantinopoulou, Katia},
  title =               {Contention Issues in Congestion Games},
  editor =              {Czumaj, Artur and Mehlhorn, Kurt and Pitts, Andrew
                         and Wattenhofer, Roger},
  booktitle =           {{P}roceedings of the 39th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'12)~-- Part~{II}},
  acronym =             {{ICALP}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7392},
  pages =               {623-635},
  year =                {2012},
  month =               jul,
  doi =                 {10.1007/978-3-642-31585-5_55},
}
[KPA03] Kåre J. Kristoffersen, Christian Pedersen, and Henrik Reif Andersen. Runtime Verification of Timed LTL Using Disjunctive Normalized Equation Systems. In RV'03, Electronic Notes in Theoretical Computer Science 89(2). Elsevier, 2003. 
@inproceedings{rv2003-KPA,
  author =              {Kristoffersen, K{\aa}re J. and Pedersen, Christian
                         and Andersen, Henrik Reif},
  title =               {Runtime Verification of Timed {LTL} Using
                         Disjunctive Normalized Equation Systems},
  editor =              {Cook, Byron and Stoller, Scott and Viser, Willem},
  booktitle =           {{P}roceedings of the 3rd {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'03)},
  acronym =             {{RV}'03},
  publisher =           {Elsevier},
  series =              {Electronic Notes in Theoretical Computer Science},
  volume =              {89},
  number =              {2},
  year =                {2003},
  confyear =            {2003},
  confmonth =           {7},
}
[KPR98] Yonit Kesten, Amir Pnueli, and Li-on Raviv. Algorithmic Verification of Linear Temporal Logic Specifications. In ICALP'98, Lecture Notes in Computer Science 1443, pages 1-16. Springer-Verlag, July 1998. 
@inproceedings{icalp1998-KPR,
  author =              {Kesten, Yonit and Pnueli, Amir and Raviv, Li-on},
  title =               {Algorithmic Verification of Linear Temporal Logic
                         Specifications},
  editor =              {Larsen, Kim Guldstrand and Skyum, Sven and Winskel,
                         Glynn},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'98)},
  acronym =             {{ICALP}'98},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1443},
  pages =               {1-16},
  year =                {1998},
  month =               jul,
}
[KPS+99] Yonit Kesten, Amir Pnueli, Joseph Sifakis, and Sergio Yovine. Decidable Integration Graphs. Information and Computation 150(2):209-243. Academic Press, May 1999. 
@article{icomp150(2)-KPSY,
  author =              {Kesten, Yonit and Pnueli, Amir and Sifakis, Joseph
                         and Yovine, Sergio},
  title =               {Decidable Integration Graphs},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {150},
  number =              {2},
  pages =               {209-243},
  year =                {1999},
  month =               may,
  doi =                 {10.1006/inco.1998.2774},
}
[KPS+02] Yonit Kesten, Amir Pnueli, Elad Shahar, and Lenore D. Zuck. Network Invariants in Action. In CONCUR'02, Lecture Notes in Computer Science 2421, pages 101-115. Springer-Verlag, August 2002. 
@inproceedings{concur2002-KPSZ,
  author =              {Kesten, Yonit and Pnueli, Amir and Shahar, Elad and
                         Zuck, Lenore D.},
  title =               {Network Invariants in Action},
  editor =              {Brim, Lubo{\v s} and Jan{\v c}ar, Petr and K{\v
                         r}et{\'\i}nsk{\'y}, Mojm{\'\i}r and Ku{\v c}era,
                         Anton{\'\i}n},
  booktitle =           {{P}roceedings of the 13th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'02)},
  acronym =             {{CONCUR}'02},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2421},
  pages =               {101-115},
  year =                {2002},
  month =               aug,
}
[KPV01] Orna Kupferman, Nir Piterman, and Moshe Y. Vardi. Extended Temporal Logic Revisited. In CONCUR'01, Lecture Notes in Computer Science 2154, pages 519-535. Springer-Verlag, August 2001. 
@inproceedings{concur2001-KPV,
  author =              {Kupferman, Orna and Piterman, Nir and Vardi, Moshe
                         Y.},
  title =               {Extended Temporal Logic Revisited},
  editor =              {Larsen, Kim Guldstrand and Nielsen, Mogens},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'01)},
  acronym =             {{CONCUR}'01},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2154},
  pages =               {519-535},
  year =                {2001},
  month =               aug,
}
[KPV12] Orna Kupferman, Amir Pnueli, and Moshe Y. Vardi. Once and For All. Journal of Computer and System Sciences 78(3):981-996. Elsevier, May 2012. 
@article{jcss78(3)-KPV,
  author =              {Kupferman, Orna and Pnueli, Amir and Vardi, Moshe
                         Y.},
  title =               {{\emph{Once}} and {\emph{For All}}},
  publisher =           {Elsevier},
  journal =             {Journal of Computer and System Sciences},
  volume =              {78},
  number =              {3},
  pages =               {981-996},
  year =                {2012},
  month =               may,
  doi =                 {10.1016/j.jcss.2011.08.006},
}
[KPV16] Orna Kupferman, Giuseppe Perelli, and Moshe Y. Vardi. Synthesis with rational environments. Annals of Mathematics and Artificial Intelligence 78(1):3-20. Kluwer Academic, September 2016. 
@article{amai78(1)-KPV,
  author =              {Kupferman, Orna and Perelli, Giuseppe and Vardi,
                         Moshe Y.},
  title =               {Synthesis with rational environments},
  publisher =           {Kluwer Academic},
  journal =             {Annals of Mathematics and Artificial Intelligence},
  volume =              {78},
  number =              {1},
  pages =               {3-20},
  year =                {2016},
  month =               sep,
  doi =                 {10.1007/s10472-016-9508-8},
}
[KR13] Jim Kurose and Keith Ross. Computer Networks – A top-down approach. Pearson, 2013. 
@book{KR13-CN,
  author =              {Kurose, Jim and Ross, Keith},
  title =               {Computer Networks~-- A~top-down approach},
  publisher =           {Pearson},
  year =                {2013},
}
[Kre87] Mark W. Krentel. The Complexity of Optimization Problems. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, USA, 1987. 
@phdthesis{phd-krentel,
  author =              {Krentel, Mark W.},
  title =               {The Complexity of Optimization Problems},
  year =                {1987},
  school =              {Department of Computer Science, Cornell University,
                         Ithaca, New York, USA},
  type =                {{PhD} thesis},
}
[Kre88] Mark W. Krentel. The Complexity of Optimization Problems. Journal of Computer and System Sciences 36(3):490-509. Academic Press, June 1988. 
@article{jcss36(3)-Kre,
  author =              {Krentel, Mark W.},
  title =               {The Complexity of Optimization Problems},
  publisher =           {Academic Press},
  journal =             {Journal of Computer and System Sciences},
  volume =              {36},
  number =              {3},
  pages =               {490-509},
  year =                {1988},
  month =               jun,
}
[Kri59] Saul A. Kripke. A Completeness Theorem in Modal Logic. Journal of Symbolic Logic 24(1):1-14. Association for Symbolic Logic, March 1959. 
@article{jsl24(1)-Kri,
  author =              {Kripke, Saul A.},
  title =               {A Completeness Theorem in Modal Logic},
  publisher =           {Association for Symbolic Logic},
  journal =             {Journal of Symbolic Logic},
  volume =              {24},
  number =              {1},
  pages =               {1-14},
  year =                {1959},
  month =               mar,
}
[Kri63] Saul A. Kripke. Semantical Considerations on Modal Logic. Acta Philosophica Fennica 16:83-94. Philosophical Society of Finland, 1963. 
@article{apf16()-Kri,
  author =              {Kripke, Saul A.},
  title =               {Semantical Considerations on Modal Logic},
  publisher =           {Philosophical Society of Finland},
  journal =             {Acta Philosophica Fennica},
  volume =              {16},
  pages =               {83-94},
  year =                {1963},
}
[Kri63] Saul A. Kripke. Semantical Analysis of Modal Logic I: Normal Modal Propositional Calculi. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 9(5-6):67-96. Deutscher Verlag der Wissenschaften, 1963. 
@article{zml9(5-6)-Kri,
  author =              {Kripke, Saul A.},
  title =               {Semantical Analysis of Modal Logic~{I}: Normal Modal
                         Propositional Calculi},
  publisher =           {Deutscher Verlag der Wissenschaften},
  journal =             {Zeitschrift fur mathematische Logik und Grundlagen
                         der Mathematik},
  volume =              {9},
  number =              {5-6},
  pages =               {67-96},
  year =                {1963},
}
[KRS97] Marek Karpinski, Wojciech Rytter, and Ayumi Shinohara. An Efficient Pattern-Matching Algorithm for Strings with Short Description. Nordic Journal of Computing 4(2):172-186. Publishing Association Nordic Journal of Computing, 1997. 
@article{njc4(2)-KRS,
  author =              {Karpinski, Marek and Rytter, Wojciech and Shinohara,
                         Ayumi},
  title =               {An Efficient Pattern-Matching Algorithm for Strings
                         with Short Description},
  publisher =           {Publishing Association Nordic Journal of Computing},
  journal =             {Nordic Journal of Computing},
  volume =              {4},
  number =              {2},
  pages =               {172-186},
  year =                {1997},
}
[KRT09] Dominik Klein, Frank G. Radmacher, and Wolfgang Thomas. The Complexity of Reachability in Randomized Sabotage Games. In FSEN'09, Lecture Notes in Computer Science 5961, pages 162-177. Springer-Verlag, April 2009. 
@inproceedings{fsen2009-KRT,
  author =              {Klein, Dominik and Radmacher, Frank G. and Thomas,
                         Wolfgang},
  title =               {The Complexity of Reachability in Randomized
                         Sabotage Games},
  editor =              {Arbab, Farhad and Sirjani, Marjan},
  booktitle =           {{R}evised {S}elected {P}apers of the 3rd
                         {I}nternational {C}onference on {F}undamentals of
                         {S}oftware {E}ngineering ({FSEN}'09)},
  acronym =             {{FSEN}'09},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5961},
  pages =               {162-177},
  year =                {2009},
  month =               apr,
}
[KS83] Paris C. Kanellakis and Scott A. Smolka. CCS expressions finite state processes, and three problems of equivalence. In PODC'83, pages 228-240. ACM Press, August 1983. 
@inproceedings{podc1983-KS,
  author =              {Kanellakis, Paris C. and Smolka, Scott A.},
  title =               {{CCS} expressions finite state processes, and three
                         problems of equivalence},
  booktitle =           {{P}roceedings of the 2nd {ACM} {S}ymposium on
                         {P}rinciples of {D}istributed {C}omputing
                         ({PODC}'83)},
  acronym =             {{PODC}'83},
  publisher =           {ACM Press},
  pages =               {228-240},
  year =                {1983},
  month =               aug,
}
[KS88] S. Rao Kosaraju and Gregory F. Sullivan. Detecting cycles in dynamic graphs in polynomial time. In STOC'88, pages 398-406. ACM Press, May 1988. 
@inproceedings{stoc1988-KS,
  author =              {Kosaraju, S. Rao and Sullivan, Gregory F.},
  title =               {Detecting cycles in dynamic graphs in polynomial
                         time},
  booktitle =           {{P}roceedings of the 20th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'88)},
  acronym =             {{STOC}'88},
  publisher =           {ACM Press},
  pages =               {398-406},
  year =                {1988},
  month =               may,
  doi =                 {10.1145/62212.62251},
}
[KS90] Paris C. Kanellakis and Scott A. Smolka. CCS expressions finite state processes, and three problems of equivalence. Information and Computation 86(1):43-68. Academic Press, May 1990. 
@article{icomp86(1)-KS,
  author =              {Kanellakis, Paris C. and Smolka, Scott A.},
  title =               {{CCS} expressions finite state processes, and three
                         problems of equivalence},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {86},
  number =              {1},
  pages =               {43-68},
  year =                {1990},
  month =               may,
}
[KS02] Antonín Kučera and Jan Strejček. The Stuterring Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. Technical Report FIMU-RS-2002-03, Faculty of Informatics, Masaryk University, Brno, Czech Republic, July 2002. 
@techreport{fimu-rs-2002-03-KS,
  author =              {Ku{\v c}era, Anton{\'\i}n and Strej{\v c}ek, Jan},
  title =               {The Stuterring Principle Revisited: On the
                         Expressiveness of Nested~{X} and~{U} Operators in
                         the Logic {LTL}},
  number =              {FIMU-RS-2002-03},
  year =                {2002},
  month =               jul,
  institution =         {Faculty of Informatics, Masaryk University, Brno,
                         Czech Republic},
  type =                {Technical Report},
}
[KS03] Dimitris J. Kavvadias and Elias C. Stavropoulos. Monotone Boolean Dualization is in co-NP[log2(n)]. Information Processing Letters 85(1):1-8. Elsevier, January 2003. 
@article{ipl85(1)-KS,
  author =              {Kavvadias, Dimitris J. and Stavropoulos, Elias C.},
  title =               {Monotone Boolean Dualization is in
                         co-{NP}{\([\log^2(n)]\)}},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {85},
  number =              {1},
  pages =               {1-8},
  year =                {2003},
  month =               jan,
}
[KS05] Spyros Kontogiannis and Paul G. Spirakis. Atomic selfish routing in networks: a survey. In WINE'05, Lecture Notes in Computer Science 3828, pages 989-1002. Springer-Verlag, December 2005. 
@inproceedings{wine2005-KS,
  author =              {Kontogiannis, Spyros and Spirakis, Paul G.},
  title =               {Atomic selfish routing in networks: a~survey},
  editor =              {Deng, Xiaotie and Ye, Yinyu},
  booktitle =           {{P}roceedings of the 1st {I}nternational {W}orkshop
                         on {I}nternet and {N}etwork {E}conomics ({WINE}'05)},
  acronym =             {{WINE}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3828},
  pages =               {989-1002},
  year =                {2005},
  month =               dec,
  doi =                 {10.1007/11600930_100},
}
[KS05] Antonín Kučera and Jan Strejček. The Stuttering Principle Revisited. Acta Informatica 41(7-8):415-434. Springer-Verlag, June 2005. 
@article{acta41(7-8)-KS,
  author =              {Ku{\v c}era, Anton{\'\i}n and Strej{\v c}ek, Jan},
  title =               {The Stuttering Principle Revisited},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {41},
  number =              {7-8},
  pages =               {415-434},
  year =                {2005},
  month =               jun,
  doi =                 {10.1007/s00236-005-0164-4},
}
[KS05] Antonín Kučera and Jan Strejček. Characteristic Patterns for LTL. In SOFSEM'05, Lecture Notes in Computer Science 3381, pages 239-249. Springer-Verlag, January 2005. 
@inproceedings{sofsem2005-KS,
  author =              {Ku{\v c}era, Anton{\'\i}n and Strej{\v c}ek, Jan},
  title =               {Characteristic Patterns for {LTL}},
  editor =              {Vojt{\'a}s, Peter and Bielikov{\'a}, M{\'a}ria and
                         Charron-Bost, Bernadette and S{\'y}kora, Ondrej},
  booktitle =           {{P}roceedings of the 31st {C}onference on {C}urrent
                         {T}rends in {T}heory and {P}ractice of {I}nformatics
                         ({SOFSEM}'05)},
  acronym =             {{SOFSEM}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3381},
  pages =               {239-249},
  year =                {2005},
  month =               jan,
}
[KS11] Ronald Koch and Martin Skutella. Nash equilibria and the price of anarchy for flows over time. Theory of Computing Systems 49(1):71-97. Springer-Verlag, July 2011. 
@article{tocsys49(1)-ks,
  author =              {Koch, Ronald and Skutella, Martin},
  title =               {{N}ash equilibria and the price of anarchy for flows
                         over time},
  publisher =           {Springer-Verlag},
  journal =             {Theory of Computing Systems},
  volume =              {49},
  number =              {1},
  pages =               {71-97},
  year =                {2011},
  month =               jul,
  doi =                 {10.1007/s00224-010-9299-y},
}
[KS15] Denis Kuperberg and Michal Skrzypczak. On determinisation of good-for-games automata. In ICALP'15, Lecture Notes in Computer Science 9135, pages 299-310. Springer-Verlag, July 2015. 
@inproceedings{icalp2015-KS,
  author =              {Kuperberg, Denis and Skrzypczak, Michal},
  title =               {On determinisation of good-for-games automata},
  editor =              {Halld{\'o}rsson, Magn{\'u}s M. and Iwana, Kazuo and
                         Kobayashi, Naoki and Speckmann, Bettina},
  booktitle =           {{P}roceedings of the 42nd {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'15)~-- Part~{II}},
  acronym =             {{ICALP}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9135},
  pages =               {299-310},
  year =                {2015},
  month =               jul,
  doi =                 {10.1007/978-3-662-47666-6_24},
}
[KSC08] Egor V. Kuzmin, Valery A. Sokolov, and Dmitry Y. Chaly. Boundedness Problems for Minsky Counter Machines. Doklady Mathematics 78(1):604-606. Pleiades Publishing, 2008. 
@article{doklady78(1)-KSC,
  author =              {Kuzmin, Egor V. and Sokolov, Valery A. and Chaly,
                         Dmitry Y.},
  title =               {Boundedness Problems for {M}insky Counter Machines},
  publisher =           {Pleiades Publishing},
  journal =             {Doklady Mathematics},
  volume =              {78},
  number =              {1},
  pages =               {604-606},
  year =                {2008},
}
[KST+99] Takuya Kida, Yusuke Shibata, Masayuki Takeda, Ayumi Shinohara, and Setsuo Arikawa. A Unifying Framework for Compressed Pattern Matching. In SPIRE/CRIWG'99, pages 89-96. IEEE Comp. Soc. Press, September 1999. 
@inproceedings{spire1999-KSTSA,
  author =              {Kida, Takuya and Shibata, Yusuke and Takeda,
                         Masayuki and Shinohara, Ayumi and Arikawa, Setsuo},
  title =               {A Unifying Framework for Compressed Pattern
                         Matching},
  booktitle =           {{P}roceedings of the 6th {S}tring {P}rocessing and
                         {I}nformation {R}etrieval {S}ymposium \&
                         {I}nternational {W}orkshop on {G}roupware
                         ({SPIRE/CRIWG}'99)},
  acronym =             {{SPIRE/CRIWG}'99},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {89-96},
  year =                {1999},
  month =               sep,
}
[KSV96] Orna Kupferman, Shmuel Safra, and Moshe Y. Vardi. Relating Word and Tree Automata. In LICS'96, pages 322-332. IEEE Comp. Soc. Press, July 1996. 
@inproceedings{lics1996-KSV,
  author =              {Kupferman, Orna and Safra, Shmuel and Vardi, Moshe
                         Y.},
  title =               {Relating Word and Tree Automata},
  booktitle =           {{P}roceedings of the 11th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'96)},
  acronym =             {{LICS}'96},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {322-332},
  year =                {1996},
  month =               jul,
  doi =                 {10.1109/LICS.1996.561360},
}
[KSV06] Orna Kupferman, Shmuel Safra, and Moshe Y. Vardi. Relating Word and Tree Automata. Annals of Pure and Applied Logic 138(1-3):126-146. Elsevier, March 2006. 
@article{apal138(1-3)-KSV,
  author =              {Kupferman, Orna and Safra, Shmuel and Vardi, Moshe
                         Y.},
  title =               {Relating Word and Tree Automata},
  publisher =           {Elsevier},
  journal =             {Annals of Pure and Applied Logic},
  volume =              {138},
  number =              {1-3},
  pages =               {126-146},
  year =                {2006},
  month =               mar,
}
[KSW87] Johannes Köbler, Uwe Schöning, and Klaus W. Wagner. The difference and truth-table hierarchies for NP. RAIRO – Informatique Théorique et Applications 21(4):419-435. EDP Sciences, 1987. 
@article{rairo-ita21(4)-KSW,
  author =              {K{\"o}bler, Johannes and Sch{\"o}ning, Uwe and
                         Wagner, Klaus W.},
  title =               {The difference and truth-table hierarchies for~{NP}},
  publisher =           {EDP Sciences},
  journal =             {RAIRO~-- Informatique Th{\'e}orique et Applications},
  volume =              {21},
  number =              {4},
  pages =               {419-435},
  year =                {1987},
}
[KT09] Moez Krichen and Stavros Tripakis. Conformance testing for real-time systems. Formal Methods in System Design 34(3):238-304. Springer-Verlag, June 2009. 
@article{fmsd34(3)-KT,
  author =              {Krichen, Moez and Tripakis, Stavros},
  title =               {Conformance testing for real-time systems},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {34},
  number =              {3},
  pages =               {238-304},
  year =                {2009},
  month =               jun,
  doi =                 {10.1007/s10703-009-0065-1},
}
[Kuc12] Antonín Kučera. Playing Games with Counter Automata. In RP'12, Lecture Notes in Computer Science 7550, pages 29-41. Springer-Verlag, September 2012. 
@inproceedings{rp2012-Kuc,
  author =              {Ku{\v c}era, Anton{\'\i}n},
  title =               {Playing Games with Counter Automata},
  editor =              {Finkel, Alain and Leroux, J{\'e}r{\^o}me and
                         Potapov, Igor},
  booktitle =           {{P}roceedings of the 6th {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'12)},
  acronym =             {{RP}'12},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {7550},
  pages =               {29-41},
  year =                {2012},
  month =               sep,
  doi =                 {10.1007/978-3-642-33512-9_4},
}
[Kun80] Kenneth Kunen. Set Theory. Elsevier, 1980. 
@book{SetT-Kunen,
  author =              {Kunen, Kenneth},
  title =               {Set Theory},
  publisher =           {Elsevier},
  year =                {1980},
}
[Kup95] Orna Kupferman. Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions. In CAV'95, Lecture Notes in Computer Science 939, pages 325-338. Springer-Verlag, July 1995. 
@inproceedings{cav1995-Kup,
  author =              {Kupferman, Orna},
  title =               {Augmenting Branching Temporal Logics with
                         Existential Quantification over Atomic Propositions},
  editor =              {Wolper, Pierre},
  booktitle =           {{P}roceedings of the 7th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'95)},
  acronym =             {{CAV}'95},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {939},
  pages =               {325-338},
  year =                {1995},
  month =               jul,
  doi =                 {10.1007/3-540-60045-0_60},
}
[Kup95] Orna Kupferman. Model Checking for Branching-Time Temporal Logics. PhD thesis, Israel Institute of Technology, Haifa, Israel, 1995. 
@phdthesis{phd-kupferman,
  author =              {Kupferman, Orna},
  title =               {Model Checking for Branching-Time Temporal Logics},
  year =                {1995},
  school =              {Israel Institute of Technology, Haifa, Israel},
  type =                {{PhD} thesis},
}
[Kup99] Orna Kupferman. Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions. Journal of Logic and Computation 9(2):135-147. Oxford University Press, April 1999. 
@article{jlc9(2)-Kup,
  author =              {Kupferman, Orna},
  title =               {Augmenting Branching Temporal Logics with
                         Existential Quantification over Atomic Propositions},
  publisher =           {Oxford University Press},
  journal =             {Journal of Logic and Computation},
  volume =              {9},
  number =              {2},
  pages =               {135-147},
  year =                {1999},
  month =               apr,
}
[Kur02] Agi Kurucz. S5 × S5 × S5 lacks the finite model property. In AIML'00, pages 321-327. World Scientific, 2002. 
@inproceedings{aiml2000-Kur,
  author =              {Kurucz, Agi},
  title =               {{{\(S5\times S5\times S5\)}} lacks the finite model
                         property},
  editor =              {de Rijke, Marteen and Wansing, Heinrich and Wolter,
                         Frank and Zakharyaschev, Michael},
  booktitle =           {{P}roceedings of the 3rd {W}orkshop on {A}dvances in
                         {M}odal {L}ogic ({AIML}'00)},
  acronym =             {{AIML}'00},
  publisher =           {World Scientific},
  pages =               {321-327},
  year =                {2002},
  confyear =            {2000},
  confmonth =           {10},
}
[KV97] Orna Kupferman and Moshe Y. Vardi. Weak Alternating Automata Are Not That Weak. In ISTCS'97, pages 147-158. IEEE Comp. Soc. Press, June 1997. 
@inproceedings{istcs1997-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Weak Alternating Automata Are Not That Weak},
  booktitle =           {{P}roceedings of the 5th {I}srael {S}ymposium on
                         {T}heory of {C}omputing {S}ystems ({ISTCS}'97)},
  acronym =             {{ISTCS}'97},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {147-158},
  year =                {1997},
  month =               jun,
}
[KV97] Orna Kupferman and Moshe Y. Vardi. Module Checking Revisited. In CAV'97, Lecture Notes in Computer Science 1254, pages 36-47. Springer-Verlag, June 1997. 
@inproceedings{cav1997-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Module Checking Revisited},
  editor =              {Grumberg, Orna},
  booktitle =           {{P}roceedings of the 9th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'97)},
  acronym =             {{CAV}'97},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1254},
  pages =               {36-47},
  year =                {1997},
  month =               jun,
}
[KV98] Orna Kupferman and Moshe Y. Vardi. Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time. In LICS'98, pages 81-92. IEEE Comp. Soc. Press, June 1998. 
@inproceedings{lics1998-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Freedom, Weakness, and Determinism: From Linear-Time
                         to Branching-Time},
  booktitle =           {{P}roceedings of the 13th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'98)},
  acronym =             {{LICS}'98},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {81-92},
  year =                {1998},
  month =               jun,
}
[KV98] Orna Kupferman and Moshe Y. Vardi. Weak Alternating Automata and Tree Automata Emptiness. In STOC'98, pages 224-233. ACM Press, May 1998. 
@inproceedings{stoc1998-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Weak Alternating Automata and Tree Automata
                         Emptiness},
  booktitle =           {{P}roceedings of the 30th {A}nnual {ACM} {S}ymposium
                         on the {T}heory of {C}omputing ({STOC}'98)},
  acronym =             {{STOC}'98},
  publisher =           {ACM Press},
  pages =               {224-233},
  year =                {1998},
  month =               may,
}
[KV99] Orna Kupferman and Moshe Y. Vardi. Model Checking of Safety Properties. In CAV'99, Lecture Notes in Computer Science 1633, pages 172-183. Springer-Verlag, July 1999. 
@inproceedings{cav1999-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Model Checking of Safety Properties},
  editor =              {Halbwachs, Nicolas and Peled, Doron A.},
  booktitle =           {{P}roceedings of the 11th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'99)},
  acronym =             {{CAV}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1633},
  pages =               {172-183},
  year =                {1999},
  month =               jul,
}
[KV99] Orna Kupferman and Moshe Y. Vardi. Robust Satisfaction. In CONCUR'99, Lecture Notes in Computer Science 1664, pages 383-398. Springer-Verlag, August 1999. 
@inproceedings{concur1999-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Robust Satisfaction},
  editor =              {Baeten, Jos C. M. and Mauw, Sjouke},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'99)},
  acronym =             {{CONCUR}'99},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1664},
  pages =               {383-398},
  year =                {1999},
  month =               aug,
}
[KV00] Orna Kupferman and Moshe Y. Vardi. An Automata-Theoretic Approach to Reasoning about Infinite-State Systems. In CAV'00, Lecture Notes in Computer Science 1855, pages 36-52. Springer-Verlag, July 2000. 
@inproceedings{cav2000-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {An Automata-Theoretic Approach to Reasoning about
                         Infinite-State Systems},
  editor =              {Emerson, E. Allen and Sistla, A. Prasad},
  booktitle =           {{P}roceedings of the 12th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'00)},
  acronym =             {{CAV}'00},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {1855},
  pages =               {36-52},
  year =                {2000},
  month =               jul,
}
[KV01] Orna Kupferman and Moshe Y. Vardi. Model Checking of Safety Properties. Formal Methods in System Design 19(3):291-314. Kluwer Academic, November 2001. 
@article{fmsd19(3)-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Model Checking of Safety Properties},
  publisher =           {Kluwer Academic},
  journal =             {Formal Methods in System Design},
  volume =              {19},
  number =              {3},
  pages =               {291-314},
  year =                {2001},
  month =               nov,
}
[KV01] Orna Kupferman and Moshe Y. Vardi. Synthesizing Distributed Systems. In LICS'01, pages 389-398. IEEE Comp. Soc. Press, June 2001. 
@inproceedings{lics2001-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Synthesizing Distributed Systems},
  booktitle =           {{P}roceedings of the 16th {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'01)},
  acronym =             {{LICS}'01},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {389-398},
  year =                {2001},
  month =               jun,
  doi =                 {10.1109/LICS.2001.932514},
}
[KV03] Orna Kupferman and Moshe Y. Vardi. Safraless Decision Procedures. In FOCS'03. IEEE Comp. Soc. Press, October 2003. 
@inproceedings{focs2003-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Safraless Decision Procedures},
  booktitle =           {{P}roceedings of the 44th {A}nnual {S}ymposium on
                         {F}oundations of {C}omputer {S}cience ({FOCS}'03)},
  acronym =             {{FOCS}'03},
  publisher =           {IEEE Comp. Soc. Press},
  year =                {2003},
  month =               oct,
}
[KV03] Orna Kupferman and Moshe Y. Vardi. Π2∩Σ2≡ AFMC. In ICALP'03, Lecture Notes in Computer Science 2719, pages 697-713. Springer-Verlag, June 2003. 
@inproceedings{icalp2003-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {{{\(\Pi_2\cap\Sigma_2\equiv \textup{AFMC}\)}}},
  editor =              {Baeten, Jos C. M. and Lenstra, Jan Karel and Parrow,
                         Joachim and Woeginger, Gerhard J.},
  booktitle =           {{P}roceedings of the 30th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'03)},
  acronym =             {{ICALP}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2719},
  pages =               {697-713},
  year =                {2003},
  month =               jun,
}
[KV06] Orna Kupferman and Moshe Y. Vardi. Memoryful Branching-Time Logic. In LICS'06, pages 265-274. IEEE Comp. Soc. Press, July 2006. 
@inproceedings{lics2006-KV,
  author =              {Kupferman, Orna and Vardi, Moshe Y.},
  title =               {Memoryful Branching-Time Logic},
  booktitle =           {{P}roceedings of the 21st {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'06)},
  acronym =             {{LICS}'06},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {265-274},
  year =                {2006},
  month =               jul,
}
[KVW00] Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An Automata-Theoretic Approach to Branching-Time Model-Checking. Journal of the ACM 47(2):312-360. ACM Press, March 2000. 
@article{jacm47(2)-KVW,
  author =              {Kupferman, Orna and Vardi, Moshe Y. and Wolper,
                         Pierre},
  title =               {An Automata-Theoretic Approach to Branching-Time
                         Model-Checking},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {47},
  number =              {2},
  pages =               {312-360},
  year =                {2000},
  month =               mar,
}
[KVW01] Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. Module Checking. Information and Computation 164(2):322-344. Academic Press, January 2001. 
@article{icomp164(2)-KVW,
  author =              {Kupferman, Orna and Vardi, Moshe Y. and Wolper,
                         Pierre},
  title =               {Module Checking},
  publisher =           {Academic Press},
  journal =             {Information and Computation},
  volume =              {164},
  number =              {2},
  pages =               {322-344},
  year =                {2001},
  month =               jan,
}
[KVW15] Igor V. Konnov, Helmut Veith, and Josef Widder. SMT and POR bea Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. In CAV'15, Lecture Notes in Computer Science 9206, pages 85-102. Springer-Verlag, July 2015. 
@inproceedings{cav2015-KVW,
  author =              {Konnov, Igor V. and Veith, Helmut and Widder, Josef},
  title =               {{SMT} and {POR} bea Counter Abstraction:
                         Parameterized Model Checking of Threshold-Based
                         Distributed Algorithms},
  editor =              {Kroening, Daniel and Pasareanu, Corina S.},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'15)},
  acronym =             {{CAV}'15},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {9206},
  pages =               {85-102},
  year =                {2015},
  month =               jul,
  doi =                 {10.1007/978-3-319-21690-4_6},
}
[KW03] Detlef Kähler and Thomas Wilke. Program complexity of dynamic LTL model checking. In CSL'03, Lecture Notes in Computer Science 2803, pages 271-284. Springer-Verlag, August 2003. 
@inproceedings{csl2003-KW,
  author =              {K{\"a}hler, Detlef and Wilke, Thomas},
  title =               {Program complexity of dynamic {LTL} model checking},
  editor =              {Baaz, Matthias and Makowsky, Johann A.},
  booktitle =           {{P}roceedings of the 17th {I}nternational {W}orkshop
                         on {C}omputer {S}cience {L}ogic ({CSL}'03)},
  acronym =             {{CSL}'03},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {2803},
  pages =               {271-284},
  year =                {2003},
  month =               aug,
  doi =                 {10.1007/978-3-540-45220-1_23},
}
[KW05] Shmuel Tomi Klein and Yair Wiseman. Parallel Lempel-Ziv Coding. Discrete Applied Mathematics 146(2):180-191. Elsevier, March 2005. 
@article{dam146(2)-KW,
  author =              {Klein, Shmuel Tomi and Wiseman, Yair},
  title =               {Parallel {L}empel-{Z}iv Coding},
  publisher =           {Elsevier},
  journal =             {Discrete Applied Mathematics},
  volume =              {146},
  number =              {2},
  pages =               {180-191},
  year =                {2005},
  month =               mar,
}
[KWN+08] Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel, and Andreas Podelski. Faster Than Uppaal?. In CAV'08, Lecture Notes in Computer Science 5123, pages 552-555. Springer-Verlag, July 2008. 
@inproceedings{cav2008KWNP,
  author =              {Kupferschmid, Sebastian and Wehrle, Martin and
                         Nebel, Bernhard and Podelski, Andreas},
  title =               {Faster Than {U}ppaal?},
  editor =              {Gupta, Aarti and Malik, Sharad},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'08)},
  acronym =             {{CAV}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5123},
  pages =               {552-555},
  year =                {2008},
  month =               jul,
}
[KWZ+03] Agi Kurucz, Frank Wolter, Michael Zakharyaschev, and Dov M. Gabbay. Many-Dimensional Modal Logics: Theory and Applications. Elsevier, 2003. 
@book{mdml2003-KWZG,
  author =              {Kurucz, Agi and Wolter, Frank and Zakharyaschev,
                         Michael and Gabbay, Dov M.},
  title =               {Many-Dimensional Modal Logics: Theory and
                         Applications},
  publisher =           {Elsevier},
  year =                {2003},
}
List of authors