Jansen, David N.; Prabhakar, Pavithra (eds.): Formal Modeling and Analysis of Timed Systems: 16th International Conference, FORMATS 2018; Beijing, China, September 4–6, 2018; Proceedings. Cham: Springer, 2018. (Lecture notes in computer science, 11022). Online version
Li, Yongjian; Duan, Kaiqiang; Jansen, David N.; Pang, Jun; Zhang, Lijun; Lv, Yi; Cai, Shaowei: An automatic proving approach to parameterized verification. ACM transactions on computational logic 2018. Forthcoming.
Zhang, Lijun; Yang, Pengfei; Song, Lei; Hermanns, Holger; Eisentraut, Christian; Jansen, David N.; Godskesen, Jens Chr.: Probabilistic bisimulation for realistic schedulers. Acta informatica 55 (6), 2018. pp. 461–488. Online version
Feng, Yijun; Zhang, Lijun; Jansen, David N.; Zhan, Naijun; Xia, Bican: Finding polynomial loop invariants for probabilistic programs. In: D’Souza, Deepak; Narayan Kumar, K. (eds.): Automated technology for verification and analysis: ... ATVA. Cham: Springer, 2017. (Lecture notes in computer science, 10482). pp. 400–416. Online version
Feng, Yijun; Zhang, Lijun; Jansen, David N.; Zhan, Naijun; Xia, Bican: Finding polynomial loop invariants for probabilistic programs. Eprint arXiv: 1707.02690, 2017. Online version
Fu, Chen; Deng, Yuxin; Jansen, David N.; Zhang, Lijun: On equivalence checking of nondeterministic finite automata. In: Larsen, Kim Guldstrand; Sokolsky, Oleg; Wang, Ji (eds.): Dependable software engineering: theories, tools and applications; ... SETTA. Cham: Springer, 2017. (Lecture notes in computer sciennce, 10606). pp. 216–231. Online version
Groote, Jan Friso; Jansen, David N.; Keiren, Jeroen J. A.; Wijs, Anton: An O(m log n) algorithm for computing stuttering equivalence and branching bisimulation. ACM transactions on computational logic 18 (2), 2017. Article 13. Online version
Yang, Pengfei; Jansen, David N.; Zhang, Lijun: Distribution-based bisimulation for labelled Markov processes. In: Abate, Alessandro; Geeraerts, Gilles (eds.): Formal modeling and analysis of timed systems: ... FORMATS. Cham: Springer, 2017. (Lecture notes in computer science, 10419). pp. 170–186. Online version
Some proofs are not published here, but only in an appendix, which was available to the reviewers and is included in the following technical report.
Yang, Pengfei; Jansen, David N.; Zhang, Lijun: Distribution-based bisimulation for labelled Markov processes. Eprint arXiv: 1706.10049, 2017. Online version
Jansen, David N.; Keiren, Jeroen J. A.: Stuttering equivalence is too slow! Eprint arXiv: 1603.05789, 2016. Online version
Smetsers, Rick; Moerman, Joshua; Jansen, David N.: 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
Xu, Ming; Zhang, Lijun; Jansen, David N.; Zhu, Huibiao; Yang, Zongyuan: Multiphase until formulas over Markov reward models: an algebraic approach. Theoretical computer science 611, 2016. pp. 116–135. Online version
Zhang, Lijun; Jansen, David N.: A space-efficient simulation algorithm on probabilistic automata. Information and computation 249, 2016. pp. 138–159. Online version
van Dijk, Tom; Hahn, Ernst Moritz; Jansen, David N.; Li, Yong; Neele, Thomas; Stoelinga, Mariëlle; Turrini, Andrea; Zhang, Lijun: 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; Moerman, Joshua; Vaandrager, Frits; Jansen, David N.: 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
Dehnert, Christian; Gebler, Daniel; Volpato, Michele; Jansen, David N.: 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
Jansen, David N.: 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
Jansen, David N.: More or less true: DCTL for continuous-time MDPs. Nijmegen: Radboud Universiteit, 2013. (Technical Report, ICIS-R13006). Online version
Jansen, David N.; Song, Lei; Zhang, Lijun: 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.
Jansen, David N.; Song, Lei; Zhang, Lijun: Revisiting weak simulation for substochastic Markov chains. Nijmegen: Radboud Universiteit, 2013. (Technical Report, ICIS-R13005). Online version
Jansen, David N.; Nielson, Flemming; Zhang, Lijun: 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
Jansen, David N.; Nielson, Flemming; Zhang, Lijun: Belief bisimulation for hidden Markov models: logical characterisation and decision algorithm. Nijmegen: Radboud Universiteit, 2012. (Technical report, ICIS-R12002). Online version
Zhang, Lijun; Jansen, David N.; Nielson, Flemming; Hermanns, Holger: Efficient CSL model checking using stratification. Logical methods in computer science 8 (2), 2012. Paper 17. Online version
Jansen, David N.: Erratum to: Model-checking continuous-time Markov chains by Aziz et al. Eprint arXiv: 1102.2079, 2011. Online version
Jansen, David N.: Understanding Fox and Glynn’s “Computing Poisson probabilities”. Nijmegen: Radboud Universiteit, 2011. (Technical report, ICIS-R11001) Online version
Katoen, Joost-Pieter; Zapreev, Ivan S.; Hahn, Ernst Moritz; Hermanns, Holger; Jansen, David N.: The ins and outs of the probabilistic model checker MRMC. Performance evaluation 68 (2), 2011. pp. 90–104. Online version
Zhang, Lijun; Jansen, David N.; Nielson, Flemming; Hermanns, Holger: 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
Zhang, Lijun; Jansen, David N.; Nielson, Flemming; Hermanns, Holger: Automata-based CSL model checking. Eprint arXiv: 1104.4983, 2011. Online version
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
Berendsen, Jasper; Jansen, David N.; Vaandrager, Frits: 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
Jansen, D. N.; Klabes, S. G.; Wendler, E.: The impact of GSM-R on railway capacity. In: Ning, B. (ed.): Advanced train control systems. Southampton: WIT, 2010. pp. 143–152. Online information
Mader, Angelika; Bohnenkamp, Henrik; Usenko, Yaroslav S.; Jansen, David N.; Hurink, Johann; Hermanns, Holger: Synthesis and stochastic assessment of cost-optimal schedules. International journal on software tools for technology transfer 12 (5), 2010. pp. 305–318. Online version
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. Berlin: Springer, 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 modelchecking voor het vwo. In: Vodegel, Frans; Loots, Marijke (ed.): NIOC proceedings. Hogeschool Utrecht, 2009. pp. 135–137. 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. (eds.): Computers in railways XI. Southampton: WIT, 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 (4), 2008. Paper 6. 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. Berlin: Springer, 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. Berlin: Springer, 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 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
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: QEST 2004: First international conference on the quantitative evaluation of systems. 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
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.)
Berendsen, Jasper: Reachability in Weighted Probabilistic Timed Automata. Finished December 2005. (See also our publications Probably on time and within budget in 2006.)
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.
September 2018, David N. Jansen