Publications

Journals

• 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

Conferences and Workshops

• 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


• 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


• How to Employ Reverse Search in Distributed Single-Source Shortest Paths. Lubos Brim, Ivana Cerna, Pavel Krcal, and Radek Pelanek. SOFSEM 2001. Abstract Postscript (C) Springer-Verlag Bibtex

Other

• Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. Pavel Krcal and Wang Yi. A chapter in the book ARTES - A network for Real-Time research and graduate Education in Sweden 1997-2006. ISBN 91-506-1859-8. Editor Hans Hansson. Year 2006. Pages 259-280.


• Distributed Bounded Explicit LTL Model Checking. Pavel Krcal. Faculty of Informatics, Masaryk University, Brno , Master's Thesis, 2003. Abstract Postscript Bibtex

Technical Reports

• R-automata. Parosh Aziz Abdulla, Pavel Krcal and Wang Yi. Uppsala University, Technical Report 2008-016, full version of the CONCUR'08 paper. Abstract PDF Bibtex


• Communicating Timed Automata: The More Synchronous, the More Difficult to Verify. Pavel Krcal and Wang Yi. Uppsala University, Technical Report 2006-006, full version of the CAV'06 paper. Abstract PDF Bibtex


• Reachability Relations and Sampled Semantics of Timed Systems. Pavel Krcal and Radek Pelanek. Technical Report FIMU-RS-2005-09, 31 pages, full version of the FSTTCS'05 paper. Abstract PDF Bibtex


• Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata. Pavel Krcal and Wang Yi. Uppsala University, Technical Report 2003-051, full version of the TACAS'04 paper. Abstract PDF Bibtex


• Model Checking in IPv6 Hardware Router Design. Jiri Barnat, Tomas Brazdil, Pavel Krcal, Vojtech Rehak, and David Safranek. CESNET technical report number 8/2002, 2002. Abstract Postscript Bibtex


• YAHODA: Verification Tools Database. Jitka Crhova, Pavel Krcal, Jan Strejcek, David Safranek, and Pavel Simecek. Tools Day affiliated to CONCUR'02, FIMU-RS-2002-05. Abstract Postscript Bibtex


• Distributed LTL Model-Checking Based on Negative Cycle Detection. Lubos Brim, Ivana Cerna, Pavel Krcal, and Radek Pelanek. Technical Report FIMU-RS-2001-01, 19 pages, full version of the FSTTCS'01 paper. Abstract Postscript Bibtex


• How to Employ Reverse Search in Distributed Single-Source Shortest Paths. Lubos Brim, Ivana Cerna, Pavel Krcal, and Radek Pelanek. Technical Report FIMU-RS-2001-09, 22 pages, full version of the SOFSEM 01 paper. Abstract Postscript Bibtex