Research Output 1992 2018

Filter
Report
2013

Correct and Efficient Accelerator Programming (Dagstuhl Seminar 13142)

Cohen, A., Donaldson, A. F., Huisman, M. & Katoen, J. P. 2013 Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 17 p.

Research output: ScientificReport

Technical presentations
Particle accelerators
Computer science

Modelling, Reduction and Analysis of Markov Automata (extended version)

Guck, D., Hatefi, H., Hermanns, H., Katoen, J. P. & Timmer, M. 30 May 2013 Ithaca, NY, USA: Cornell University. 27 p.

Research output: ScientificReport

Petri nets
Static analysis
Semantics
Chemical analysis
2012

Efficient Modelling and Generation of Markov Automata (extended version)

Timmer, M., Katoen, J. P., van de Pol, J. C. & Stoelinga, M. I. A. 11 Jun 2012 Enschede: Centre for Telematics and Information Technology (CTIT). 35 p. (CTIT Technical Report Series; no. TR-CTIT-12-16)

Research output: ScientificReport

Specifications
Syntactics
Linearization
Chemical analysis
2010
Process algebra
Symbolic analysis
Probabilistic automata
Linear process
Bisimulation
2008
1 Citations

Symmetry Reduction For Stochastic Hybrid Systems

Bujorianu, L. M. & Katoen, J. P. 18 Mar 2008 Enschede: Centre for Telematics and Information Technology (CTIT). 25 p. (CTIT Technical Report Series; no. TR-CTIT-08-27)

Research output: ProfessionalReport

Model checking
Hybrid systems
Observability
2006
20 Citations

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

Berendsen, J., Jansen, D. N. & Katoen, J. P. Jun 2006 Enschede: Centrum voor Telematica en Informatie Technologie. 29 p. (CTIT Technical Report Series; no. 06-26)

Research output: ProfessionalReport

Timed automata
Reachability
Termination
Branching
Exceed
2005

Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability

Katoen, J. P. & Zapreev, I. S. Nov 2005 Enschede: Formal Methods and Tools (FMT). 32 p. (CTIT Technical Report Series; no. TR-CTIT-05-52)

Research output: ProfessionalReport

Model checking
Transient analysis
Experiments
2004

Comparative Branching-Time Semantics for Markov Chains

Baier, C., Katoen, J. P., Hermanns, H. & Wolf, V. Aug 2004 Enschede: Centre for Telematics and Information Technology (CTIT). 64 p. (1381-3625; no. 04-32)

Research output: ProfessionalReport

Semantics
Temporal logic
Markov processes
7 Citations
Markov decision process
Continuous time
Continuous-time Markov chain
Nondeterminism
Delay time

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

Random processes
Markov processes
Quality of service
Semantics
Specifications

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

Temporal logic
Model checking
Semantics
2002
27 Citations

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: Other research outputReport

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: Other research outputReport

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

2001

Model Checking Dynamic Allocation and Deallocation

Distefano, D. S., Rensink, A. & Katoen, J. P. Dec 2001 Enschede: Centre for Telematics and Information Technology (CTIT). (CTIT technical report series; no. TR-CTIT-01-40)

Research output: Other research outputReport

Temporal logic
Tableau
Operational semantics
Model checking
Automata
2000

n a Temporal Logic for Object-Based Systems

Distefano, D. S., Katoen, J. P. & Rensink, A. 2000 Enschede: Centre for Telematics and Information Technology (CTIT). 17 p.

Research output: ProfessionalReport

1998
1997
17 Citations

Causal ambiguity and partial orders in event structures

Langerak, R., Brinksma, H. & Katoen, J. P. Apr 1997 Enschede: Centre for Telematics and Information Technology (CTIT). 21 p. (CTIT technical report series; no. TR-CTIT-97-11)

Research output: ProfessionalReport

Semantics
Syntactics
Model structures
41 Citations

The Bounded Retransmission Protocol must be on time!

d' Argenio, P. R., Katoen, J. P., Ruys, T. C. & Tretmans, G. J. 1997 Enschede: Centre for Telematics and Information Technology (CTIT). 63 p. (CTIT technical report; no. 97-03)

Research output: ProfessionalReport

Model checking
1996

B-ISDN to the Cell Site Switch versus B-ISDN the Mobile Terminal

Karagiannis, G., Katoen, J. P. & Niemegeers, I. G. M. M. 1996 University of Twente, Enschede: Centre for Telematics and Information Technology (CTIT). 5 p.

Research output: ProfessionalReport

Modelling and Verifying a Bounded Retransmission Protocol

Tretmans, G. J., d' Argenio, P. R., Katoen, J. P. & Ruys, T. C. 1996 University of Twente, Enschede: Centre for Telematics and Information Technology (CTIT). 14 p.

Research output: ProfessionalReport

1993

Evolution Strategies Towards UMTS

Katoen, J. P. & Kremer, H. H. C. 30 Sep 1993 Enschede: Universiteit Twente.

Research output: ProfessionalReport