To appear |
|
M. Luttenberger and M. Schlund. Convergence of Newton's Method over Commutative Semirings. Information and Computation, ?(?):??–??, To appear. |
|
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. |
|
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. |
|
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. |
|
|
Stefan Kiefer, Ines Marusic, and James Worrell. Minimisation of multiplicity tree automata. Logical Methods in Computer Science (LMCS), 13(1), 2017. |
|
2016 |
|
Eike Best and Javier Esparza. Existence of home states in petri nets is decidable. Inf. Process. Lett., 116(6):423–427, 2016. |
|
|
Jérôme Leroux Javier Esparza, Pierre Ganty and Rupak Majumdar. Verification of population protocols. Acta Informatica, 2016. To appear. |
|
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. |
|
2015 |
|
Salomon Sickert. Converting linear temporal logic to deterministic (generalized) rabin automata. Archive of Formal Proofs, September 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. |
|
|
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. |
|
|
Javier Esparza, Jan Kretinsky, and Salomon Sickert. From ltl to deterministic automata–a safraless compositional approach. Submitted, 2015. |
|
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. |
|
|
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. |
|
|
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. |
|
|
Rene Neumann. Promela formalization. Archive of Formal Proofs, May 2014. Formal proof development. |
|
|
Javier Esparza and Philipp Hoffmann. Negotiation games. CoRR, abs/1405.6820, 2014. |
|
2013 |
|
Corneliu Popeea and Wei-Ngan Chin. Dual analysis for proving safety and finding bugs. Sci. Comput. Program., 78(4):390–411, April 2013. |
|
|
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. |
|
|
Stefan Kiefer. BPA bisimilarity is EXPTIME-hard. Information Processing Letters (IPL), 113(4):101–106, 2013. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
|
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. |
|
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. |
|
|
Javier Esparza, Orna Kupferman, and Moshe Vardi. Verification. In Hanbook on Automata Theory. European Mathematical Society, 2012. To appear. |
|
|
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. |
|
|
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. |
|
|
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. |
|
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. |
|
|
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Derivation tree analysis for accelerated fixed-point computation. Theoretical Computer Science, 412(28):3226–3241, 2011. |
|
|
Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Proving program termination. Commun. ACM, 54(5):88–98, 2011. |
|
|
J. Esparza, M. Leucker, and M. Schlund. Learning workflow Petri nets. Fundamenta Informaticae, 113(3-4):205–228, 2011. |
|
2010 |
|
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Newtonian program analysis. Journal of the ACM, 57(6):33:1–33:47, October 2010. |
|
|
Rene Neumann. Functional binomial queues. Archive of Formal Proofs, October 2010. Formal proof development. |
|
|
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. |
|
|
Andrey Rybalchenko and Viorica Sofronie-Stokkermans. Constraint solving for interpolation. J. Symb. Comput., 45(11):1212–1233, 2010. |
|
|
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. |
|
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. |
|
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. |
|
|
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. |
|
|
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. |
|
|
Javier Esparza, Pradeep Kanade, and Stefan Schwoon. A negative result on depth-first unfoldings. Software Tools for Technology Transfer, 10(2):161–166, 2008. |
|
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. |
|
|
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. |
|
|
M. Nickles. Social acquisition of ontologies from communication processes. Journal of Applied Ontology, special issue "Formal Ontologies for Communicating Agents", 2007. |
|
|
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. |
|
2006 |
|
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Logical Methods in Computer Science, 2006. |
|
|
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. |
|
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. |
|
|
Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. Electronic Notes in Theoretical Computer Science, 138(3):153–178, 2005. |
|
|
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. |
|
|
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. |
|
|
M. Nickles, M. Rovatsos, and G. Weiß. Expectation-oriented modeling. Engineering Applications of Artificial Intelligence (EAAI), 18, 2005. |
|
2004 |
|
Markus Holzer and Stefan Schwoon. Assembling molecules in Atomix is hard. Theoretical Computer Science, 303(3):447–462, February 2004. |
|
|
J. Esparza. A polynomial-time algorithm for checking consistency of free-choice signal transition graphs. Fundamenta Informaticae, 62(2):197–220, 2004. |
|
|
Matthias Hopf, Michael Luttenberger, and Thomas Ertl. Hierarchical splatting of scattered 4d data. IEEE Computer Graphics and Applications, 24(04):64–72, 2004. |
|
|
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. |
|
|
G. Weiß, J. Duscher, M. Rovatsos, and M. Nickles. Spezifikation von Softwareautonomie. Künstliche Intelligenz (KI), 4/04, 2004. |
|
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. |
|
|
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. |
|
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. |
|
|
J. Esparza, S. Römer, and W. Vogler. An improvement of McMillan's unfolding algorithm. Formal Methods in System Design, 20:285–310, 2002. |
|
|
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. |
|
2001 |
|
J. Esparza and C. Schröter. Unfolding based algorithms for the reachability problem. Fundamenta Informaticae, 47(3–4):231–245, 2001. |
|
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. |
|
|
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. |
|
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. |
|
|
P. Jančar, J. Esparza, and F. Moller. Petri nets and regular behaviours. Journal of Computer and System Sciences, 59(3):476–503, 1999. |
|
1998 |
J. Esparza. Reachability in live and safe free-choice Petri nets is  -complete. Theoretical Computer Science, 198(1–2):211–224, 1998. |
|
1997 |
|
O. Burkart and J. Esparza. More infinite results. Bulletin of the EATCS 62 (Concurrency Column), 1997. |
|
|
J. Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. Fundamenta Informaticae, 31:13–26, 1997. |
|
|
J. Esparza. Decidability of model-checking for infinite-state concurrent systems. Acta Informatica, 34:85–107, 1997. |
|
1996 |
|
O. Burkart and J. Esparza. More infinite results. Electronic Notes in Theoretical Computer Science, 6, 1996. |
|
|
J. Esparza and G. Bruns. Trapping mutual exclusion in the box calculus. Theoretical Computer Science, 153(1):95–128, 1996. |
|
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. |
|
|
J. Desel and J. Esparza. Shortest paths in reachability graphs. Journal of Computer and System Sciences, 51(2):314–323, 1995. |
|
|
Allan Cheng, Javier Esparza, and Jens Palsberg. Complexity results for 1-safe nets. Theoretical Computer Science, 147(1&2):117–136, 1995. |
|
1994 |
|
J. Esparza and M. Nielsen. Decibility issues for Petri nets - a survey. Journal of Informatik Processing and Cybernetics, 30(3):143–160, 1994. |
|
|
J. Esparza. Reduction and synthesis of live and bounded free choice Petri nets. Information and Computation, 114(1):50–87, 1994. |
|
|
J. Esparza. Model checking using net unfoldings. Science of Computer Programming, 23:151–195, 1994. |
|
1993 |
|
J. Desel and J. Esparza. Reachability in cyclic extended free-choice systems. Theoretical Computer Science, 114:93–118, 1993. |
|
1992 |
|
E. Best, J. Desel, and J. Esparza. Traps characterise home states in free choice systems. Theoretical Computer Science, 101:161–176, 1992. |
|
|
J. Esparza and M. Silva. A polynomial time algorithm to decide liveness of bounded free choice nets. Theoretical Computer Science, 102:185–205, 1992. |
|
|
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. |
|
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. |
|
Contact
