Conference Proceedings

  1. Mohan Dantam, Richard Mayr. Approximating the Value of Energy-Parity Objectives in Simple Stochastic Games. MFCS 2023, LIPIcs, Vol. 272. 2023. ArXiv (full version) and Local copy (full version). LIPIcs (without appendix)..

  2. Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke. Transience in Countable MDPs. CONCUR 2021, LIPIcs, Vol. 203. 2021. ArXiv (full version) and Local copy (full version). LIPIcs (without appendix)..

  3. Richard Mayr, Eric Munday. Strategy Complexity of Mean Payoff, Total Payoff and Point Payoff Objectives in Countable MDPs. CONCUR 2021, LIPIcs, Vol. 203. 2021. ArXiv (full version) and Local copy (full version). LIPIcs (without appendix)..

  4. Richard Mayr, Sven Schewe, Patrick Totzke, Dominik Wojtczak. Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP. FOSSACS 2021, LNCS volume 12650. 2021. ArXiv (full version) and Local copy (full version).

  5. Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke. Strategy Complexity of Parity Objectives in Countable MDPs. CONCUR 2020, LIPIcs, Vol. 171. 2020. ArXiv (full version) and Local copy (full version) and LIPIcs proceedings (without appendix).

  6. Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke, Dominik Wojtczak. How to Play in Infinite MDPs. ICALP 2020, LIPIcs, Vol. 168. Saarbrücken. 2020. LIPIcs proceedings and Local copy.

  7. Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke. Büchi Objectives in Countable MDPs. ICALP 2019, LIPIcs, Vol. 132. Athens, Greece. 2019. ArXiv (full version) and Local copy (full version) and LIPIcs proceedings (without appendix).

  8. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, Patrick Totzke. Universal Safety for Timed Petri Nets is PSPACE-complete. CONCUR 2018, LIPIcs (DOI: 10.4230/LIPIcs.CONCUR.2018.6). Beijing, China. 2018. LIPICS proceedings (without appendix), ArXiv (full version) and Local copy (full version).

  9. Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Dominik Wojtczak. On Strong Determinacy of Countable Stochastic Games. LICS 2017, IEEE. Reykjavik, Iceland. 2017. ArXiv and Local copy.

  10. Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Dominik Wojtczak. Parity Objectives in Countable MDPs. LICS 2017, IEEE. Reykjavik, Iceland. 2017. ArXiv and Local copy.

  11. Richard Mayr, Sven Schewe, Patrick Totzke, Dominik Wojtczak. MDPs with Energy-Parity Objectives. LICS 2017, IEEE. Reykjavik, Iceland. 2017. ArXiv.

  12. Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, James Worrell. Model Checking Flat Freeze LTL on One-Counter Automata. CONCUR 2016, LIPIcs. Québec, Canada. 2016. ArXiv, and Local copy.

  13. Parosh Aziz Abdulla, Radu Ciobanu, Richard Mayr, Arnaud Sangnier, Jeremy Sproston. Qualitative Analysis of VASS-Induced MDPs. FOSSACS 2016, LNCS 9634. Eindhoven, The Netherlands. 2016. ArXiv, and Local copy.

  14. Ricardo Almeida, Lukas Holik, Richard Mayr. Reduction of Nondeterministic Tree Automata. TACAS 2016, LNCS 9636. Eindhoven, The Netherlands. 2016. ArXiv, and Local copy.

  15. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofmann, K. Narayan Kumar, Richard Mayr, Patrick Totzke. Infinite-State Energy Games. Proc. of CSL-LICS 2014. Vienna, Austria. 2014. Link.

  16. Piotr Hofmann, Slawomir Lasota, Richard Mayr, Patrick Totzke. Simulation over One-Counter Nets is PSPACE-complete. Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). IIT Guwahati, India. 2013. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik 2013 LIPIcs ISBN 978-3-939897-64-4.

  17. Richard Mayr and Patrick Totzke. Branching-Time Model Checking Gap-Order Constraint Systems. The 7th International Workshop on Reachability Problems. RP 2013. Uppsala, Sweden. Volume 8169 in LNCS. 2013. (See also arxiv).

  18. Parosh Aziz Abdulla, Richard Mayr, Arnaud Sangnier, Jeremy Sproston. Solving Parity Games on Integer Vectors. 24th International Conference on Concurrency Theory (CONCUR 2013). Buenos Aires, Argentina. Volume 8052 in LNCS. 2013. Full version: University of Edinburgh Technical Report EDI-INF-RR-1417 . (See also arXiv and Local copy.)

  19. Parosh Aziz Abdulla, Lorenzo Clemente, Richard Mayr, Sven Sandberg. Stochastic Parity Games on Lossy Channel Systems. 10th International Conference on Quantitative Evaluation of SysTems (QEST 2013). Buenos Aires, Argentina. Volume 8054 in LNCS. 2013. Full version: University of Edinburgh Technical Report EDI-INF-RR-1416 . (See also arXiv and Local copy.)

  20. Piotr Hofman, Richard Mayr and Patrick Totzke. Decidability of Weak Simulation on One-counter Nets. 28th Annual IEEE Symposium on Logic in Computer Science (LICS 2013). New Orleans, USA. 2013. Full version: University of Edinburgh Technical Report EDI-INF-RR-1415 . (See also arXiv and Local copy.)

  21. Lorenzo Clemente and Richard Mayr. Advanced Automata Minimization. POPL 2013: 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Rome, Italy. Jan. 2013. Full version: University of Edinburgh Technical Report EDI-INF-RR-1414 . (See also arXiv and Local copy.) The LMCS journal version is significantly extended and much better.

  22. Parosh Aziz Abdulla and Richard Mayr. Petri Nets with Time and Cost. Infinity 2012. EPTCS volume 107, pages 9-24. 2012. Link to the paper.

  23. Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukas Holik, Chih-Duo Hong, Richard Mayr, Tomas Vojnar. Advanced Ramsey-based Buchi Automata Inclusion Testing . Proc. of CONCUR 2011, 22nd International Conference on Concurrency Theory. Aachen, Germany. Volume 6901 in LNCS. 2011.

  24. Parosh Aziz Abdulla and Richard Mayr. Computing Optimal Coverability Costs in Priced Timed Petri Nets . 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011). Toronto, Canada. 2011. arXiv.org .

  25. Lorenzo Clemente and Richard Mayr. Multipebble Simulations for Alternating Automata . Proc. of CONCUR 2010, 21st International Conference on Concurrency Theory. Paris, France. Volume 6269 in LNCS. 2010. (This is the long version with the appendix, i.e., University of Edinburgh Technical Report EDI-INF-RR-1376. )

  26. Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukas Holik, Chih Duo Hong, Richard Mayr and Tomas Vojnar. Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing. Proc. of CAV 2010. 22nd International Conference on Computer Aided Verification. Edinburgh, UK. Volume 6174 in LNCS. 2010.

  27. Parosh Aziz Abdulla, Yu-Fang Chen, Lukas Holik, Richard Mayr and Tomas Vojnar. When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata). Proc. of TACAS 2010, Sixteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Paphos, Cyprus. Volume 6015 in LNCS. 2010. (EATCS Best Theory Paper Award, 2010.)

  28. Stefan Göller, Richard Mayr and Anthony Widjaja To. On the Computational Complexity of Verifying One-Counter Processes. 24th Annual IEEE Symposium on Logic in Computer Science (LICS 2009). Los Angeles, USA. IEEE. 2009.

  29. Parosh Aziz Abdulla and Richard Mayr. Minimal Cost Reachability/Coverability in Priced Timed Petri Nets. Proc. FOSSACS 2009, 12th International Conference on Foundations of Software Science and Computation Structures. York, UK. Volume 5504 in LNCS. 2009.

  30. Parosh Aziz Abdulla, Noomene Ben Henda, Luca de Alfaro, Richard Mayr, and Sven Sandberg. Stochastic Games with Lossy Channels. Proc. FOSSACS 2008, 11th International Conference on Foundations of Software Science and Computation Structures. Budapest, Hungary. Volume 4962 in LNCS. 2008. (Here is the technical report with the full proofs.)

  31. Parosh Abdulla, Noomene Ben Henda, Richard Mayr and Sven Sandberg. Eager Markov Chains. Fourth international symposium on Automated Technology for Verification and Analysis (ATVA 2006). Beijing, China. Volume 4218 in LNCS. 2006.

  32. Parosh Abdulla, Noomene Ben Henda, Richard Mayr and Sven Sandberg. Limiting Behavior of Markov Chains with Eager Attractors. 3rd International Conference on the Quantitative Evaluation of SysTems (QEST) 2006. University of California, Riverside, USA. IEEE. 2006.

  33. Parosh Abdulla, Noomene Ben Henda and Richard Mayr. Verifying Infinite Markov Chains with a Finite Attractor or the Global Coarseness Property. Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005). Chicago, USA. IEEE. 2005.

  34. Javier Esparza, Antonin Kucera and Richard Mayr. Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances. Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005). Chicago, USA. IEEE. 2005.

  35. Parosh Abdulla, Pritha Mahata and Richard Mayr. Decidability of Zenoness, Syntactic Boundedness and Token-Liveness for Dense-Timed Petri Nets. 24th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Chennai, India. Volume 3328 in LNCS. 2004. (Here is the complete version with the appendix containing the proofs.)

  36. Javier Esparza, Antonin Kucera and Richard Mayr. Model Checking Probabilistic Pushdown Automata. Nineteenth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2004). Turku, Finland. IEEE. 2004. (The journal version has appeared in LMCS.)

  37. Antonin Kucera and Richard Mayr. A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata. In proceedings of the 3rd IFIP International Conference on Theoretical Computer Science (IFIP TCS 2004, Toulouse, France), pages 395-408, Kluwer, 2004. (There is also a technical report with an extended version.)

  38. Stefan Leue, Richard Mayr, Wei Wei. A Scalable Incomplete Test for the Boundedness of UML RT Models. Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004). Barcelona, Spain. Volume 2988 in LNCS. 2004.

  39. Stefan Leue, Richard Mayr, Wei Wei. A Scalable Incomplete Test for Message Buffer Overflow in Promela Models. 11th International SPIN Workshop on Model Checking of Software (SPIN 2004). Barcelona, Spain. Volume 2989 in LNCS. 2004.

  40. Richard Mayr. Undecidability of Weak Bisimulation Equivalence for 1-Counter Processes. 30th International Colloquium on Automata, Languages and Programming (ICALP 2003), Eindhoven, The Netherlands. Volume 2719 in LNCS. 2003.

  41. Richard Mayr. Weak Bisimilarity and Regularity of Context-free Processes is EXPTIME-hard. EXPRESS'03, 10th International Workshop on Expressiveness in Concurrency, Marseille, France. 2003. Electronic Notes in Theoretical Computer Science (ENTCS), volume 96. (An extended journal version has appeared in TCS.)

  42. Antonin Kucera and Richard Mayr. Why is Simulation Harder Than Bisimulation? 13th International Conference on Concurrency Theory (CONCUR 2002), Brno, Czech Republic. Volume 2421 in LNCS. 2002. (There is also a technical report with an extended version.)

  43. Antonin Kucera and Richard Mayr. On the Complexity of Semantic Equivalences for Pushdown Automata and BPA. 27th International Symposium on Mathematical Foundations of Computer Science (MFCS 2002), Warszawa - Otwock, Poland. Volume 2420 in LNCS. 2002. (There is also a technical report with the complete proofs.)

  44. Ahmed Bouajjani and Peter Habermehl and Richard Mayr. Automatic Verification of Recursive Procedures with one Integer Parameter. 26th International Symposium on Mathematical Foundations of Computer Science (MFCS 2001), Marianske Lazne, Czech Republic. Volume 2136 in LNCS. 2001. ( Abstract in English and French.) ( Journal version has appeared in TCS (volume 295).)

  45. Richard Mayr. On the Complexity of Bisimulation Problems for Pushdown Automata. IFIP International Conference on Theoretical Computer Science (IFIP TCS'2000), Sendai, Japan. Volume 1872 in LNCS. 2000.

  46. Richard Mayr. On the Complexity of Bisimulation Problems for Basic Parallel Processes. International Colloquium on Automata, Languages and Programming (ICALP'2000), Geneva, Switzerland. Volume 1853 in LNCS. 2000.

  47. Richard Mayr. Undecidable Problems in Unreliable Computations. International Symposium on Latin American Theoretical Informatics (LATIN'2000), Punta del Este, Uruguay. Volume 1776 in LNCS. 2000. (A longer journal version has appeared in TCS.)

  48. Antonin Kucera and Richard Mayr. Weak Bisimilarity with Infinite-State Systems can be Decided in Polynomial Time. International Conference on Concurrency Theory (CONCUR'99), Eindhoven, The Netherlands. Volume 1664 in LNCS. 1999. (The journal version has appeared in TCS.)

  49. Javier Esparza, Alain Finkel, Richard Mayr. On the Verification of Broadcast Protocols. 14th IEEE Symposium on Logic in Computer Science (LICS'99). Trento, Italy. IEEE. 1999.

  50. Antonin Kucera and Richard Mayr. Simulation Preorder on Simple Process Algebras. International Colloquium on Automata, Languages and Programming (ICALP'99), Prague, Czech Republic. Volume 1644 in LNCS. 1999. (The journal version has appeared in Information and Computation.)

  51. Ahmed Bouajjani and Richard Mayr. Model Checking Lossy Vector Addition Systems. Symposium on Theoretical Aspects of Computer Science (STACS'99), Trier, Germany. Volume 1563 in LNCS, pages 323-333. 1999. (There is also an inofficial extended version. If this topic interests you then you should also read the following related paper. (which has appeared in TCS))

  52. Richard Mayr. Strict Lower Bounds for Model Checking BPA. In MFCS'98 Workshop on Concurrency - Algorithms and Tools, Tech. Report FIMU-RS-98-06, Masaryk University, Brno, Czech Republic, pages 141--148, 1998. (There is an extended version in ENTCS.)

  53. Petr Jancar, Antonin Kucera, Richard Mayr. Deciding Bisimulation-Like Equivalences with Finite-State Processes. International Colloquium on Automata, Languages and Programming (ICALP'98), Aalborg, Denmark. Volume 1443 in LNCS, pages 200-211, 1998. (There is also a journal version in TCS with the complete proofs.)

  54. Richard Mayr. Combining Petri Nets and PA-Processes. Theoretical Aspects of Computer Software (TACS'97), Sendai, Japan. Volume 1281 in LNCS, pages 547-561, 1997.

  55. Richard Mayr. Model Checking PA-Processes. Conference on Concurrency Theory (CONCUR'97), Warsaw, Poland. Volume 1243 in LNCS, pages 332-346, 1997. (The journal version is better. Richard Mayr. Decidability of Model Checking with the Temporal Logic EF. TCS, volume 256, pages 31-62, 2001.)

  56. Richard Mayr. Tableau Methods for PA-Processes. Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'97), Pont-a-Mousson, France. Volume 1227 in LNAI, pages 276-290. 1997.

  57. Richard Mayr. Weak Bisimulation and Model Checking for Basic Parallel Processes. Proc. of FST&TCS'96, Hyderabad, India. Number 1180 in LNCS, pages 88-99. 1996. (This is an old paper. If you are interested in the model-checking part of it then read the chapter on BPP in my PhD thesis. If you are interested in the bisimulation part of it then read the following journal paper (TCS, volume 258, pages 409--433) which contains much more general results.)

  58. Richard Mayr. Semantic reachability for simple process algebras. In B. Steffen and T. Margaria, editors, Proceedings of INFINITY'96, Pisa, Italy. Number MIP-9614 in Technical report series of the University of Passau. 1996.

Journals

  1. Richard Mayr and Eric Munday. Strategy Complexity of Point Payoff, Mean Payoff and Total Payoff Objectives in Countable MDPs.. Logical Methods in Computer Science 19(1). 2023.

  2. Lorenzo Clemente and Richard Mayr. Efficient reduction of nondeterministic automata with application to language inclusion testing. Logical Methods in Computer Science 15(1). 2019. ( Local copy available.)

  3. Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, James Worrell. Model Checking Flat Freeze LTL on One-Counter Automata. Logical Methods in Computer Science 14(4). 2018. ( Local copy available.)

  4. Antonin Kucera and Richard Mayr. A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata. Journal of Computer and System Sciences. 91: 82-103 (2018).

  5. Piotr Hofman, Slawomir Lasota, Richard Mayr and Patrick Totzke. Simulation Problems Over One-Counter Nets. Logical Methods in Computer Science. Volume 12, Issue 1, Paper 6. 2016. ( Local copy available.)

  6. Richard Mayr and Patrick Totzke. Branching-Time Model Checking Gap-Order Constraint Systems. Fundamenta Informaticae 143, 339-353. 2016.

  7. Parosh Aziz Abdulla, Lorenzo Clemente, Richard Mayr and Sven Sandberg. Stochastic Parity Games on Lossy Channel Systems. Logical Methods in Computer Science. Volume 10, Issue 4, Paper 21. 2014. ( Local copy available.)

  8. Parosh Aziz Abdulla and Richard Mayr. Priced Timed Petri Nets. Logical Methods in Computer Science. Volume 9, Issue 4, Paper 10. 2013. ( Local copy available.)

  9. Antonin Kucera and Richard Mayr. On the Complexity of Checking Semantic Equivalences between Pushdown Processes and Finite-state Processes. Information and Computation. 208(7):772-796, 2010.

  10. S.Heber, R.Mayr, J.Stoye. Common Intervals of Multiple Permutations. Algorithmica 60(2):175-206. 2011. ISSN 0178-4617 (Print), 1432-0541 (Online), DOI 10.1007/s00453-009-9332-1. Local copy , Link .

  11. Parosh Abdulla, Noomene Ben Henda, Richard Mayr. Decisive Markov Chains. Logical Methods in Computer Science. Volume 3, Issue 4, Paper 7. 2007.

  12. Parosh Abdulla, Pritha Mahata, Richard Mayr. Dense-Timed Petri Nets: Checking Zenoness, Token Liveness and Boundedness. Logical Methods in Computer Science. Volume 3, Issue 1, Paper 1. 2007.

  13. Javier Esparza, Antonin Kucera, Richard Mayr. Model Checking Probabilistic Pushdown Automata. Logical Methods in Computer Science. Volume 2, Issue 1, Paper 2. 2006.

  14. Richard Mayr. Weak Bisimilarity and Regularity of Context-free Processes is EXPTIME-hard. TCS, volume 330, pages 553-575, 2005.

  15. Ahmed Bouajjani, Peter Habermehl and Richard Mayr. Automatic Verification of Recursive Procedures with one Integer Parameter. TCS, volume 295/1-3, pages 85-106, 2003.

  16. Antonin Kucera and Richard Mayr. Simulation Preorder over Simple Process Algebras. Information and Computation, 173(2):184-198, 2002.

  17. Richard Mayr. Undecidable Problems in Unreliable Computations. TCS 1-3(297):337-354, 2003.

  18. Antonin Kucera and Richard Mayr. Weak Bisimilarity between Finite-State Systems and BPA or Normed BPP is Decidable in Polynomial Time. TCS, volume 270, pages 677-700, 2001.

  19. Petr Jancar, Antonin Kucera, Richard Mayr. Deciding Bisimulation-Like Equivalences with Finite-State Processes. TCS, volume 258, pages 409-433, 2001.

  20. Richard Mayr. Decidability of Model Checking with the Temporal Logic EF. TCS, volume 256, pages 31-62, 2001.

  21. Richard Mayr. Process Rewrite Systems. Information and Computation. Volume 156. Number 1. Pages 264-286. 2000. Postscript-file. , PDF-file. (There is also a paper in INFINITY'98 about a related topic: Richard Mayr and Michael Rusinowitch. Reachability is decidable for ground AC rewrite systems. )

  22. Richard Mayr and Tobias Nipkow. Higher-Order Rewrite Systems and their Confluence. TCS, volume 192, pages 3-29, 1998.

  23. Richard Mayr. Weak Bisimilarity and Regularity of Context-free Processes is EXPTIME-hard. Electronic Notes in Theoretical Computer Science (ENTCS), volume 96. Proceedings of the Workshop "Expressiveness in Concurrency" (EXPRESS 2003), Barcelona, Spain, 2003.

  24. Richard Mayr. Strict Lower Bounds for Model Checking BPA. Electronic Notes in Theoretical Computer Science (ENTCS), volume 18. Extended version of a paper in the MFCS'98 Workshop on Concurrency - Algorithms and Tools, Masaryk University, Brno, Czech Republic, 1998.

  25. Richard Mayr. Process Rewrite Systems. Electronic Notes in Theoretical Computer Science (ENTCS), volume 7. Proceedings of the Workshop "Expressiveness in Concurrency" (EXPRESS'97), Santa Margherita Ligure, Italy, 1997.

  26. Richard Mayr. Semantic reachability. Electronic Notes in Theoretical Computer Science (ENTCS), volume 5. Extended version of the proceedings of the Workshop on the Verification of Infinite State Systems (INFINITY'96), Pisa, Italy, 1996.