Pavel Krcal

Box 337

Dept. of Information Technology

Uppsala University

751 05

Uppsala

Sweden

MIC, Polacksbacken

Lagerhyddsvagen 2

Building 1, Room 1217

Phone: +46 18 - 471 73 41

Fax: +46 18 - 55 02 25

Mobile: +46 76 - 785 11 85

I have defended my PhD thesis at the Department of Information Technology at Uppsala University.
My supervisor was professor Wang Yi and I worked in the UPPAAL group.
I'm from Czechia, where I studied at Faculty of Informatics, Masaryk University Brno.
I was very much involved in the activities of the Parallel and Distributed Systems Laboratory (Paradise) there.

Infinite Structures in Timed Systems. Pavel Krcal . PhD Thesis. May 2009. PDF

Sampled Semantics of Timed Automata. Parosh Aziz Abdulla, Pavel Krcal and Wang Yi. Accepted for publication in LMCS. PDF

Universality of R-automata with Value Copying. Parosh Aziz Abdulla, Pavel Krcal and Wang Yi. INFINITY 2008. PDF

R-automata. Parosh Aziz Abdulla, Pavel Krcal and Wang Yi. CONCUR 2008. Abstract PDF (C) Springer-Verlag Bibtex

Multi-Processor Schedulability Analysis of Preemptive Real-Time Tasks with Variable Execution Times. Pavel Krcal, Martin Stigge and Wang Yi. FORMATS 2007. Abstract Postscript (C) Springer-Verlag Bibtex

Task Automata: Schedulability, Decidability and Undecidability. Elena Fersman, Pavel Krcal, Paul Pettersson and Wang Yi. Information and Computation, 2007. Abstract PDF (C) Elsevier B.V. Bibtex

Sampled Universality of Timed Automata. Parosh Aziz Abdulla, Pavel Krcal and Wang Yi. FOSSACS 2007. Abstract Postscript (C) Springer-Verlag Bibtex

Communicating Timed Automata: The More Synchronous, the More Difficult to Verify. Pavel Krcal and Wang Yi. CAV 2006. Abstract Postscript (C) Springer-Verlag Bibtex Full version of the paper is here (pdf file).

On Sampled Semantics of Timed Systems. Pavel Krcal and Radek Pelanek. FSTTCS 2005. Abstract Postscript (C) Springer-Verlag Bibtex Full version of the paper is here (pdf file).

Timed vs. Time-Triggered Automata. Pavel Krcal, Leonid Mokrushin, P.S. Thiagarajan, and Wang Yi. CONCUR 2004. Abstract Postscript (C) Springer-Verlag Bibtex

Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. Pavel Krcal and Wang Yi. TACAS 2004. Abstract Postscript (C) Springer-Verlag Bibtex

Distributed Bounded Explicit LTL Model Checking. Pavel Krcal. PDMC Workshop 2003. Abstract Postscript (C) Elsevier Bibtex

Distributed LTL Model-Checking Based on Negative Cycle Detection. Lubos Brim, Ivana Cerna, Pavel Krcal, and Radek Pelanek. FSTTCS 2001. Abstract Postscript (C) Springer-Verlag Bibtex