Research interests

My main research interests concern the formal analysis of processes involving probability and nondeterminism. In particular current research topics are about 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.

I am also interested in the study of cryptographic protocols; in particular I am workin on the development of a framework based on probabilistic automata which can provide a rigorous mathematical background that formally justifies the correctness of the analysis as well as the management of nondeterminism in order to avoid undesirable behaviors induced by the resolution of nondeterminism.
Probability is a key ingredient in the definition of security of cryptographic primitives while nondeterminism arises from the interaction of several parties involved in a protocol specification as well as from the adversary that tries to attack the protocol.

Besides these two 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

Publications

Journals and Conferences

• A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions, Chen, Y.-F.; Havlena, V.; Lengál, O. and Turrini, A. In J. Syst. Softw., 2023.
• Modular Mix-and-Match Complementation of Büchi Automata, Havlena, V.; Lengál, O.; Li, Y.; Šmahl'iková, B. and Turrini, A. In TACAS, LNCS , 2023.
• EPMC Gets Knowledge in Multi-agent Systems, Fu, C.; Hahn, E. M.; Li, Y.; Schewe, S.; Sun, M.; Turrini, A. and Zhang, L. In VMCAI, pages 93-107, Springer, Lecture Notes in Computer Science 13182, 2022.
• Model Checking for Probabilistic Multiagent Systems, Fu, C.; Turrini, A.; Huang, X.; Song, L.; Feng, Y. and Zhang, L. In Journal of Computer Science and Technology, 2022.
• Synthesizing Ranking Functions for Loop Programs via SVM, Li, Y.; Li, X.; Li, Y.; Sun, X.; Turrini, A. and Zhang, L. In TCS, 2022.
• Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition, Li, Y.; Turrini, A.; Feng, W.; Vardi, M. Y. and Zhang, L. In CAV, pages 152-173, Springer, Lecture Notes in Computer Science 13372, 2022.
• An Introduction to Quantum Model Checking, Turrini, A. In Applied Sciences, 12, 2022.
• Congruence Relations for Büchi Automata, Li, Y.; Tsay, Y.-K.; Turrini, A.; Vardi, M. Y. and Zhang, L. In FM, pages 465-482, Springer, Lecture Notes in Computer Science 13047, 2021.
• Synthesizing Good-Enough Strategies for LTLf Specifications, Li, Y.; Turrini, A.; Vardi, M. Y. and Zhang, L. In IJCAI, pages 4144-4151, ijcai.org, 2021.
• An Axiom System of Probabilistic Mu-Calculus, Liu, W.; Xu, J.; Jansen, D. N.; Turrini, A. and Zhang, L. In Tsinghua Science and Technology, 27: 372-385, 2021.
• On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report, Budde, C. E.; Hartmanns, A.; Klauck, M.; Kret'inský, J.; Parker, D.; Quatmann, T.; Turrini, A. and Zhang, Z. In ISoLA (4), pages 216-241, Springer, Lecture Notes in Computer Science 12479, 2020.
• A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving, Chen, Y.-F.; Havlena, V.; Lengál, O. and Turrini, A. In APLAS, pages 343-363, Springer, 2020.
• Modelling and Implementation of Unmanned Aircraft Collision Avoidance, Feng, W.; Huang, C.-C.; Turrini, A. and Li, Y. In SETTA, pages 52-69, Springer, Lecture Notes in Computer Science 12153, 2020.
• SVMRanker: A General Termination Analysis Framework of Loop Programs via SVM, Li, X.; Li, Y.; Li, Y.; Sun, X.; Turrini, A. and Zhang, L. In ESEC/FSE, pages 1635-1639, ACM, 2020.
• Probabilistic Preference Planning Problem for Markov Decision Processes, Li, M.; Turrini, A.; Hahn, E. M.; She, Z. and Zhang, L. In IEEE Trans. Software Eng., 48: 1545-1559, 2020.
• Proving Non-Inclusion of Büchi Automata based on Monte Carlo Sampling, Li, Y.; Turrini, A.; Sun, X. and Zhang, L. In ATVA, pages 467-483, Springer, LNCS 12302, 2020.
• Interval Markov Decision Processes with Multiple Objectives: from Robust Strategies to Pareto Curves, Hahn, E. M.; Hashemi, V.; Hermanns, H.; Lahijanian, M. and Turrini, A. In TOMACS, 29, 2019.
• Synthesizing Nested Ranking Functions for Loop Programs via SVM, Li, Y.; Sun, X.; Li, Y.; Turrini, A. and Zhang, L. In ICFEM, pages 438-454, LNCS 11852, 2019.
• ROLL 1.0: ω-Regular Language Learning Library, Li, Y.; Sun, X.; Turrini, A.; Chen, Y.-F. and Xu, J. In TACAS, pages 365-371, LNCS 11427, 2019.
• Advanced Automata-based Algorithms for Program Termination Checking, Chen, Y.-F.; Heizmann, M.; Lengál, O.; Li, Y.; Tsai, M.-H.; Turrini, A. and Zhang, L. In PLDI, pages 135-150, 2018.
• The Quest for Minimal Quotients for Probabilistic and Markov Automata, Eisentraut, C.; Hermanns, H.; Schuster, J.; Turrini, A. and Zhang, L. In Inf. Comput., 262: 162-186, 2018.
• Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems, Fu, C.; Turrini, A.; Huang, X.; Song, L.; Feng, Y. and Zhang, L. In IJCAI, pages 4757-4763, ijcai.org, 2018.
• Learning Büchi Automata and Its Applications, Li, Y.; Turrini, A.; Chen, Y.-F. and Zhang, L. In Engineering Trustworthy Software Systems - 4th International School, SETSS 2018, Chongqing, China, April 7-12, 2018, Tutorial Lectures, pages 38-98, Springer, Lecture Notes in Computer Science 11430, 2018.
• Learning to Complement Büchi Automata, Li, Y.; Turrini, A.; Zhang, L. and Schewe, S. In VMCAI, pages 313-335, Springer, LNCS 10747, 2018.
• JANI: Quantitative Model and Tool Interaction, Budde, C. E.; Dehnert, C.; Hahn, E. M.; Hartmanns, A.; Junges, S. and Turrini, A. In TACAS, pages 151-168, LNCS 10206, 2017.
• Model Checking ω-regular Properties for Quantum Markov Chains, Feng, Y.; Hahn, E. M.; Turrini, A. and Ying, S. In CONCUR, pages 35:1-35:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, LIPIcs 85, 2017.
• Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes, Hahn, E. M.; Hashemi, V.; Hermanns, H.; Lahijanian, M. and Turrini, A. In QEST, pages 207-223, LNCS 10503, 2017.
• Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games, Hahn, E. M.; Schewe, S.; Turrini, A. and Zhang, L. In VMCAI, pages 266-287, LNCS 10145, 2017.
• Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs, Hashemi, V.; Turrini, A.; Hahn, E. M.; Hermanns, H. and Elbassioni, K. In SETTA, pages 25-41, LNCS 10606, 2017. (Best paper award)
• Deciding Probabilistic Automata Weak Bisimulation: Theory and Practice, Ferrer Fioriti, L. M.; Hashemi, V.; Hermanns, H. and Turrini, A. In Formal Aspects of Computing, 28: 109-143, 2016.
• Exploiting Robust Optimization for Interval Probabilistic Bisimulation, Hahn, E. M.; Hashemi, V.; Hermanns, H. and Turrini, A. In QEST, pages 55-71, LNCS 9826, 2016.
• A Simple Algorithm for Solving Qualitative Probabilistic Parity Games, Hahn, E. M.; Schewe, S.; Turrini, A. and Zhang, L. In CAV, pages 291-311, LNCS 9780, 2016.
• Compositional Bisimulation Minimization for Interval Markov Decision Processes, Hashemi, V.; Hermanns, H.; Song, L.; Subramani, K.; Turrini, A. and Wojciechowski, P. In LATA'16, pages 114-126, LNCS 9618, 2016.
• An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties, Li, Y.; Liu, W.; Turrini, A.; Hahn, E. M. and Zhang, L. In SETTA, pages 280-296, LNCS 9984, 2016.
• QPMC: A Model Checker for Quantum Programs and Protocols, Feng, Y.; Hahn, E. M.; Turrini, A. and Zhang, L. In Twentieth international symposium of the Formal Methods Europe association (FM), pages 265-272, Springer, Lecture Notes in Computer Science 9109, 2015.
• Lazy Probabilistic Model Checking without Determinisation, Hahn, E. M.; Li, G.; Schewe, S.; Turrini, A. and Zhang, L. In CONCUR, pages 354-367, LIPIcs 42, 2015.
• Preference Planning for Markov Decision Processes, Li, M.; She, Z.; Turrini, A. and Zhang, L. In The Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI-15), pages 3313-3319, AAAI Press, 2015.
• Polynomial Time Decision Algorithms for Probabilistic Automata, Turrini, A. and Hermanns, H. In Information and Computation, 244: 134-171, 2015.
• A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking, van Dijk, T.; Hahn, E. M.; Jansen, D. N.; Li, Y.; Neele, T.; Stoelinga, M.; Turrini, A. and Zhang, L. In Dependable Software Engineering, Theories, Tools, and Applications. First International Symposium (SETTA 2015), pages 35-54, Springer, Lecture Notes in Computer Science 9409, 2015.
• IscasMC: A Web-Based Probabilistic Model Checker, Hahn, E. M.; Li, Y.; Schewe, S.; Turrini, A. and Zhang, L. In Nineteenth international symposium of the Formal Methods Europe association (FM), pages 312-317, Springer, Lecture Notes in Computer Science 8442, 2014.
• Cost Preserving Bisimulations for Probabilistic Automata, Turrini, A. and Hermanns, H. In Logical Methods in Computer Science, 4: 1-58, 2014.
• Deciding Bisimilarities on Distributions, Eisentraut, C.; Hermanns, H.; Krämer, J.; Turrini, A. and Zhang, L. In Quantitative Evaluation of Systems - 10th International Conference (QEST), pages 72-88, Springer, Lecture Notes in Computer Science 8054, 2013.
• The Quest for Minimal Quotients for Probabilistic Automata, Eisentraut, C.; Hermanns, H.; Schuster, J.; Turrini, A. and Zhang, L. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference (TACAS), pages 16-31, Springer, Lecture Notes in Computer Science 7795, 2013.
• On the Efficiency of Deciding Probabilistic Automata Weak Bisimulation, Hashemi, V.; Hermanns, H. and Turrini, A. In ECEASST, 66, 2013.
• Cost Preserving Bisimulations for Probabilistic Automata, Hermanns, H. and Turrini, A. In Concurrency Theory - 24th International Conference (CONCUR), pages 349-363, Springer, Lecture Notes in Computer Science 8052, 2013.
• Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time, Hermanns, H. and Turrini, A. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 435-447, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, LIPIcs 18, 2012.
• Conditional Automata: a Tool for Safe Removal of Negligible Events, Segala, R. and Turrini, A. In Concurrency Theory, 21th International Conference (CONCUR), pages 539-551, Springer, Lecture Notes in Computer Science 6269, 2010.
• A Quantitative Doxastic Logic for Probabilistic Processes and Applications to Information-hiding, Kramer, S.; Palamidessi, C.; Segala, R.; Andrea, T. and Braun, C. In Journal of Applied Non-classical Logics, 19: 489-516, 2009.
• Approximated Computationally Bounded Simulation Relations for Probabilistic Automata, Segala, R. and Turrini, A. In 20th IEEE Computer Security Foundations Symposium (CSF), pages 140-154, IEEE Computer Society, 2007.
• Comparative Analysis of Bisimulation Relations on Alternating and Non-Alternating Probabilistic Models, Segala, R. and Turrini, A. In Second International Conference on the Quantitative Evaluation of Systems (QEST), pages 44-53, IEEE Computer Society, 2005.

Thesis

• Hierarchical and Compositional Verification of Cryptographic Protocols, Turrini, A. Ph.D. Thesis, University of Verona, 2009.

Teaching activities

• WS17: Instructior 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