Proceedings Publications

• [22] Height-Deterministic Pushdown Automata
  by D. Nowotka and J. Srba.
  In Proceedings of 32nd International Symposium on Mathematical Foundations of Computer Science (MFCS'07), 10 pages, volume of LNCS, Springer-Verlag, 2007.
  To appear.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [21] Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols
  by G. Delzanno, J. Esparza and J. Srba.
  In Proceedings of 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), pages 415-429, volume 4218 of LNCS, Springer-Verlag, 2006.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [20] Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation
  by J. Srba.
  In Proceedings of 15th Annual Conference on Computer Science Logic (CSL'06), pages 89-103, volume 4207 of LNCS, Springer-Verlag, 2006.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [19] Undecidability Results for Bisimilarity on Prefix Rewrite Systems
  by P. Jancar and J. Srba.
  In Proceedings of 9th Foundations of Software Science and Computation Structures (FOSSACS'06), pages 277-291, volume 3921 of LNCS, Springer-Verlag, 2006.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [18] On Counting the Number of Consistent Genotype Assignments for Pedigrees
  by J. Srba.
  In Proceedings of 25th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'05), pages 470-482, volume 3821 of LNCS, Springer-Verlag, 2005.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [17] Timed-Arc Petri Nets vs. Networks of Timed Automata
  by J. Srba.
  In Proceedings of 26th International Conference on Application and Theory of Petri Nets (ICATPN'05), pages 385-402, volume 3536 of LNCS, Springer-Verlag, 2005.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [16] Recursion vs. Replication in Simple Cryptographic Protocols
  by H. Huttel and J. Srba.
  In Proceedings of 31st Annual Conference on Current Trends in Theory and Practice of Informatics (SOFSEM'05), pages 175-184, volume 3381 of LNCS, Springer-Verlag, 2005.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [15] Highly Undecidable Questions for Process Algebras
  by P. Jancar and J. Srba.
  In Proceedings of 3rd IFIP International Conference on Theoretical Computer Science (TCS'04), pages 507-520, Kluwer Academic Publishers, 2004.
  Abstract       BibTex       (Postscript, PDF) © Kluwer
  
  
• [14] Recursive Ping-Pong Protocols
  by H. Huttel and J. Srba.
  In Proceedings of 4th International Workshop on Issues in the Theory of Security (WITS'04), pages 129-140, 2004.
  Abstract       BibTex       (Postscript, PDF) 
  
  
• [13] Completeness Results for Undecidable Bisimilarity Problems
  by J. Srba.
  In Proccedings of the 5th International Workshop on Verification of Infinite-State Systems (INFINITY'03), pages 5-19, volume 98 of ENTCS, Springer-Verlag, 2004.
  Abstract       BibTex       (Postscript, PDF) © Elsevier Science
  
  
• [12] Undecidability of Weak Bisimilarity for PA-Processes
  by J. Srba.
  In Proceedings of 6th International Conference on Developments in Language Theory (DLT'02), pages 197-208, volume 2450 of LNCS, Springer-Verlag, 2003.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [11] Undecidability of Weak Bisimilarity for Pushdown Processes
  by J. Srba.
  In Proceedings of 13th International Conference on Concurrency Theory (CONCUR'02), pages 579-593, volume 2421 of LNCS, Springer-Verlag, 2002.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [10] Strong Bisimilarity and Regularity of Basic Process Algebra is PSPACE-Hard
  by J. Srba.
  In Proceedings of 29th International Colloquium on Automata, Languages and Programming (ICALP'02), pages 716-727, volume 2380 of LNCS, Springer-Verlag, 2002.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [9] Note on the Tableau Technique for Commutative Transition Systems
  by J. Srba.
  In Proceedings of 5th Foundations of Software Science and Computation Structures (FOSSACS'02), pages 387-401, volume 2303 of LNCS, Springer-Verlag, 2002.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [8] Strong Bisimilarity and Regularity of Basic Parallel Processes is PSPACE-Hard
  by J. Srba.
  In Proceedings of 19th International Symposium on Theoretical Aspects of Computer Science (STACS'02), pages 535-546, volume 2285 of LNCS, Springer-Verlag, 2002.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [7] Properties of Distributed Timed-Arc Petri Nets
  by M. Nielsen, V. Sassone and J. Srba.
  In Proceedings of 21st International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'01), pages 280-291, volume 2245 of LNCS, Springer-Verlag, 2001.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [6] On the Power of Labels in Transition Systems
  by J. Srba.
  In Proceedings of 12th International Conference on Concurrency Theory (CONCUR'01), pages 277-291, volume 2154 of LNCS, Springer-Verlag, 2001.
  Abstract       (Postscript, PDF) © Springer-Verlag
  
  
• [5] Towards a Notion of Distributed Time for Petri Nets
  by M. Nielsen, V. Sassone and J. Srba.
  In Proceedings of 22nd International Conference on Application and Theory of Petri Nets (ICATPN'01), pages 23-31, volume 2075 of LNCS, Springer-Verlag, 2001.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [4] Complexity of Weak Bisimilarity and Regularity for BPA and BPP
  by J. Srba.
  In Proceedings of the 7th International Workshop on Expressiveness in Concurrency (EXPRESS'00), volume 39 (1) of ENTCS, Elsevier Science Publishers, 2000.
  See also the journal version.
  Abstract       BibTex       (Postscript, PDF) © Elsevier Science
  
  
• [3] Matching Modulo Associativity and Idempotency is NP-Complete
  by O. Klima and J. Srba.
  In Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science (MFCS'00), pages 456-466, volume 1893 of LNCS, Springer-Verlag, 2000.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [2] Pattern Equations and Equations with Stuttering
  by I. Cerna, O. Klima and J. Srba.
  In Proceedings of 26th Annual Conference on Current Trends in Theory and Practice of Informatics (SOFSEM'99), pages 369-378, volume 1725 of LNCS, Springer-Verlag, 1999.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [1] Deadlocking States in Context-Free Process Algebra
  by J. Srba.
  In Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS'98), pages 388-398, volume 1450 of LNCS, Springer-Verlag, 1998.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  

Journal Publications

• [8] Decidability Issues for Extended Ping-Pong Protocol
  by H. Huttel and J. Srba.
  Journal of Automated Reasoning. Kluwer Academic Publishers, 2005.
  To appear.
  Abstract       BibTex       (Postscript, PDF) © Kluwer
  
  
• [7] Roadmap of Infinite Results
  by J. Srba.
  Current Trends in Theoretical Computer Science, The Challenge of the New Century, Vol 2: Formal Models and Semantics, pages 337-350, World Scientific Publishing Co., 2004.
  Updated version of the EATCS Bulletin contribution. See also this project with an updated on-line version.
  Abstract       BibTex      
  
  
• [6] On the Computational Complexity of Bisimulation, Redux
  by F. Moller, S. Smolka and J. Srba.
  Information and Computation, pages 129-143, volume 192(2), Springer-Verlag, 2004.
  Abstract       BibTex       (Postscript, PDF) © Elsevier Science
  
  
• [5] Roadmap of Infinite Results
  by J. Srba.
  Bulletin of the European Association for Theoretical Computer Science, pages 163-175, volume 78, columns: Concurrency, 2002.
  See also this project with an updated on-line version.
  Abstract       BibTex      
  
  
• [4] Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds
  by J. Srba.
  Acta Informatica, pages 469-499, volume 39, Springer-Verlag, 2003.
  Abstract       BibTex       (Postscript, PDF) © Springer-Verlag
  
  
• [3] Undecidability of Domino Games and Hhp-Bisimilarity
  by M. Jurdzinski, M. Nielsen and J. Srba.
  Information and Computation, pages 343-368, volume 184(2), Springer-Verlag, 2003.
  Abstract       BibTex       (Postscript, PDF) © Elsevier Science
  
  
• [2] Complexity of Weak Bisimilarity and Regularity for BPA and BPP
  by J. Srba.
  Mathematical Structures in Computer Science, pages 567-587, volume 13, Cambridge University Press, 2003.
  Abstract       BibTex       (Postscript, PDF) © Cambridge University Press
  
  
• [1] Basic Process Algebra with Deadlocking States
  by J. Srba.
  Theoretical Computer Science, pages 605-630, volume 266 (1-2), Elsevier Science, 2001.
  Abstract       BibTex       (Postscript, PDF) © Elsevier Science
  
  

Edited Volumes

• Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05)
  by S. Smolka and J. Srba.
  Preliminary proceedings appeared in NS-05-4, BRICS Notes Series, 70 pages, 2005.
  Final version published in ENTCS, volume 149, issue 1, 2006.
  
  

Technical Reports

• [16] Deterministic Context-Free Model Checking
  by J. Esparza, D. Nowotka and J. Srba.
  Technical report of Stuttgart University, 20 pages, 2007.
  Note: the nonregular model-checking algorithm works in fact trivially also for any context-free language.
  
  
• [15] Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols
  by G. Delzanno, J. Esparza and J. Srba.
  Technical report RS-06-14, BRICS Research Series, 31 pages, 2006.
  
  
• [14] Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation
  by J. Srba.
  Technical report RS-06-13, BRICS Research Series, 21 pages, 2006.
  
  
• [13] Undecidability Results for Bisimilarity on Prefix Rewrite Systems
  by P. Jancar and J. Srba.
  Technical report RS-06-7, BRICS Research Series, 20 pages, 2006.
  
  
• [12] On Counting the Number of Consistent Genotype Assignments for Pedigrees
  by J. Srba.
  Technical report RS-05-28, BRICS Research Series, 15 pages, 2005.
  
  
• [11] Recursion vs. Replication in Simple Cryptographic Protocols
  by H. Huttel and J. Srba.
  Technical report RS-04-23, BRICS Research Series, 26 pages, 2004.
  
  
• [10] Highly Undecidable Questions for Process Algebras
  by P. Jancar and J. Srba.
  Technical report RS-04-8, BRICS Research Series, 25 pages, 2004.
  
  
• [9] Recursive Ping-Pong Protocols
  by H. Huttel and J. Srba.
  Technical report RS-03-47, BRICS Research Series, 21 pages, 2004.
  
  
• [8] Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds
  by J. Srba.
  Technical report RS-02-16, BRICS Research Series, 33 pages, 2002.
  
  
• [7] Note on the Tableau Technique for Commutative Transition Systems
  by J. Srba.
  Technical report RS-01-50, BRICS Research Series, 19 pages, 2001.
  
  
• [6] On the Power of Labels in Transition Systems
  by J. Srba.
  Technical report RS-01-19, BRICS Research Series, 22 pages, 2001.
  
  
• [5] Complexity of Weak Bisimilarity and Regularity for BPA and BPP
  by J. Srba.
  Technical report RS-00-16, BRICS Research Series, 20 pages, 2000.
  
  
• [4] Matching Modulo Associativity and Idempotency is NP-Complete
  by O. Klima and J. Srba.
  Technical report RS-00-13, BRICS Research Series, 19 pages, 2000.
  
  
• [3] Complexity Issues of the Pattern Equations in Idempotent Semigroups
  by O. Klima and J. Srba.
  Technical report FIMU-RS-99-02, Faculty of Informatics MU, 14 pages, 1999.
  
  
• [2] On the Pattern Equations
  by I. Cerna, O. Klima and J. Srba.
  Technical report FIMU-RS-99-01, Faculty of Informatics MU, 11 pages, 1999.
  
  
• [1] Comparing the Classes BPA and BPA with Deadlocks
  by J. Srba.
  Technical report FIMU-RS-98-05, Faculty of Informatics MU, 36 pages, 1998.
  
  

Conference Talks

• ATVA'06
  2006, Beijing, China.
  
  
• CSL'06
  2006, Szeged, Hungary.
  
  
• FOSSACS'06
  2006, Vienna, Austria. Participation.
  
  
• FSTTCS'05
  2005, Hyderabad, India.
  
  
• CONCUR'05
  2005, San Francisco, California, USA. Organization of INFINITY'05
  
  
• ICATPN'05
  2005, Miami, Florida, USA.
  
  
• STTI'05
  2005, Prague, Czech Republic.
  
  
• TCS'04
  2004, Toulouse, France.
  
  
• WITS'04
  2004, Barcelona, Spain.
  
  
• INFINITY'03
  2003, Marseille, France.
  
  
• DLT'02
  2002, Kyoto, Japan.
  
  
• INFINITY'02 (short presentation - ps,pdf)
  2002, Brno, Czech Republic.
  
  
• CONCUR'02
  2002, Brno, Czech Republic.
  
  
• ICALP'02
  2002, Malaga, Spain.
  
  
• FOSSACS'02
  2002, Grenoble, France.
  
  
• STACS'02
  2002, Juan les Pins, France.
  
  
• FSTTCS'01
  2001, Bangalore, India.
  
  
• CONCUR'01
  2001, Aalborg, Denmark.
  
  
• EXPRESS'00
  2000, State College, Pennsylvania, USA.
  
  
• MFCS'00
  2000, Bratislava, Slovak Republic.
  
  
• ICALP'99
  1999, Prague, Czech Republic. Participation.
  
  
• SOFSEM'99
  1999, Milovy, Czech Republic.
  
  
• MFCS'98
  1998, Brno, Czech Republic.
  
  

Other Talks

• Verification of Recursive Ping-Pong Protocols
  20. 12. 2006, Faculty of Informatics, Masaryk Univesity, Brno, Czech Republic.
  
  
• Verification Techniques for Visibly Pushdown Automata
  15. 12. 2006, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
  
  
• Verification Techniques for Visibly Pushdown Automata
  29. 11. 2006, BRICS Seminars Series, Aalborg, Denmark.
  
  
• Distributed Timed-Arc Petri Nets
  14. 11. 2002, BRICS Seminars Series, Aalborg, Denmark.
  
  
• Bisimilarity Checking of Simple Process Algebras: Complexity Lower Bounds
  17. 6. 2002, Oberseminar, Freiburg, Germany.
  
  
• Complexity of Bisimilarity Problems for Simple Process Algebras
  14. 2. 2002, BRICS Seminars Series, Aalborg, Denmark.
  
  
• Interleaving and Independence Models in Concurrency (qualifying exam)
  24. 1. 2001, Basic Research in Computer Science, Aarhus, Denmark.
  
  
• Pattern Equations and Equations with Stuttering
  19. 11. 1999, Basic Research in Computer Science, Aarhus, Denmark.
  
  
• Process Theory of Commutative Context-Free Grammars
  24. 3. 1999, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
  
  
• Applications of Semigroups in Basic Parallel Processes
  19. 11. 1998, Faculty of Science, Dept. of Mathematics, Masaryk University, Brno, Czech Republic.
  
  
• Context-Free Process Algebras Extended with Deadlocks
  5. 3. 1998, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
  
  

Grant Participation

• 2005-:Institute for Theoretical Computer Science
  Project No. 1M0545.
  
  
• 2003-2005: Verification of Infinite-state Systems
  Grant Agency of Czech Republic, Project No. 201/03/1161.
  
  
• 2000-2003: Infinite-State Concurrent Systems - Models and Verification
  Grant Agency of Czech Republic, Project No. 201/00/0400.
  
  
• 1997-2000: Algorithmic Verification Boundaries for Infinite-State Systems
  Grant Agency of Czech Republic, Project No. 201/97/0456.
  
  
• 1999: Verification of Infinite-State Concurrent Processes
  Fund for Development of Universities, FRVS - 0409/1999.
  
  

Dissertation Theses

• Decidability and Complexity Issues for Infinite-State Processes
  by J. Srba.
  BRICS, Department of Computer Science, University of Aarhus, Denmark. 171 pages, 2003.
  Supervisor: Mogens Nielsen, Examiners: Petr Jancar and Colin Stirling.
  (Postscript, PDF) 
  
  
• Selected Techniques for Verification of Infinite-State Systems
  by J. Srba.
  Faculty of Informatics, Masaryk University, Czech Republic. 124 pages, 2005.
  Supervisor: Mojmir Kretinsky, Examiners: Milan Ceska and Antonin Kucera.
  (Postscript, PDF) 
  
  

Master Thesis

• Context-Free Process Algebras Extended with Deadlocks
  by J. Srba.
  Faculty of Informatics, Masaryk University, Brno, Czech Republic. 42 pages, 1998.
  Examiners: Ivana Cerna (supervisor) and Antonin Kucera.
  (Postscript, PDF)