Publications of David N. Jansen

2016

; : Stuttering equivalence is too slow! Eprint arXiv: 1603.05789, 2016. Online version

; ; : Minimal separating sequences for all pairs of states. In: Dediua, Adrian-Horia; Janoušek, Jan; Martín-Vide, Carlos; Truthe, Bianca (eds.): Languages and automata theory and applications: ... LATA. [s. l.]: Springer, 2016. (Lecture notes in computer science, 9618). pp. 181–193. Online version

; ; ; ; : Multiphase until formulas over Markov reward models: an algebraic approach. Theoretical Computer Science 611, 2016. pp. 116–135. Online version

; : A space-efficient simulation algorithm on probabilistic automata. Information and Computation 249, 2016. pp. 138–159. Online version

2015

; ; ; Li, Yong; ; ; ; : A comparative study of BDD packages for probabilistic symbolic model checking.. In: Li, Xuandong; Liu, Zhiming; Yi, Wang (eds.): Dependable software engineering: theories, tools, and applications; ... SETTA. Cham: Springer, 2015. (Lecture notes in computer science, 9409). pp. 35–51. Online version

Smeenk, Wouter; ; ; : Applying automata learning to embedded control software. In: Butler, Michael; Conchon, Sylvain; Zaïdi, Fatiha (ed.): Formal methods and software engineering: ... ICFEM. Cham: Springer, 2015. (Lecture notes in computer science, 9407). pp. 67–83. Online version

2014

; ; : On abstraction of probabilistic systems. In: Remke, Anne; Stoelinga, Mariëlle (eds.): Stochastic model checking: rigorous dependability analysis using model checking techniques for stochastic systems; international autumn school, ROCKS 2012. Heidelberg: Springer, 2014. (Lecture Notes in Computer Science, 8453). pp. 87–116. Online version

2013

: More or less true: DCTL for continuous-time MDPs. In: Braberman, Víctor; Fribourg, Laurent (eds.): Formal modeling and analysis of timed systems: ... FORMATS. Heidelberg: Springer, 2013. (Lecture notes in computer science, 8053). pp. 137–151. Online version

: More or less true: DCTL for continuous-time MDPs. Nijmegen: Radboud Universiteit, 2013. (Technical Report, ICIS-R13006). Online version

; ; : Revisiting weak simulation for substochastic Markov chains. In: Joshi, Kaustubh; Siegle, Markus; Stoelinga, Mariëlle; D’Argenio, Pedro (eds.): Quantitative evaluation of systems: ... QEST. Heidelberg: Springer, 2013. (Lecture notes in computer science, 8054). pp. 209–224. Online version
Please note that we have refuted Conjecture 26 in the meantime. The following technical report contains an appendix with a counterexample.

; ; : Revisiting weak simulation for substochastic Markov chains. Nijmegen: Radboud Universiteit, 2013. (Technical Report, ICIS-R13005). Online version

2012

; ; : Belief bisimulation for hidden Markov models: logical characterisation and decision algorithm. In: Goodloe, Alwyn E.; Person, Suzette (eds.): NASA formal methods: ... NFM. Heidelberg: Springer, 2012. (Lecture notes in computer science, 7226). pp. 326–340. Online version

; ; : Belief bisimulation for hidden Markov models: logical characterisation and decision algorithm. Nijmegen: Radboud Universiteit, 2012. (Technical report, ICIS-R12002). Online version

; ; ; : Efficient CSL model checking using stratification. Logical methods in computer science 8 (2), 2012. Paper 17. Online version

2011

: Erratum to: Model-checking continuous-time Markov chains by Aziz et al. Eprint arXiv: 1102.2079, 2011. Online version

: Understanding Fox and Glynn’s “Computing Poisson probabilities”. Nijmegen: Radboud Universiteit, 2011. (Technical report, ICIS-R11001) Online version

; ; ; ; : The ins and outs of the probabilistic model checker MRMC. Performance Evaluation 68 (2), 2011. pp. 90–104. Online version

; ; ; : Automata-based CSL model checking. In: Aceto, Luca; Henzinger, Monika; Sgall, Jiří (eds.): Automata, languages and programming: ... ICALP. Part II. Heidelberg: Springer, 2011. (Lecture notes in computer science, 6756). pp. 271–282. Online version

; ; ; : Automata-based CSL model checking. Eprint arXiv: 1104.4983, 2011. Online version

2010

; ; ; : The axiomatization of override and update. Journal of applied logic 8 (1), 2010. pp. 141–150. Online version

; ; : Fortuna: model checking priced probabilistic timed automata. In: QEST 2010: Seventh international conference on the quantitative evaluation of systems. Los Alamitos, CA: IEEE Computer Society, 2010. pp. 273–281. Online version

; ; : The impact of GSM-R on railway capacity. In: Ning, B. (ed.): Advanced train control systems. Southampton: WIT, 2010. pp. 143–152. Online information

; ; ; ; ; : Synthesis and stochastic assessment of cost-optimal schedules. International journal on software tools for technology transfer 12 (5), 2010. pp. 305–318. Online version

2009

; ; : 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. Berlin: Springer, 2009. (Lecture notes in computer science, 5532). pp. 128–137. Online version
Errata:

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

; ; 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

; ; : 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. (eds.): Computers in railways XI. Southampton: WIT, 2008. pp. 233–242. Online version

; ; ; : Flow faster: efficient decision algorithms for probabilistic simulations. Logical methods in computer science 4 (4), 2008. Paper 6. Online version

2007

; ; ; ; : 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. Berlin: Springer, 2008. (Lecture notes in computer science, 4899). pp. 69–85. Online version

; Kemna, Tim; ; : 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. Berlin: Springer, 2007. (Lecture notes in computer science, 4424). pp. 87–101. Online version

; ; ; : Flow faster: efficient decision algorithms for probabilistic simulations. In: Grumberg, Orna; Huth, Michael (eds.): Tools and algorithms for the construction and analysis of systems: ... TACAS. Berlin: Springer, 2007. (Lecture notes in computer science, 4424). pp. 155–169. Online version

2006

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

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

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

; ; : A comparative reliability analysis of ETCS train radio communications. Transregional Collaborative Research Center 14 AVACS, Germany, February 2005. (Technical report, 2) Online version

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

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

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

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

2004

; ; ; ; : 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.

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

2003

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

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

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

: 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

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

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

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

2001

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

; : 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.)

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

Master theses under the supervision of David N. Jansen

Vos, Mathijs: [Compressing the MPX signal for FM audio.] Started March 2015.

van de Goor, Martin: Indoor localization in wireless sensor networks. Finished March 2009.

Oldenkamp, Marcel: Experimental comparison of probabilistic model checkers. Finished May 2007. (See also our publication How fast and fat is your probabilistic model checker? in 2007.)

ter Horst, Ivo: Performance evaluation in an early development phase. Finished February 2007.
From the abstract: Performance evaluation of combat management systems at Thales Naval Nederland is currently performed too late in the development process. Failure to meet performance goals can be costly and should be avoided, so early discovery of problems is important. Instead of the calculations in large Excel sheets which were used, this thesis presents a UML model with which the structure and performance information of a system can clearly be defined.
Performance information can be added to all elements of the structural model of a system in terms of budgets. A budget defines an amount of resources provided by the hardware or required by the software system.
As the UML models of systems tend to grow large and a lot of budgets and constraints are added, evaluation of the constraints becomes a hard task. Automatic constraint verification is therefore provided by our System Verifier Tool, which integrates with Rational Software Architect (RSA), the tool used within Thales to create UML models.

Kemna, Tim: Bisimulation Minimisation and Probabilistic Model Checking. Finished August 2006. (See also our publication Bisimulation minimisation mostly speeds up probabilistic model checking in 2007.)

: Reachability in Weighted Probabilistic Timed Automata. Finished December 2005. (See also our publications Probably on time and within budget in 2006.)

Bachelor theses under the supervision of David N. Jansen

Top, Joep: Een BASS-FinLog architectuuranalyse. Finished January 2014.

Yanik, Koray: Hoe ontwerpt men een minimalistisch maar functioneel besturingssysteem met zo min mogelijk geheugen- en processorverbruik? Finished August 2012.

August 2015, David N. Jansen