Trustworthy Intelligent Systems

Andrea Turrini (图安睿)'s Homepage

Research interests

My main research interests concern the formal analysis of processes involving probability and nondeterminism. I am currently focused on model checking probabilistic nondeterministic systems against ω-regular properties, like the ones expressible by nondeterministic Büchi automata. For this kind of automata, I am also working on practical improvements of their operations, such as automata determinization and complementation (to other classes of ω-regular automata), as well as language inclusion.

I am also working in applying model checking results to improve reinforcement learning algorithms in self-driving for autonomous vehicles, so to have better guarantees about their safety and robustness to noise in the sim-to-real transfer of the trained policies.

I worked in the formal analysis of properties of the Segala’s Probabilistic Automata model; its comparison with other probabilistic models; the development of conservative extensions of such model, like cost/reward decorated probabilistic automata. This permits to formally define and study properties of real systems using an uniform approach.

Besides these topics, I am also interested in the analysis of quantum systems with respect to branching time and linear time properties. I also work in the practical aspects of termination of programs. The termination analysis can make use of Büchi automata and several operations on them, on which I also focus my research to improve their practical applicability in program analysis.

To contact me, send me an email to <family name>@ios.ac.cn.

Professional activities

Publications

  • Ji Guan, Yuan Feng (), Andrea Turrini, Mingsheng Ying: Measurement-based Verification of Quantum Markov Chains. In Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III, volume 14683 of Lecture Notes in Computer Science, pages 533-554, 2024. DOI BIB
  • Yu-Fang Chen (), Vojtech Havlena, Ondrej Lengál, Andrea Turrini: A symbolic algorithm for the case-split rule in solving word constraints with extensions. In J. Syst. Softw. 201:111673, 2023. DOI BIB
  • Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y. Vardi (), Lijun Zhang: On the power of finite ambiguity in Büchi complementation. In Inf. Comput. 292:105032, 2023. DOI BIB
  • Chen Fu, Andrea Turrini, Xiaowei Huang (), Lei Song, Yuan Feng (), Lijun Zhang: Model Checking for Probabilistic Multiagent Systems. In Journal of Computer Science and Technology 38(4):1-25, 2023. DOI BIB
  • Vojtech Havlena, Ondrej Lengál, Yong Li, Barbora Smahlíková, Andrea Turrini: Modular Mix-and-Match Complementation of Büchi Automata. In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part I, volume 13993 of Lecture Notes in Computer Science, pages 249-270, 2023. DOI BIB
  • Ying Liu, Andrea Turrini, Ernst Moritz Hahn (), Bai Xue (), Lijun Zhang: Scenario Approach for Parametric Markov Models. In Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part I, volume 14215 of Lecture Notes in Computer Science, pages 158-180, 2023. DOI BIB
  • Chen Fu, Ernst Moritz Hahn (), Yong Li, Sven Schewe (), Meng Sun (), Andrea Turrini, Lijun Zhang: EPMC Gets Knowledge in Multi-agent Systems. In Verification, Model Checking, and Abstract Interpretation - 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings, volume 13182 of Lecture Notes in Computer Science, pages 93-107, 2022. DOI BIB
  • Yi Li, Xie Li, Yong Li, Xuechao Sun, Andrea Turrini, Lijun Zhang: Synthesizing ranking functions for loop programs via SVM. In Theor. Comput. Sci. 935:1-20, 2022. DOI BIB
  • Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y. Vardi (), Lijun Zhang: Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition. In Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 152-173, 2022. DOI BIB
  • Meilun Li, Andrea Turrini, Ernst Moritz Hahn (), Zhikun She, Lijun Zhang: Probabilistic Preference Planning Problem for Markov Decision Processes. In IEEE Trans. Software Eng. 48(5):1545-1559, 2022. DOI BIB
  • Wanwei Liu, Junnan Xu, David N. Jansen (), Andrea Turrini, Lijun Zhang: An Axiom System of Probabilistic Mu-Calculus. In Tsinghua Science and Technology 27(2):372-385, 2022. DOI BIB
  • Andrea Turrini: An Introduction to Quantum Model Checking. In Applied Sciences 12(4), 2022. DOI BIB
  • Yong Li, Yih-Kuen Tsay (), Andrea Turrini, Moshe Y. Vardi (), Lijun Zhang: Congruence Relations for Büchi Automata. In Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 465-482, 2021. DOI BIB
  • Yong Li, Andrea Turrini, Moshe Y. Vardi (), Lijun Zhang: Synthesizing Good-Enough Strategies for LTLf Specifications. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pages 4144-4151, 2021. DOI BIB
  • Yong Li, Andrea Turrini, Xuechao Sun, Lijun Zhang: Proving Non-inclusion of Büchi Automata Based on Monte Carlo Sampling. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, volume 12302 of Lecture Notes in Computer Science, pages 467-483, 2020. DOI BIB
  • Carlos E. Budde, Arnd Hartmanns (), Michaela Klauck, Jan Kretínský, David Parker, Tim Quatmann, Andrea Turrini, Zhen Zhang: On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report. In Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part IV, volume 12479 of Lecture Notes in Computer Science, pages 216-241, 2020. DOI BIB
  • Yu-Fang Chen (), Vojtech Havlena, Ondrej Lengál, Andrea Turrini: A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. In Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings, volume 12470 of Lecture Notes in Computer Science, pages 343-363, 2020. DOI BIB
  • Weizhi Feng, Cheng-Chao Huang, Andrea Turrini, Yong Li: Modelling and Implementation of Unmanned Aircraft Collision Avoidance. In Dependable Software Engineering. Theories, Tools, and Applications - 6th International Symposium, SETTA 2020, Guangzhou, China, November 24-27, 2020, Proceedings, volume 12153 of Lecture Notes in Computer Science, pages 52-69, 2020. DOI BIB
  • Xie Li, Yi Li, Yong Li, Xuechao Sun, Andrea Turrini, Lijun Zhang: SVMRanker: a general termination analysis framework of loop programs via SVM. In ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, November 8-13, 2020, pages 1635-1639, 2020. DOI BIB
  • Ernst Moritz Hahn (), Vahid Hashemi, Holger Hermanns (), Morteza Lahijanian, Andrea Turrini: Interval Markov Decision Processes with Multiple Objectives: From Robust Strategies to Pareto Curves. In ACM Trans. Model. Comput. Simul. 29(4):27:1-27:31, 2019. DOI BIB
  • Yi Li, Xuechao Sun, Yong Li, Andrea Turrini, Lijun Zhang: Synthesizing Nested Ranking Functions for Loop Programs via SVM. In Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings, volume 11852 of Lecture Notes in Computer Science, pages 438-454, 2019. DOI BIB
  • Yong Li, Xuechao Sun, Andrea Turrini, Yu-Fang Chen (), Junnan Xu: ROLL 1.0: ω-Regular Language Learning Library. In Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, volume 11427 of Lecture Notes in Computer Science, pages 365-371, 2019. DOI BIB
  • Yu-Fang Chen (), Matthias Heizmann, Ondrej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, Lijun Zhang: Advanced automata-based algorithms for program termination checking. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pages 135-150, 2018. DOI BIB
  • Christian Eisentraut, Holger Hermanns (), Johann Schuster, Andrea Turrini, Lijun Zhang: The quest for minimal quotients for probabilistic and Markov automata. In Inf. Comput. 262:162-186, 2018. DOI BIB
  • Chen Fu, Andrea Turrini, Xiaowei Huang (), Lei Song, Yuan Feng (), Lijun Zhang: Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, pages 4757-4763, 2018. DOI BIB
  • Yong Li, Andrea Turrini, Yu-Fang Chen (), Lijun Zhang: Learning Büchi Automata and Its Applications. In Engineering Trustworthy Software Systems - 4th International School, SETSS 2018, Chongqing, China, April 7-12, 2018, Tutorial Lectures, volume 11430 of Lecture Notes in Computer Science, pages 38-98, 2018. DOI BIB
  • Yong Li, Andrea Turrini, Lijun Zhang, Sven Schewe (): Learning to Complement Büchi Automata. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, volume 10747 of Lecture Notes in Computer Science, pages 313-335, 2018. DOI BIB
  • Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn (), Arnd Hartmanns (), Sebastian Junges (), Andrea Turrini: JANI: Quantitative Model and Tool Interaction. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II, volume 10206 of Lecture Notes in Computer Science, pages 151-168, 2017. DOI BIB
  • Yuan Feng (), Ernst Moritz Hahn (), Andrea Turrini, Shenggang Ying: Model Checking Omega-regular Properties for Quantum Markov Chains. In 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 35:1-35:16, 2017. DOI BIB
  • Ernst Moritz Hahn (), Vahid Hashemi, Holger Hermanns (), Morteza Lahijanian, Andrea Turrini: Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes. In Quantitative Evaluation of Systems - 14th International Conference, QEST 2017, Berlin, Germany, September 5-7, 2017, Proceedings, volume 10503 of Lecture Notes in Computer Science, pages 207-223, 2017. DOI BIB
  • Ernst Moritz Hahn (), Sven Schewe (), Andrea Turrini, Lijun Zhang: Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, volume 10145 of Lecture Notes in Computer Science, pages 266-287, 2017. DOI BIB
  • Vahid Hashemi, Andrea Turrini, Ernst Moritz Hahn (), Holger Hermanns (), Khaled M. Elbassioni: Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs. In Dependable Software Engineering. Theories, Tools, and Applications - Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings, volume 10606 of Lecture Notes in Computer Science, pages 25-41, 2017. Best paper. DOI BIB
  • Luis María Ferrer Fioriti, Vahid Hashemi, Holger Hermanns (), Andrea Turrini: Deciding probabilistic automata weak bisimulation: theory and practice. In Formal Aspects Comput. 28(1):109-143, 2016. DOI BIB
  • Ernst Moritz Hahn (), Vahid Hashemi, Holger Hermanns (), Andrea Turrini: Exploiting Robust Optimization for Interval Probabilistic Bisimulation. In Quantitative Evaluation of Systems - 13th International Conference, QEST 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings, volume 9826 of Lecture Notes in Computer Science, pages 55-71, 2016. DOI BIB
  • Ernst Moritz Hahn (), Sven Schewe (), Andrea Turrini, Lijun Zhang: A Simple Algorithm for Solving Qualitative Probabilistic Parity Games. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, volume 9780 of Lecture Notes in Computer Science, pages 291-311, 2016. DOI BIB
  • Vahid Hashemi, Holger Hermanns (), Lei Song, K. Subramani, Andrea Turrini, Piotr Wojciechowski: Compositional Bisimulation Minimization for Interval Markov Decision Processes. In Language and Automata Theory and Applications - 10th International Conference, LATA 2016, Prague, Czech Republic, March 14-18, 2016, Proceedings, volume 9618 of Lecture Notes in Computer Science, pages 114-126, 2016. DOI BIB
  • Yong Li, Wanwei Liu, Andrea Turrini, Ernst Moritz Hahn (), Lijun Zhang: An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties. In Dependable Software Engineering: Theories, Tools, and Applications - Second International Symposium, SETTA 2016, Beijing, China, November 9-11, 2016, Proceedings, volume 9984 of Lecture Notes in Computer Science, pages 280-296, 2016. DOI BIB
  • Tom van Dijk (), Ernst Moritz Hahn (), David N. Jansen (), Yong Li, Thomas Neele (), Mariëlle Stoelinga (), Andrea Turrini, Lijun Zhang: A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. In Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings, volume 9409 of Lecture Notes in Computer Science, pages 35-51, 2015. DOI BIB
  • Yuan Feng (), Ernst Moritz Hahn (), Andrea Turrini, Lijun Zhang: QPMC: A Model Checker for Quantum Programs and Protocols. In FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, volume 9109 of Lecture Notes in Computer Science, pages 265-272, 2015. DOI BIB
  • Ernst Moritz Hahn (), Guangyuan Li, Sven Schewe (), Andrea Turrini, Lijun Zhang: Lazy Probabilistic Model Checking without Determinisation. In 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 354-367, 2015. DOI BIB
  • Meilun Li, Zhikun She, Andrea Turrini, Lijun Zhang: Preference Planning for Markov Decision Processes. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA, pages 3313-3319, 2015. DOI BIB
  • Andrea Turrini, Holger Hermanns (): Polynomial time decision algorithms for probabilistic automata. In Inf. Comput. 244:134-171, 2015. DOI BIB
  • Ernst Moritz Hahn (), Yi Li, Sven Schewe (), Andrea Turrini, Lijun Zhang: IscasMc: A Web-Based Probabilistic Model Checker. In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pages 312-317, 2014. DOI BIB
  • Andrea Turrini, Holger Hermanns (): Cost Preserving Bisimulations for Probabilistic Automata. In Log. Methods Comput. Sci. 10(4), 2014. DOI BIB
  • Christian Eisentraut, Holger Hermanns (), Julia Krämer, Andrea Turrini, Lijun Zhang: Deciding Bisimilarities on Distributions. In Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8054 of Lecture Notes in Computer Science, pages 72-88, 2013. DOI BIB
  • Christian Eisentraut, Holger Hermanns (), Johann Schuster, Andrea Turrini, Lijun Zhang: The Quest for Minimal Quotients for Probabilistic Automata. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7795 of Lecture Notes in Computer Science, pages 16-31, 2013. DOI BIB
  • Vahid Hashemi, Holger Hermanns (), Andrea Turrini: On the Efficiency of Deciding Probabilistic Automata Weak Bisimulation. In Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 66, 2013. DOI BIB
  • Holger Hermanns (), Andrea Turrini: Cost Preserving Bisimulations for Probabilistic Automata. In CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, volume 8052 of Lecture Notes in Computer Science, pages 349-363, 2013. DOI BIB
  • Daniel Gebler, Vahid Hashemi, Andrea Turrini: Computing Behavioral Relations for Probabilistic Concurrent Systems. In Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems - International Autumn School, ROCKS 2012, Vahrn, Italy, October 22-26, 2012, Advanced Lectures, volume 8453 of Lecture Notes in Computer Science, pages 117-155, 2012. DOI BIB
  • Holger Hermanns (), Andrea Turrini: Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India, volume 18 of LIPIcs, pages 435-447, 2012. DOI BIB
  • Roberto Segala, Andrea Turrini: Conditional Automata: A Tool for Safe Removal of Negligible Events. In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 539-553, 2010. DOI BIB
  • Simon Kramer, Catuscia Palamidessi, Roberto Segala, Andrea Turrini, Christelle Braun: A quantitative doxastic logic for probabilistic processes and applications to information-hiding. In J. Appl. Non Class. Logics 19(4):489-516, 2009. DOI BIB
  • Roberto Segala, Andrea Turrini: Approximated Computationally Bounded Simulation Relations for Probabilistic Automata. In 20th IEEE Computer Security Foundations Symposium, CSF 2007, 6-8 July 2007, Venice, Italy, pages 140-156, 2007. DOI BIB
  • Roberto Segala, Andrea Turrini: Comparative Analysis of Bisimulation Relations on Alternating and Non-Alternating Probabilistic Models. In Second International Conference on the Quantitative Evaluaiton of Systems (QEST 2005), 19-22 September 2005, Torino, Italy, pages 44-53, 2005. DOI BIB

Thesis

  • Andrea Turrini: Hierarchical and compositional verification of cryptographic protocols. University of Verona, Italy, 2009. URL BIB.

Teaching activities

  • WS17: Instructor in the Course on Symbolic verification
  • SS13: Assistant in the Data Network course by Prof. Verena Wolf
  • SS12: Instructor in the Concurrent and Mobile Languages course for Master and Bachelor students in Computer Science.
  • WS11/12: Instructor in the Probabilistic Concurrency Models doctoral privatissimum jointly with Prof. Dr.-Ing Holger Hermanns ()
  • Sept.04/Mar.08: Assistant in courses on Algorithms and Data Structure, Operating Systems, and Compilers at the Department of Computer Science, University of Verona