Research Output 1992 2017

Filter
Conference contribution
2016
5 Citations

The Probabilistic Model Checking Landscape

Katoen, J. P. Jul 2016 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016). USA: ACM, p. 31-45 15 p.

Research output: ScientificConference contribution

Model checking
Distributed computer systems
2015
5 Citations

Fault Trees on a Diet - Automated Reduction by Graph Rewriting

Junges, S., Guck, D., Katoen, J. P., Rensink, A. & Stoelinga, M. I. A. Nov 2015 Proceedings of the First International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015). Li, X., Liu, Z. & Yi, W. (eds.). Berlin: Springer Verlag, p. 3-18 16 p. (Lecture Notes in Computer Science; vol. 9409)

Research output: Scientific - peer-reviewConference contribution

Directed graphs
Scalability
Experiments

Probabilistic Programming: A True Verification Challenge

Katoen, J. P. Oct 2015 Proceedings of the 13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015. Finkbeiner, B., Pu, G. & Zhang, L. (eds.). London: Springer, p. 1-3 3 p. (Lecture Notes in Computer Science; vol. 9364, no. 9364)

Research output: ScientificConference contribution

Competitive intelligence
Describing functions
Epidemiology
Bioinformatics
Semantic Web
2014

Model Checking Gigantic Markov Models

Katoen, J. P. Sep 2014 Proceedings of the 12th International Conference on Software Engineering and Formal Methods, SEFM 2014. Giannakopoulou, D. & Salaün, G. (eds.). London: Springer Verlag, p. xv-xvii 2 p. (Lecture Notes in Computer Science; vol. 8702)

Research output: ScientificConference contribution

4 Citations

Probably safe or live

Katoen, J. P., Song, L. & Zhang, L. Jul 2014 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). New York: ACM, p. 55 10 p.

Research output: Scientific - peer-reviewConference contribution

Hinges
Decomposition
6 Citations

Smart railroad maintenance engineering with stochastic model checking

Guck, D., Katoen, J. P., Stoelinga, M. I. A., Luiten, T. & Romijn, J. Apr 2014 Proceedings of the Second International Conference on Railway Technology: Research, Development and Maintenance, Railways 2014. Pombo, J. (ed.). Stirlingshire, UK: Civil Comp Press, p. 299 15 p. (Civil-Comp Proceedings; vol. 104)

Research output: Scientific - peer-reviewConference contribution

Availability
Fault tree analysis
Costs
Railroads
Railroad engineering
2013

Concurrency meets probability: theory and practice (abstract)

Katoen, J. P. Aug 2013 24th International Conference on Concurrency Theory, CONCUR 2013. London: Springer Verlag, p. 44-45 2 p. (Lecture Notes in Computer Science; vol. 8052)

Research output: ScientificConference contribution

Semantics
Petri nets
Chemical analysis
Linear programming
Markov processes
19 Citations

Modelling, Reduction and Analysis of Markov Automata

Guck, D., Hatefi, H., Hermanns, H., Katoen, J. P. & Timmer, M. Aug 2013 Proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST). Joshi, K. R., Siegle, M., Stoelinga, M. I. A. & d' Argenio, P. R. (eds.). Berlin: Springer, p. 55-71 17 p. (Lecture Notes in Computer Science; vol. 8054)

Research output: Scientific - peer-reviewConference contribution

Petri nets
Static analysis
Semantics
Chemical analysis
3 Citations

Taming confusion for modeling and implementing probabilistic concurrent systems

Katoen, J. P. & Peled, D. Mar 2013 Proceedings of the 22nd European Symposium on Programming (ESOP 2013). Felleisen, M. & Gardner, P. (eds.). London: Springer Verlag, p. 411-430 20 p. (Lecture Notes in Computer Science; vol. 7792)

Research output: Scientific - peer-reviewConference contribution

Petri nets
Scheduling algorithms
Parallel algorithms
2012
21 Citations

Efficient Modelling and Generation of Markov Automata

Timmer, M., Katoen, J. P., van de Pol, J. C. & Stoelinga, M. I. A. 31 Mar 2012 10th Workshop on Quantitative Aspects of Programming Languages, QAPL 2012. Pisa: Istituto di Scienza e Tecnologie dell'Informazione, p. - 4 p.

Research output: ScientificConference contribution

State space
Probabilistic automata
Linearization
Automata
Transform
50 Citations

Formal correctness, safety, dependability, and performance analysis of a satellite

Esteve, M. A., Katoen, J. P., Nguyen, V. Y., Postma, B. & Yushstein, Y. Jun 2012 34th International Conference on Software Engineering, ICSE 2012. USA: IEEE Computer Society, p. 1022-1031 10 p. (ACM Proceedings - International Conference on Software Engineering)

Research output: Scientific - peer-reviewConference contribution

Software engineering
Hybrid systems
14 Citations

GSPNs Revisited: Simple Semantics and New Analysis Algorithms

Katoen, J. P. Jun 2012 12th International Conference on Application of Concurrency to System Design, ACSD 2012. USA: IEEE Computer Society, p. 6-11 6 p.

Research output: ScientificConference contribution

Petri nets
Markov processes
Semantics
Reliability analysis
2 Citations

Model checking: one can do much more than you think!

Katoen, J. P. 2012 Fundamentals of Software Engineering: fourth IPM International Conference, FSEN 2011. Berlin: Springer, p. 1-14 14 p. (Lecture Notes in Computer Science; vol. 7141)

Research output: Scientific - peer-reviewConference contribution

Model checking
Scheduling
Temporal logic
Software design
NASA
28 Citations

Quantitative timed analysis of interactive Markov chains

Guck, D., Han, T., Katoen, J. P. & Neuhausser, M. Apr 2012 4th International Symposium on NASA Formal Methods, NFM 2012. Berlin: Springer, p. 8-23 15 p. (Lecture Notes in Computer Science; vol. 7226)

Research output: Scientific - peer-reviewConference contribution

Markov processes
Scalability
Semantics
2010

Advances in Probabilistic Model Checking

Katoen, J. P. Jan 2010 11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010. Barthe, G. & Hermenegildo, M. (eds.). Berlin: Springer Verlag, p. 25-25 1 p. (Lecture Notes in Computer Science; vol. 5944)

Research output: Scientific - peer-reviewConference contribution

Model checking
Parallel algorithms
Markov processes
Specifications
5 Citations

A linear process-algebraic format for probabilistic systems with data

Katoen, J. P., van de Pol, J. C., Stoelinga, M. I. A. & Timmer, M. Jun 2010 Application of Concurrency to System Design, Tenth International Conference on. Gomes, L., Khomenko, V. & Fernandes, J. M. (eds.). Los Alamitos: IEEE Computer Society Press, p. 213-222 10 p. 10.1109/ACSD.2010.18

Research output: Scientific - peer-reviewConference contribution

Process algebra
Symbolic analysis
Probabilistic automata
Linear process
Bisimulation

Quantitative Verification in Practice

Haverkort, B. R. H. M., Katoen, J. P. & Larsen, K. G. 2010 4th International Symposium on Leveraging Applications, ISoLA 2010. Berlin: Springer Verlag, p. 127-127 1 p. (Lecture Notes in Computer Science; vol. 6416)

Research output: ScientificConference contribution

Systems analysis
Model checking
Embedded systems
Data structures
Cables
24 Citations

The How and Why of Interactive Markov Chains

Hermanns, H. & Katoen, J. P. 2010 Symposium on Formal Methods for Components and Objects, FMCO 2009. de Boer, F. S., Bonsangue, S. H. & Leuschel, M. (eds.). Berlin: Springer Verlag, p. 311-337 27 p. (Lecture Notes in Computer Science; vol. 6286)

Research output: Scientific - peer-reviewConference contribution

Model
Generalized stochastic Petri net
Stochastic process algebra
Fault tree
Labeled transition system
2009
24 Citations

Compositional Abstraction of Stochastic Systems

Katoen, J. P., Klink, D. & Neuhausser, M. 3 Sep 2009 Formal Modeling and Analysis of Timed Systems. Berlin: Springer Verlag, p. 195-211 17 p. 10.1007/978-3-642-04368-0_16. (Lecture Notes in Computer Science; vol. 5813)

Research output: Scientific - peer-reviewConference contribution

Markov chain
Transition systems
Reachability
Stochastic systems
Correctness
29 Citations

Delayed Nondeterminism in Continuous-Time Markov Decision Processes

Neuhausser, M., Stoelinga, M. I. A. & Katoen, J. P. 27 Mar 2009 Foundations of Software Science and Computational Structures. Berlin: Springer Verlag, p. 364-379 16 p. 10.1007/978-3-642-00596-1_26. (Lecture Notes in Computer Science; vol. 5504)

Research output: Scientific - peer-reviewConference contribution

21 Citations

Maximizing System Lifetime by Battery Scheduling

Jongerden, M. R., Haverkort, B. R. H. M., Bohnenkamp, H. C. & Katoen, J. P. 29 Jun 2009 Proceedings of the 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2009. Los Alamitos: IEEE Computer Society Press, p. 63-72 10 p.

Research output: Scientific - peer-reviewConference contribution

Scheduling
Mobile devices
Recovery
25 Citations

Quantitative model checking of continuous-time Markov chains against timed automata specifications

Chen, T., Han, T., Katoen, J. P. & Mereacre, A. Aug 2009 2009 24th Annual IEEE Symposium on Logic In Computer Science. Piscataway: IEEE Computer Society, p. 309-318 10 p. 10.1109/LICS.2009.21

Research output: Scientific - peer-reviewConference contribution

System of integral equations
Timed automata
Reachability
Path
Computing
10 Citations

Simulation-based CTMC Model Checking: An Empirical Evaluation

Katoen, J. P. & Zapreev, I. S. Sep 2009 Sixth International Conference on the Quantitative Evaluation of Systems. Los Alamitos: IEEE Computer Society Press, p. 31-40 10 p. 10.1109/QEST.2009.25

Research output: Scientific - peer-reviewConference contribution

Model checking
Acceptance sampling
Sequential sampling
Continuous-time Markov chain
Hypothesis testing

Symmetry reduction for stochastic hybrid systems

Bujorianu, L. M. & Katoen, J. P. 6 Jan 2009 47th IEEE Conference on Decision and Control, CDC 2008. Los Alamitos: IEEE Computer Society, p. 233-238 6 p. 10.1109/CDC.2008.4739086

Research output: Scientific - peer-reviewConference contribution

Hybrid systems
Model checking
Observability
66 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. Sep 2009 Sixth International Conference on the Quantitative Evaluation of Systems. Los Alamitos: IEEE Computer Society Press, p. 167-176 10 p. 10.1109/QEST.2009.11

Research output: Scientific - peer-reviewConference contribution

Model checking
Discrete event simulation
1 Citations

Time-Bounded Reachability in Tree-Structured QBDs by Abstraction

Klink, D., Remke, A. K. I., Haverkort, B. R. H. M. & Katoen, J. P. Sep 2009 Sixth International Conference on the Quantitative Evaluation of Systems, (QEST '09). IEEE Computer Society, p. 133-142 10 p. 10.1109/QEST.2009.9

Research output: Scientific - peer-reviewConference contribution

Reachability
Probabilistic automata
Birth-death process
Pushdown automata
Uniformization
2008
30 Citations

Approximate parameter synthesis for probabilistic time-bounded reachability

Han, T., Katoen, J. P. & Mereacre, A. Dec 2008 Proceedings of the IEEE Real-Time Systems Symposium (RTSS 2008). Los Alamitos: IEEE Computer Society Press, p. 173-182 10 p. 10.1109/RTSS.2008.19

Research output: Scientific - peer-reviewConference contribution

Real time systems
Markov processes
Polynomials
9 Citations

Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains

Han, T., Katoen, J. P. & Mereacre, A. Apr 2008 Hybrid Systems: Computation and Control (HSCC). Berlin: Springer Verlag, p. 244-258 15 p. 10.1007/978-3-540-78929-1. (Lecture Notes in Computer Science; vol. 4981, no. 69160R)

Research output: Scientific - peer-reviewConference contribution

Bisimulation
Piecewise deterministic Markov process
Congruence relation
Continuous-time Markov chain
Rate function
37 Citations

How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison

Jansen, D. N., Katoen, J. P., Oldenkamp, M., Stoelinga, M. I. A. & Zapreev, I. S. Feb 2008 Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007. Yohav, K. (ed.). London: Springer Verlag, p. 69-85 17 p. 10.1007/978-3-540-77966-7_9. (Lecture Notes in Computer Science; vol. 4899, no. 2008/16200)

Research output: Scientific - peer-reviewConference contribution

experiment
11 Citations

Perspectives in probabilistic verification

Katoen, J. P. Jun 2008 Proceedings 2nd IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering. Los Alamitos: IEEE Computer Society, p. 3-10 8 p. 10.1109/TASE.2008.44

Research output: ScientificConference contribution

Model checking
Finite automata
Parallel algorithms

Reachability in continuous-time Markov reward decision processes

Baier, C., Haverkort, B. R. H. M., Hermanns, H. & Katoen, J. P. Feb 2008 Logic and Automata: History and Perspectives. Flum, J., Graedel, E. & Wilke, T. (eds.). Amsterdam: Amsterdam University Press, p. 53-71 19 p. (Texts in Logic and Games; vol. 2)

Research output: Scientific - peer-reviewConference contribution

Polynomials
13 Citations

Regular Expressions for PCTL Counterexamples

Damman, B., Han, T. & Katoen, J. P. Sep 2008 Proceedings of the 5th International Conference on the Quantitative Evaluaiton of Systems (QEST 2008). Los Alamitos: IEEE Computer Society Press, p. 179-188 10 p. 10.1109/QEST.2008.11

Research output: Scientific - peer-reviewConference contribution

Markov processes
Experiments
5 Citations

Time-Abstracting Bisimulation for Probabilistic Timed Automata

Chen, T., Han, T. & Katoen, J. P. Jun 2008 Proceedings of the 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE). IEEE Computer Society, p. 177-184 8 p. 10.1109/TASE.2008.29

Research output: Scientific - peer-reviewConference contribution

Bisimulation
Timed automata
Probabilistic automata
Equivalence class
Polyhedron
2007
13 Citations

Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes

Neuhausser, M. & Katoen, J. P. Sep 2007 18th International Conference on Concurrency Theory (CONCUR). London: Springer Verlag, p. 412-427 16 p. 10.1007/978-3-540-74407-8_28. (Lecture Notes in Computer Science; vol. 4703, no. Supplement)

Research output: Scientific - peer-reviewConference contribution

Bisimulation
Markov decision process
Continuous time
Measure theory
Continuous-time Markov chain
73 Citations

Bisimulation minimisation mostly speeds up probabilistic model checking

Katoen, J. P., Katoen, J. P., Kemna, T., Zapreev, I. S. & Jansen, D. N. 2007 Tools and algorithms for the construction and analysis of systems. Grumberg, O. & Huth, M. (eds.). Berlin: Springer, p. 87-101 15 p. 10.1007/978-3-540-71209-1_9. (Lecture notes in computer science; vol. 4424, no. 2)

Research output: Scientific - peer-reviewConference contribution

Model checking
Markov processes
36 Citations

Counterexamples in probabilistic model checking

Han, T. & Katoen, J. P. 31 Jul 2007 Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems. Grumberg, O. & Huth, M. (eds.). Berlin, Germany: Springer Verlag, p. 72-86 15 p. 10.1007/978-3-540-71209-1_8. (Lecture Notes in Computer Science; vol. 4424, no. Supplement)

Research output: Scientific - peer-reviewConference contribution

Counterexample
Probability bounds
Shortest path algorithm
Shortest path problem
Reachability
10 Citations

Motor: The MoDeST Tool Environment

Bohnenkamp, H. C., Hermanns, H. & Katoen, J. P. 2007 Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems. Berlin: Springer Verlag, p. 500-504 5 p. 10.1007/978-3-540-71209-1_38. (Lecture Notes in Computer Science; vol. 4424, no. Supplement)

Research output: Scientific - peer-reviewConference contribution

Performance evaluation
Language modeling
Simulation
Formal semantics
13 Citations

Providing evidence of likely being on time - Counterexample generation for CTMC model checking

Han, T. & Katoen, J. P. 2007 Providing evidence of likely being on time: Counterexample generation for CTMC model checking. Namjoshi, K., Yoneda, T., Higashino, T. & Okamura, Y. (eds.). Springer, p. 331-346 16 p. 10.1007/978-3-540-75596-8_24. (Lecture Notes in Computer Science; vol. 4762, no. Supplement)

Research output: Scientific - peer-reviewConference contribution

Diagnostics
Violations
2006
3 Citations

Bisimulation and Simulation Relations for Markov Chains

Baier, C., Hermanns, H., Katoen, J. P. & Wolf, V. 2006 Essays on Algebraic Process Calculi. Aceto, L. & Gordon, A. (eds.). Amsterdam: ELSEVIER, p. 73-78 6 p. (Electronic Notes in Theoretical Computer Science; vol. 162, no. 10)

Research output: ScientificConference contribution

Markov processes
Algebra

Probably on time and within budget - On reachability in priced probabilistic timed automata

Berendsen, J., Jansen, D. N. & Katoen, J. P. Sep 2006 Quantitative Evaluation of Systems (QEST). Los Alamitos: IEEE Computer Society, p. 311-322 12 p. 10.1109/QEST.2006.43

Research output: Scientific - peer-reviewConference contribution

Timed automata
Reachability
Termination
Branching
Exceed
14 Citations

Safe on-the-fly steady-state detection for time-bounded reachability

Katoen, J. P. & Zapreev, I. S. Sep 2006 Quantitative Evaluation of Systems (QEST). Los Alamitos: IEEE Computer Society Press, p. 301-310 10 p. 10.1109/QEST.2006.47

Research output: Scientific - peer-reviewConference contribution

Markov processes
Model checking
Transient analysis
Experiments
7 Citations

Safety and Liveness in Concurrent Pointer Programs

Distefano, D. S., Katoen, J. P. & Rensink, A. 2006 Proceedings of the 4th Internatinal Symposium on Formal Methods for Components and Objects. de Boer, F. S., Bonsangue, M. M., Graf, S. & de Roever, W-P. (eds.). Berlin: Springer Verlag, p. 280-312 33 p. 10.1007/11804192_14. (Lecture Notes in Computer Science; vol. 4111, no. suppl 2/4111)

Research output: Scientific - peer-reviewConference contribution

Temporal logic
Model checking
8 Citations

Towards a logic for performance and mobility

De Nicola, R., Katoen, J. P., Latella, D. & Massink, M. 2006 3rd Workshop on Quantitative Aspects of Programming Languages. Cerone, A. & Wiklicky, H. (eds.). Amsterdam: ELSEVIER, p. 161-175 15 p. (Electronic Notes in Theoretical Computer Science; vol. 153, no. 2)

Research output: Scientific - peer-reviewConference contribution

Modeling
Dynamic systems
Programming
Quantitative analysis
Symposium
14 Citations

YMCA: Why Markov Chain Algebra?

Bravetti, M., Hermanns, H. & Katoen, J. P. 2006 Essays on Algebraic Process Calculi. Aceto, L. & Gordon, A. (eds.). Amsterdam: ELSEVIER, p. 107-112 6 p. (Electronic Notes in Theoretical Computer Science; vol. 162, no. 10)

Research output: ScientificConference contribution

Continuous-time Markov chain
Markov chain
System reliability
Concurrency
System performance
2005
156 Citations

A Markov reward model checker

Katoen, J. P., Maneesh Khattri, M., Zapreev, I. S. & Zapreev, I. S. 2005 2nd Int. Conf. on Quantitative Evaluation of Systems. Los Alamitos, California: IEEE Computer Society, p. 243-245 3 p.

Research output: Scientific - peer-reviewConference contribution

7 Citations

Are You Still There? - A Lightweight Algorithm to Monitor Node Presence in Self-Configuring Networks

Bohnenkamp, H. C., Gorter, J., Gorter, J., Guidi, J. & Katoen, J. P. 2005 Int. Conf. on Dependable Systems and Networks. Los Alamitos, California: IEEE Computer Society, p. 704-709 7 p.

Research output: Scientific - peer-reviewConference contribution

Parallel algorithms
Personal digital assistants
Mobile phones
Topology
Availability
21 Citations

Model Checking Markov Reward Models with Impulse Rewards

Cloth, L., Katoen, J. P., Maneesh Khattri, M. & Pulungan, R. Jul 2005 Int. Conf. on Dependable Systems and Networks. Dr. Bondavalli, A., Prof.dr.ir. Haverkort, B. R. H. M. & Prof. Tang, D. (eds.). Los Alamitos: IEEE Computer Society, p. 722-731 10 p.

Research output: Scientific - peer-reviewConference contribution

Model checking
Markov processes
Energy utilization
Power management
2004

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. 29 Mar 2004 Tools and algorithms for the construction and analysis of systems. Jensen, K. & Podelski, A. (eds.). Berlin: Springer, p. 61-76

Research output: Scientific - peer-reviewConference contribution

Embedded software analysis with MOTOR

Katoen, J. P., Bohnenkamp, H. C., Klaren, J. & Hermanns, H. 13 Sep 2004 Formal methods for the design of real-time systems. Bernardo, M. & Corradini, F. (eds.). Berlin: Springer, p. 268-293

Research output: Scientific - peer-reviewConference contribution

Quality of service
11 Citations

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: Scientific - peer-reviewConference contribution