Conference Proceedings

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofmann, K. Narayan Kumar, Richard Mayr, Patrick Totzke.
InfiniteState Energy Games.
Proc. of CSLLICS 2014. Vienna, Austria. 2014.
Link.

Piotr Hofmann, Slawomir Lasota, Richard Mayr, Patrick Totzke.
Simulation over OneCounter Nets is PSPACEcomplete.
Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013).
IIT Guwahati, India. 2013. Schloss Dagstuhl  LeibnizZentrum fuer Informatik 2013 LIPIcs ISBN 9783939897644.

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

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 EDIINFRR1417
.
(See also arXiv
and Local copy.)

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 EDIINFRR1416
.
(See also arXiv
and Local copy.)

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

Lorenzo Clemente and Richard Mayr. Advanced Automata Minimization. POPL 2013:
40th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages.
Rome, Italy. Jan. 2013.
Full version: University of Edinburgh Technical Report EDIINFRR1414
.
(See also arXiv
and Local copy.)

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

Parosh Aziz Abdulla, YuFang Chen, Lorenzo Clemente,
Lukas Holik, ChihDuo Hong, Richard Mayr, Tomas Vojnar.
Advanced Ramseybased Buchi Automata Inclusion Testing
.
Proc. of CONCUR 2011, 22nd International Conference on Concurrency Theory.
Aachen, Germany. Volume 6901 in LNCS. 2011.

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 .

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 EDIINFRR1376.
)

Parosh Aziz Abdulla, YuFang Chen, Lorenzo Clemente, Lukas Holik, Chih Duo Hong, Richard Mayr and
Tomas Vojnar.
Simulation Subsumption in Ramseybased 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.

Parosh Aziz Abdulla, YuFang 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.)

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

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.

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.)

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.

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.

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.

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.

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

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.)

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

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. Springer Verlag. 2004.

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. Springer Verlag. 2004.

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

Richard Mayr.
Weak Bisimilarity and Regularity of
Contextfree Processes is EXPTIMEhard.
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.)

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. Springer Verlag. 2002.
(There is also a
technical report with an extended version.)

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. Springer Verlag. 2002.
(There is also a
technical report with the complete proofs.)

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. Springer Verlag. 2001.
(
Abstract in English and French.)
(
Journal version has appeared in TCS (volume 295).)

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. Springer Verlag. 2000.

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. Springer Verlag. 2000.

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

Antonin Kucera and Richard Mayr.
Weak Bisimilarity with InfiniteState 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.)

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.

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.)

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 323333. 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))

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

Petr Jancar, Antonin Kucera, Richard Mayr.
Deciding BisimulationLike Equivalences with FiniteState Processes.
International Colloquium on Automata, Languages and Programming (ICALP'98),
Aalborg, Denmark. Volume 1443 in LNCS, pages 200211, 1998.
(There is also a
journal version in TCS
with the complete proofs.)

Richard Mayr.
Combining Petri Nets and PAProcesses.
Theoretical Aspects of Computer Software (TACS'97), Sendai, Japan.
Volume 1281 in
LNCS, pages 547561, 1997.

Richard Mayr.
Model Checking PAProcesses.
Conference on Concurrency Theory (CONCUR'97), Warsaw, Poland. Volume 1243 in
LNCS, pages 332346, 1997.
(The journal version is better.
Richard Mayr.
Decidability of Model Checking with the Temporal Logic EF.
TCS, volume 256, pages 3162, 2001.)

Richard Mayr.
Tableau Methods for PAProcesses.
Conference on Automated Reasoning with Analytic Tableaux and
Related Methods (TABLEAUX'97), PontaMousson, France.
Volume 1227 in LNAI, pages 276290. Springer
Verlag, 1997.

Richard Mayr.
Weak Bisimulation and Model Checking for Basic Parallel Processes.
Proc. of FST&TCS'96, Hyderabad, India.
Number 1180 in LNCS, pages 8899. Springer Verlag, 1996.
(This is an old paper. If you are interested in the modelchecking
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 409433)
which contains much more general results.)

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

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.)

Antonin Kucera and Richard Mayr.
On the Complexity of Checking Semantic Equivalences between Pushdown Processes and Finitestate Processes.
Information and Computation. 208(7):772796, 2010.

S.Heber, R.Mayr, J.Stoye. Common Intervals of Multiple Permutations.
Algorithmica 60(2):175206. 2011.
ISSN 01784617 (Print), 14320541 (Online),
DOI 10.1007/s0045300993321.
Local copy ,
Link .

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

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

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

Richard Mayr.
Weak Bisimilarity and Regularity of
Contextfree Processes is EXPTIMEhard.
TCS, volume 330, pages 553575, 2005.

Ahmed Bouajjani, Peter Habermehl and Richard Mayr.
Automatic Verification of Recursive Procedures with one Integer Parameter.
TCS, volume 295/13, pages 85106, 2003.

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

Richard Mayr.
Undecidable Problems in Unreliable Computations.
TCS 13(297):337354, 2003.

Antonin Kucera and Richard Mayr.
Weak Bisimilarity between FiniteState Systems and BPA or Normed BPP
is Decidable in Polynomial Time.
TCS, volume 270, pages 677700, 2001.

Petr Jancar, Antonin Kucera, Richard Mayr.
Deciding BisimulationLike Equivalences with FiniteState Processes.
TCS, volume 258, pages 409433, 2001.

Richard Mayr.
Decidability of Model Checking with the Temporal Logic EF.
TCS, volume 256, pages 3162, 2001.

Richard Mayr.
Process Rewrite Systems. Information and Computation.
Volume 156. Number 1. Pages 264286. 2000.
Postscriptfile. ,
PDFfile.
(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. )

Richard Mayr and Tobias Nipkow.
HigherOrder Rewrite Systems and their
Confluence. TCS, volume 192, pages 329, 1998.

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

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.

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.

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.