• Skip the Organizational structure panel
• Organizational structure

  On selecting a constituent part of MU the "Staff" page will be displayed with information relevant to the selected constituent part. The "Staff" page is not available for non-activated items.

  Masaryk University

  • Faculties
  • Law
  • Medicine
  • Science
  • Arts
  • Education
  • Economics
  • Informatics
  • Social Studies
  • Sports Studies

  • Institutes
  • Computer Science
  • CEITEC MU
  • Politica
  • Specialized Units
  • Hostels & Canteens
  • University Press
  • Telč Centre
  • UCB Management

  • Rector`s Office
  • Rectorate
  • Other Units
  • Archive
  • Language Centre
  • International Studies
  • Disabled Students
  • Technology Transfer
  • Biostatistics
  • Mendel Museum
  • CERIT
  • Civic Education
  • Project Team CEITEC

   

RNDr. Jan Strejček, Ph.D.

 

• Jan Strejček, born 21 May, 1977 in Brno, Czechoslovakia. Married.

• Department of Computer Science
  Faculty of Informatics
  Masaryk University
  Botanická 68a
  602 00 Brno
  Czech Republic

• Assistant professor

• 2007: RNDr. in Informatics, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
• 2005: Ph.D. in Computer Science, Faculty of Informatics, Masaryk University, Brno, Czech Republic. Thesis: Linear Temporal Logic: Expressiveness and Model Checking. Supervisor: Mojmír Křetínský.
• 2001: Mgr. (master's degree) in Informatics, Faculty of Informatics, Masaryk University, Brno, Czech Republic. Thesis: Models of Infinite-State Systems with Constraints. Supervisor: Antonín Kučera.
• 2000: Mgr. (master's degree) in Mathematics, Faculty of Science, Masaryk University, Brno, Czech Republic. Thesis: Constrained Rewrite Transition Systems. Supervisor: Luboš Brim.

• 2006-now: Assistant professor, Department of Computer Science, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
• 2005-2006: Post-doc researcher, LaBRI, University of Bordeaux 1, France.
• 2005: Assistant professor, Department of Computer Science, Faculty of Informatics, Masaryk University, Brno, Czech Republic.

• 2006-now: Automata and Grammars
• 2008-now: Formal Verification Methods
• 2008-now: Seminar on Concurrency
• 2007-now: Computational Logic (seminar tutor)
• 2008-now: Design of Algorithms I (seminar tutor)
• 2007-now: Formal Languages and Automata I (seminar tutor)
• 2008-now: Selected topics on automata theory (seminar tutor)
• 2003-2004, 2006: Computability and Complexity (seminar tutor)
• 1998-2002: Computability (seminar tutor)

• Properties of modal and temporal logics and their fragments.
• Formal verification of concurrent systems and software systems.
• Models of infinite-state systems, their expressiveness and decidability issues.

• 2005: A one-week research stay at LIAFA, University Paris 7, France.
• 2005: A three-months research stay at the Institute for Formal Methods in Computer Science, University of Stuttgart, Germany.

• 2007: Dean's award for distinguished PhD thesis, Faculty of Informatics, Masaryk Univeristy, Brno, Czech Republic.
• 2001: Annual dean's prize, Faculty of Informatics, Masaryk Univeristy, Brno, Czech Republic.
• 2001: 2nd place in SVOČ (a Czech mathematical research contest for undergraduate students), category Theoretical Informatics.
• 2000: Annual rector's prize, Masaryk Univeristy, Brno, Czech Republic.
• 1999: Annual prize of Section of Mathematics, Faculty of Science, Masaryk Univeristy, Brno, Czech Republic.

• BABIAK, Tomáš a Mojmír KŘETÍNSKÝ a Vojtěch ŘEHÁK a Jan STREJČEK. LTL to Büchi Automata Translation: Fast and More Deterministic. In Cormac Flanagan, Barbara König. TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2012. od s. 95-109, 15 s. ISBN 978-3-642-28755-8. doi:10.1007/978-3-642-28756-5_8. URL info
• BOZZELLI, Laura a Mojmír KŘETÍNSKÝ a Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL Model Checking for Process Rewrite Systems. Acta informatica, Berlin: Springer-Verlag, 46, 1, od s. 1-28, 28 s. ISSN 0001-5903. 2009. URL info
• KŘETÍNSKÝ, Mojmír a Vojtěch ŘEHÁK a Jan STREJČEK. Reachability is decidable for weakly extended process rewrite systems. Information and Computation, Elsevier, 207, 6, od s. 671-680, 10 s. ISSN 0890-5401. 2009. URL info
• KŘETÍNSKÝ, Mojmír a Vojtěch ŘEHÁK a Jan STREJČEK. Petri Nets Are Less Expressive Than State-Extended PA. Theoretical Computer Science, Amsterdam, North Holland: Elsevier Science Publishers, 394, 1-2, od s. 134-140, 7 s. ISSN 0304-3975. 2008.  info
• BOUAJJANI, Ahmed a Jan STREJČEK a Tayssir TOUILI. On Symbolic Verification of Weakly Extended PAD. In Proceedings of the 13th International Workshop on Expressiveness in Concurrency (EXPRESS 2006). Neuveden: Elsevier, 2007. od s. 47-64, 18 s. ISSN 1571-0661. URL info
• KŘETÍNSKÝ, Mojmír a Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL+Past Model Checking for Process Rewrite Systems. In Proc. of 9th Internat. Workshop on Verification of Infinite-State Systems. 2007.  info
• KŘETÍNSKÝ, Mojmír a Vojtěch ŘEHÁK a Jan STREJČEK. Refining Undecidability Border of Weak Bisimilarity. In Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05). 2006. vyd. Amsterdam, The Netherlands: Elsevier Science, 2006. od s. 17-36, 20 s. ISSN 1571-0661. URL info
• BOZZELLI, Laura a Mojmír KŘETÍNSKÝ a Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL Model Checking for Process Rewrite Systems. In FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings. Berlin: Springer-Verlag, 2006. od s. 248-259, 12 s. ISBN 978-3-540-49994-7.  info
• BOUAJJANI, Ahmed a Jan STREJČEK a Tayssir TOUILI. On Symbolic Verification of Weakly Extended PAD. In Preliminary Proceedings - 13th International Workshow on Expressiveness in Concurrency - EXPRESS'06. London: Imperial College London, 2006. od s. 29-41, 13 s.  info
• KUČERA, Antonín a Jan STREJČEK. Characteristic Patterns for LTL. P. Vojtas, M. Bielikova, B. Charron-Bost, O. Sykora (Eds.). In SOFSEM 2005: Theory and Practice of Computer Science. Berlin, Heidelberg: Springer-Verlag, 2005. od s. 239-249, 11 s. ISBN 3-540-24302-X.  info
• KUČERA, Antonín a Jan STREJČEK. The stuttering principle revisited. Acta informatica, Berlin: Springer-Verlag, 41, 7/8, od s. 415-434, 20 s. ISSN 0001-5903. 2005.  info
• KŘETÍNSKÝ, Mojmír a Vojtěch ŘEHÁK a Jan STREJČEK. Refining Undecidability Border of Weak Bisimilarity. BRICS Notes Series, San Francisco, USA, 2005, NS-05-4, od s. 3-14, 12 s. ISSN 0909-3206. 2005. URL info
• KŘETÍNSKÝ, Mojmír a Vojtěch ŘEHÁK a Jan STREJČEK. Reachability of Hennessy - Milner properties for weakly extended PRS. In FSTTCS 2005: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 25th International Conference. Berlin, Heidelberg: Springer-Verlag, 2005. od s. 213-224, 12 s. ISBN 3-540-30495-9.  info
• BOUAJJANI, Ahmed a Javier ESPARZA a Stefan SCHWOON a Jan STREJČEK. Reachability Analysis of Multithreaded Software with Asynchronous Communication. In FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference. Berlin, Heidelberg: Springer-Verlag, 2005. od s. 348-359, 12 s. ISBN 3-540-30495-9.  info
• PELÁNEK, Radek a Jan STREJČEK. Deeper Connections between LTL and Alternating Automata. In Implementation and Application of Automata. Berlin, Heidelberg: Springer-Verlag, 2005. od s. 238-249, 12 s. ISBN 978-3-540-31023-5.  info
• STREJČEK, Jan. Linear Temporal Logic: Expressiveness and Model Checking. : Faculty of Informatics, Masaryk University, 2005. 148 s.  info
• KŘETÍNSKÝ, Mojmír a Vojtěch ŘEHÁK a Jan STREJČEK. Extended Process Rewrite Systems: Expressiveness and Reachability. In CONCUR 2004 - Concurrency Theory. LNCS 3170. Berlin, Heidelberg, New York: Springer, 2004. od s. 355-370, 16 s. ISBN 3-540-22940-X.  info
• KŘETÍNSKÝ, Mojmír a Vojtěch ŘEHÁK a Jan STREJČEK. 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. 2004. vyd. Amsterdam, The Netherlands: Elsevier Science, 2004. od s. 75-88, 14 s. ISSN 1571-0661. URL info
• KUČERA, Antonín a Jan STREJČEK. The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. J. Bradfield (Ed.). In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'02). Berlin: Springer, 2002. s. 276-291. ISBN 3-540-44240-5.  info
• CRHOVÁ, Jitka a Pavel KRČÁL a Jan STREJČEK a David ŠAFRÁNEK a Pavel ŠIMEČEK. YAHODA: verification tools database. In Proceedings of Tools Day. Brno: FI MU, 2002. s. 99-103. FI MU Report Series info
• STREJČEK, Jan. Boundaries and Efficiency of Verification. In Proceedings of summer school MOVEP 2002. Nantes (France): IRCCyN, Ecole Centrale de Nantes, France, 2002. s. 403-408.  info
• STREJČEK, Jan. Models of infinite-state systems with constraints. Brno, 2001. iii, 44 s.  info
• STREJČEK, Jan. Rewrite Systems with Constraints. In EXPRESS'01 the 8th International Workshop on Expressiveness in Concurrency. Aalborg (Denmark): Elsevier Science, 2001. s. 1-20. URL info

Last update: 2008/07/23