I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Technical Reports

2016

Javier Esparza, Pierre Ganty, Jerome Leroux, and Rupak Majumdar. Model checking population protocols. Technical report, Technical University of Munich, 2016. Submitted for publication.
PDF (502 kB)
Info
See arxiv.org ...
Javier Esparza, Michael Luttenberger, and Maximilian Schlund. A brief history of Strahler numbers — with a preface. Technical report, Technical University of Munich, 2016.
PDF (424 kB)
Info
Conference version
Nathanaël Fijalkow, Stefan Kiefer, and Mahsa Shirmohammadi. Minimisation of multiplicity tree automata. Technical report, arXiv.org, 2016. Available at http://arxiv.org/abs/1510.09102.
Info
See arxiv.org ...
Conference version
Stefan Kiefer and A. Prasad Sistla. Distinguishing hidden Markov chains. Technical report, arXiv.org, 2016. Available at https://arxiv.org/abs/1507.02314.
Info
See arxiv.org ...
Conference version
Dmitry Chistikov, Stefan Kiefer, Ines Marusic, Mahsa Shirmohammadi, and James Worrell. On restricted nonnegative matrix factorization. Technical report, arXiv.org, 2016. Available at https://arxiv.org/abs/1605.07061.
Info
See arxiv.org ...
Conference version
Maria Bruna, Radu Grigore, Stefan Kiefer, Joël Ouaknine, and James Worrell. Proving the Herman-protocol conjecture. Technical report, arXiv.org, 2016. Available at https://arxiv.org/abs/1504.01130.
Info
See arxiv.org ...
Conference version
Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller, and James Worrell. Markov chains and unambiguous Büchi automata. Technical report, arXiv.org, 2016. Available at https://arxiv.org/abs/1605.00950.
Info
See arxiv.org ...
Conference version

2015

Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, and Rupak Majumdar. Model checking parameterized asynchronous shared-memory systems. Technical report, CoRR, 2015.
PDF (333 kB)
Info
See arxiv.org ...
Stefan Kiefer, Ines Marusic, and James Worrell. Minimisation of multiplicity tree automata. Technical report, arXiv.org, 2015. Available at http://arxiv.org/abs/1410.5352.
Info
See arxiv.org ...
Conference version, Journal version
Tomáš Brázdil, Stefan Kiefer, Antonín Kučera, and Petr Novotný. Long-run average behaviour of probabilistic vector addition systems. Technical report, arXiv.org, 2015. Available at http://arxiv.org/abs/1505.02655.
Info
See arxiv.org ...
Conference version
Christoph Haase and Stefan Kiefer. The odds of staying on budget. Technical report, arXiv.org, 2015. Available at http://arxiv.org/abs/1409.8228.
Info
See arxiv.org ...
Conference version
Radu Grigore and Stefan Kiefer. Tree buffers. Technical report, arXiv.org, 2015. Available at http://arxiv.org/abs/1504.04757.
Info
See arxiv.org ...
Conference version

2014

Stefan Kiefer and Björn Wachter. Stability and complexity of minimising probabilistic automata. Technical report, arXiv.org, May 2014. Available at http://arxiv.org/abs/1404.6673.
Info
See arxiv.org ...
Conference version
Javier Esparza and Jan Kretínský. From LTL to deterministic automata: A safraless compositional approach. Technical report, arxiv.org, 2014.
PDF (418 kB)
Info
Conference version, Journal version
Javier Esparza and Jörg Desel. On negotiation as concurrency primitive ii: Deterministic cyclic negotiations. Technical report, arXiv.org, 2014.
PDF (391 kB)
Info
Conference version
Rémi Bonnet, Stefan Kiefer, and Anthony W. Lin. Analysis of probabilistic basic parallel processes. Technical report, arXiv.org, January 2014. Available at http://arxiv.org/abs/1401.4130.
Info
See arxiv.org ...
Conference version
Tomáš Brázdil, Stefan Kiefer, Antonín Kučera, Petr Novotný, and Joost-Pieter Katoen. Zero-reachability in probabilistic multi-counter automata. Technical report, arXiv.org, 2014. Available at http://arxiv.org/abs/1401.6840.
Info
See arxiv.org ...
Conference version
Taolue Chen and Stefan Kiefer. On the total variation distance of labelled Markov chains. Technical report, arXiv.org, 2014. Available at http://arxiv.org/abs/1405.2852.
Info
See arxiv.org ...
Conference version

2013

Javier Esparza and Jörg Desel. On negotiation as concurrency primitive. Technical report, arXiv.org, 2013.
PDF (442 kB)
Info
Conference version
Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. Technical report, arXiv.org, 2013.
Info
Conference version
Krishnendu Chatterjee, Andreas Gaiser, and Jan Kretinsky. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. Technical Report abs/1304.5281, arXiv.org, 2013.
Info
Jan Kretinsky and Salomon Sickert. On refinements of Boolean and parametric modal transition systems. Technical Report abs/1304.5278, arXiv.org, 2013.
Info
Nikola Benes, Benoit Delahaye, Uli Fahrenberg, Jan Kretinsky, and Axel Legay. Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory. Technical Report abs/1306.0741, arXiv.org, 2013.
Info
Holger Hermanns, Jan Krcal, and Jan Kretinsky. Compositional verification and optimization of interactive Markov chains. Technical Report abs/1305.7332, arXiv.org, 2013.
Info

2012

Taolue Chen, Klaus Dräger, and Stefan Kiefer. Model checking stochastic branching processes. Technical report, arXiv.org, June 2012. Available at http://arxiv.org/abs/1206.1317.
Info
See arxiv.org ...
Conference version
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. Technical report, arXiv.org, April 2012. Available at http://arxiv.org/abs/1204.2932.
Info
See arxiv.org ...
Conference version
Javier Esparza, Pierre Ganty, and Rupak Majumdar. A perfect model for bounded verification. Technical report, arXiv.org, 2012.
Info
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. Technical Report abs/1106.1424, arXiv.org, 2012.
Info
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. On the complexity of the equivalence problem for probabilistic automata. Technical report, arXiv.org, January 2012. Available at http://arxiv.org/abs/1112.4644.
PDF (206 kB)
Info
See arxiv.org ...
Conference version
Nikola Benes, Jan Kretinsky, Kim G. Larsen, Mikael H. Moller, and Jiri Srba. Dual-priced modal transition systems with time durations. Technical report FIMU-RS-2012-01, Faculty of Informatics, Masaryk University, Brno, 2012.
Info
Jan Kretinsky and Javier Esparza. Deterministic automata for the (F,G)-fragment of LTL. Technical Report abs/1106.1424, arXiv.org, 2012.
Info
Nikola Benes and Jan Kretinsky. Modal process rewrite systems. Technical report FIMU-RS-2012-02, Faculty of Informatics, Masaryk University, Brno, 2012.
Info
Tomas Brazdil, Holger Hermanns, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Verification of open interactive markov chains. Technical report FIMU-RS-2012-04, Faculty of Informatics, Masaryk University, Brno, 2012.
Info

2011

Tomáš Brázdil and Stefan Kiefer. Stabilization of branching queueing networks. Technical report, arXiv.org, December 2011. Available at http://arxiv.org/abs/1112.1041.
PDF (594 kB)
Info
See arxiv.org ...
Conference version
Michael Luttenberger. An extension of Parikh's theorem beyond idempotence. Technical report, Technische Universität München, Institut für Informatik, December 2011.
Info
See arxiv.org ...
Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, James Worrell, and Lijun Zhang. On stabilization in Herman's algorithm. Technical report, arXiv.org, April 2011. Available at http://arxiv.org/abs/1104.3100.
PDF (253 kB)
Info
See arxiv.org ...
Conference version
Tomáš Brázdil, Stefan Kiefer, and Antonín Kučera. Efficient analysis of probabilistic programs with an unbounded counter. Technical report, arXiv.org, April 2011. Available at http://arxiv.org/abs/1102.2529.
Info
See arxiv.org ...
Conference version, Journal version
Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. Technical report, Technische Universität München, 2011. Available via arxiv.org (arXiv:1106.1364).
Info
Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. Technical report, Technische Universität München, 2011. Available via arxiv.org (arXiv:1106.1364).
Info
Tomas Brazdil, Jan Krcal, Jan Kretinsky, Antonin Kucera, and Vojtech Rehak. Measuring performance of continuous-time stochastic processes using timed automata. Technical Report abs/1101.4204, arXiv.org, 2011.
Info
Tomas Brazdil, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Fixed-delay events in generalized semi-markov processes revisited. Technical Report abs/1106.1424, arXiv.org, 2011.
Info
Nikola Benes, Jan Kretinsky, Kim G. Larsen, Mikael H. Moller, and Jiri Srba. Parametric modal transition systems. Technical report FIMU-RS-2011-03, Faculty of Informatics, Masaryk University, Brno, 2011.
Info

2010

Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. Technical report, Technische Universität München, Institut für Informatik, December 2010.
PDF (426 kB)
Info
Javier Esparza and Andreas Gaiser. Probabilistic abstractions with arbitrary domains. Technical report, Technische Universität München, Institut für Informatik, December 2010.
PDF (426 kB)
Info
Stefan Kiefer and Dominik Wojtczak. On probabilistic parallel programs with process creation and synchronisation. Technical report, arXiv.org, December 2010. Available at http://arxiv.org/abs/1012.2998.
PDF (254 kB)
Info
See arxiv.org ...
Conference version
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Newtonian program analysis. Technical report, Technische Universität München, Institut für Informatik, September 2010. This is a late draft of the article in the Journal of the ACM.
PDF (422 kB)
Info
Journal version
Tomáš Brázdil, Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Space-efficient scheduling of stochastically generated tasks. Technical report, arXiv.org, April 2010. Available at http://arxiv.org/abs/1004.4286.
PDF (278 kB)
Info
See arxiv.org ...
Conference version, Journal version
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Computing the least fixed point of positive polynomial systems. Technical report, arXiv.org, January 2010. Available at http://arxiv.org/abs/1001.0340.
PDF (899 kB)
Info
See arxiv.org ...
Journal version
Tomas Brazdil, Jan Krcal, Jan Kretinsky, Antonin Kucera, and Vojtech Rehak. Stochastic real-time games with qualitative timed automata objectives. Technical report FIMU-RS-2010-05, Faculty of Informatics, Masaryk University, Brno, 2010.
Info
Nikola Benes and Jan Kretinsky. Process algebra for modal transition systemses. Technical report FIMU-RS-2010-11, Faculty of Informatics, Masaryk University, Brno, 2010.
Info
Nikola Benes, Ivana Cerna, and Jan Kretinsky. Disjunctive modal transition systems and generalized LTL model checking. Technical report FIMU-RS-2010-12, Faculty of Informatics, Masaryk University, Brno, 2010.
Info

2009

Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Computing least fixed points of probabilistic systems of polynomials. Technical report, Technische Universität München, Institut für Informatik, December 2009.
PDF (349 kB)
Info
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Computing least fixed points of probabilistic systems of polynomials. Technical report, Technische Universität München, Institut für Informatik, December 2009.
PDF (349 kB)
Info
Tomáš Brázdil, Javier Esparza, and Stefan Kiefer. On the memory consumption of probabilistic pushdown automata. Technical Report FIMU-RS-2009-07, Faculty of Informatics, Masaryk University, October 2009.
PDF (447 kB)
Info
Conference version
Andreas Holzer, Visar Januzaj, Stefan Kugele, Christian Schallhart, Michael Tautschnig, Helmut Veith, and Boris Langer. Slope testing for activity diagrams and safety critical software. Technical Report TUD-CS-2009-0184, Technische Universität Darmstadt, October 2009.
PDF (403 kB)
Info
Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, and Jiri Srba. Checking thorough refinement on modal transition systems is exptime-complete. Technical report FIMU-RS-2009-03, Faculty of Informatics, Masaryk University, Brno, 2009.
Info
Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera. Continuous-time stochastic games with time-bounded reachability. Technical report FIMU-RS-2009-09, Faculty of Informatics, Masaryk University, Brno, 2009.
Info
Morten Kühnrich, Stefan Schwoon, Jiří Srba, and Stefan Kiefer. Interprocedural dataflow analysis over weight domains with infinite descending chains. Technical Report 0901.0501, Computing Research Repository, 2009.
PDF (242 kB)
Info
Conference version
Andreas Gaiser and Stefan Schwoon. Comparison of algorithms for checking emptiness on Büchi automata. Technical Report 0910.3766, Computing Research Repository, 2009.
PDF (160 kB)
Info
Conference version

2008

Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Derivation tree analysis for accelerated fixed-point computation. Technical report, Technische Universität München, Institut für Informatik, September 2008.
GZipped PostScript (174 kB)
PDF (220 kB)
Info
Conference version
Javier Esparza, Thomas Gawlitza, Stefan Kiefer, and Helmut Seidl. Approximative methods for monotone systems of min-max-polynomial equations. Technical report, Technische Universität München, Institut für Informatik, February 2008.
GZipped PostScript (181 kB)
PDF (267 kB)
Info
Conference version
Tomas Brazdil, Vojtech Forejt, Jan Kretinsky, and Antonin Kucera. The satisfiability problem for probabilistic CTL. Technical report FIMU-RS-2008-03, Faculty of Informatics, Masaryk University, Brno, 2008.
Info

2007

Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Convergence thresholds of Newton's method for monotone polynomial equations. Technical report, Technische Universität München, Institut für Informatik, October 2007.
GZipped PostScript (206 kB)
PDF (287 kB)
Info
Conference version
Stefan Kugele, Michael Tautschnig, Andreas Bauer, Christian Schallhart, Stefano Merenda, Wolfgang Haberl, Christian Kühnel, Florian Müller, Zhonglei Wang, Doris Wild, Sabine Rittmann, and Martin Wechs. COLA – The component language. Technical Report TUM-I0714, Institut für Informatik, Technische Universität München, September 2007.
PDF (427 kB)
Info
Christian Kühnel, Andreas Bauer, and Michael Tautschnig. Compatibility and reuse in component-based systems via type and unit inference. Technical Report TUM-I0716, Institut für Informatik, Technische Universität München, May 2007.
PDF (225 kB)
Info
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. An extension of Newton's method to -continuous semirings. Technical report, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, March 2007.
GZipped PostScript (196 kB)
PDF (193 kB)
Info
Conference version

2006

Javier Esparza, Stefan Kiefer, and Michael Luttenberger. On fixed point equations over commutative semirings. Technical report, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, December 2006.
GZipped PostScript (217 kB)
PDF (214 kB)
Info
Conference version
J. Esparza, P. Jančar, and A. Miller. On the complexity of consistency and complete state coding. Technical report, University of Stuttgart, July 2006.
GZipped PostScript (126 kB)
PDF (184 kB)
Info
Conference version, Journal version
G. Delzanno, J. Esparza, and J. Srba. Monotonic set-extended prefix rewriting and verification of recursive ping-pong protocols. Technical report, BRICS, 2006.
GZipped PostScript (227 kB)
PDF (304 kB)
Info
Conference version
Javier Esparza, Stefan Kiefer, and Stefan Schwoon. Abstraction refinement with Craig interpolation and symbolic pushdown systems. Technical Report 2006/02, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, January 2006.
GZipped PostScript (219 kB)
PDF (219 kB)
Info
Conference version, Journal version
Dejvuth Suwimonteerabuth, Stefan Schwoon, and Javier Esparza. Efficient algorithms for alternating pushdown systems: Application to certificate chain discovery with threshold subjects. Technical Report 2006/09, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, 2006.
GZipped PostScript (216 kB)
Info
Conference version

2005

Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, and Helmut Veith. Malware normalization. Technical Report 1539, University of Wisconsin, Madison, Wisconsin, USA, November 2005.
PDF (312 kB)
Info
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejček. Reachability analysis of multithreaded software with asynchronous communication. Technical Report 2005/06, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, November 2005.
GZipped PostScript (65 kB)
PDF (183 kB)
Info
Conference version
Stefan Schwoon, Hao Wang, Somesh Jha, and Thomas Reps. Distributed certificate-chain discovery in SPKI/SDSI. Technical Report TR-1526, Computer Sciences Department, University of Wisconsin, August 2005.
GZipped PostScript (160 kB)
Info
Conference version
Hao Wang, Somesh Jha, Thomas Reps, Stefan Schwoon, and Stuart Stubblebine. Reducing the dependence of trust-management systems on PKI. Technical Report TR-1527, Computer Sciences Department, University of Wisconsin, August 2005.
GZipped PostScript (126 kB)
Info
Conference version
Javier Esparza, Antonín Kučera, and Richard Mayr. Quantitative analysis of probabilistic pushdown automata: Expectations and variances. Technical Report FIMU-RS-2005-07, Masaryk University, 2005.
PDF (253 kB)
Info
Conference version
F. Fischer and M. Nickles. Towards a notion of generalised statement-level trust. Technical Report FKI-249-05, Institut für Informatik, Technical University of Munich, 2005.
Info

2004

Stefan Schwoon and Javier Esparza. A note on on-the-fly verification algorithms. Technical Report 2004/06, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, November 2004.
GZipped PostScript (93 kB)
PDF (179 kB)
Info
See www.fmi.uni-stuttgart.de ...
Conference version
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Technical report, Faculty of Informatics, Masaryk University, Brno, 2004.
GZipped PostScript (206 kB)
PDF (738 kB)
Info
Conference version, Journal version

2003

Thomas Reps, Stefan Schwoon, and Somesh Jha. Weighted pushdown systems and their application to interprocedural dataflow analysis. Technical Report TR-1470, Computer Sciences Department, University of Wisconsin, February 2003.
GZipped PostScript (261 kB)
Info
See www.fmi.uni-stuttgart.de ...
Conference version, Journal version
Stefan Schwoon, Somesh Jha, Thomas Reps, and Stuart Stubblebine. On generalized authorization problems. Technical Report TR-1469, Computer Sciences Department, University of Wisconsin, January 2003.
GZipped PostScript (168 kB)
Info
See www.fmi.uni-stuttgart.de ...
Conference version

2001

Javier Esparza, Antonín Kučera, and Stefan Schwoon. Model-checking LTL with regular valuations for pushdown systems. Informatics Research Report EDI-INF-RR-0044, University of Edinburgh, School of Informatics, August 2001.
PDF (224 kB)
Info
Conference version, Journal version
Markus Holzer and Stefan Schwoon. Assembling molecules in Atomix is hard. Technical Report TUM-I0101, Technische Universität München, May 2001.
GZipped PostScript (75 kB)
Info
Journal version
J. Esparza and K. Heljanko. Implementing LTL model checking with net unfoldings. Research Report A68, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, March 2001.
GZipped PostScript (271 kB)
PDF (281 kB)
Info
Conference version
M. Nickles. SYSTEMATICS - Ein XML-basiertes Internet-Datenbanksystem für klassifikationsgestützte Sprachbeschreibungen. Technical Report CIS-Report 01-129, Centre for Information and Language Processing (CIS), University of Munich, 2001.
Info
M. Nickles. Towards a multiagent system for competitive website ratings. Technical Report FKI-243-01, Institut für Informatik, Technische Universität München, 2001.
Info

2000

Javier Esparza, David Hansel, Peter Rossmanith, and Stefan Schwoon. Efficient algorithms for model checking pushdown systems. Technical Report TUM-I0002, SFB-Bericht 342/1/00 A, Technische Universität München, Institut für Informatik, February 2000.
GZipped PostScript (166 kB)
Info
Conference version

1995

P. Jancar and J. Esparza. Deciding finiteness of Petri nets up to bisimulation. SFB-Bericht Nr. 342/23/95A, TU München, 1995.
GZipped PostScript (356 kB)
PDF (826 kB)
Info
Conference version, Journal version