Selected Publication

2013

Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis. Automatic Verification of Competitive Stochastic Systems. Formal Methods in System Design, Springer. 2013.
Taolue Chen, Tingting Han, Marta Z. Kwiatkowska. On the complexity of model checking interval-valued discrete time Markov chains. Information Processing Letters. 113(7): 210-216, 2013.
Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis. PRISM-games: A Model Checker for Stochastic Multi-Player Games. TACAS 2013, Lecture Notes in Computer Science 7795, pp. 185-191, Springer, 2013.
Taolue Chen, Marco Diciolla, Marta Z. Kwiatkowska, Alexandru Mereacre. A Simulink Hybrid Heart Model for Quantitative Verification of Cardiac Pacemakers. Proc. of HSCC'13. To appear.

2012

Taolue Chen, Chris Chilton, Bengt Jonsson, Marta Z. Kwiatkowska. A Compositional Specification Theory for Component Behaviours. ESOP'12, Lecture Notes in Computer Science 7211, pp. 148-168, Springer, 2012.
Taolue Chen, Marco Diciolla, Marta Z. Kwiatkowska, Alexandru Mereacre. Verification of linear duration properties over continuous-time Markov chains. Proc. of HSCC'12, pp. 265-274, ACM, 2012.
Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, Aistis Simaitis. Automatic Verification of Competitive Stochastic Systems. TACAS'12, Lecture Notes in Computer Science 7214, pp. 315-330, Springer, 2012.
Taolue Chen, Marco Diciolla, Marta Kwiatkowska, and Alexandru Mereacre. Quantitative Verification of Implantable Cardiac Pacemakers. Proc. of RTSS 2012, pp. 263-272, IEEE.
Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, Aistis Simaitis, Ashutosh Trivedi, Michael Ummels. Playing Stochastic Games Precisely. CONCUR'12, Lecture Notes in Computer Science 7454, pp. 348-363, Springer, 2012.
Taolue Chen, Klaus Dräger, Stefan Kiefer. Model Checking Stochastic Branching Processes. MFCS'12, Lecture Notes in Computer Science 7464, pp. 271-282, Springer, 2012.

2011

Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Reachability Probabilities in Markovian Timed Automata. Proc. of CDC'11, pp. 7075-7080, IEEE Press, 2011.
Taolue Chen, Marco Diciolla, Marta Kwiatkowska and Alexandru Mereacre. Time-Bounded Verification of CTMCs Against Real-Time Specifications. FORMATS'11, Lecture Notes in Computer Science 6919, pp. 26-42, Springer, 2011.
Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Observing Continuous-Time MDPs by 1-Clock Timed Automata. RP'11, Lecture Notes in Computer Science 6945, pp. 2-25, Spriner, 2011.
Taolue Chen, Marta Kwiatkowska, David Parker and Aistis Simaitis. Verifying Team Formation Protocols with Probabilistic Model Checking. CLIMA XII, Lecture Notes in Computer Science 6814, pp. 190-207, Springer, 2011.
Benoit Barbot, Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Efficient CTMC Model Checking of Linear Real-Time Objectives. TACAS'11, Lecture Notes in Computer Science 6605, pp. 128-142, Springer, 2011.
Luca Aceto, Taolue Chen, Anna Ingolfsdottir, Bas Luttik and Jaco van de Pol. On the Axiomatizability of Priority II. TCS. 412(28): 3035-3044, 2011.
Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. Logical Methods in Computer Science, 7(1-2):1-34, 2011. Also available from ArXiv.

2010

Taolue Chen and Jian Lu. Towards Analysis of Semi-Markov Decision Processes. AICI'10, Lecture Notes in Computer Science 6319, pp. 41-48, Springer 2010.
Taolue Chen and Wan Fokkink. The Saga of Finite Equational Bases over BCCSP. NVTI (Dutch Association for Theoretical Computer Science) Newsletter, 2010. (Invited contribution.)

2009

Taolue Chen, Tingting Han, Joost-Pieter Katoen and Alexandru Mereacre. LTL Model Checking of Time-Inhomogeneous Markov Chains. ATVA'09, Lecture Notes in Computer Science 5799, pp. 104-119, Springer, 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. of the 24th Annual IEEE Symposium on Logic in Computer Science (LICS'09), pp. 309-318, IEEE Press, 2009.
Taolue Chen, Wan Fokkink and Rob van Glabbeek. On Finite Bases for Weak Semantics: Failures versus Impossible Futures. In Proc. 35th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'09). Lecture Notes in Computer Science 5404, pp. 167-180, Springer, 2009.
Jasper Berendsen, Taolue Chen and David. N. Jansen. Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata. In Proc. 6th Annual Conference of Theory and Applications of Models of Computation (TAMC'09), Lecture Notes in Computer Science 5532, pp. 128-137, Springer, 2009.
Taolue Chen, Tingting Han and Jian Lu. On Behavioral Metric for Probabilistic Systems: Definition and Approximation Algorithm. Journal of Computer & Mathematics with Application. Elsevier. 57(6):991-999, Elsevier, 2009.

2008

Taolue Chen and Wan Fokking. On the Axiomatizability of Impossible Futures: Preorder versus Equivalence. In Proc. of The Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS'08), pp. 156-165, IEEE.
Taolue Chen, Jaco van de Pol and Yanjing Wang. Model Checking and Axiomatization for PDL on Accelerated Labelled Transition Systems. In Proc. of The 2nd IEEE Theoretical Aspects of Software Engineering Conference (TASE'08), pp. 193-200, IEEE.
Taolue Chen, Tingting Han and Joost-Pieter Katoen. Time-abstracting Bisimulation for Probabilistic Timed Automata. In Proc. of The 2nd IEEE Theoretical Aspects of Software Engineering Conference (TASE'08), pp. 177-184, IEEE.
Taolue Chen and Jian Lu. Complete Axiomatization for Divergent-sensitive Bisimulations in Basic Process Algebra with Prefix Iteration. In Proc. of The First International Conference on Foundations of Informatics, Computing and Software (FICS'08), June 3 - 6, 2008, Shanghai, China. Electronic Notes in Theoretical Computer Science 212: 55-70. Elsevier.
Taolue Chen, Wan Fokkink and Rob van Glabbeek. Ready to Preorder: The Case of Weak Process Semantics. Information Processing Letters,109(2): 104-111, Elsevier, 2008.
Taolue Chen and Jian Lu. Towards the Complexity of Controls for Timed Automata with a Small Number of Clocks . In Proc. 5th International Conference on Fuzzy Systems and Knowledge Discovery (FSKD'08), vol.5, pp. 134-138, IEEE.
Luca Aceto, Taolue Chen, Wan Fokkink and Anna Ingolfsdottir. On the Axiomatizability of Priority. Mathematical Structure in Computer Science, 18(1): 5-28, Cambridge University Press, 2008.
Taolue Chen, Wan Fokkink, Bas Luttik and Sumit Nain. On Finite Alphabets and Infinite Bases. Information and Computation, 206(5): 492-519, Elsevier, 2008.

2007

Taolue Chen and Jian Lu. Probabilistic Alternating-time Temporal Logic and Model Checking Algorithm. In Proc. 4th International Conference on Fuzzy Systems and Knowledge Discovery (FSKD'07), vol.2, pp. 35-39, IEEE.
Taolue Chen, Tingting Han and Jian Lu. On Behavioral Metric for Probabilistic Systems: Definition and Approximation Algorithm. In Proc. 4th International Conference on Fuzzy Systems and Knowledge Discovery (FSKD'07), vol.2, pp. 21-25, IEEE.
Taolue Chen, Bas Ploeger, Jaco van de Pol and Tim Willemse. Equivalence Checking for Infinite Systems using Parameterized Boolean Equation Systems. In Proc. 18th Conference on Concurrency Theory (CONCUR'07), Lecture Notes in Computer Science 4703, pp. 120-135, Springer.

2006

Taolue Chen, Wan Fokkink and Sumit Nain. On Finite Alphabets and Infinite Bases II: Completed and Ready Simulation. In (L. Aceto and A. Ingolfsdottir, eds) Proc. 9th Conference on Foundations of Software Science and Computation Structures (FoSSaCS'06), Vienna, March, 2006. Lecture Notes in Computer Science 3921, Springer, 2006.
Taolue Chen, Tingting Han and Jian Lu. On the Complete Axiomatization for Prefix Iteration modulo Observation Congruence. Acta Cybernetica: 17(3), 2006.
Luca Aceto, Taolue Chen, Wan Fokkink and Anna Ingolfsdottir. On the Axiomatizability of Priority. In Proc. 33rd Colloquium on Automata, Languages and Programming (ICALP'06), Venice, Lecture Notes in Computer Science, Springer (July 2006).
Taolue Chen and Wan Fokkink. On Finite Alphabets and Infinite Bases III: Simulation. In Proc. 17th Conference on Concurrency Theory (CONCUR'06), Bonn, Lecture Notes in Computer Science, Springer (August 2006).
Taolue Chen, Tingting Han and Jian Lu. On the Markovian Randomized Strategy of Controller for Markov Decision Processes. In Proc. 3rd International Conference on Fuzzy Systems and Knowledge Discovery (FSKD'06), Xi'an, Lecture Notes in Artificial Intelligence, pp. 149-158, Springer. 2006.

2005

Tingting Han, Taolue Chen and Jian Lu. Structure Analysis for Dynamic Software Architecture based on Spatial Logic. In Proc. of the 29th Annual International Computer Software and Applications Conference (COMPSAC 2005), Edinburgh, Scotland, July 26-28, 2005, pp. 71-76, IEEE Computer Society.
Taolue Chen, Tingting Han and Jian Lu. A Modal Logic for Pi Calculus and Model Checking Algorithms. 11th Workshop on Logic, Language, Information and Computation (WoLLIC'2004), Paris-Fontainebleau, France, July 19-22, 2004. Electronic Notes in Theoretical Computer Science 123, 2005.
Taolue Chen, Tingting Han and Jian Lu. Analysis of A Leader Election Algorithm in muCRL. In Proc. Fifth International Conference on Computer and Information Technology (CIT 2005), 21-23 September 2005, Shanghai, China. IEEE Computer Society 2005.
Taolue Chen, Tingting Han and Jian Lu. On the Bisimulation Congruence in chi-Calculus. In Proc. 25th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'05), Hyderabad, India, December 15-18, 2005. Lecture Notes in Computer Science 3821, Springer, 2005.

2004

Taolue Chen, Jingyang Zhou, Tingting Han and Jian Lu. Checking Open Congruence in Chi Calculus. Computing: The Australasian Theory Symposium (CATS'04), 2004 University of Otago, Dunedin, New Zealand, January 18-22, 2004. Electronic Notes in Theoretical Computer Science 91, 2004.
Taolue Chen, Tingting Han and Jian Lu. Towards a Modal Logic for Pi Calculus, Proceeding of the 28th Annual International Computer Software and Applications Conference (COMPSAC 2004), Hong Kong, September 28-30, 2004, pp. 330-335, IEEE computer Society Press.
Taolue Chen, Tingting Han and Jian Lu. Framework of Performance Evaluation for Mobile Process based on Mobile Ambient, Proceeding of the 2004 International Conference on Computer and Information Technology (CIT'04), Wuhan, China, September, 14-16, 2004, pp. 540-545, IEEE Computer Society Press.
Taolue Chen, Tingting Han and Jian Lu. Tree Logic with Recursion and Model Checking Algorithm. IASTED International Conference on Software Engineering and Applications (SEA 2004), Nov. 9 -11, 2004, MIT Cambridge, USA.

2003

Taolue Chen, Tingting Han and Jian Lu. Intensionality of Modal Logic for Robust Ambient Calculus. FGC: Foundations of Global Computing (FGC'03), 2nd EATCS Workshop, June 28-29, 2003, Eindhoven, The Netherlands. Electronic Notes in Theoretical Computer Science 85(1), 2003.