Research Output 1992 2018

Filter
Article
2017
4 Citations

Fault trees on a diet: automated reduction by graph rewriting

Junges, S., Guck, D., Katoen, J. P., Rensink, A. & Stoelinga, M. 2017 In : Formal aspects of computing. 29, 4, p. 651-703

Research output: Scientific - peer-reviewArticle

Directed graphs
Nutrition
Scalability
Experiments
2016
2 Citations

Confluence reduction for Markov automata

Timmer, M., Katoen, J. P., van de Pol, J. & Stoelinga, M. I. A. 6 Dec 2016 In : Theoretical computer science. 655, B, p. 193-219 27 p.

Research output: Scientific - peer-reviewArticle

Explosions
Specifications
2014
17 Citations

Analysis of timed and long-run objectives for Markov automata

Guck, D., Hatefi, H., Hermanns, H., Katoen, J. P. & Timmer, M. 10 Sep 2014 In : Logical methods in computer science. 10, 3, p. 17 29 p.

Research output: Scientific - peer-reviewArticle

Petri nets
Markov processes
Semantics
Chemical analysis
Modeling languages
16 Citations

Spacecraft early design validation using formal methods

Bozzano, M., Cimatti, A., Katoen, J. P., Katsaros, P., Mokos, K., Nguyen, V. Y., Noll, T., Postma, B. & Roveri, M. Dec 2014 In : Reliability engineering & system safety. 132, p. 20-35 16 p.

Research output: Scientific - peer-reviewArticle

Spacecraft
Model checking
Industry
Inspection
Personnel
2013
10 Citations

Model checking for performability

Baier, C., Hahn, E. M., Haverkort, B. R. H. M., Hermanns, H. & Katoen, J. P. Aug 2013 In : Mathematical structures in computer science. 23, Special Issue 04, p. 751-795 45 p.

Research output: Scientific - peer-reviewArticle

Model checking
Temporal logic
Stochastic models
2012
7 Citations

A linear process-algebraic format with data for probabilistic automata

Di Pierro, A. (ed.), Katoen, J. P., van de Pol, J. C., Norman, G. (ed.), Stoelinga, M. I. A. & Timmer, M. 6 Jan 2012 In : Theoretical computer science. 413, 1, p. 36-57 22 p.

Research output: Scientific - peer-reviewArticle

Algebra
2011
33 Citations

Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

Chen, T., Han, T., Katoen, J. P. & Mereacre, A. 2011 In : Logical methods in computer science. 7, 1-12, p. 12:1-12:34 34 p.

Research output: Scientific - peer-reviewArticle

Markov processes
Integral equations
Clocks
Specifications
Linear equations
120 Citations

The ins and outs of the probabilistic model checker MRMC

Katoen, J. P., Zapreev, I. S., Hahn, E. M., Hermanns, H. & Jansen, D. N. Feb 2011 In : Performance evaluation. 68, 2, p. 90-104 15 p.

Research output: Scientific - peer-reviewArticle

Model checking
Discrete event simulation
4 Citations

Time-bounded reachability in tree-structured QBDs by abstraction

Klink, D., Remke, A. K. I., Haverkort, B. R. H. M. & Katoen, J. P. Feb 2011 In : Performance evaluation. 68, 2, p. 105-125 21 p.

Research output: Scientific - peer-reviewArticle

Markov processes
Model checking
2010
27 Citations

Computing Optimal Schedules of Battery Usage in Embedded Systems

Jongerden, M. R., Mereacre, A., Bohnenkamp, H. C., Haverkort, B. R. H. M. & Katoen, J. P. 2010 In : IEEE transactions on industrial informatics. 6, 3, p. 276-286 11 p.

Research output: Scientific - peer-reviewArticle

Scheduling
Mobile devices
Recovery
20 Citations

Performability assessment by model checking of Markov reward models

Baier, C., Cloth, L., Haverkort, B. R. H. M., Hermanns, H. & Katoen, J. P. 2010 In : Formal methods in system design. 36, 1, p. 1-36 36 p.

Research output: Scientific - peer-reviewArticle

Model checking
Specifications
Computational complexity
Communication systems
Semantics
47 Citations

Performance Evaluation and Model Checking Join Forces

Baier, C., Haverkort, B. R. H. M., Hermanns, H. & Katoen, J. P. Sep 2010 In : Communications of the ACM. 53, 9, p. 76-85 10 p.

Research output: Scientific - peer-reviewArticle

2009
63 Citations

Counterexample Generation in Probabilistic Model Checking

Han, T., Katoen, J. P. & Damman, B. 2009 In : IEEE transactions on software engineering. 35, 2, p. 241-257 17 p., 10.1109/TSE.2009.5

Research output: Scientific - peer-reviewArticle

Model checking
Markov processes

Towards an Information Retrieval Theory of Everything

Hiemstra, D., Lammerink, J. M. W. (ed.), Katoen, J. P. (ed.), Kok, J. N. (ed.), van de Pol, J. C. (ed.) & Raamsdonk, F. (ed.) 2009 In : Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica. 2009, p. 27-38 12 p.

Research output: ScientificArticle

Information retrieval
2007
41 Citations

Model checking mobile stochastic logic.

De Nicola, R., Katoen, J. P., Latella, D., Loreti, M. & Massink, M. 2007 In : Theoretical computer science. 382, Supplement/1, p. 42-70 29 p., 10.1016/j.tcs.2007.05.008

Research output: Scientific - peer-reviewArticle

Stochastic models
Specifications
2006
83 Citations

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

Bohnenkamp, H. C., d' Argenio, P. R., Hermanns, H. & Katoen, J. P. 2006 In : IEEE transactions on software engineering. 32, 10/10, p. 812-830 19 p., 10.1109/TSE.2006.104

Research output: Scientific - peer-reviewArticle

Random processes
Markov processes
Quality of service
Semantics
Specifications
2005
22 Citations

A theory of stochastic systems. Part II: Process algebra

d' Argenio, P. R. & Katoen, J. P. 2005 In : Information and computation. 203, 1, p. 39-74 36 p.

Research output: Scientific - peer-reviewArticle

Algebra
Clocks
Semantics
Stochastic systems
Discrete event simulation
41 Citations

A theory of stochastic systems part I: Stochastic automata

d' Argenio, P. R. & Katoen, J. P. 2005 In : Information and computation. 203, 1, p. 1-38 38 p.

Research output: Scientific - peer-reviewArticle

Real time systems
Markov processes
Semantics
86 Citations

Comparative branching-time semantics for Markov chains

Baier, C., Katoen, J. P., Hermanns, H. & Wolf, V. 2005 In : Information and computation. 200, 2, p. 149-214 66 p.

Research output: Scientific - peer-reviewArticle

Temporal logic
Semantics
89 Citations
Markov processes
Time delay

Model checking meets performance evaluation

Baier, C., Haverkort, B. R. H. M., Hermanns, H. & Katoen, J. P. 2005 In : SIGMETRICS performance evaluation review. 32, 4, p. 10-16 7 p.

Research output: Scientific - peer-reviewArticle

Markov processes

Performance and verification

Haverkort, B. R. H. M. & Katoen, J. P. 2005 In : SIGMETRICS performance evaluation review. 32, 4, p. 3-3 1 p.

Research output: ScientificArticle

Embedded systems
Communication systems
Throughput
Formal verification
Formal specification

QoS modelling and analysis with UML-statecharts: the StoCharts approach

Jansen, D. N., Haverkort, B. R. H. M. (ed.), Hermanns, H. & Katoen, J. P. (ed.) Mar 2005 In : SIGMETRICS performance evaluation review. 32, 4, p. 28-33 6 p.

Research output: Scientific - peer-reviewArticle

Quality of service
Random processes
2004

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: Scientific - peer-reviewArticle

14 Citations

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: Scientific - peer-reviewArticle

Markov processes
Polynomials
2003
49 Citations

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: Scientific - peer-reviewArticle

Markov processes
Temporal logic
Model checking

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: Scientific - peer-reviewArticle

485 Citations

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: Scientific - peer-reviewArticle

Markov processes
Model checking
Mathematical operators
Temporal logic
Linear equations
26 Citations

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: Scientific - peer-reviewArticle

Markov processes
Model checking
Petri nets
Algebra
Explosions
2002

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: Scientific - peer-reviewArticle

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: ScientificArticle

Model checking birth and death.

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

Research output: Scientific - peer-reviewArticle

147 Citations

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: Scientific - peer-reviewArticle

Algebra
Network architecture
Random processes
Random variables
Markov processes

Real-time and probabilistic systems - Foreword

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

Research output: Scientific - peer-reviewArticle

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: Scientific - peer-reviewArticle

2001

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: Scientific - peer-reviewArticle

First passage time analysis of stochastic process algebra using partial orders

Ruys, T. C., Langerak, R., Katoen, J. P., Latella, D. & Massink, M. 2001 In : Lecture notes in artificial intelligence. 2031, p. - 16 p.

Research output: Scientific - peer-reviewArticle

Hooggespannen verwachtingen model checking

Brinksma, H. & Katoen, J. P. 2001 In : Bits en chips. 3, 4, p. - 4 p.

Research output: ProfessionalArticle

Hooggespannen verwachtingen model checking

Brinksma, H. & Katoen, J. P. 2001 In : Bits en chips. 3, 4, p. 31-34 4 p.

Research output: ScientificArticle

16 Citations

Metric semantics for true concurrent real time

Katoen, J. P., Baier, C. & Latella, D. 2001 In : Theoretical computer science. 254, 1/2, p. 501-542 42 p., 10.1016/S0304-3975(99)00342-4

Research output: Scientific - peer-reviewArticle

Semantics
Equivalence classes
Algebra
Synchronization

Performance analysis := (process algebra + model checking) x Markov chains

Hermanns, H. & Katoen, J. P. 2001 In : Lecture notes in artificial intelligence. 2154, p. - 23 p.

Research output: Scientific - peer-reviewArticle

2000

Automated compositional Markov chain generation for a plain-old telephone system

Hermanns, H. & Katoen, J. P. 2000 In : Science of computer programming. 36, 1, p. 97-127 31 p.

Research output: Scientific - peer-reviewArticle

58 Citations

Automated compositional Markov chain generation for a plain-old telephone system

Hermanns, H. & Katoen, J. P. Jan 2000 In : Science of computer programming. 36, 1, p. 97-127 31 p.

Research output: Scientific - peer-reviewArticle

Telephone systems
Markov processes
Random processes
Algebra
Queueing networks

Pattern-matching algorithms based on term rewrite systems

Katoen, J. P. & Nymeyer, A. 2000 In : Theoretical computer science. 238, 1-2, p. 439-463 25 p., 10.1016/S0304_3975(00)00041-4

Research output: Scientific - peer-reviewArticle

Redundancy

On generative parallel composition

d' Argenio, P. R., Hermanns, H. & Katoen, J. P. 1999 In : Theoretical computer science. 22, p. - 25 p.

Research output: Scientific - peer-reviewArticle

1998

A consistent causality-based view on a fined process algebra including urgent interaction

Katoen, J. P., Latella, D., Langerak, R., Brinksma, H. & Bolognesi, T. 1998 In : Formal methods in system design. 12, 2, p. 189-216 28 p.

Research output: Scientific - peer-reviewArticle

14 Citations

A consistent causality-based view on a timed process algebra including urgent interactions

Katoen, J. P., Latella, D., Langerak, R., Brinksma, H. & Bolognesi, T. 1998 In : Formal methods in system design. 12, 2, p. 189-216 28 p.

Research output: Scientific - peer-reviewArticle

Semantics
Algebra
Specification languages
17 Citations

Automatic verification of a lip-synchronisation protocol using Uppaal

Bowman, H., Faconti, G., Katoen, J-P., Latella, D. & Massink, M. 1998 In : Formal aspects of computing. 10, p. 550-575 26 p., 10.1007/s001650050032

Research output: Scientific - peer-reviewArticle

Synchronization
Specifications
Jitter
Formal verification
Formal specification