Prof. RNDr. Mojmír Křetínský, CSc.

Basic CV Supervisor Qualifications Publications Projects Teaching

Person Identification

prof. RNDr. Mojmír Křetínský, CSc.; born May 9, 1950 in Vyskov, Czechoslovakia; married

Workplace

Department of Computer Science, Faculty of Informatics, Masaryk University
Botanicka 68a, 602 00 Brno, Czech Republic

Education and Academic Qualifications

2006: Professor in Computer Science, Masaryk University, Brno;
1997: Associate Professor (Docent) in Computer Science, Fac.of Informatics, MU Brno; habilitation thesis: "Infinite-state concurrent processes"
1990: Associate Professor (Docent) in Theoretical Computer Science and Cybernetics, Fac.of Science, MU Brno; habilitation thesis: "Semantic analyses of computer programs"
1986: CSc. (PhD) in Computer Science, Czechoslovak Academy of Science, Prague; supervisor: doc.RNDr.Jiri Horejs, CSc., thesis: "Pre-execution time analysis of computer programs"
1975: RNDr. in Computer Science, Faculty of Science, University of Brno; thesis: "Semi-top-down syntax analysis of detCFLs"
1973: graduated (with honors) in mathematics (MSc), Faculty of Science, University of Brno; thesis: "Parsing of deterministic CF languages"

Employment Summary

1994 - now: Associate Professor, since 2006 Professor, Dept. of Computer Science (Head), Faculty of Informatics, MU Brno
1990 - 1994: Associate Prof.(Docent) in Computer Science, Fac. of Science, MU Brno
1982 - 1990: Senior Lecturer of Computer Science, Dept. of Comp. Science, MU Brno
1979 - 1982: leading researcher, Institute of Computing Science, University of Brno
1974 - 1979: researcher, Dept. of Applied Mathematics, Fac.of Science, University of Brno

Pedagogical Activities

Currently taught courses:
Formal Languages and Automata, Automata Theory, Compiler Construction, Theory of Concurrent Processes, Concurrency Club (seminar on Current Trends in Concurrency Theory)
PhD students (successfully finished studies):
Antonin Kucera, Jiri Srba, Jan Strejcek, Vojtech Rehak.

Scientific and Research Activities

Specialisation:
main field: Concurrent and Distributed Systems
other fields: Formal Languages and Automata; Programming Languages, semantics, compilers;
current research interests: concurrency theory; models, semantics, decidability, verification, concurrent constraint programming methods
Grants:
2009 - 2011: Czech Science Foundation: "Verification and Analysis of Large-Scale Computer Systems" (co-worker)
2005 - 2011: Grant of Ministry of Education: Research Intent of Faculty of Informatics, MU: "Highly parallel and distributed computing systems", project no. MSM 0021622419 (concurrency group leader)
2005 - 2008: Grant Agency of The Czech Academy of Science: "Techniques for automatic verification and validation of software and hardware systems", the grant no. 1ET-408050503 (co-worker)
2005 - now: Grant of Ministry of Education: Research Centre ITI (Institute of Theoretical Computer Science), project no. 1M0021620808 (co-worker)
2006 - 2008: Grant Agency of The Czech Republic: "Automatic Verification of Software Systems", grant no. 201/06/1338 (co-worker)
2003 - 2005: Grant Agency of The Czech Republic: "Verification of Infinite State Systems", grant no. 201/03/1161 (project leader)
2000 - 2002: Grant Agency of The Czech Republic: "Infinite State Concurrent Systems -- Models and Verification", grant no. 201/00/0400 (project leader)
1999 - 2004: Research Intent of Faculty of Informatics, MU: "Models of Nonsequentinal Computing", project no.: CEZ: J07/98: 143300001 (co-worker, project leader: J. Gruska)
1999 - 2003: STINT (The Swedish Foundation for Internat.Cooperation in Research and Higher Education): "Verification of Infinite State Systems" (project leader at FI MU) jointly with Uppsala University, (project leader at UU: Faron Moller, Dept.of Comp.Sci.)
1997 - 1999: Grant Agency of The Czech Republic: "Algorithmic verification boundaries for infinite state systems", grant no. 201/97/0456(project leader at FI MU; project leader: P.Jancar, TU Ostrava)
1995 - 1999: Royal Academy, U.K.: "Temporal and distributed concurrent constraint systems" (co-worker)
1993 - 1996: EU COST 247.01 "Verification and validation methods for formal description" (co-worker)
1993 - 1995: Grant Agency of The Czech Repuplic "Analysis of concurrent infinite state systems", grant number 201/93/2123 (project leader)
1998 - 2000: advisor of a POST-DOC grant, Grant Agency of The Czech Republic: "Decidability problems in process algebras", grant no. 201/98/P046, post-doc researcher: A. Kučera
1999 - 2000: advisor of a POST-DOC grant GA ČR, Grant Agency of The Czech Repuplic "Decidability and complexity of behavioral equivalences on infinite-state processes", grant no. 201/99/D026, post-doc researcher: J. Stříbrná
1993 - now: several grants of FRVŠ (Fund for the development of universities); including grants where I served as the advisor of PhD student grants (PhD students: A.Kucera, J.Srba, J.Strejcek, V.Rehak)
1992 - 1994: TEMPUS JEP 2891 "Technology Transfer in Information Technologies",
1991 - 1995: individual grants EU: Grant COPERNICUS (European Community's Action for Cooperation in Science and Technology with Central and Eastern European Countries, 1993), Tempus--IMG grants (1991, 1995)
1980 - 1990: Grants of SPZV ČSAV ("Program Correctness", 1980 -- 1985; "Modern Programming Methodologies", 1986 -- 1990), Czechoslovak Academy of Science (co-worker, projects leader: J.Horejs)
Publications: more than 60 journal and conference papers, and research reports; reviews in professional review journals (Computers and Artificial Inteligence, Information Systems, and Zentrallblatt fuer Mathematics and Computer Science).

Academical Stays

1979: State University of Leningrad, USSR, 2 months
1982: University of Edinburgh, UK, 5 months
1992: Staffordshire University, School of Computing, Stafford, UK, 2 months
1993: University of Edinburgh, UK, 1 month
1993: City University of London, UK, 3 months
1994: Imperial College, University of London, UK, 2 weeks
1995: University of Edinburgh, UK, 6 weeks
1997 - now: City University of London, Namur University -- short stays

Current University Activities

1994 - now: member of Scientific Council, Faculty of Informatics, Masaryk University
1994 - now: member of Advisory Board for PhD studies in Computer Science (Faculty of Informatics, Masaryk University)
2000 - now: member of Advisory Board for PhD studies in Algebra (Faculty of Science, Masaryk University)
1996 - now: member of academic senat (till 2005: MU; since 2006: FI MU)

Extrauniversity Activities

2000 - 2010: member of Scientific Council, Faculty of EE and Informatics, VSB-TU Ostrava
2002 - 2008: Grant Agency of The Czech Republic (Czech Science Foundation), member of the committee for Mathematics and Informatics
2004 - 2006: member of Scientific Council, Institute of Informatics, Czech Academy of Science, Prague
1998 - 2004: member of IFIP Technical Committee TC-2
1998 - 2003: member of Czech National IFIP Committee
1992 - 1994: member of Scientific Council, Faculty of EE and Informatics, TU (VUT) Brno

Programme Committee member of internat.conferences and workshops

CONCUR (2002, co-chair)
MFCS (2000, 2003)
ICALP (1999)
SOFSEM (1996, 1998, 1999, 2001, 2002, 2008)
MEMICS (2007 co-chair, 2008 co-chair, 2009, 2010, 2011)
MFCS'98 Workshop on Concurrency (1998, co-chair)
IPSICALA (1993)

Selected Publications

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. On Decidability of LTL+Past Model Checking for Process Rewrite Systems. In Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008). 2009. vyd. Amsterdam, The Netherlands: Elsevier Science Publishers, 2009. od s. 105-117, 13 s. ISSN 1571-0661. 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
ČEŠKA, Milan a Zdeněk KOTÁSEK a Mojmír KŘETÍNSKÝ a Luděk MATYSKA a Tomáš VOJNAR. Proceedings of the International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2008) - selected papers. Electronic Notes in Theoretical Computer Science, Amsterdam, The Netherlands: Elsevier B.V., 251, 96 s. ISSN 1571-0661. 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
ČEŠKA, Milan a Zdeněk KOTÁSEK a Mojmír KŘETÍNSKÝ a Luděk MATYSKA a Tomáš VOJNAR a David ANTOŠ. MEMICS 2008, Fourth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. 1. vyd. Brno: Ing. Zdeněk Novotný CSc., Ondráčkova 105, 628 00 Brno, 2008. od s. 1-286, 286 s. ISBN 978-80-7355-082-0. URL info
BRIM, Luboš a Mojmír KŘETÍNSKÝ. Model Checking Large Finite-State Systems and Beyond. In 33rd Conference on Current Trends in Theory and Practice of Computer Science. Berlin: Springer-Verlag, 2007. od s. 9-28, 20 s. ISBN 978-3-540-69506-6. 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
MATYSKA, Luděk a David ANTOŠ a Milan ČEŠKA a Mojmír KŘETÍNSKÝ a Petr HLINĚNÝ. MEMICS 2007: Third Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. 1. vyd. Brno: Ing. Zdeněk Novotný CSc., Ondráčkova 105, 62800 Brno, 2007. 290 s. ISBN 978-80-7355-077-6. URL info
MATYSKA, Luděk a David ANTOŠ a Milan ČEŠKA a Mojmír KŘETÍNSKÝ a Petr HLINĚNÝ. MEMICS 2007: Third Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. 2007. URL 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
BOZZELLI, Laura a Mojmír KŘETÍNSKÝ a Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems. Brno: FI MU, 2006. FIMU-RS-2006-05. 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. Refining Undecidability Border of Weak Bisimilarity. (full version of INFINITY 2005 paper). Brno: FI MU, 2005. FIMU-RS-2005-06. 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
KŘETÍNSKÝ, Mojmír a Vojtěch ŘEHÁK a Jan STREJČEK. On the Expressive Power of Extended Process Rewrite Systems. BRICS Report Series, Aarhus: Basic Research in Computer Science, 2004, RS-04-7, od s. 1-18, 18 s. ISSN 0909-0878. 2004. URL 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
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 Prelim.Proc.of the 5th Internat.Workshop on Verification of Infinite-State Systems (INFINITY'2003). Marseille, France: Universite de Provence, Marseille, 2003. od s. 73-86, 14 s. info
KŘETÍNSKÝ, Mojmír a Vojtěch ŘEHÁK a Jan STREJČEK. Process Rewrite Systems with Weak Finite-State Unit (full version of INFINITY'2003 paper). Brno: FI MU, 2003. 23 s. FIMU-RS-2003-05. info
BRIM, Luboš a Jean-Marie JACQUET a David GILBERT a Mojmír KŘETÍNSKÝ. Coordination by means of Synchronous and Asynchronous Communication in Concurrent constraint Programming. Electronic Notes in Theoretical Computer Science, Amsterdam: Elsevier Science, 68, 3s. 1-24. ISSN 0444514163. 2003. URL info
BRIM, Luboš a Jean-Marie JACQUET a David GILBERT a Mojmír KŘETÍNSKÝ. Modelling Multi-Agents Systems as Concurrent Constraint Processes. Computing and Informatics, 21, 6, od s. 565-590, 25 s. ISSN 1335-9150. 2003. info
BRIM, Luboš a Petr JANČAR a Mojmír KŘETÍNSKÝ a Antonín KUČERA. CONCUR 2002 - Concurrency Theory. 13th International Conference. Proceedings. Berlin, Heidelberg, New York: Springer, 2002. 609 s. Lecture Notes in Computer Science, vol. 2421. ISBN 3-540-44043-7. info
BRIM, Luboš a Jean-Marie JACQUET a David GILBERT a Mojmír KŘETÍNSKÝ. Coordination by means of Synchronous and Asynchronous Communication in Concurrent constraint Programming. In Foundations of Coordination Languages and Software Architecture (FOCLASA`02). Amsterdam: Namur University, 2002. s. 1-24. info
BRIM, Luboš a Jean-Marie JACQUET a David GILBERT a Mojmír KŘETÍNSKÝ. Multi-Agents Systems as Concurrent Constraint Processes. In SOFSEM 2001 28th Conf.on Current Trends in Theory and Practice of Informatics. Heldelberg: Springer Verlag, 2001. s. 201-210. Lecture Notes in Computer Science, vol.2234. ISBN 0302-9743. info
ČERNÁ, Ivana a Mojmír KŘETÍNSKÝ a Antonín KUČERA. Comparing Expressibility of Normed BPA and Normed BPP Processes. Acta informatica, Berlin: Springer-Verlag, 36, 3s. 233-256. ISSN 0001-5903. 1999. info
BRIM, Luboš a Jean-Marie JACQUET a David GILBERT a Mojmír KŘETÍNSKÝ. A Fully Abstract Semantics for a Version of Synchronous Concurrent Constraint Programming. FI MU Report Series, Brno: FI MU, 1999, 08s. 1-62. 1999. URL info
MFCS´98 Workshop on Concurrency, August_27-29,_1998, Brno, Czech Republic : pre-proceedings. Edited by Petr Jančar - Mojmír Křetínský. Brno: Faculty of Informatics, 1998. 209 s. info
JANČAR, Petr a Mojmír KŘETÍNSKÝ. Proceedings of the MFCS'98 Workshop on Concurrency. Electronic Notes in Theoretical Computer Science, Elsevier, 1998, Vol.18s. 1-200. 1998. ENTCS home page info
JANČAR, Petr a Mojmír KŘETÍNSKÝ. MFCS´98 Workshop on Concurrency, August_27-29,_1998, Brno, Czech Republic : pre-proceedings. FI MU Report Series, Brno: FI MU, 1998, 06s. 1-209. 1998. info
BRIM, Luboš a David GILBERT a Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. A fully abstract semantics for synchronous and asynchronous ccp. Technical Report of Namur University, Namur: Namur University, 1998, 1s. 1-48. 1998. info
BRIM, Luboš a David GILBERT a Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. Temporal Synchronous Concurrent Constraint Programming. In COTIC 97, 1st Int.Workshop on Contr.programming for time critical systems. Piza, Italy: COTIC 97, 1997. s. 35-50. tical appl. info
ČERNÁ, Ivana a Mojmír KŘETÍNSKÝ a Antonín KUČERA. Bisimilarity is Decidable in the Union of Normed BPA and Normed BPP Processes. Electronic Notes in Theoretical Computer Science, Elsevier, 1997, 5s. 1-24. 1997. ENTCS home page info
BRIM, Luboš a David GILBERT a Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. Adding Time via Timed Transitions to Concurrent Constraint Programming. In ERCIM/COMPULOG Workshop. Linz, Austria: ERCIM, 1997. s. 23-34. info
BRIM, Luboš a David GILBERT a Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. A process Algebra for Synchronous Concurrent Constraint Programming. TR City University, U.K., London: City University London, 1996, 6s. 1-15. ISSN 1364-4009. 1996. info
BRIM, Lubos a David GILBERT a Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. A process algebra for Synchronous Concurrent Constraint Programming. In ALP96: Fifth Int. Conference on Algebraic and Logic Programm. Aachen, Germany: Springer-Verlag, 1996. s. 165-178. LNCS 1139. ISBN 3-540-61735-3. info
ČERNÁ, Ivana a Mojmír KŘETÍNSKÝ a Antonín KUČERA. On the Relationship between Sequential and Parallel Compositions in Process Algebras. In CSL96 - The 1996 Annual Conference of the European Assoc.. Ultrech, The Netherlands: Department of Philosophy, Ulterech University, 1996. s. 11-13. info
BRIM, Luboš a David GILBERT a Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. Synchronisation in Scc. In ILPS´95. Portland, Oregon, U.S.A: MIT Press, 1995. s. 282-283. ISBN 0-262-62099-5. info
BRIM, Lubos a David GILBERT a Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. New versions of Ask and Tell for synchronous communication in CCP. TR City University, U.K., London: City University London, 1995, 10s. 1-18. ISSN 1364-4009. 1995. info
BRIM, Luboš a David GILBERT a Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. On Synchronous Communication in Concurrent Constraint Programming. Technical Report of Namur University, Namur: Namur University, 1994, prelim.reps. 1-25. 1994. info
BRIM, Luboš a David GILBERT a Jean-Marie JACQUET a Mojmír KŘETÍNSKÝ. Operational semantics of concurrent logical systems. In ALP-UK Workshop on Cocurrency in Computational Logic. London,U.K.: City University London, 1993. s. 13-18. info

Last update: 2011/01/11

top