### Research interests

Main research interests concern the formal analysis of processes involving probability and nondeterminism. In particular current research topics are formal analysis of properties of the Segala’s Probabilistic Automata model with respect to other probabilistic models and in developing conservative extensions of such model in order to formally define and study properties of real systems using an uniform approach.

I am also interested in the study of cryptographic protocols for the development of a framework based on probabilistic automata in order to provide a rigorous mathematical background that justifies such analyses 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.

To contact me, send me an email to

<family name>@ios.ac.cn

### Publications

#### Journals and Conferences

- JANI: Quantitative Model and Tool Interaction, In TACAS, LNCS , 2017.
- Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games, In VMCAI, LNCS 10145, 2017.
- Deciding Probabilistic Automata Weak Bisimulation: Theory and Practice, In Formal Aspects of Computing, 28: 109-143, 2016.
- Compositional Bisimulation Minimization for Interval Markov Decision Processes, In LATA'16, pages 114-126, LNCS 9618, 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.
- An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties, In SETTA, pages 280-296, LNCS 9984, 2016.
- 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.
- Polynomial Time Decision Algorithms for Probabilistic Automata, In Information and Computation, 244: 134-171, 2015.
- Lazy Probabilistic Model Checking without Determinisation, In CONCUR, pages 354-367, LIPIcs 42, 2015.
- 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.
- Preference Planning for Markov Decision Processes, In The Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI-15), pages 3313-3319, AAAI Press, 2015.
- Cost Preserving Bisimulations for Probabilistic Automata, In Logical Methods in Computer Science, 4: 1-58, 2014.
- 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.
- 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 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.
- 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

- 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