Taolue Chen, Tingting Han and Marta Z. Kwiatkowska. On the complexity of model checking Interval-Valued Discrete Time Markov Chains. In Information Processing Letters, 113(7): 210-216, 2013.
Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Model checking of continuous-time Markov chains against timed automata specifications. In Logical Methods in Computer Science, 7(1): 1-34, 2011.
Tingting Han, Joost-Pieter Katoen and Berteun Damman. Counterexamples in probabilistic model checking. In IEEE Transactions on Software Engineering, 35(2): 241–257, 2009.
Taolue Chen, Tingting Han and Jian Lu. On Behavioral Metric for Probabilistic Systems: Definition and Approximation Algorithm. In Journal of Computer & Mathematics with Application, 57(6):991-999, 2009.
2013
Taolue Chen, Ernst Moritz Hahn, Tingting Han, Marta Z. Kwiatkowska, Hongyang Qu and Lijun Zhang. Model Repair for Markov Decision Processes. In Proc. 7th International Symposium on Theoretical Aspects of Software Engineering (TASE), to appear, 2013.
Lucia Gallina, Andrea Marin, Sabina Rossi, Tingting Han and Marta Kwiatkowska. A Proces-Algebraic Framework for Estimating the Energy Consumption in Ad-hoc Wireless Sensor Networks. In Proc. 16th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM), to appear, 2013.
Tingting Han, Christian Krause, Marta Z. Kwiatkowska and Holger Giese. Abstract probabilistic timed automata. In Proc. 11th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL), pages 66-80, 2013.
2012
Lucia Gallina, Tingting Han, Marta Z. Kwiatkowska, Andrea Marin, Sabina Rossi and Alvise Spanò. Automatic verification of energy and throughput efficiency in mobile ad hoc networks. In Proc. 2012 IFIP Wireless Days Conference (WD), pages 1-6, 2012.
Dennis Guck, Tingting Han, Joost-Pieter Katoen and Martin R. Neuhaeusser. Quantitative timed analysis of interactive Markov chains. In Proceeding of NASA Formal Methods Symposium (NFM), Volume 7226 of Lecture Notes in Computer Science, pages 8-23, 2012.
2011
Lu Feng, Tingting Han, Marta Z. Kwiatkowska and David Parker. Learning-based compositional verification for synchronous probabilistic systems. In Proc. 9th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 6996 of Lecture Notes in Computer Science, pages 511-521, 2011.
Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Observing continuous-time MDPs by 1-clock timed automata. In Proc. 5th International Workshop on Reachability Problems (RP), volume 6945 of Lecture Notes in Computer Science, pages 2-25, 2011.
Ernst Moritz Hahn, Tingting Han and Lijun Zhang. Synthesis for PCTL in parametric Markov decision processes. In Proc. 3rd NASA Formal Methods Symposium (NFM), volume 6617 of Lecture Notes in Computer Science, pages 146-161, 2011.
Benoît Barbot, Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Efficient CTMC model checking of linear real-time specifications. In Proc. 17th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pages 128-142, 2011.
Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Reachability probabilities in Markovian Timed Automata. In Proc. 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC), pages 7075-7080, 2011.
2009
Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Quantitative model checking of continuous-time Markov chains against timed automata specifications. In Proc. 24th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 309-318, 2009.
Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. LTL model checking of time-inhomogeneous Markov chains. In Proc. 7th International Symposium on Automated Technology for Verification and Analysis (ATVA), pages 104-119, 2009.
2008
Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Approximate parameter synthesis for probabilistic time-bounded reachability. In Proc. 29th IEEE Real-Time Systems Symposium (RTSS), pages 173-182, 2008.
Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Compositional modeling and minimization of time-inhomogeneous Markov chains. In Proc. 11th International Workshop on Hybrid Systems: Computation and Control (HSCC), pages 244-258, 2008.
Taolue Chen, Tingting Han and Joost-Pieter Katoen. Time-abstracting bisimulation for probabilistic timed automata. In Proc. 2nd IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 177-184, 2008.
Berteun Damman, Tingting Han and Joost-Pieter Katoen. Regular expressions for PCTL counterexamples. In Proc. 5th International Conference on the Quantitative Evaluation of Systems (QEST), pages 179-188, 2008.
2007
Tingting Han and Joost-Pieter Katoen. Counterexamples in probabilistic model checking. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2007.
Tingting Han and Joost-Pieter Katoen. Providing evidence of likely being on time — Counterexample generation for CTMC model checking. In Automated Technology for Verification and Analysis (ATVA), 2007.
Taolue Chen, Tingting Han and Jian Lu. On behavioral metric for probabilistic systems: Definition and approximation algorithm. In Fuzzy Systems and Knowledge Discovery (FSKD), 2007.
2006
Taolue Chen, Tingting Han and Jian Lu. On the Markovian randomized strategy of controller for Markov decision processes. In Fuzzy Systems and Knowledge Discovery (FSKD), 2006.
Tingting Han. Diagnosis, Synthesis and Analysis of Probabilistic Models. PhD Thesis, University of Twente and RWTH Aachen University, 2009.