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, In J. Syst. Softw., 2023.
- On the Power of Finite Ambiguity in Büchi Complementation, In Inf. Comput., 2023.
- Modular Mix-and-Match Complementation of Büchi Automata, In TACAS, LNCS , 2023.
- Scenario Approach for Parametric Markov Models, In ATVA, LNCS , 2023.
- EPMC Gets Knowledge in Multi-agent Systems, In VMCAI, pages 93-107, Springer, Lecture Notes in Computer Science 13182, 2022.
- Model Checking for Probabilistic Multiagent Systems, In Journal of Computer Science and Technology, 2022.
- Synthesizing Ranking Functions for Loop Programs via SVM, In TCS, 2022.
- Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition, In CAV, pages 152-173, Springer, Lecture Notes in Computer Science 13372, 2022.
- An Introduction to Quantum Model Checking, In Applied Sciences, 12, 2022.
- Congruence Relations for Büchi Automata, In FM, pages 465-482, Springer, Lecture Notes in Computer Science 13047, 2021.
- Synthesizing Good-Enough Strategies for LTLf Specifications, In IJCAI, pages 4144-4151, ijcai.org, 2021.
- An Axiom System of Probabilistic Mu-Calculus, In Tsinghua Science and Technology, 27: 372-385, 2021.
- On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report, 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, In APLAS, pages 343-363, Springer, 2020.
- Modelling and Implementation of Unmanned Aircraft Collision Avoidance, In SETTA, pages 52-69, Springer, Lecture Notes in Computer Science 12153, 2020.
- SVMRanker: A General Termination Analysis Framework of Loop Programs via SVM, In ESEC/FSE, pages 1635-1639, ACM, 2020.
- Probabilistic Preference Planning Problem for Markov Decision Processes, In IEEE Trans. Software Eng., 48: 1545-1559, 2020.
- Proving Non-Inclusion of Büchi Automata based on Monte Carlo Sampling, In ATVA, pages 467-483, Springer, LNCS 12302, 2020.
- Interval Markov Decision Processes with Multiple Objectives: from Robust Strategies to Pareto Curves, In TOMACS, 29, 2019.
- Synthesizing Nested Ranking Functions for Loop Programs via SVM, In ICFEM, pages 438-454, LNCS 11852, 2019.
- ROLL 1.0: ω-Regular Language Learning Library, In TACAS, pages 365-371, LNCS 11427, 2019.
- Advanced Automata-based Algorithms for Program Termination Checking, In PLDI, pages 135-150, 2018.
- The Quest for Minimal Quotients for Probabilistic and Markov Automata, In Inf. Comput., 262: 162-186, 2018.
- Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems, In IJCAI, pages 4757-4763, ijcai.org, 2018.
- 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, pages 38-98, Springer, Lecture Notes in Computer Science 11430, 2018.
- Learning to Complement Büchi Automata, In VMCAI, pages 313-335, Springer, LNCS 10747, 2018.
- JANI: Quantitative Model and Tool Interaction, In TACAS, pages 151-168, LNCS 10206, 2017.
- Model Checking ω-regular Properties for Quantum Markov Chains, 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, In QEST, pages 207-223, LNCS 10503, 2017.
- Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games, In VMCAI, pages 266-287, LNCS 10145, 2017.
- Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs, In SETTA, pages 25-41, LNCS 10606, 2017. (Best paper award)
- Deciding Probabilistic Automata Weak Bisimulation: Theory and Practice, In Formal Aspects of Computing, 28: 109-143, 2016.
- Exploiting Robust Optimization for Interval Probabilistic Bisimulation, In QEST, pages 55-71, LNCS 9826, 2016.
- A Simple Algorithm for Solving Qualitative Probabilistic Parity Games, In CAV, pages 291-311, LNCS 9780, 2016.
- Compositional Bisimulation Minimization for Interval Markov Decision Processes, In LATA'16, pages 114-126, LNCS 9618, 2016.
- An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties, In SETTA, pages 280-296, LNCS 9984, 2016.
- QPMC: A Model Checker for Quantum Programs and Protocols, 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, In CONCUR, pages 354-367, LIPIcs 42, 2015.
- Preference Planning for Markov Decision Processes, In The Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI-15), pages 3313-3319, AAAI Press, 2015.
- Polynomial Time Decision Algorithms for Probabilistic Automata, In Information and Computation, 244: 134-171, 2015.
- A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking, 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, 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, In Logical Methods in Computer Science, 4: 1-58, 2014.
- Deciding Bisimilarities on Distributions, 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, 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, In ECEASST, 66, 2013.
- Cost Preserving Bisimulations for Probabilistic Automata, 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, 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, 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, In Journal of Applied Non-classical Logics, 19: 489-516, 2009.
- Approximated Computationally Bounded Simulation Relations for Probabilistic Automata, 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, 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, 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