arXiv subjects

Ali Asadi

Publications and source records attributed to Ali Asadi.

21 records · Page 2Linked to original sources

arXiv2020

Inductive Reachability Witnesses

In this work, we consider the fundamental problem of reachability analysis over imperative programs with real variables. The reachability property requires that a program can reach certain target states during its execution. Previous works that tackle reachability analysis are either unable to handle programs consisting of general loops (e.g. symbolic execution), or lack completeness guarantees (e.g. abstract interpretation), or are not automated (e.g. incorrectness logic/reverse Hoare logic). In contrast, we propose a novel approach for reachability analysis that can handle general programs, is (semi-)complete, and can be entirely automated for a wide family of programs. Our approach extends techniques from both invariant generation and ranking-function synthesis to reachability analysis through the notion of (Universal) Inductive Reachability Witnesses (IRWs/UIRWs). While traditional invariant generation uses over-approximations of reachable states, we consider the natural dual problem of under-approximating the set of program states that can reach a target state. We then apply an argument similar to ranking functions to ensure that all states in our under-approximation can indeed reach the target set in finitely many steps.

cs.PL↗

arXiv2020

Faster Algorithms for Quantitative Analysis of Markov Chains and Markov Decision Processes with Small Treewidth

Discrete-time Markov Chains (MCs) and Markov Decision Processes (MDPs) are two standard formalisms in system analysis. Their main associated quantitative objectives are hitting probabilities, discounted sum, and mean payoff. Although there are many techniques for computing these objectives in general MCs/MDPs, they have not been thoroughly studied in terms of parameterized algorithms, particularly when treewidth is used as the parameter. This is in sharp contrast to qualitative objectives for MCs, MDPs and graph games, for which treewidth-based algorithms yield significant complexity improvements. In this work, we show that treewidth can also be used to obtain faster algorithms for the quantitative problems. For an MC with $n$ states and $m$ transitions, we show that each of the classical quantitative objectives can be computed in $O((n+m)\cdot t^2)$ time, given a tree decomposition of the MC that has width $t$. Our results also imply a bound of $O(κ\cdot (n+m)\cdot t^2)$ for each objective on MDPs, where $κ$ is the number of strategy-iteration refinements required for the given input and objective. Finally, we make an experimental evaluation of our new algorithms on low-treewidth MCs and MDPs obtained from the DaCapo benchmark suite. Our experimental results show that on MCs and MDPs with small treewidth, our algorithms outperform existing well-established methods by one or more orders of magnitude.

cs.DS↗

arXiv2014

Hydrodynamics in black brane with hyperscaling violation metric background

In this paper we consider a metric with hyperscaling violation on black brane background. In this background we calculate the ratio of shear viscosity to entropy density with hydrodynamics information. The calculation of this quantity lead us to constraint $θ$ as $3\leqθ<4$, and $θ\leq0$. In that case we show that the quantity of $\fracη{s}$ not dependent to hyperscaling violation parameter $θ.$ Our results about ratio of shear viscosity to entropy density in direct of $QCD$ point of view agree with other works in literature as $1/4π$.

hep-th↗