Joost P. Katoen

prof.dr.ir.

1992 …2018
If you made any changes in Pure these will be visible here soon.

Research Output 1992 2018

2004
5 Downloads (Pure)

Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes

Jensen, K. (ed.), Baier, C., Haverkort, B. R. H. M., Podelski, A. (ed.), Hermanns, H. & Katoen, J. P., 2004, p. 61-76. 16 p.

Research output: Contribution to conferencePaperAcademicpeer-review

File
7 Citations (Scopus)
32 Downloads (Pure)

Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes

Baier, C., Haverkort, B. R. H. M., Hermanns, H. & Katoen, J. P., 2004, Enschede: Elektrotechniek, Wiskunde & Informatica. 30 p. (1381-3625; no. 03-50)

Research output: Book/ReportReportProfessional

File
2 Citations (Scopus)
19 Downloads (Pure)

Embedded software analysis with MOTOR

Katoen, J-P., Bohnenkamp, H., Klaren, R. & Hermanns, H., 2004, Formal Methods for the Design of Real-Time Systems: International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004. Revised Lectures. Bernardo, M. & Corradini, F. (eds.). Springer, p. 268-293 26 p. (Lecture Notes in Computer Science; vol. 3185).

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

Open Access
File
Embedded software
Quality of service
Network protocols

Model checking dependabiliy attributes of wireless group communication

Massink, M., Katoen, J. P. & Latella, D., 2004, p. 711-720. 10 p.

Research output: Contribution to conferencePaperAcademicpeer-review

11 Citations (Scopus)

Model checking dependabiliy attributes of wireless group communication

Massink, M., Katoen, J. P. & Latella, D., 28 Jun 2004, 2004 international conference on dependable systems and networks (DSN'04). Los Alamitos: IEEE Computer Society, p. 711-720

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

66 Downloads (Pure)

MoDeST: A compositional modeling formalism for real-time and stochastic systems

Bohnenkamp, H. C., d' Argenio, P. R., Hermanns, H. & Katoen, J. P., Nov 2004, Enschede: INF-Centre for Telematics and Information Techn. 36 p. (CTIT technical report series; no. 1381-3625)

Research output: Book/ReportReportProfessional

File

Probabilistic weak simulation is decidable in polynomial time

Baier, C., Hermanns, H. & Katoen, J. P., 2004, In : Information processing letters. 89, 3, p. 123-140

Research output: Contribution to journalArticleAcademicpeer-review

15 Citations (Scopus)

Probabilistic weak simulation is polynomially decidable

Baier, C., Hermanns, H. & Katoen, J. P., 2004, In : Information processing letters. 89, 3, p. 123-252 130 p., 10.1016/j.ipl.2003.10.001.

Research output: Contribution to journalArticleAcademicpeer-review

QEST 2004: First International Conference on the Quantitative Evaluation of Systems: Proceedings

Haverkort, B. R. H. M., Franceschinis, G., Katoen, J. P. & Woodside, M., 2004, Los Alamitos, CA, USA: IEEE Computer Society. 360 p.

Research output: Book/ReportBook editingAcademic

Validation of stochastic systems

Baier, C., Haverkort, B. R. H. M., Hermanns, H., Katoen, J. P. & Siegle, M., 2004, Berlin: Springer. 467 p. (Lecture notes in computer science; no. 2925)

Research output: Book/ReportBook editingAcademic

19 Citations (Scopus)

Who is pointing when to whom?

Distefano, D. S., Katoen, J. P. & Rensink, A., 16 Dec 2004, FSTTCS 2004: foundations of software technology and theoretical computer science. Lodaya, K. & Mahajan, M. (eds.). Berlin: Springer, p. 250-262

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Who is pointing when to whom?

Distefano, D. S., Lodaya, K. (ed.), Katoen, J. P., Mahajan, M. (ed.) & Rensink, A., 2004, p. 250-262. 13 p.

Research output: Contribution to conferencePaperAcademicpeer-review

2003
5 Downloads (Pure)

An efficient algorithm tocompute the minimal and maximal probabilities for timed reachability incontinuous-time Markov decision processes

Baier, C., Haverkort, B. R. H. M., Hermanns, H. & Katoen, J. P., Oct 2003, Enschede: Centre for Telematics and Information Technology (CTIT). (CTIT technical report series; no. TR-CTI)

Research output: Book/ReportReportOther research output

File
21 Citations (Scopus)

A QoS-oriented extension of UML statecharts

Jansen, D. N., Hermanns, H. & Katoen, J. P., 2003, «UML» 2003: the unified modeling language. Stevens, P., Whittle, J. & Booch, G. (eds.). Berlin, Germany: Springer, p. 76-91 16 p. (Lecture Notes in Computer Science; vol. 2863, no. XIV).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

A tool for model-checking Markov chains

Hermanns, H., Katoen, J. P., Meyer-Kayser, J. & Siegle, M., 2003, In : International journal on software tools for technology transfer. 4, 2, p. - 20 p.

Research output: Contribution to journalArticleAcademicpeer-review

51 Citations (Scopus)
30 Downloads (Pure)

A tool for model-checking Markov chains

Hermanns, H., Katoen, J. P., Meyer-Kayser, J. & Siegle, M., 2003, In : International journal on software tools for technology transfer. 4, 2, p. 153-172 20 p., 10.1007/s100090100072.

Research output: Contribution to journalArticleAcademicpeer-review

File
12 Citations (Scopus)
44 Downloads (Pure)

Comparative branching-time semantics for Markov chains

Baier, C., Hermanns, H., Katoen, J. P. & Wolf, V., 2003, Concurrency Theory (CONCUR). Amadio, R. & Lugiez, D. (eds.). Berlin: Springer, p. 492-507 16 p. (Lecture Notes in Computer Science; vol. 2761, no. XI).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

File
45 Downloads (Pure)

Discrete-time rewards model-checked

Larsen, K. G. (ed.), Andova, S., Niebert, P. (ed.), Hermanns, H. & Katoen, J. P., 2003, p. 88-104. 16 p.

Research output: Contribution to conferencePaperAcademicpeer-review

File

Discrete-time rewards model-checked (to appear)

Andova, S., Hermanns, H. & Katoen, J. P., 6 Sep 2003, Formal modeling and analysis of timed systems: FORMATS. Larsen, K. G. & Niebert, P. (eds.). Berlin: Springer, p. 88-104 16 p.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

64 Downloads (Pure)

Extensions of Statecharts with probability, time, and stochastic timing

Jansen, D. N., 29 Oct 2003, Bern: Inmarks. 159 p.

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

Open Access
File

Extentions of Statecharts with Probability, Time and Stochastic Timing

Jansen, D. N., 29 Oct 2003, Bern, Zwitserland: Inmarks ag. 159 p.

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

515 Citations (Scopus)

Model-checking algorithms for continuous-time Markov chains

Baier, C., Haverkort, B. R. H. M., Hermanns, H. & Katoen, J. P., Jun 2003, In : IEEE transactions on software engineering. 29, 6, p. 524-541 18 p., 10.1109/TSE.2003.1205180.

Research output: Contribution to journalArticleAcademicpeer-review

29 Citations (Scopus)
32 Downloads (Pure)

Model-checking large structured Markov chains

Buchholz, P., Katoen, J. P., Kemper, P. & Tepper, C., May 2003, In : Journal of logic and algebraic programming. 56, 1-2, p. 69-97 28 p.

Research output: Contribution to journalArticleAcademicpeer-review

Open Access
File
Continuous-time Markov Chain
Model checking
Markov processes
Model Checking
Markov chain
2 Downloads (Pure)

Model Checking pathCSL

Cloth, L., Haverkort, B., Hermanns, H., Katoen, J-P. & Baier, C., 6 Sep 2003, PMCCS-6: The Sixth International Workshop on Performability Modeling of Computer and Communication Systems. Bobbio, A., Deavours, D. & Ma, Y. (eds.). Urbana-Champaign: University of Illinois at Urbana-Champaign, p. 19-22

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

Open Access
File
Performability
Reward
Model Checking
Logic
Path
7 Citations (Scopus)
19 Downloads (Pure)

On integrating the MÖBIUS and MODEST modeling tools

Bohnenkamp, H. C., Courtney, T., Daly, D., Derisavi, S., Hermanns, H., Katoen, J. P., Klaren, J., Vi Lam, V. & Sanders, W. H., 22 Jun 2003, 2003 International conference on dependable systems and networks. Los Alamitos, USA: IEEE Computer Society, p. 671- 1 p.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

File
76 Downloads (Pure)

On Model Checking the Dynamics of Object-Based Software: A Foundational Approach

Distefano, D. S., 2003, Enschede: Twente University Press (TUP). 313 p.

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

File
15 Citations (Scopus)

The MoDeST modeling tool and its implementation

Bohnenkamp, H. C., Hermanns, H., Katoen, J. P. & Klaren, J., 2 Sep 2003, Computer performance evaluations. modelling techniques and tools: 13th International Conference, TOOLS 2003, Urbana, IL, USA, September 2-5, 2003. Proceedings. Kemper, P. & Sanders, W. (eds.). Berlin: Springer, p. 116-133 (Lecture notes in computer science; vol. 2794).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Simulators
Specifications
9 Downloads (Pure)

Who is pointing when to whom: on model-checking pointer structures

Distefano, D. S., Rensink, A. & Katoen, J. P., Apr 2003, Enschede: Centre for Telematics and Information Technology (CTIT). 79 p. (CTIT-technical reports; no. 2003-..)

Research output: Book/ReportReportProfessional

File
2002

A probabilistic extension of UML statecharts: specification and verification

Jansen, D. N., Hermanns, H. & Katoen, J. P., 2002, Formal techniques in real-time and fault-tolerant systems: ... FTRTFT. Damm, W. & Olderog, E-R. (eds.). Berlin, Germany: Springer, p. 355-374 20 p. (Lecture Notes in Computer Science; vol. 2469).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

31 Citations (Scopus)
18 Downloads (Pure)

A probabilistic extension of UML statecharts: specification and verification

Jansen, D. N., Hermanns, H. & Katoen, J. P., Sep 2002, Enschede: Centre for Telematics and Information Technology (CTIT). 25 p. (CTIT technical report series; no. TR-CTIT-02-31)

Research output: Book/ReportReportOther research output

File

Automated performance and dependability evaluation using model checking

Baier, C., Haverkort, B. R. H. M., Hermanns, H. & Katoen, J. P., 2002, Lecture Notes in Computer Science 2459: Performance Evaluation of Complex Systems: Techniques and Tools, Performance 2002, Tutorial Lectures. Calzarossa, M. & Tucci, S. (eds.). Rome, Italy: Springer, p. - 29 p.

Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

22 Citations (Scopus)
20 Downloads (Pure)

Automated performance and dependability evaluation using model checking

Baier, C., Haverkort, B. R. H. M., Hermanns, H. & Katoen, J. P., 2002, Computer Performance Evaluation. Calzarossa, M. & Tucci, S. (eds.). Berlin: Springer, p. 261-289 29 p. (Lecture Notes in Computer Science; vol. 2459).

Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

File

Guest editors'introduction: Model checking in a nutshell

Hermanns, H. & Katoen, J. P., 2002, In : Journal of logic and algebraic programming. 0, C, p. 1-5

Research output: Contribution to journalArticleAcademicpeer-review

63 Downloads (Pure)

Guest editors' introduction: Model checking in a nutshell

Hermanns, H. & Katoen, J. P., 2002, In : Journal of logic and algebraic programming. 52-53, 10.1016/S1567-8326(02)00030-9, p. 1-5 5 p., 10.1016/S1567-8326(02)00030-9.

Research output: Contribution to journalArticleAcademic

File
33 Downloads (Pure)

Model-Checking Algorithms for Continuous-Time Markov Chains

Baier, C., Haverkort, B. R. H. M., Hermanns, H. & Katoen, J. P., Apr 2002, Enschede: Centre for Telematics and Information Technology (CTIT). (CTIT technical report series; no. TR-CTI)

Research output: Book/ReportReportOther research output

File
12 Citations (Scopus)
36 Downloads (Pure)

Model checking birth and death

Distefano, D. S., Rensink, A. & Katoen, J. P., 2002, p. 435-447. 13 p.

Research output: Contribution to conferencePaperAcademicpeer-review

File

Model checking birth and death.

Distefano, D. S., Rensink, A. & Katoen, J. P., 2002, In : Theoretical computer science. p. -

Research output: Contribution to journalArticleAcademicpeer-review

Model checking for dynamic allocation and deallocation

Distefano, D. S., Rensink, A. & Katoen, J. P., 2002, Centre for Telematics and Information Technology (CTIT). 57 p. (CTIT Technical Report Series; no. 01-40)

Research output: Book/ReportReportAcademic

56 Citations (Scopus)

Model-checking performability properties

Haverkort, B. R. H. M., Cloth, L., Hermanns, H., Katoen, J. P. & Baier, C., 2002, Proceedings of the Int. IEEE Conference on Dependable Systems and Networks (DSN). Washingthon (D.C.), USA: IEEE CS Press, p. - 10 p.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

13 Downloads (Pure)

Model-checking performability properties

Haverkort, B. R. H. M., Cloth, L., Hermanns, H., Katoen, J. P. & Baier, C., 2002, p. 103-112. 10 p.

Research output: Contribution to conferencePaperAcademicpeer-review

File
Model checking
Formal logic
Mobile computing
Computational complexity
151 Citations (Scopus)
23 Downloads (Pure)

Process algebra for performance evaluation

Hermanns, H., Herzog, U. & Katoen, J. P., 2002, In : Theoretical computer science. 274, 1-2, p. 43-87 44 p., 10.1016/S0304-3975(00)00305-4.

Research output: Contribution to journalArticleAcademicpeer-review

File

Real-time and probabilistic systems - Foreword

Katoen, J. P., 2002, In : Theoretical computer science. 282, 1, p. 1-3

Research output: Contribution to journalArticleAcademicpeer-review

Simulation for continuous-time Markov chains

Baier, C., Katoen, J. P., Hermanns, H. & Haverkort, B. R. H. M., 2002, In : Lecture notes in artificial intelligence. 2421, p. -

Research output: Contribution to journalArticleAcademicpeer-review

17 Citations (Scopus)
8 Downloads (Pure)

Simulation for continuous-time Markov chains

Brim, J. (ed.), Baier, C., Katoen, J. P., Jancar, P. (ed.), Hermanns, H., Kretnsk, M. (ed.), Haverkort, B. R. H. M. & Kucera, A. (ed.), 2002, p. 473-489. 15 p.

Research output: Contribution to conferencePaperAcademicpeer-review

File

Tools and Algerithms for the Construction and Analysis of Systems

Katoen, J. P. & Stevens, P., 2002, Grenoble, France: Springer. 451 p. (Lecture Notes in Computer Science; no. 2280)

Research output: Book/ReportBookAcademic

Tools and Algorithms for the Construction and Analysis of Systems

Katoen, J. P. (ed.) & Stevens, P. (ed.), 2002, Berlin: Springer. 451 p. (Lecture Notes in Computer Science; vol. 2280)

Research output: Book/ReportBook editingAcademic

2001
10 Downloads (Pure)

A model checker for performance and dependability properties

Hermanns, H., Karelse, F. (ed.), Katoen, J. P., Meyer-Kayser, J. & Siegle, M., 2001, p. 83-88. 6 p.

Research output: Contribution to conferencePaperAcademic

File

A Model Checker for Performance and Dependability Properties

Hermanns, H., Katoen, J. P. & Meyer-Kayser, J., 2001, Proceedings of the 2nd Workshop on Embedded Systems. Veldhoven, the Netherlands: STW Technology Foundation, p. - 6 p.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Beyond memoryless distributions: model checking semi-Markov chains

Infante lopez, G. G., Hermanns, H. & Katoen, J. P., 2001, In : Lecture notes in artificial intelligence. 2165, p. -

Research output: Contribution to journalArticleAcademicpeer-review

38 Citations (Scopus)
52 Downloads (Pure)

Beyond memoryless distributions: model checking semi-Markov chains

Infante lopez, G. G., de Alfaro, L. (ed.), Gilmore, S. (ed.), Hermanns, H. & Katoen, J. P., 2001, p. 57-70. 14 p.

Research output: Contribution to conferencePaperAcademicpeer-review

File