Jan Strejcek - Publications

[ Journal papers | Proceedings papers | Technical reports & unreviewed papers | Thesis ]
Journal papers
  1. T. Babiak, V. Rehak, and J. Strejcek: Almost Linear Büchi Automata, Mathematical Structures in Computer Science 22(02):203-235, 2012. [DOI link, preprint PDF]

  2. M. Kretinsky, V. Rehak, and J. Strejcek: Reachability is Decidable for Weakly Extended Process Rewrite Systems. Information and Computation 207(6):671-680, 2009. [DOI link, preprint PDF]

  3. L. Bozzelli, M. Kretinsky, V. Rehak, and J. Strejcek: On decidability of LTL model checking for process rewrite systems. Acta Informatica 46(1):1-28, 2009. [DOI link, preprint PDF]

  4. M. Kretinsky, V. Rehak, and J. Strejcek: Petri Nets Are Less Expressive Than State-Extended PA. Theoretical Computer Science 394(1-2):134-140, 2008.

  5. A. Kucera and J. Strejcek: The Stuttering Principle Revisited. Acta Informatica 41(7-8):415-434, 2005. [PDF, © Springer-Verlag]
Proceedings papers
  1. T. Babiak, M. Kretinsky, V. Rehak, and J. Strejcek: LTL to Büchi Automata Translation: Fast and More Deterministic, in Proceedings of TACAS 2012, volume 7214 of LNCS, pages 95-109. Springer-Verlag, 2012. [DOI link, preprint PDF, © Springer-Verlag, LNCS, full version on arXiv]

  2. V. Rehak, P. Slovak, J. Strejcek, and L. Helouet: Decidable Race Condition and Open Coregions in HMSC, in Proceedings of GT-VMT 2010, volume 29 of Electronic Communications of the EASST, 12 pages, 2010. [PDF]

  3. T. Babiak, V. Rehak, and J. Strejcek: Almost Linear Büchi Automata, in Proceedings of EXPRESS 2009, volume 8 of EPTCS, pages 16-25, 2009. [DOI link, PDF]

  4. M. Kretinsky, V. Rehak, and J. Strejcek: On Decidability of LTL+Past Model Checking for Process Rewrite Systems, in Proceedings of INFINITY 2007, volume 239 of ENTCS, pages 105-117. Elsevier, 2009. [DOI link, preprint PDF]

  5. L. Bozzelli, M. Kretinsky, V. Rehak, and J. Strejcek: On Decidability of LTL Model Checking for Process Rewrite Systems, in Proceedings of FSTTCS 2006, volume 4337 of LNCS, pages 248-259. Springer-Verlag, 2006. [PDF, © Springer-Verlag, LNCS]

  6. A. Bouajjani, J. Strejcek, and T. Touili: On Symbolic Verification of Weakly Extended PAD, in Proceedings of EXPRESS 2006, volume 175(3) of ENTCS, pages 47-64. Elsevier Science Publishers, 2007. [DOI link, preprint PDF; full version can be found below as LIAFA tech. report 2006-001]

  7. A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejcek: Reachability analysis of multithreaded software with asynchronous communication, in Proceedings of Software Verification: Infinite-State Model Checking and Static Program Analysis, Dagstuhl Seminar Proceedings 06081, 18 pages. IBFI, 2006. [PDF]

  8. A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejcek: Reachability Analysis of Multithreaded Software with Asynchronous Communication, in Proceedings of FSTTCS 2005, volume 3821 of LNCS, pages 348-359. Springer-Verlag, 2005. [PDF, © Springer-Verlag, LNCS]

  9. M. Kretinsky, V. Rehak, and J. Strejcek: Reachability of Hennessy-Milner Properties for Weakly Extended PRS, in Proceedings of FSTTCS 2005, volume 3821 of LNCS, pages 213-224. Springer-Verlag, 2005. [PDF, © Springer-Verlag, LNCS]

  10. M. Kretinsky, V. Rehak, and J. Strejcek: Refining the Undecidability Border of Weak Bisimilarity, in Proceedings of INFINITY 2005, volume 149 of ENTCS, pages 17-36. Elsevier Science Publishers, 2006. [Elsevier web, preprint PDF; full version can be found below as tech. report FIMU-RS-2005-06]

  11. R. Pelanek and J. Strejcek: Deeper Connections between LTL and Alternating Automata, in Proceedings of CIAA 2005, volume 3845 of LNCS, pages 238-249. Springer-Verlag, 2006. [PDF, © Springer-Verlag, LNCS]

  12. A. Kucera and J. Strejcek: Characteristic Patterns for LTL, in SOFSEM 2005: Theory and Practice of Computer Science, 31st Conference on Current Trends in Theory and Practice of Computer Science, volume 3381 of LNCS, pages 239-249. Springer-Verlag, 2005. [postscript, © Springer-Verlag, LNCS]

  13. M. Kretinsky, V. Rehak, and J. Strejcek: Extended Process Rewrite Systems: Expressiveness and Reachability, in CONCUR 2004 - Concurrency Theory, volume 3170 of LNCS pages 355-370. Springer-Verlag, 2004. [postscript, © Springer-Verlag, LNCS]

  14. M. Kretinsky, V. Rehak, and J. Strejcek: On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit, in INFINITY 2003: 5th International Workshop on Verification of Infinite-State Systems, volume 98 of ENTCS, pages 75-88. Elsevier Science Publishers, 2003. [full version can be found below as tech. report FIMU-RS-2003-05]

  15. A. Kucera and J. Strejcek: The Stuttering Principle Revisited: On the Expressiveness of Nested X and U operators in the Logic LTL, in CSL 2002: 11th Annual Conference of the European Association for Computer Science Logic, volume 2471 of LNCS, pages 276-291. Springer-Verlag, 2002. [postscript, © Springer-Verlag, LNCS]

  16. J. Crhova, P. Krcal, J. Strejcek, D. Safranek, and P. Simecek: YAHODA: verification tools database, in Proceedings of Tools Day, FI MU Report Series, FIMU-RS-2002-05, pages 99-103. 2002. [postscript]

  17. J. Strejcek: Boundaries and Efficiency of Verification, in Proceedings of summer school on Modelling and Verification of Parallel processes (MOVEP'02), pages 403-408. IRCCyN, Ecole Centrale de Nantes, 2002. [postscript]

  18. J. Strejcek: Rewrite Systems with Constraints, in Proceedings of EXPRESS'01: 8th International Workshop on Expressiveness in Concurrency, volume 52 of ENTCS, 20 pages. Elsevier Science Publishers, 2002. [preprint postscript]
Technical reports & unreviewed papers
  1. T. Babiak, M. Kretinsky, V. Rehak, and J. Strejcek: A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness, 2010. [arXiv:1011.4214v1, PDF]

  2. V. Rehak, P. Slovak, J. Strejcek, and L. Helouet: Decidable Race Condition for HMSC, FI MU Report Series, FIMU-RS-2009-10, 2009. [PDF]

  3. L. Bozzelli, M. Kretinsky, V. Rehak, and J. Strejcek: On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems, FI MU Report Series, FIMU-RS-2006-05, 2006. Full version of FSTTCS'06 paper. [PDF]

  4. A. Bouajjani, J. Strejcek, and T. Touili: On Symbolic Verification of Weakly Extended PAD, Technical Report 2006-001, LIAFA, CNRS and University of Paris 7, 2006. Full version of EXPRESS'06 paper. [PDF]

  5. A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejcek: Reachability Analysis of Multithreaded Software with Asynchronous Communication, Technical Report 2005/06, Universität Stuttgart, Facultät Informatik, Elektrotechnik und Informationstechnik, November 2005. Full version of FSTTCS'05 paper. [postscript]

  6. M. Kretinsky, V. Rehak, and J. Strejcek: Refining the Undecidability Border of Weak Bisimilarity, FI MU Report Series, FIMU-RS-2005-06, 2005. Full version of INFINITY'05 paper. [postscript]

  7. A. Kucera and J. Strejcek: Characteristic Patterns for LTL, FI MU Report Series, FIMU-RS-2004-10, 2004. Full version of SOFSEM'05 paper. [postscript]

  8. R. Pelanek and J. Strejcek: Deeper Connections between LTL and Alternating Automata, FI MU Report Series, FIMU-RS-2004-08, 2004. [postscript]

  9. A. Kucera and J. Strejcek: An Effective Characterization of Properties Definable by LTL Formulae with a Bounded Nesting Depth of the Next-Time Operator, FI MU Report Series, FIMU-RS-2004-04, 2004. [postscript]

  10. M. Kretinsky, V. Rehak, and J. Strejcek: On the Expressive Power of Extended Process Rewrite Systems, Technical Report RS-04-07, Basic Research in Computer Science, Aarhus, Denmark, 2004. [postscript]

  11. M. Kretinsky, V. Rehak, and J. Strejcek: Process Rewrite Systems with Weak Finite-State Unit, FI MU Report Series, FIMU-RS-2003-05, 2003. Full version of INFINITY'03 paper. [postscript]

  12. A. Kucera and J. Strejcek: The Stuttering Principle Revisited: On the Expressiveness of Nested X and U operators in the Logic LTL, FI MU Report Series, FIMU-RS-2002-03, 2002. Full version of CSL'02 paper. [postscript]

  13. J. Strejcek: Constrained Rewrite Transition Systems, FI MU Report Series, FIMU-RS-2000-12, 2000. Full version of master's thesis. [postscript]
Thesis
  1. Linear Temporal Logic: Expressiveness and Model Checking, Ph.D. thesis, Faculty of Informatics, Masaryk University in Brno, 2004. [postscript]

  2. Models of Infinite-State Systems with Constraints, Master's thesis, Faculty of Informatics, Masaryk University in Brno, 2001. [postscript]

  3. Constrained Rewrite Transition Systems, Master's thesis, Faculty of Science, Masaryk University in Brno, 2000. [postscript]
strejcek@fi.muni.cz