Dr H Qu
Department of Automatic Control & Systems Engineering
Rm F40, SCentRo (Sheffield Centre for Robotics), Pam Liversidge Building
University of Sheffield
Tel: (+44) (0)114 222 5666
Email: h.qu @ sheffield.ac.uk
Dr Hongyang Qu is a Senior Research Fellow in the Department of Automatic Control & Systems Engineering (ACSE), University of Sheffield. Before joining ACSE in 2013, Hongyang had been a computer scientist for a decade, having completed his BSc (Beijing Institute of Technology, 1995), MSc (Chinese Academy of Science, 2001) and PhD (University of Warwick, 2006) studies in Computer Science. As a post-doctoral researcher, he spent one and a half years at Université de Provence, two years at Imperial College London, and four years at Oxford University. During this time he developed many model checking techniques and software. He is the lead developer of the Model Checker for Multi-Agent Systems (MCMAS) and a major contributor to the development of the well-known probabilistic model checker PRISM.
Dr Qu's research interests lie in the broad area of verification and model checking. Most of his activity involves efficient model checking techniques for discrete systems, real-time systems and probabilistic systems, as well as their application. Since joining ACSE, he has shifted his focus to the development of model checking techniques for solving control engineering problems. Currently, his main research interests are:
- Modelling and verification of coordination of autonomous robots;
- Verification-based synthesis of robot motion planning and control;
- BDD based model checking techniques for verification of multi-agent systems;
- Incremental verification techniques for probabilistic systems;
- GPU-based model checking algorithms.
- Royal Society International Exchanges Scheme grant, GPU-based fast parameter synthesis for robot coordination, 16/03/2015 to 15/03/2016, £6,000, PI.
- Alessio Lomuscio, Hongyang Qu, Franco Raimondi MCMAS: An open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer (To appear)
- Simon Busard, Charles Pecheur, Hongyang Qu, Franco Raimundi Reasoning about Strategies under Partial Observability and Fairness Constraints. Information and Computation (To appear)
- Warda El-Kholy, Mohamed El-Menshawy, Jamal Bentahar, Hongyang Qu, Rachida Dssouli. Formal Specification and Automatic Verification of Conditional Commitments. IEEE Intelligent Systems 30(2): 36-44, 2015
- Warda El-Kholy, Mohamed El-Menshawy, Jamal Bentahar, Hongyang Qu, Rachida Dssouli. Conditional Commitments: Reasoning and Model Checking. ACM Transactions on Software Engineering and Methodology 24(2): Article 9, 2014
- Warda El-Kholy, Mohamed El-Menshawy, Jamal Bentahar, Hongyang Qu, Rachida Dssouli. Modelling and Verifying Choreographed Multi-agent-based Web Service Compositions Regulated by Commitment Protocols. Expert Systems With Applications 41(16): 7478–7494, 2014
- Klaus Draeger, Marta Kwiatkowska, David Parker, Hongyang Qu. Local Abstraction Refinement for Probabilistic Timed Programs. Theoretical Computer Science 538: 37-53, 2014
- Marta Kwiatkowska, Gethin Norman, David Parker, Hongyang Qu. Compositional Probabilistic Verification through Multi-Objective Model Checking. Information and Computation 232: 38-65, 2013
- Alessio Lomuscio, Hongyang Qu, Monika Solanki. Towards verifying contract regulated service composition. Autonomous Agents and Multi-Agent Systems. 24(3): 345-373, 2012
- Mohamed El-Menshawy, Jamal Bentahar, Hongyang Qu, Rachida Dssouli. Communicative Commitments: Model Checking and Complexity Analysis. Knowledge-Based Systems 35: 21-34, 2012
- Alessio Lomuscio, Wojciech Penczek, Hongyang Qu. Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems. Fundamenta Informaticae 101(1-2): 71-90, 2010
- Saddek Bensalem, Doron Peled, Hongyang Qu, Stavros Tripakis. Automatic Generation of Path Conditions for Concurrent Timed Systems. Theoretical Computer Science 404: 275-292, 2008
Conference papers (peer reviewed)
- Warda El-Kholy, Mohamed El-Menshawy, Jamal Bentahar, Hongyang Qu, Rachida Dssouli. Verifying Multiagent-based Web Service Compositions Regulated by Commitment Protocols. 21th IEEE International Conference on Web Services (ICWS'14), pages 49-56, IEEE CS Press, 2014
- Hongyang Qu, Andreas Kolling, Sandor M Veres. Formulating Robot Pursuit-Evasion Strategies by Model Checking. 19th World Congress of the International Federation of Automatic Control (IFAC’14), pages 3048-3055, 2014
- Hongyang Qu, Sandor M Veres. On Efficient Consistency Checks by Robots. 13th European Control Conference (ECC’14) : 336-343, 2014
- Simon Busard, Charles Pecheur, Hongyang Qu, Franco Raimundi. Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints. 16th International Conference on Formal Engineering Methods (ICFEM’14), LNCS 8819, page 27-42, Springer, 2014
- Simon Busard, Charles Pecheur, Hongyang Qu, Franco Raimundi. Reasoning about Strategies under Partial Observability and Fairness Constraints. 1st International Workshop on Strategic Reasoning (SR'13), pages 71-79, EPTCS 2013
- Vojtech Forejt, Marta Kwiatkowska, Gethin Norman, David Parker, Hongyang Qu. Assume-Guarantee Verification for Probabilistic Systems. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), LNCS 6605, page 112-127, Springer, 2011
- Marta Kwiatkowska, David Parker, Hongyang Qu. Incremental Quantitative Verification for Markov Decision Processes. 41st IEEE/IFIP International Conference on Dependable Systems and Networks, (DSN'11), page 359-370, IEEE CS Press, 2011
- Mohamed El-Menshawy, Jamal Bentahar, Hongyang Qu, Rachida Dssouli. On the Verification of Social Commitments and Time. 10th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'11), page 483-490, IFAAMAS, 2011
- Henri Hansen, Marta Kwiatkowska, Hongyang Qu. Partial order reduction for Model checking MDPs under unconditional fairness. 8th International Conference on Quantitative Evaluation of SysTems (QEST'11), page 203-212, IEEE CS Press 2011
- Marta Kwiatkowska, Gethin Norman, David Parker, Hongyang Qu. Assume-Guarantee Verification for Probabilistic Systems. 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), LNCS 6015, page 23-37, Springer, 2010
- Marta Kwiatkowska, Alessio Lomuscio, Hongyang Qu. Parallel Model Checking for Temporal Epistemic Logic. 19th European Conference on Artificial Intelligence (ECAI'10), page 543-548, IOS Press 2010
- Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu. A symmetry reduction technique for model checking temporal epistemic logic. 21st International Joint Conference on Artificial Intelligence (IJCAI'09), page 721-726, AAAI Press, 2009
- Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu. A data symmetry reduction technique for temporal-epistemic logic. 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), LNCS 5799, page 69-83, Springer, 2009
- Alessio Lomuscio, Hongyang Qu, Franco Raimondi. MCMAS: A Model Checker for the Verification of Multi-Agent Systems. 21st International Conference on Computer Aided Verification (CAV'09), LNCS 5643, page 682-688, Springer, 2009
- Nicolás Wolovick, Pedro D'Argenio, Hongyang Qu. Optimizing Probabilities of Real-Time Test Case Execution. 2nd International Conference on Software Testing Verification and Validation (ICST'09), page 446-455, IEEE CS Press, 2009
- DBLP http://www.informatik.uni-trier.de/~ley/pers/hd/q/Qu:Hongyang.html
- Google Scholar http://scholar.google.co.uk/citations?user=PACmB9IAAAAJ&hl=en
- ResearchGate https://www.researchgate.net/profile/Hongyang_Qu
- MCMAS http://vas.doc.ic.ac.uk/software/mcmas/: a Model Checker for Multi-Agent Systems.
- PRISM http://www.prismmodelchecker.org/: a probabilistic model checker.
- MCGTL http://www.sheffield.ac.uk/acse/research/groups/asrg/acl/mcgtl: a Model Checker for Game-Theoretic Learning algorithms.