I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications by Stefan Kiefer

2017

Dmitry Chistikov, Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell. On rationality of nonnegative matrix factorization. In Proceedings of the 28th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 1290–1305. SIAM, 2017.
PDF (465 kB)
Info
See dx.doi.org ...
Christoph Haase, Stefan Kiefer, and Markus Lohrey. Computing quantiles in Markov chains with multi-dimensional costs. In Proceedings of the 32nd Annual Symposium on Logic in Computer Science (LICS). IEEE, 2017.
PDF (516 kB)
Info
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Dominik Wojtczak. On strong determinacy of countable stochastic games. In Proceedings of the 32nd Annual Symposium on Logic in Computer Science (LICS). IEEE, 2017.
PDF (363 kB)
Info
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Dominik Wojtczak. Parity objectives in countable MDPs. In Proceedings of the 32nd Annual Symposium on Logic in Computer Science (LICS). IEEE, 2017.
PDF (356 kB)
Info
Slides 
Dmitry Chistikov, Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell. Nonnegative matrix factorization requires irrationality. SIAM Journal on Applied Algebra and Geometry (SIAGA), 1(1):285–307, 2017.
PDF (439 kB)
Info
See doi.org ...
Stefan Kiefer, Ines Marusic, and James Worrell. Minimisation of multiplicity tree automata. Logical Methods in Computer Science (LMCS), 13(1), 2017.
Info
See doi.org ...
Conference version

2016

Christoph Haase and Stefan Kiefer. The complexity of the th largest subset problem and related problems. Information Processing Letters (IPL), 116(2):111–115, 2016.
PDF (254 kB)
Info
See dx.doi.org ...
Nathanaël Fijalkow, Stefan Kiefer, and Mahsa Shirmohammadi. Trace refinement in labelled Markov decision processes. In Bart Jacobs and Christof Löding, editors, Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 9634 of LNCS, pages 303–318, Eindhoven, The Netherlands, 2016. Springer.
PDF (534 kB)
Info
Tech report version
Stefan Kiefer and A. Prasad Sistla. Distinguishing hidden Markov chains. In Proceedings of the 31st Annual Symposium on Logic in Computer Science (LICS), pages 66–75, New York, USA, 2016. ACM.
PDF (376 kB)
Info
Slides 
Tech report version
Dmitry Chistikov, Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell. On restricted nonnegative matrix factorization. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), volume 55 of Leibniz International Proceedings in Informatics (LIPIcs), pages 103:1–103:14, 2016.
PDF (605 kB)
Info
See drops.dagstuhl.de ...
Tech report version
Maria Bruna, Radu Grigore, Stefan Kiefer, Joël Ouaknine, and James Worrell. Proving the Herman-protocol conjecture. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), volume 55 of Leibniz International Proceedings in Informatics (LIPIcs), pages 104:1–104:12, 2016.
PDF (503 kB)
Info
See drops.dagstuhl.de ...
Tech report version
Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. Markov chains and unambiguous Büchi automata. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV), volume 9779 of LNCS, pages 23–42, 2016.
PDF (428 kB)
Info
See dx.doi.org ...
Tech report version

2015

Tomás Brázdil, Stefan Kiefer, Antonín Kučera, and Ivana Hutarová Vareková. Runtime analysis of probabilistic programs with unbounded recursion. Journal of Computer and System Sciences, 81(1):288–310, February 2015.
PDF (587 kB)
Info
See dx.doi.org ...
Conference version
Stefan Kiefer, Ines Marusic, and James Worrell. Minimisation of multiplicity tree automata. In Andrew Pitts, editor, Proceedings of the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 9034 of LNCS, pages 297–311, London, UK, 2015. Springer.
PDF (289 kB)
Info
Tech report version, Journal version
Tomáš Brázdil, Stefan Kiefer, Antonín Kučera, and Petr Novotný. Long-run average behaviour of probabilistic vector addition systems. In Proceedings of the 30th Annual Symposium on Logic in Computer Science (LICS), pages 44–55, Kyoto, Japan, 2015. IEEE.
PDF (321 kB)
Info
Tech report version
Christoph Haase and Stefan Kiefer. The odds of staying on budget. In Proceedings of the 42nd International Colloquium on Automata, Languages and Programming (ICALP), part II, volume 9135 of LNCS, pages 234–246, Kyoto, Japan, 2015. Springer.
PDF (245 kB)
Info
Tech report version
Radu Grigore and Stefan Kiefer. Tree buffers. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV), part I, volume 9206 of LNCS, pages 290–306, San Francisco, California, USA, 2015. Springer.
PDF (2 MB)
Info
Tech report version

2014

Tomáš Brázdil, Stefan Kiefer, and Antonín Kučera. Efficient analysis of probabilistic programs with an unbounded counter. Journal of the ACM, 61(6):41:1–41:35, December 2014.
PDF (558 kB)
Info
See dx.doi.org ...
Conference version
Vojtěch Forejt, Petr Jančar, Stefan Kiefer, and James Worrell. Language equivalence of probabilistic pushdown automata. Information and Computation, 237:1–11, October 2014.
PDF (274 kB)
Info
Rémi Bonnet, Stefan Kiefer, and Anthony W. Lin. Analysis of probabilistic basic parallel processes. In Anca Muscholl, editor, Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 8412 of LNCS, pages 43–57, Grenoble, France, 2014. Springer.
PDF (327 kB)
Info
Slides 
Tech report version
Stefan Kiefer and Björn Wachter. Stability and complexity of minimising probabilistic automata. In J. Esparza et al., editor, Proceedings of the 41st International Colloquium on Automata, Languages and Programming (ICALP), part II, volume 8573 of LNCS, pages 268–279, Copenhagen, Denmark, 2014. Springer.
PDF (262 kB)
Info
Slides 
Tech report version
Tomáš Brázdil, Stefan Kiefer, Antonín Kučera, Petr Novotný, and Joost-Pieter Katoen. Zero-reachability in probabilistic multi-counter automata. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 22:1–22:10, Vienna, Austria, 2014.
PDF (368 kB)
Info
Tech report version
Taolue Chen and Stefan Kiefer. On the total variation distance of labelled Markov chains. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 33:1–33:10, Vienna, Austria, 2014.
PDF (334 kB)
Info
Slides 
Tech report version

2013

Stefan Kiefer. BPA bisimilarity is EXPTIME-hard. Information Processing Letters (IPL), 113(4):101–106, 2013.
PDF (160 kB)
Info
See dx.doi.org ...
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. On the complexity of equivalence and minimisation for Q-weighted automata. Logical Methods in Computer Science (LMCS), 9(1:8):1–22, 2013.
PDF (247 kB)
Info
See arxiv.org ...
Conference version
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. A strongly polynomial algorithm for criticality of branching processes and consistency of stochastic context-free grammars. Information Processing Letters (IPL), 113(10–11):381–385, 2013.
PDF (167 kB)
Info
See dx.doi.org ...
Michael Benedikt, Stefan Göller, Stefan Kiefer, and Andrzej S. Murawski. Bisimilarity of pushdown automata is nonelementary. In Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 488–498, New Orleans, Louisiana, USA, 2013.
PDF (366 kB)
Info
See doi.ieeecomputersociety.org ...
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. Algorithmic probabilistic game semantics – playing games with automata. Formal Methods in System Design, 43(2):285–312, 2013.
PDF (1 MB)
Info
Tomáš Brázdil, Javier Esparza, Stefan Kiefer, and Antonín Kučera. Analyzing probabilistic pushdown automata. Formal Methods in System Design, 43(2):124–163, 2013.
PDF (1 MB)
Info

2012

Tomáš Brázdil and Stefan Kiefer. Stabilization of branching queueing networks. In C. Dürr and T. Wilke, editors, Proceedings of the 29th International Symposium on Theoretical Aspects of Computer Science (STACS), pages 507–518, Paris, France, 2012.
PDF (675 kB)
Info
Slides 
Tech report version
Tomáš Brázdil, Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Space-efficient scheduling of stochastically generated tasks. Information and Computation, 210:87–110, January 2012.
PDF (418 kB)
Info
Conference version
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. On the complexity of the equivalence problem for probabilistic automata. In Lars Birkedal, editor, Proceedings of the 15th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 7213 of LNCS, pages 467–481, Tallinn, Estonia, 2012. Springer.
PDF (281 kB)
Info
Slides 
Tech report version, Journal version
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. Apex: An analyzer for open probabilistic programs. In Madhusudan Parathasarathy and Sanjit A. Seshia, editors, Proceedings of the 24th International Conference on Computer Aided Verification (CAV), volume 7358 of LNCS, pages 693–698, Berkeley, California, USA, 2012. Springer.
PDF (280 kB)
Info
Slides 
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. In Madhusudan Parathasarathy and Sanjit A. Seshia, editors, Proceedings of the 24th International Conference on Computer Aided Verification (CAV), volume 7358 of LNCS, pages 123–138, Berkeley, California, USA, 2012. Springer.
PDF (372 kB)
Info
Tech report version
Taolue Chen, Klaus Dräger, and Stefan Kiefer. Model checking stochastic branching processes. In Vladimiro Sassone and Peter Widmayer, editors, Proceedings of the 37th International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 7464 of LNCS, pages 271–282, Bratislava, Slovakia, 2012. Springer.
PDF (357 kB)
Info
Slides 
Tech report version
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. Three tokens in Herman's algorithm. Formal Aspects of Computing, 24(4):671–678, 2012.
PDF (281 kB)
Info
See dx.doi.org ...
Vojtěch Forejt, Petr Jančar, Stefan Kiefer, and James Worrell. Bisimilarity of probabilistic pushdown automata. In Deepak D'Souza, Telikepalli Kavitha, and Jaikumar Radhakrishnan, editors, Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Leibniz International Proceedings in Informatics (LIPIcs), pages 448–460, Hyderabad, India, 2012.
PDF (565 kB)
Info
See drops.dagstuhl.de ...

2011

Stefan Kiefer and Dominik Wojtczak. On probabilistic parallel programs with process creation and synchronisation. In P.A. Abdulla and K.R.M. Leino, editors, Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 6605 of LNCS, pages 296–310, Saarbrücken, Germany, 2011. Springer.
PDF (176 kB)
Info
Slides 
Tech report version
Javier Esparza, Pierre Ganty, Stefan Kiefer, and Michael Luttenberger. Parikh's theorem: A simple and direct automaton construction. Information Processing Letters (IPL), 111(12):614–619, 2011.
PDF (217 kB)
Info
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Derivation tree analysis for accelerated fixed-point computation. Theoretical Computer Science, 412(28):3226–3241, 2011.
PDF (279 kB)
Info
Conference version
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, James Worrell, and Lijun Zhang. On stabilization in Herman's algorithm. In L. Aceto, M. Henzinger, and J. Sgall, editors, Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP), volume 6756 of LNCS, pages 466–477, Zürich, Switzerland, 2011. Springer.
PDF (190 kB)
Info
Slides 
Tech report version
Tomáš Brázdil, Stefan Kiefer, Antonín Kučera, and Ivana Hutařová Vařeková. Runtime analysis of probabilistic programs with unbounded recursion. In L. Aceto, M. Henzinger, and J. Sgall, editors, Proceedings of the 38th International Colloquium on Automata, Languages and Programming (ICALP), volume 6756 of LNCS, pages 319–331, Zürich, Switzerland, 2011. Springer.
PDF (157 kB)
Info
Journal version
Tomáš Brázdil, Stefan Kiefer, and Antonín Kučera. Efficient analysis of probabilistic programs with an unbounded counter. In G. Gopalakrishnan and S. Qadeer, editors, Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), volume 6806 of LNCS, pages 208–224, Snowbird, Utah, USA, 2011. Springer.
PDF (177 kB)
Info
Slides 
Tech report version, Journal version
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. Language equivalence for probabilistic automata. In G. Gopalakrishnan and S. Qadeer, editors, Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), volume 6806 of LNCS, pages 526–540, Snowbird, Utah, USA, 2011. Springer.
PDF (202 kB)
Info

2010

Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Newtonian program analysis. Journal of the ACM, 57(6):33:1–33:47, October 2010.
Info
Tech report version
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Computing least fixed points of probabilistic systems of polynomials. In Proceedings of the 27th International Symposium on Theoretical Aspects of Computer Science (STACS), pages 359–370, Nancy, France, 2010.
PDF (182 kB)
Info
Slides 
Tech report version
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Computing the least fixed point of positive polynomial systems. SIAM Journal on Computing, 39(6):2282–2335, 2010.
PDF (845 kB)
Info
Tech report version
Tomáš Brázdil, Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Space-efficient scheduling of stochastically generated tasks. In Samson Abramsky et al., editor, Proceedings of the 37th International Colloquium on Automata, Languages and Programming (ICALP), part II, volume 6199 of LNCS, ARCoSS, pages 539–550, Bordeaux, France, 2010. Springer.
PDF (151 kB)
Info
Slides 
Tech report version, Journal version

2009

Morten Kühnrich, Stefan Schwoon, Jiří Srba, and Stefan Kiefer. Interprocedural dataflow analysis over weight domains with infinite descending chains. In Luca de Alfaro, editor, Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS), volume 5504 of LNCS, pages 440–455, York, UK, March 2009. Springer.
PDF (211 kB)
Info
Tech report version
Tomáš Brázdil, Javier Esparza, and Stefan Kiefer. On the memory consumption of probabilistic pushdown automata. In Ravi Kannan and K. Narayan Kumar, editors, Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Leibniz International Proceedings in Informatics, pages 49–60, Kanpur, India, 2009.
PDF (162 kB)
Info
See drops.dagstuhl.de ...
Slides 
Tech report version
Stefan Kiefer. Solving systems of positive polynomial equations. PhD thesis, Technische Universität München, 2009.
PDF (931 kB)
Info
Slides 

2008

Javier Esparza, Stefan Kiefer, and Stefan Schwoon. Abstraction refinement with Craig interpolation and symbolic pushdown systems. Journal on Satisfiability, Boolean Modeling and Computation, 5:27–56, June 2008. Special Issue on Constraints to Formal Verification.
PDF (653 kB)
Info
Tech report version, Conference version
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Convergence thresholds of Newton's method for monotone polynomial equations. In Pascal Weil and Susanne Albers, editors, Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS), pages 289–300, Bordeaux, France, 2008. Available at http://arxiv.org/abs/0802.2856.
GZipped PostScript (210 kB)
PDF (199 kB)
Info
See arxiv.org ...
Tech report version
Javier Esparza, Thomas Gawlitza, Stefan Kiefer, and Helmut Seidl. Approximative methods for monotone systems of min-max-polynomial equations. In Luca Aceto et al., editor, Proceedings of the 35th International Colloquium on Automata, Languages and Programming (ICALP), part I, volume 5125 of LNCS, pages 698–710, Reykjavik, Iceland, 2008. Springer.
GZipped PostScript (115 kB)
PDF (147 kB)
Info
Tech report version
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Solving monotone polynomial equations. In Fifth IFIP International Conference On Theoretical Computer Science (TCS), volume 273 of IFIP International Federation for Information Processing, pages 285–298, Milano, Italy, 2008. Springer. Invited paper.
GZipped PostScript (67 kB)
PDF (107 kB)
Info
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Newton's method for -continuous semirings. In Luca Aceto et al., editor, Proceedings of the 35th International Colloquium on Automata, Languages and Programming (ICALP), part II, volume 5126 of LNCS, pages 14–26, Reykjavik, Iceland, 2008. Springer. Invited paper.
GZipped PostScript (113 kB)
PDF (140 kB)
Info
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Derivation tree analysis for accelerated fixed-point computation. In Masami Ito and Masafumi Toyama, editors, Proceedings of the 12th International Conference on Developments in Language Theory (DLT), volume 5257 of LNCS, pages 301–313, Kyoto, Japan, 2008. Springer.
GZipped PostScript (127 kB)
PDF (147 kB)
Info
Tech report version, Journal version

2007

Javier Esparza, Stefan Kiefer, and Michael Luttenberger. On fixed point equations over commutative semirings. In Wolfgang Thomas and Pascal Weil, editors, Proceedings of the 24th International Symposium on Theoretical Aspects of Computer Science (STACS), volume 4393 of LNCS, pages 296–307, Aachen, Germany, 2007. Springer.
GZipped PostScript (179 kB)
PDF (162 kB)
Info
Tech report version
Stefan Kiefer, Michael Luttenberger, and Javier Esparza. On the convergence of Newton's method for monotone systems of polynomial equations. In Proceedings of the 39th ACM Symposium on Theory of Computing (STOC), pages 217–226, San Diego, California, USA, 2007. ACM.
GZipped PostScript (192 kB)
PDF (183 kB)
Info
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. An extension of Newton's method to -continuous semirings. In Tero Harju, Juhani Karhumäki, and Arto Lepistö, editors, Proceedings of the 11th International Conference on Developments in Language Theory (DLT), volume 4588 of LNCS, pages 157–168, Turku, Finland, 2007. Springer.
GZipped PostScript (178 kB)
PDF (167 kB)
Info
Tech report version

2006

Javier Esparza, Stefan Kiefer, and Stefan Schwoon. Abstraction refinement with Craig interpolation and symbolic pushdown systems. In Holger Hermanns and Jens Palsberg, editors, Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3920 of LNCS, pages 489–503, Vienna, Austria, 2006. Springer.
GZipped PostScript (182 kB)
PDF (174 kB)
Info
Tech report version, Journal version

2005

Stefan Kiefer. Abstraction refinement for pushdown systems. Master's thesis, Universität Stuttgart, 2005.
GZipped PostScript (329 kB)
PDF (557 kB)
Info

2003

Stefan Kiefer. Die Menge der virtuellen Verbindungen im Spiel Hex ist PSPACE-vollständig. Studienarbeit Nr. 1887, Universität Stuttgart, Juli 2003. In German.
GZipped PostScript (280 kB)
PDF (375 kB)
Info