Showing 1–14 of 14 results for author: Turrini, A

Scenario Approach for Parametric Markov Models

Authors: Ying Liu, Andrea Turrini, Moritz Hahn, Bai Xue, Lijun Zhang

Abstract: In this paper, we propose an approximating framework for analyzing parametric Markov models. Instead of computing complex rational functions encoding the reachability probability and the reward values of the parametric model, we exploit the scenario approach to synthesize a relatively simple polynomial approximation. The approximation is probably approximately correct (PAC), meaning that with high… ▽ More In this paper, we propose an approximating framework for analyzing parametric Markov models. Instead of computing complex rational functions encoding the reachability probability and the reward values of the parametric model, we exploit the scenario approach to synthesize a relatively simple polynomial approximation. The approximation is probably approximately correct (PAC), meaning that with high confidence, the approximating function is close to the actual function with an allowable error. With the PAC approximations, one can check properties of the parametric Markov models. We show that the scenario approach can also be used to check PRCTL properties directly, without synthesizing the polynomial at first hand. We have implemented our algorithm in a prototype tool and conducted thorough experiments. The experimental results demonstrate that our tool is able to compute polynomials for more benchmarks than state of the art tools such as PRISM and Storm, confirming the efficacy of our PAC-based synthesis. △ Less

Submitted 13 November, 2023; v1 submitted 17 April, 2023; originally announced April 2023.

Comments: 24 pages, 8 figures; updated to add acknowledgements and data availability

A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions (Technical Report)

Authors: Yu-Fang Chen, Vojtěch Havlena, Ondřej Lengál, Andrea Turrini

Abstract: Case split is a core proof rule in current decision procedures for the theory of string constraints. Its use is the primary cause of the state space explosion in string constraint solving, since it is the only rule that creates branches in the proof tree. Moreover, explicit handling of the case split rule may cause recomputation of the same tasks in multiple branches of the proof tree. In this pap… ▽ More Case split is a core proof rule in current decision procedures for the theory of string constraints. Its use is the primary cause of the state space explosion in string constraint solving, since it is the only rule that creates branches in the proof tree. Moreover, explicit handling of the case split rule may cause recomputation of the same tasks in multiple branches of the proof tree. In this paper, we propose a symbolic algorithm that significantly reduces such a redundancy. In particular, we encode a string constraint as a regular language and proof rules as rational transducers. This allows us to perform similar steps in the proof tree only once, alleviating the state space explosion. We also extend the encoding to handle arbitrary Boolean combinations of string constraints, length constraints, and regular constraints. In our experimental results, we validate that our technique works in many practical cases where other state-of-the-art solvers fail to provide an answer; our Python prototype implementation solved over 50 % of string constraints that could not be solved by the other tools. △ Less

Submitted 2 March, 2023; originally announced March 2023.

Comments: An extended version of a paper from APLAS'20, accepted to Journal of Systems and Software

Modular Mix-and-Match Complementation of Büchi Automata (Technical Report)

Authors: Vojtěch Havlena, Ondřej Lengál, Yong Li, Barbora Šmahlíková, Andrea Turrini

Abstract: Complementation of nondeterministic Büchi automata (BAs) is an important problem in automata theory with numerous applications in formal verification, such as termination analysis of programs, model checking, or in decision procedures of some logics. We build on ideas from a recent work on BA determinization by Li et al. and propose a new modular algorithm for BA complementation. Our algorithm all… ▽ More Complementation of nondeterministic Büchi automata (BAs) is an important problem in automata theory with numerous applications in formal verification, such as termination analysis of programs, model checking, or in decision procedures of some logics. We build on ideas from a recent work on BA determinization by Li et al. and propose a new modular algorithm for BA complementation. Our algorithm allows to combine several BA complementation procedures together, with one procedure for a subset of the BA's strongly connected components (SCCs). In this way, one can exploit the structure of particular SCCs (such as when they are inherently weak or deterministic) and use more efficient specialized algorithms, regardless of the structure of the whole BA. We give a general framework into which partial complementation procedures can be plugged in, and its instantiation with several algorithms. The framework can, in general, produce a complement with an Emerson-Lei acceptance condition, which can often be more compact. Using the algorithm, we were able to establish an exponentially better new upper bound of $O(4n)$ for complementation of the recently introduced class of elevator automata. We implemented the algorithm in a prototype and performed a comprehensive set of experiments on a large set of benchmarks, showing that our framework complements well the state of the art and that it can serve as a basis for future efficient BA complementation and inclusion checking algorithms. △ Less

Submitted 4 January, 2023; originally announced January 2023.

Comments: To appear in Proc. of TACAS'23

Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition

Authors: Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y. Vardi, Lijun Zhang

Abstract: The determinization of a nondeterministic Büchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synthesis. The standard determinization constructions, such as the ones based on the Safra-Piterman's approach, work on the whole NBA. In this work we propose a divide-and-conquer determinization approach. To this end, we fir… ▽ More The determinization of a nondeterministic Büchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synthesis. The standard determinization constructions, such as the ones based on the Safra-Piterman's approach, work on the whole NBA. In this work we propose a divide-and-conquer determinization approach. To this end, we first classify the strongly connected components (SCCs) of the given NBA as inherently weak, deterministic accepting, and nondeterministic accepting. We then present how to determinize each type of SCC independently from the others; this results in an easier handling of the determinization algorithm that takes advantage of the structure of that SCC. Once all SCCs have been determinized, we show how to compose them so to obtain the final equivalent deterministic Emerson-Lei automaton, which can be converted into a deterministic Rabin automaton without blow-up of states and transitions. We implement our algorithm in a our tool COLA and empirically evaluate COLA with the state-of-the-art tools Spot and OWL on a large set of benchmarks from the literature. The experimental results show that our prototype COLA outperforms Spot and OWL regarding the number of states and transitions. △ Less

Submitted 27 June, 2022; originally announced June 2022.

Comments: This is an extended version of our CAV'22 paper

ACM Class: F.4.3

On the Power of Finite Ambiguity in Büchi Complementation

Authors: Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang

Abstract: In this work, we exploit the power of \emph{finite ambiguity} for the complementation problem of Büchi automata by using reduced run directed acyclic graphs (DAGs) over infinite words, in which each vertex has at most one predecessor; these reduced run DAGs have only a finite number of infinite runs, thus obtaining the finite ambiguity in Büchi complementation. We show how to use this type of redu… ▽ More In this work, we exploit the power of \emph{finite ambiguity} for the complementation problem of Büchi automata by using reduced run directed acyclic graphs (DAGs) over infinite words, in which each vertex has at most one predecessor; these reduced run DAGs have only a finite number of infinite runs, thus obtaining the finite ambiguity in Büchi complementation. We show how to use this type of reduced run DAGs as a unified tool to optimize both rank-based and slice-based complementation constructions for Büchi automata with a finite degree of ambiguity. As a result, given a Büchi automaton with $n$ states and a finite degree of ambiguity, the number of states in the complementary Büchi automaton constructed by the classical rank-based and slice-based complementation constructions can be improved from $2^{\mathsf{O}(n \log n)}$ and $\mathsf{O}((3n)^{n})$ to $\mathsf{O}(6^{n}) \subseteq 2^{\mathsf{O}(n)}$ and $\mathsf{O}(4^{n})$, respectively. We further show how to construct such reduced run DAGs for limit deterministic Büchi automata and obtain a specialized complementation algorithm, thus demonstrating the generality of the power of finite ambiguity. △ Less

Submitted 2 March, 2023; v1 submitted 27 September, 2021; originally announced September 2021.

Congruence Relations for Büchi Automata

Authors: Yong Li, Yih-Kuen Tsay, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang

Abstract: We revisit here congruence relations for Büchi automata, which play a central role in the automata-based verification. The size of the classical congruence relation is in $3^{\mathcal{O}(n^2)}$, where $n$ is the number of states of a given Büchi automaton $\mathcal{A}$. Here we present improved congruence relations that can be exponentially coarser than the classical one. We further give asymptoti… ▽ More We revisit here congruence relations for Büchi automata, which play a central role in the automata-based verification. The size of the classical congruence relation is in $3^{\mathcal{O}(n^2)}$, where $n$ is the number of states of a given Büchi automaton $\mathcal{A}$. Here we present improved congruence relations that can be exponentially coarser than the classical one. We further give asymptotically optimal congruence relations of size $2^{\mathcal{O}(n \log n)}$. Based on these optimal congruence relations, we obtain an optimal translation from Büchi automata to a family of deterministic finite automata (FDFW) that accepts the complementary language. To the best of our knowledge, our construction is the first direct and optimal translation from Büchi automata to FDFWs. △ Less

Submitted 10 May, 2021; v1 submitted 8 April, 2021; originally announced April 2021.

ACM Class: F.4.3

Proving Non-Inclusion of Büchi Automata based on Monte Carlo Sampling

Authors: Yong Li, Andrea Turrini, Xuechao Sun, Lijun Zhang

Abstract: The search for a proof of correctness and the search for counterexamples (bugs) are complementary aspects of verification. In order to maximize the practical use of verification tools it is better to pursue them at the same time. While this is well-understood in the termination analysis of programs, this is not the case for the language inclusion analysis of Büchi automata, where research mainly f… ▽ More The search for a proof of correctness and the search for counterexamples (bugs) are complementary aspects of verification. In order to maximize the practical use of verification tools it is better to pursue them at the same time. While this is well-understood in the termination analysis of programs, this is not the case for the language inclusion analysis of Büchi automata, where research mainly focused on improving algorithms for proving language inclusion, with the search for counterexamples left to the expensive complementation operation. In this paper, we present $\mathsf{IMC}^2$, a specific algorithm for proving Büchi automata non-inclusion $\mathcal{L}(\mathcal{A}) \not\subseteq \mathcal{L}(\mathcal{B})$, based on Grosu and Smolka's algorithm $\mathsf{MC}^2$ developed for Monte Carlo model checking against LTL formulas. The algorithm we propose takes $M = \lceil \ln δ/ \ln (1-ε) \rceil$ random lasso-shaped samples from $\mathcal{A}$ to decide whether to reject the hypothesis $\mathcal{L}(\mathcal{A}) \not\subseteq \mathcal{L}(\mathcal{B})$, for given error probability $ε$ and confidence level $1 - δ$. With such a number of samples, $\mathsf{IMC}^2$ ensures that the probability of witnessing $\mathcal{L}(\mathcal{A}) \not\subseteq \mathcal{L}(\mathcal{B})$ via further sampling is less than $δ$, under the assumption that the probability of finding a lasso counterexample is larger than $ε$. Extensive experimental evaluation shows that $\mathsf{IMC}^2$ is a fast and reliable way to find counterexamples to Büchi automata inclusion. △ Less

Submitted 6 July, 2020; v1 submitted 5 July, 2020; originally announced July 2020.

Comments: Accepted to ATVA 2020; typos corrected; authors corrected

Model Checking Applied to Quantum Physics

Authors: Ji Guan, Yuan Feng, Andrea Turrini, Mingsheng Ying

Abstract: Model checking has been successfully applied to verification of computer hardware and software, communication systems and even biological systems. In this paper, we further push the boundary of its applications and show that it can be adapted for applications in quantum physics. More explicitly, we show how quantum statistical and many-body systems can be modeled as quantum Markov chains, and some… ▽ More Model checking has been successfully applied to verification of computer hardware and software, communication systems and even biological systems. In this paper, we further push the boundary of its applications and show that it can be adapted for applications in quantum physics. More explicitly, we show how quantum statistical and many-body systems can be modeled as quantum Markov chains, and some of their properties that interest physicists can be specified in linear-time temporal logics. Then we present an efficient algorithm to check these properties. A few case studies are given to demonstrate the use of our algorithm to actual quantum physical problems. △ Less

Submitted 8 February, 2019; originally announced February 2019.

Compositional Reasoning for Interval Markov Decision Processes

Authors: Vahid Hashemi, Holger Hermanns, Andrea Turrini

Abstract: Model checking probabilistic CTL properties of Markov decision processes with convex uncertainties has been recently investigated by Puggelli et al. Such model checking algorithms typically suffer from the state space explosion. In this paper, we address probabilistic bisimulation to reduce the size of such an MDP while preserving the probabilistic CTL properties it satisfies. In particular, we di… ▽ More Model checking probabilistic CTL properties of Markov decision processes with convex uncertainties has been recently investigated by Puggelli et al. Such model checking algorithms typically suffer from the state space explosion. In this paper, we address probabilistic bisimulation to reduce the size of such an MDP while preserving the probabilistic CTL properties it satisfies. In particular, we discuss the key ingredients to build up the operations of parallel composition for composing interval MDP components at run-time. More precisely, we investigate how the parallel composition operator for interval MDPs can be defined so as to arrive at a congruence closure. As a result, we show that probabilistic bisimulation for interval MDPs is congruence with respect to two facets of parallelism, namely synchronous product and interleaving. △ Less

Submitted 28 July, 2016; originally announced July 2016.

MSC Class: 68Q10; 68Q60; 68Q85; 68Q25

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games

Authors: Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, Lijun Zhang

Abstract: 2.5 player parity games combine the challenges posed by 2.5 player reachability games and the qualitative analysis of parity games. These two types of problems are best approached with different types of algorithms: strategy improvement algorithms for 2.5 player reachability games and recursive algorithms for the qualitative analysis of parity games. We present a method that - in contrast to exist… ▽ More 2.5 player parity games combine the challenges posed by 2.5 player reachability games and the qualitative analysis of parity games. These two types of problems are best approached with different types of algorithms: strategy improvement algorithms for 2.5 player reachability games and recursive algorithms for the qualitative analysis of parity games. We present a method that - in contrast to existing techniques - tackles both aspects with the best suited approach and works exclusively on the 2.5 player game itself. The resulting technique is powerful enough to handle games with several million states. △ Less

Submitted 5 July, 2016; originally announced July 2016.

An Efficient Synthesis Algorithm for Parametric Markov Chains Against Linear Time Properties

Authors: Yong Li, Wanwei Liu, Andrea Turrini, Ernst Moritz Hahn, Lijun Zhang

Abstract: In this paper, we propose an efficient algorithm for the parameter synthesis of PLTL formulas with respect to parametric Markov chains. The PLTL formula is translated to an almost fully partitioned Büchi automaton which is then composed with the parametric Markov chain. We then reduce the problem to solving an optimisation problem, allowing to decide the satisfaction of the formula using an SMT so… ▽ More In this paper, we propose an efficient algorithm for the parameter synthesis of PLTL formulas with respect to parametric Markov chains. The PLTL formula is translated to an almost fully partitioned Büchi automaton which is then composed with the parametric Markov chain. We then reduce the problem to solving an optimisation problem, allowing to decide the satisfaction of the formula using an SMT solver. The algorithm works also for interval Markov chains. The complexity is linear in the size of the Markov chain, and exponential in the size of the formula. We provide a prototype and show the efficiency of our approach on a number of benchmarks. △ Less

Submitted 14 May, 2016; originally announced May 2016.

Cost Preserving Bisimulations for Probabilistic Automata

Authors: Andrea Turrini, Holger Hermanns

Abstract: Probabilistic automata constitute a versatile and elegant model for concurrent probabilistic systems. They are equipped with a compositional theory supporting abstraction, enabled by weak probabilistic bisimulation serving as the reference notion for summarising the effect of abstraction. This paper considers probabilistic automata augmented with costs. It extends the notions of weak transitions… ▽ More Probabilistic automata constitute a versatile and elegant model for concurrent probabilistic systems. They are equipped with a compositional theory supporting abstraction, enabled by weak probabilistic bisimulation serving as the reference notion for summarising the effect of abstraction. This paper considers probabilistic automata augmented with costs. It extends the notions of weak transitions in probabilistic automata in such a way that the costs incurred along a weak transition are captured. This gives rise to cost-preserving and cost-bounding variations of weak probabilistic bisimilarity, for which we establish compositionality properties with respect to parallel composition. Furthermore, polynomial-time decision algorithms are proposed, that can be effectively used to compute reward-bounding abstractions of Markov decision processes in a compositional manner. △ Less

Submitted 16 February, 2015; v1 submitted 30 October, 2014; originally announced October 2014.

Journal ref: Logical Methods in Computer Science, Volume 10, Issue 4 (December 18, 2014) lmcs:1050

Lazy Probabilistic Model Checking without Determinisation

Authors: Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, Lijun Zhang

Abstract: The bottleneck in the quantitative analysis of Markov chains and Markov decision processes against specifications given in LTL or as some form of nondeterministic Büchi automata is the inclusion of a determinisation step of the automaton under consideration. In this paper, we show that full determinisation can be avoided: subset and breakpoint constructions suffice. We have implemented our approac… ▽ More The bottleneck in the quantitative analysis of Markov chains and Markov decision processes against specifications given in LTL or as some form of nondeterministic Büchi automata is the inclusion of a determinisation step of the automaton under consideration. In this paper, we show that full determinisation can be avoided: subset and breakpoint constructions suffice. We have implemented our approach---both explicit and symbolic versions---in a prototype tool. Our experiments show that our prototype can compete with mature tools like PRISM. △ Less

Submitted 24 April, 2015; v1 submitted 12 November, 2013; originally announced November 2013.

Comments: 38 pages. Updated version for introducing the following changes: - general improvement on paper presentation; - extension of the approach to avoid full determinisation; - added proofs for such an extension; - added case studies; - updated old case studies to reflect the added extension

ACM Class: G.3; D.2.4

Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time

Authors: Holger Hermanns, Andrea Turrini

Abstract: Deciding in an efficient way weak probabilistic bisimulation in the context of Probabilistic Automata is an open problem for about a decade. In this work we close this problem by proposing a procedure that checks in polynomial time the existence of a weak combined transition satisfying the step condition of the bisimulation. We also present several extensions of weak combined transitions, such as… ▽ More Deciding in an efficient way weak probabilistic bisimulation in the context of Probabilistic Automata is an open problem for about a decade. In this work we close this problem by proposing a procedure that checks in polynomial time the existence of a weak combined transition satisfying the step condition of the bisimulation. We also present several extensions of weak combined transitions, such as hyper-transitions and the new concepts of allowed weak combined and hyper-transitions and of equivalence matching, that turn out to be verifiable in polynomial time as well. These results set the ground for the development of more effective compositional analysis algorithms for probabilistic systems. △ Less

Submitted 15 July, 2012; v1 submitted 2 May, 2012; originally announced May 2012.

Comments: Polished version with a more complete running example and typo fixes

ACM Class: G.3; F.2