Comparative Analysis of Bisimulation Relations on Alternating and Non-Alternating Probabilistic Models. - Roberto Segala; Andrea Turrini (QEST, 2005)

Approximated Computationally Bounded Simulation Relations for Probabilistic Automata. - Roberto Segala; Andrea Turrini (CSF, 2007)

A quantitative doxastic logic for probabilistic processes and applications to information-hiding. - Simon Kramer 001; Catuscia Palamidessi; Roberto Segala; Andrea Turrini; Christelle Braun (J. Appl. Non Class. Logics, 2009)

Hierarchical and compositional verification of cryptographic protocols. - Andrea Turrini (2009)

Conditional Automata: A Tool for Safe Removal of Negligible Events. - Roberto Segala; Andrea Turrini (CONCUR, 2010)

Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time. - Holger Hermanns; Andrea Turrini (FSTTCS, 2012)

Computing Behavioral Relations for Probabilistic Concurrent Systems. - Daniel Gebler; Vahid Hashemi; Andrea Turrini (ROCKS, 2012)

Deciding Bisimilarities on Distributions. - Christian Eisentraut; Holger Hermanns; Julia Krämer; Andrea Turrini; Lijun Zhang 001 (QEST, 2013)

The Quest for Minimal Quotients for Probabilistic Automata. - Christian Eisentraut; Holger Hermanns; Johann Schuster; Andrea Turrini; Lijun Zhang 001 (TACAS, 2013)

On the Efficiency of Deciding Probabilistic Automata Weak Bisimulation. - Vahid Hashemi; Holger Hermanns; Andrea Turrini (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

iscasMc: A Web-Based Probabilistic Model Checker. - Ernst Moritz Hahn; Yi Li; Sven Schewe; Andrea Turrini; Lijun Zhang 001 (FM, 2014)

Cost Preserving Bisimulations for Probabilistic Automata. - Andrea Turrini; Holger Hermanns (Log. Methods Comput. Sci., 2014)

Preference Planning for Markov Decision Processes. - Meilun Li; Zhikun She; Andrea Turrini; Lijun Zhang 001 (AAAI, 2015)

Lazy Probabilistic Model Checking without Determinisation. - Ernst Moritz Hahn; Guangyuan Li; Sven Schewe; Andrea Turrini; Lijun Zhang 001 (CONCUR, 2015)

QPMC: A Model Checker for Quantum Programs and Protocols. - Yuan Feng 001; Ernst Moritz Hahn; Andrea Turrini; Lijun Zhang 001 (FM, 2015)

A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. - Tom van Dijk; Ernst Moritz Hahn; David N. Jansen; Yong Li 031; Thomas Neele; Mariëlle Stoelinga; Andrea Turrini; Lijun Zhang 001 (SETTA, 2015)

Polynomial time decision algorithms for probabilistic automata. - Andrea Turrini; Holger Hermanns (Inf. Comput., 2015)

A Simple Algorithm for Solving Qualitative Probabilistic Parity Games. - Ernst Moritz Hahn; Sven Schewe; Andrea Turrini; Lijun Zhang 001 (CAV (2), 2016)

Compositional Bisimulation Minimization for Interval Markov Decision Processes. - Vahid Hashemi; Holger Hermanns; Lei Song 001; K. Subramani 001; Andrea Turrini; Piotr Wojciechowski 002 (LATA, 2016)

Exploiting Robust Optimization for Interval Probabilistic Bisimulation. - Ernst Moritz Hahn; Vahid Hashemi; Holger Hermanns; Andrea Turrini (QEST, 2016)

An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties. - Yong Li 031; Wanwei Liu; Andrea Turrini; Ernst Moritz Hahn; Lijun Zhang 001 (SETTA, 2016)

Compositional Reasoning for Interval Markov Decision Processes. - Vahid Hashemi; Holger Hermanns; Andrea Turrini (CoRR, 2016)

Deciding probabilistic automata weak bisimulation: theory and practice. - Luis María Ferrer Fioriti; Vahid Hashemi; Holger Hermanns; Andrea Turrini (Formal Aspects Comput., 2016)

Model Checking Omega-regular Properties for Quantum Markov Chains . - Yuan Feng 001; Ernst Moritz Hahn; Andrea Turrini; Shenggang Ying (CONCUR, 2017)

Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes. - Ernst Moritz Hahn; Vahid Hashemi; Holger Hermanns; Morteza Lahijanian; Andrea Turrini (QEST, 2017)

Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs. - Vahid Hashemi; Andrea Turrini; Ernst Moritz Hahn; Holger Hermanns; Khaled M. Elbassioni (SETTA, 2017)

JANI: Quantitative Model and Tool Interaction. - Carlos E. Budde; Christian Dehnert; Ernst Moritz Hahn; Arnd Hartmanns; Sebastian Junges; Andrea Turrini (TACAS (2), 2017)

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games. - Ernst Moritz Hahn; Sven Schewe; Andrea Turrini; Lijun Zhang 001 (VMCAI, 2017)

Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems. - Chen Fu; Andrea Turrini; Xiaowei Huang 001; Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (IJCAI, 2018)

Advanced automata-based algorithms for program termination checking. - Yu-Fang Chen 001; Matthias Heizmann; Ondrej Lengál; Yong Li 031; Ming-Hsien Tsai 001; Andrea Turrini; Lijun Zhang 001 (PLDI, 2018)

Learning Büchi Automata and Its Applications. - Yong Li 031; Andrea Turrini; Yu-Fang Chen 001; Lijun Zhang 001 (SETSS, 2018)

Learning to Complement Büchi Automata. - Yong Li 031; Andrea Turrini; Lijun Zhang 001; Sven Schewe (VMCAI, 2018)

The quest for minimal quotients for probabilistic and Markov automata. - Christian Eisentraut; Holger Hermanns; Johann Schuster; Andrea Turrini; Lijun Zhang 001 (Inf. Comput., 2018)

Synthesizing Nested Ranking Functions for Loop Programs via SVM. - Yi Li; Xuechao Sun; Yong Li 031; Andrea Turrini; Lijun Zhang 001 (ICFEM, 2019)

ROLL 1.0: omega -Regular Language Learning Library. - Yong Li 031; Xuechao Sun; Andrea Turrini; Yu-Fang Chen 001; Junnan Xu (TACAS (1), 2019)

Model Checking Applied to Quantum Physics. - Ji Guan 001; Yuan Feng 001; Andrea Turrini; Mingsheng Ying (CoRR, 2019)

Interval Markov Decision Processes with Multiple Objectives: From Robust Strategies to Pareto Curves. - Ernst Moritz Hahn; Vahid Hashemi; Holger Hermanns; Morteza Lahijanian; Andrea Turrini (ACM Trans. Model. Comput. Simul., 2019)

A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. - Yu-Fang Chen 001; Vojtech Havlena; Ondrej Lengál; Andrea Turrini (APLAS, 2020)

Proving Non-inclusion of Büchi Automata Based on Monte Carlo Sampling. - Yong Li 031; Andrea Turrini; Xuechao Sun; Lijun Zhang 001 (ATVA, 2020)

On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report. - Carlos E. Budde; Arnd Hartmanns; Michaela Klauck; Jan Kretínský; David Parker 001; Tim Quatmann; Andrea Turrini; Zhen Zhang 006 (ISoLA (4), 2020)

Modelling and Implementation of Unmanned Aircraft Collision Avoidance. - Weizhi Feng; Cheng-Chao Huang; Andrea Turrini; Yong Li 031 (SETTA, 2020)

SVMRanker: a general termination analysis framework of loop programs via SVM. - Xie Li; Yi Li; Yong Li 031; Xuechao Sun; Andrea Turrini; Lijun Zhang 001 (ESEC/SIGSOFT FSE, 2020)

Congruence Relations for Büchi Automata. - Yong Li 031; Yih-Kuen Tsay; Andrea Turrini; Moshe Y. Vardi; Lijun Zhang 001 (FM, 2021)

Synthesizing Good-Enough Strategies for LTLf Specifications. - Yong Li 031; Andrea Turrini; Moshe Y. Vardi; Lijun Zhang 001 (IJCAI, 2021)

Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition. - Yong Li 031; Andrea Turrini; Weizhi Feng; Moshe Y. Vardi; Lijun Zhang 001 (CAV (2), 2022)

EPMC Gets Knowledge in Multi-agent Systems. - Chen Fu; Ernst Moritz Hahn; Yong Li 031; Sven Schewe; Meng Sun 002; Andrea Turrini; Lijun Zhang 001 (VMCAI, 2022)

Synthesizing ranking functions for loop programs via SVM. - Yi Li; Xie Li; Yong Li 031; Xuechao Sun; Andrea Turrini; Lijun Zhang 001 (Theor. Comput. Sci., 2022)

Probabilistic Preference Planning Problem for Markov Decision Processes. - Meilun Li; Andrea Turrini; Ernst Moritz Hahn; Zhikun She; Lijun Zhang 001 (IEEE Trans. Software Eng., 2022)

Artifact for the CAV'22 paper "Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition". - Yong Li 031; Andrea Turrini; Weizhi Feng; Moshe Y. Vardi; Lijun Zhang 001 (Zenodo, 2022)

Artifact for the CAV'22 paper "Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition". - Yong Li 031; Andrea Turrini; Weizhi Feng; Moshe Y. Vardi; Lijun Zhang 001 (Zenodo, 2022)

Scenario Approach for Parametric Markov Models. - Ying Liu 048; Andrea Turrini; Ernst Moritz Hahn; Bai Xue 001; Lijun Zhang 001 (ATVA (1), 2023)

Modular Mix-and-Match Complementation of Büchi Automata. - Vojtech Havlena; Ondrej Lengál; Yong Li 031; Barbora Smahlíková; Andrea Turrini (TACAS (1), 2023)

Modular Mix-and-Match Complementation of Büchi Automata (Technical Report). - Vojtech Havlena; Ondrej Lengál; Yong Li 031; Barbora Smahlíková; Andrea Turrini (CoRR, 2023)

A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions (Technical Report). - Yu-Fang Chen 001; Vojtech Havlena; Ondrej Lengál; Andrea Turrini (CoRR, 2023)

On the power of finite ambiguity in Büchi complementation. - Weizhi Feng; Yong Li 031; Andrea Turrini; Moshe Y. Vardi; Lijun Zhang 001 (Inf. Comput., 2023)

Artifact for the ATVA'23 paper "Scenario Approach for Parametric Markov Models". - Ying Liu 048; Andrea Turrini; Ernst Moritz Hahn; Bai Xue 001; Lijun Zhang 001 (Zenodo, 2023)

A symbolic algorithm for the case-split rule in solving word constraints with extensions. - Yu-Fang Chen 001; Vojtech Havlena; Ondrej Lengál; Andrea Turrini (J. Syst. Softw., 2023)

Model Checking for Probabilistic Multiagent Systems. - Chen Fu; Andrea Turrini; Xiaowei Huang 001; Lei Song 001; Yuan Feng 001; Lijun Zhang 001 (J. Comput. Sci. Technol., 2023)

A Scenario Approach for Parametric Markov Decision Processes. - Zhiming Chi; Ying Liu 048; Andrea Turrini; Lijun Zhang 001; David N. Jansen (Principles of Verification (2), 2024)

Measurement-Based Verification of Quantum Markov Chains. - Ji Guan 001; Yuan Feng 001; Andrea Turrini; Mingsheng Ying (CAV (3), 2024)