Publications of David N. Jansen

2010

Katoen, Joost-Pieter; Zapreev, Ivan S.; Hahn, Ernst Moritz; Hermanns, Holger; Jansen, David N.: The ins and outs of the probabilistic model checker MRMC. To appear in Performance Evaluation. Online version

Berendsen, Jasper; Jansen, David N.; Vaandrager, Frits: Fortuna: model checking priced probabilistic timed automata. To appear in: Seventh international conference on the quantitative evaluation of systems: QEST 2010. Conference webpage

Mader, Angelika; Bohnenkamp, Henrik; Usenko, Yaroslav S.; Jansen, David N.; Hurink, Johann; Hermanns, Holger: Synthesis and stochastic asessment of cost-optimal schedules. To appear in International journal on software tools for technology transfer. Online version available since November 16, 2009.

Berendsen, Jasper; Jansen, David N.; Schmaltz, Julien; Vaandrager, Frits W.: The axiomatization of override and update. Journal of applied logic 8(1)2010, pp. 141–150. Online version

2009

Berendsen, Jasper; Chen, Taolue; Jansen, David N.: Undecidability of cost-bounded reachability in priced probabilistic timed automata. In: Chen, Jianer; Cooper, S. Barry (eds.): Theory and applications of models of computation: ... TAMC. Springer, Berlin: 2009. (Lecture notes in computer science, 5532). pp. 128–137. Online version
Errata:

• p. 134, Fig. 5 ] The state with cost rate 2 violates the requirement of stopwatch cost (i.e. cost rates ∈ {0,1}). However, one can easily replace this state by one with cost rate 1 and exit guard z = 8–2q.
• p. 135, line 3 from below, “when x_a > 1 the encoding of the counters is incorrect&rdquo ] Because x_a is actually the sum of the old and new encodings of the counters, a correct policy only ensures that x_a ≤ 1+1, but that is enough in this situation.

Katoen, Joost-Pieter; Zapreev, Ivan S.; Hahn, Ernst Moritz; Hermanns, Holger; Jansen, David N.: The ins and outs of the probabilistic model checker MRMC. In: Sixth international conference on the quantitative evaluation of systems: QEST 2009. Los Alamitos, CA: IEEE Computer Society, 2009. pp. 167–176. Online version

Vaandrager, Frits; Jansen, David N.; Koopmans, Els: Een module over modelchecking voor het vwo. In: Vodegel, Frans; Loots, Marijke (ed.): NIOC proceedings. Hogeschool Utrecht, 2009. pp. 135–137. Online version

2008

Jansen, D. N.; Klabes, S. G.; Wendler, E.: The impact of GSM-R on railway capacity. In: Allan, J.; Arias, E.; Brebbia, C. A.; Goodman, C.; Rumsey, A. F.; Sciutto, G.; Tomii, N.: Computers in railways XI. WIT, Southampton: 2008. pp. 233-242. Online version

Zhang, Lijun; Hermanns, Holger; Eisenbrand, Friedrich; Jansen, David N.: Flow faster: efficient decision algorithms for probabilistic simulations. Logical methods in computer science 4(6)2008, pp. 1–43. Online version

2007

Jansen, David N.; Katoen, Joost-Pieter; Oldenkamp, Marcel; Stoelinga, Mariëlle; Zapreev, Ivan: How fast and fat is your probabilistic model checker? An experimental performance comparison. In: Yorav, Karen (ed.): Hardware and software, verification and testing: ... Haifa verification conference, HVC. Springer, Berlin: 2008. (Lecture notes in computer science, 4899). pp. 69–85. Online version

Katoen, Joost-Pieter; Kemna, Tim; Zapreev, Ivan; Jansen, David N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, Orna; Huth, Michael (eds.): Tools and algorithms for the construction and analysis of systems: ... TACAS. Springer, Berlin: 2007. (Lecture notes in computer science, 4424). pp. 87–101. Online version

Zhang, Lijun; Hermanns, Holger; Eisenbrand, Friedrich; Jansen, David N.: Flow faster: efficient decision algorithms for proabilistic simulations. In: Grumberg, Orna; Huth, Michael (eds.): Tools and algorithms for the construction and analysis of systems: ... TACAS. Springer, Berlin: 2007. (Lecture notes in computer science, 4424). pp. 155–169. Online version

2006

Berendsen, Jasper; Jansen, David N.; Katoen, Joost-Pieter: Probably on time and within budget: On reachability in priced probabilistic timed automata. In: Third international conference on the quantitative evaluation of systems: QEST 2006. Los Alamos, CA: IEEE Computer Society, 2006. pp. 311–322. Online version

Berendsen, Jasper; Jansen, David N.; Katoen, Joost-Pieter: Probably on time and within budget: On reachability in priced probabilistic timed automata. Enschede: Centre for Telematics and Information Technology, University of Twente, 2006. (Technical report, TR-CTIT-06-26) Online version

Mader, Angelika; Bohnenkamp, Henrik; Usenko, Yaroslav S.; Jansen, David N.; Hurink, Johann; Hermanns, Holger: Synthesis and stochastic assessment of cost-optimal schedules. Enschede: Centre for Telematics and Information Technology, University of Twente, 2006. (Technical report, TR-CTIT-06-14) Online version

2005

Hermanns, Holger; Jansen, David N.; Usenko, Yaroslav S.: A comparative reliability analysis of ETCS train radio communications. Transregional Collaborative Research Center 14 AVACS, Germany, February 2005. (Technical report, 2) Online version

Hermanns, Holger; Jansen, David N.; Usenko, Yaroslav S.: From StoCharts to MoDeST: a comparative reliability analysis of train radio communications. In: Proceedings of the 5th international workshop on software and performance. Santa Fe, NM: ACM Press, 2005. pp. 13–23. Online version

Jansen, David N.; Hermanns, Holger: QoS modelling and analysis with UML-statecharts: the StoCharts approach. ACM SIGMETRICS Performance Evaluation Review, 32 (4), 2005. pp. 28–33. Online version

Zhang, Lijun; Hermanns, Holger; Jansen, David N.: Logic and model checking for hidden Markov models. In: Wang, Farn (ed.): Formal techniques for networked and distributed systems, FORTE 2005. Berlin: Springer, 2005. (Lecture notes in computer science, 3731) pp. 98–112. Online version

Zhang, Lijun; Hermanns, Holger; Jansen, David N.: Logic and model checking for hidden Markov models. Transregional Collaborative Research Center 14 AVACS, Germany, July 2005. (Technical report, 6) Online version

2004

Bohnenkamp, Henrik C.; Hermanns, Holger; Jansen, David N.; Katoen, Joost-Pieter; Usenko, Yaroslav S.: An industrial-strength formal method: a modest survey. In: Margaria, Tiziana; Steffen, Bernhard; Philippou, Anna; Reitenspieß, Manfred (eds.): International symposium on leveraging applications of formal methods: ISoLA; preliminary proceedings. Dept. of Computer Science, University of Cyprus, 2004. (Technical Report, TR-2004-6) pp. 284–295.

Jansen, David N.; Hermanns, Holger: Dependability checking with StoCharts: Is train radio reliable enough for trains? In: First international conference on the quantitative evaluation of systems: QEST 2004. Los Alamos, CA: IEEE Computer Society, 2004. pp. 250–259. Online version

2003

Jansen, David Nicolaas: Extensions of Statecharts: with probability, time, and stochastic timing. PhD thesis, University of Twente. Bern: Inmarks, 2003. Online version

Jansen, David N.; Hermanns, Holger; Katoen, Joost-Pieter: A QoS-oriented extension of UML statecharts. In: Stevens, Perdita; Whittle, Jon; Booch, Grady (eds.): «UML» 2003, the unified modeling language. Berlin: Springer, 2003. (Lecture notes in computer science, 2863) pp. 76–91. Online version

2002

Eshuis, Rik; Jansen, David N.; Wieringa, Roel: Requirements-level semantics and model checking of object-oriented statecharts. Requirements Engineering, 7 (4, special issue on model checking), December 2002. pp. 243–263. Online version

Jansen, David N.: Probabilistic UML statecharts for specification and verification: a case study. In: Critical systems development with UML: proceedings of the UML'02 workshop. München: Technische Universität, 2002. (Technical report, TUM-I0208) pp. 121–131. Online version

Jansen, David N.; Hermanns, Holger; Katoen, Joost-Pieter: A probabilistic extension of UML statecharts: specification and verification. In: Damm, Werner; Olderog, Ernst-Rüdiger (eds.): Formal techniques in real-time and fault-tolerant systems: ... FTRTFT. Berlin: Springer, 2002. (Lecture notes in computer science, 2469) pp. 355–374. Online version

Jansen, David N.; Hermanns, Holger; Katoen, Joost-Pieter: A probabilistic extension of UML statecharts: specification and verification. Enschede: Centre for Telematics and Information Technology, University of Twente, 2002. (Technical report, TR-CTIT-02-31) Online version

Jansen, David N.; Wieringa, Roel J.: Extending CTL with actions and real time. Journal of logic and computation, 12 (4), 2002. pp. 607–621. Online version

2001

Wieringa, Roel J.; Jansen, David N.: Techniques for reactive system design: the tools in TRADE. In: Dittrich, Klaus R.; Geppert, Andreas; Norrie, Moira C. (eds.): Advanced information systems engineering: ... CAiSE. Berlin: Springer, 2001. (Lecture notes in computer science, 2068) pp. 93–107. Online version

2000

Jansen, David N.; Wieringa, Roel J.: Extending CTL with actions and real-time. In: International conference on temporal logic. s.l.: s.n., 2000. pp. 105–114. (An updated version appeared in the Journal of logic and computation 12 (4), 2002, see above.)

Jansen, David N.; Wieringa, Roel J.: Reducing the extensions of CTL with actions and real time. Enschede: Centre for Telematics and Information Technology, University of Twente, 2000. (Technical report, TR-CTIT-00-27) Online version

June 2010, David N. Jansen