Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Books and Journal Articles

To appear

M. Luttenberger and M. Schlund. Convergence of Newton's Method over Commutative Semirings. Information and Computation, ?(?):??–??, To appear.
PDF (449 kB)
Info

2020

Nathanaël Fijalkow, Stefan Kiefer, and Mahsa Shirmohammadi. Trace refinement in labelled Markov decision processes. Logical Methods in Computer Science, Volume 16, Issue 2, 2020.
Info
See lmcs.episciences.org ...
Conference version

2018

Vojtěch Forejt, Petr Jančar, Stefan Kiefer, and James Worrell. Game characterization of probabilistic bisimilarity, and applications to pushdown automata. Logical Methods in Computer Science (LMCS), 14(4), 2018.
Info
See lmcs.episciences.org ...
Conference version

2017

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

Eike Best and Javier Esparza. Existence of home states in petri nets is decidable. Inf. Process. Lett., 116(6):423–427, 2016.
PDF (289 kB)
Info
Jérôme Leroux Javier Esparza, Pierre Ganty and Rupak Majumdar. Verification of population protocols. Acta Informatica, 2016. To appear.
PDF (219 kB)
Info
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 ...

2015

Salomon Sickert. Converting linear temporal logic to deterministic (generalized) rabin automata. Archive of Formal Proofs, September 2015.
Info
See afp.sf.net ...
This publication contains the formalization of LTL_to_DRA.
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
Javier Esparza, Michael Luttenberger, and Maximilian Schlund. FPSOLVE: A generic solver for fixpoint equations over semirings. Int. J. Found. Comput. Sci., 26(7):805–826, 2015.
PDF (438 kB)
Info
Javier Esparza, Jan Kretinsky, and Salomon Sickert. From ltl to deterministic automata–a safraless compositional approach. Submitted, 2015.
PDF (690 kB)
Info
Tech report version, Conference version
This publication is a major revision of EsparzaK_CAV14, contains several corrections and new material.

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
Javier Esparza, Peter Lammich, Rene Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A fully verified executable LTL model checker. Archive of Formal Proofs, May 2014. Formal proof development.
Info
See afp.sf.net ...
Rene Neumann. Promela formalization. Archive of Formal Proofs, May 2014. Formal proof development.
Info
See afp.sf.net ...
Javier Esparza and Philipp Hoffmann. Negotiation games. CoRR, abs/1405.6820, 2014.
PDF (395 kB)
Info

2013

Corneliu Popeea and Wei-Ngan Chin. Dual analysis for proving safety and finding bugs. Sci. Comput. Program., 78(4):390–411, April 2013.
Info
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. A strongly polynomial algorithm for criticality of branching processes and consistency of stochastic context-free grammars. Inf. Process. Lett., 113(10-11):381–385, 2013.
PDF (170 kB)
Info
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 ...
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
Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky, and Antonin Kucera. Continuous-time stochastic games with time-bounded reachability. Inf. Comput., 224:46–70, 2013.
Info

2012

Javier Esparza and Jörg Kreiker. Three case studies on verification of infinite-state systems. In Modern Applications of Automata Theory. World Scientific Publishing, 2012.
PDF (424 kB)
Info
Javier Esparza, Orna Kupferman, and Moshe Vardi. Verification. In Hanbook on Automata Theory. European Mathematical Society, 2012. To appear.
PDF (319 kB)
Info
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. Three tokens in Herman's algorithm. Formal Aspects of Computing, 24(4):671–678, 2012.
PDF (281 kB)
Info
See dx.doi.org ...
Nikola Benes, Jan Kretinsky, Kim G. Larsen, and Jiri Srba. Exptime-completeness of thorough refinement on modal transition systems. Inf. Comput., 218:54–68, 2012.
Info

2011

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
Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Proving program termination. Commun. ACM, 54(5):88–98, 2011.
Info
J. Esparza, M. Leucker, and M. Schlund. Learning workflow Petri nets. Fundamenta Informaticae, 113(3-4):205–228, 2011.
PDF (212 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
Rene Neumann. Functional binomial queues. Archive of Formal Proofs, October 2010. Formal proof development.
Info
See afp.sf.net ...
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
Andrey Rybalchenko and Viorica Sofronie-Stokkermans. Constraint solving for interpolation. J. Symb. Comput., 45(11):1212–1233, 2010.
Info
Nuno P. Lopes, Juan Antonio Navarro Pérez, Andrey Rybalchenko, and Atul Singh. Applying prolog to develop distributed systems. TPLP, 10(4-6):691–707, 2010.
Info

2009

Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, and Jiri Srba. On determinism in modal transition systems. Theor. Comput. Sci., 410(41):4026–4043, 2009.
Info

2008

Paolo Baldan, Andrea Corradini, Barbara König, and Stefan Schwoon. McMillan's complete prefix for contextual nets. Transactions on Petri Nets and Other Models of Concurrency, 1:199–220, November 2008. Volume 5100 of Lecture Notes in Computer Science.
GZipped PostScript (127 kB)
Info
Conference version
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 (322 kB)
Info
Tech report version, Conference version
Javier Esparza and Keijo Heljanko. Unfoldings - a partial-order approach to model checking. EATCS Monographs in Theoretical Computer Science. Springer-Verlag, 2008.
PDF (961 kB)
Info
See www.springer.com ...
Author created final book draft made available through our publishing agreement with Springer. Can not be made available on any other Web sites than the author homepages. The book can be purchased from the publisher. If you are interested, follow the link above.
J. Esparza, P. Jančar, and A. Miller. On the complexity of consistency and complete state coding for signal transition graphs. Fundamenta Informaticae, 86(3):227–253, 2008.
PDF (189 kB)
Info
Conference version, Tech report version
Javier Esparza, Pradeep Kanade, and Stefan Schwoon. A negative result on depth-first unfoldings. Software Tools for Technology Transfer, 10(2):161–166, 2008.
GZipped PostScript (80 kB)
Info

2007

Mihai Christodorescu, Johannes Kinder, Somesh Jha, Stefan Katzenbeisser, and Helmut Veith. Software transformations to improve malware detection. Journal in Computer Virology, 3(4):253–265, November 2007.
PDF (306 kB)
Info
Tech report version
Thomas Reps, Mooly Sagiv, and J. Bauer, editors. Program analysis and compilation, theory and practice, essays dedicated to reinhard wilhelm on the occasion of his 60th birthday, volume 4444 of Lecture Notes in Computer Science. Springer, 2007.
Info
M. Nickles. Social acquisition of ontologies from communication processes. Journal of Applied Ontology, special issue "Formal Ontologies for Communicating Agents", 2007.
Info
M. Nickles, M. Rovatsos, M. Schmitt, W. Brauer, F. Fischer, Th. Malsch, K. Paetow, and G. Weiß. The Empirical Semantics Approach to Communication Structure Learning and Usage: Individuals- vs. System-Views. Journal of Artificial Societies and Social Simulation (JASSS), Issue on Socionics, 2007.
Info

2006

Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Logical Methods in Computer Science, 2006.
PDF (403 kB)
Info
Tech report version, Conference version
M. Nickles, A. Pease, A. C. Schalley, and D. Zaefferer. Ontologies across the disciplines. In A. C. Schalley and D. Zaefferer, editors, Ontolinguistics. How Ontological Status Shapes the Linguistic Coding of Concepts. Mouton de Gruyter, 2006.
Info

2005

Thomas Reps, Stefan Schwoon, Somesh Jha, and David Melski. Weighted pushdown systems and their application to interprocedural dataflow analysis. Science of Computer Programming, 58(1–2):206–263, October 2005. Special Issue on the Static Analysis Symposium 2003.
GZipped PostScript (942 kB)
Info
Conference version, Tech report version
Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. Electronic Notes in Theoretical Computer Science, 138(3):153–178, 2005.
GZipped PostScript (76 kB)
PDF (137 kB)
Info
Conference version
G. Weiß, M. Nickles, M. Rovatsos, and F. Fischer. Specifying the intertwining of coordination and autonomy in agent-based systems. International Journal of Network and Computer Applications, Vol.28, 2005.
Info
T. Froehner, M. Nickles, G. Weiß, W. Brauer, and R. Franken. Integration of ontologies and knowledge from autonomous sources. Künstliche Intelligenz, 1/05, 2005.
Info
M. Nickles, M. Rovatsos, and G. Weiß. Expectation-oriented modeling. Engineering Applications of Artificial Intelligence (EAAI), 18, 2005.
Info

2004

Markus Holzer and Stefan Schwoon. Assembling molecules in Atomix is hard. Theoretical Computer Science, 303(3):447–462, February 2004.
Info
Tech report version
J. Esparza. A polynomial-time algorithm for checking consistency of free-choice signal transition graphs. Fundamenta Informaticae, 62(2):197–220, 2004.
GZipped PostScript (129 kB)
PDF (182 kB)
Info
Conference version
Matthias Hopf, Michael Luttenberger, and Thomas Ertl. Hierarchical splatting of scattered 4d data. IEEE Computer Graphics and Applications, 24(04):64–72, 2004.
Info
M. Nickles and M. Rovatsos. Towards a unified model of sociality in multiagent systems. International Journal of Computer and Information Science, 5(2):73–88, 2004.
Info
G. Weiß, J. Duscher, M. Rovatsos, and M. Nickles. Spezifikation von Softwareautonomie. Künstliche Intelligenz (KI), 4/04, 2004.
Info

2003

Javier Esparza, Antonín Kučera, and Stefan Schwoon. Model-checking LTL with regular valuations for pushdown systems. Information and Computation, 186(2):355–376, November 2003.
GZipped PostScript (202 kB)
PDF (214 kB)
Info
Conference version
A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. International Journal on Foundations of Computer Science, 14(4):551–582, 2003.
GZipped PostScript (141 kB)
PDF (371 kB)
Info
Conference version
January 2011: Michal Terepeta and Flemming Nielson have found a mistake in the paper: Lemma 1.2 does not hold as stated. We will try to repair it as soon as possible.
A. Kučera and J. Esparza. A logical viewpoint on process-algebraic quotients. Journal of Logic and Computation, 13(6):863–880, 2003.
GZipped PostScript (98 kB)
PDF (263 kB)
Info
Conference version

2002

J. Esparza and C. Lakos, editors. Applications and theory of petri nets 2002, volume 2360 of Lecture Notes in Computer Science. Springer Verlag, 2002.
Info
See link.springer.de ...
J. Esparza, S. Römer, and W. Vogler. An improvement of McMillan's unfolding algorithm. Formal Methods in System Design, 20:285–310, 2002.
GZipped PostScript (149 kB)
PDF (351 kB)
Info
Conference version
K.F. Lorentzen and M. Nickles. Ordnung aus Chaos - Prolegomena zu einer Luhmann'schen Modellierung deentropisierender Strukturbildung in Multiagentensystemen. In T. Kron, editor, Luhmann modelliert. Ans"atze zur Simulation von Kommunikationssystemen. Leske & Budrich, 2002.
Info

2001

J. Esparza and C. Schröter. Unfolding based algorithms for the reachability problem. Fundamenta Informaticae, 47(3–4):231–245, 2001.
GZipped PostScript (150 kB)
PDF (177 kB)
Info

2000

A. Bouajjani, J. Esparza, A. Finkel, O. Maler, P. Rossmanith, B. Willems, and P. Wolper. An efficient automata approach to some problems on context-free grammars. Information Processing Letters, 74(5–6):221–227, 2000.
GZipped PostScript (84 kB)
PDF (212 kB)
Info
An even more efficient approach can be found in ERS00
J. Esparza and S. Melzer. Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design, 16:159–189, 2000.
GZipped PostScript (133 kB)
PDF (331 kB)
Info

1999

J. Esparza, J.L. Lopez, and J. Sesma. Zeros of the Whittaker function associated to Coulomb waves. IMA Journal of Applied Mathematics, 63(1):71–88, 1999.
Info
P. Jančar, J. Esparza, and F. Moller. Petri nets and regular behaviours. Journal of Computer and System Sciences, 59(3):476–503, 1999.
GZipped PostScript (82 kB)
PDF (285 kB)
Info

1998

J. Esparza. Reachability in live and safe free-choice Petri nets is -complete. Theoretical Computer Science, 198(1–2):211–224, 1998.
GZipped PostScript (66 kB)
PDF (222 kB)
Info

1997

O. Burkart and J. Esparza. More infinite results. Bulletin of the EATCS 62 (Concurrency Column), 1997.
Info
J. Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. Fundamenta Informaticae, 31:13–26, 1997.
GZipped PostScript (69 kB)
PDF (226 kB)
Info
Conference version
J. Esparza. Decidability of model-checking for infinite-state concurrent systems. Acta Informatica, 34:85–107, 1997.
GZipped PostScript (83 kB)
PDF (282 kB)
Info

1996

O. Burkart and J. Esparza. More infinite results. Electronic Notes in Theoretical Computer Science, 6, 1996.
GZipped PostScript (70 kB)
PDF (296 kB)
Info
J. Esparza and G. Bruns. Trapping mutual exclusion in the box calculus. Theoretical Computer Science, 153(1):95–128, 1996.
Info

1995

Jörg Desel and Javier Esparza. Free choice Petri nets, volume 40 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, New York, NY, USA, 1995.
PDF (11 MB)
Info
See www.cambridge.org ...
The copyright of this book lies by Cambridge University Press (CUP). I have got a verbal authorization from CUP to deposit a copy here. I have repeateadly mailed CUP to obtain an official, written permission, so far without answer. Please print only one copy of the book for your personal (noncommercial) use, and do not distribute the file further. The book can be purchased from the publisher in soft-cover. If you are interested, follow the link above.
A. Cheng, J. Esparza, and J. Palsberg. Complexity results for 1-safe nets. Theoretical Computer Science, 147:117–136, 1995.
PDF (182 kB)
Info
J. Desel and J. Esparza. Shortest paths in reachability graphs. Journal of Computer and System Sciences, 51(2):314–323, 1995.
PDF (1 MB)
Info
Allan Cheng, Javier Esparza, and Jens Palsberg. Complexity results for 1-safe nets. Theoretical Computer Science, 147(1&2):117–136, 1995.
PDF (182 kB)
Info

1994

J. Esparza and M. Nielsen. Decibility issues for Petri nets - a survey. Journal of Informatik Processing and Cybernetics, 30(3):143–160, 1994.
GZipped PostScript (59 kB)
PDF (243 kB)
Info
J. Esparza. Reduction and synthesis of live and bounded free choice Petri nets. Information and Computation, 114(1):50–87, 1994.
PDF (3 MB)
Info
J. Esparza. Model checking using net unfoldings. Science of Computer Programming, 23:151–195, 1994.
Info

1993

J. Desel and J. Esparza. Reachability in cyclic extended free-choice systems. Theoretical Computer Science, 114:93–118, 1993.
PDF (2 MB)
Info
Conference version

1992

E. Best, J. Desel, and J. Esparza. Traps characterise home states in free choice systems. Theoretical Computer Science, 101:161–176, 1992.
PDF (1 MB)
Info
Conference version
J. Esparza and M. Silva. A polynomial time algorithm to decide liveness of bounded free choice nets. Theoretical Computer Science, 102:185–205, 1992.
PDF (1 MB)
Info
J. Esparza. A solution to the covering problem for 1-bounded conflict-free petri nets using linear programming. Information Processing Letters, 41:313–319, 1992.
PDF (947 kB)
Info

1991

A. Cruz, J. Esparza, and J. Sesma. Zeros of the hankel function of real order out of the principal riemann sheet. Journal of Computational und Applied Mathematics, 37:89–99, 1991.
Info