Berendsen, Jasper; Jansen, David N.; Schmaltz, Julien; Vaandrager, Frits W.: The axiomatization of overriding and update. Journal of applied logic 2010. Online version (The online version will be available shortly.)
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:
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 Model Checking voor het VWO. To appear in Proceedings NIOC 2009, Utrecht, 2009. Online version
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
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
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
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
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
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
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
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
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
November 2009, David N. Jansen