Showing 1–50 of 62 results for author: Viswanathan, M

Deciding branching hyperproperties for real time systems

Authors: Nabarun Deka, Minjian Zhang, Rohit Chadha, Mahesh Viswanathan

Abstract: Security properties of real-time systems often involve reasoning about hyper-properties, as opposed to properties of single executions or trees of executions. These hyper-properties need to additionally be expressive enough to reason about real-time constraints. Examples of such properties include information flow, side channel attacks and service-level agreements. In this paper we study computati… ▽ More Security properties of real-time systems often involve reasoning about hyper-properties, as opposed to properties of single executions or trees of executions. These hyper-properties need to additionally be expressive enough to reason about real-time constraints. Examples of such properties include information flow, side channel attacks and service-level agreements. In this paper we study computational problems related to a branching-time, hyper-property extension of metric temporal logic (MTL) that we call HCMTL*. We consider both the interval-based and point-based semantics of this logic. The verification problem that we consider is to determine if a given HCMTL* formula $\varphi$ is true in a system represented by a timed automaton. We show that this problem is undecidable. We then show that the verification problem is decidable if we consider executions upto a fixed time horizon $T$. Our decidability result relies on reducing the verification problem to the truth of an MSO formula over reals with a bounded time interval. △ Less

Submitted 20 May, 2024; originally announced May 2024.

Amide Proton Transfer (APT) imaging in tumor with a machine learning approach using partially synthetic data

Authors: Malvika Viswanathan, Leqi Yin, Yashwant Kurmi, Zhongliang Zu

Abstract: Machine learning (ML) has been increasingly used to quantify chemical exchange saturation transfer (CEST) effect. ML models are typically trained using either measured data or fully simulated data. However, training with measured data often lacks sufficient training data, while training with fully simulated data may introduce bias due to limited simulations pools. This study introduces a new platf… ▽ More Machine learning (ML) has been increasingly used to quantify chemical exchange saturation transfer (CEST) effect. ML models are typically trained using either measured data or fully simulated data. However, training with measured data often lacks sufficient training data, while training with fully simulated data may introduce bias due to limited simulations pools. This study introduces a new platform that combines simulated and measured components to generate partially synthetic CEST data, and to evaluate its feasibility for training ML models to predict amide proton transfer (APT) effect. Partially synthetic CEST signals were created using an inverse summation of APT effects from simulations and the other components from measurements. Training data were generated by varying APT simulation parameters and applying scaling factors to adjust the measured components, achieving a balance between simulation flexibility and fidelity. First, tissue-mimicking CEST signals along with ground truth information were created using multiple-pool model simulations to validate this method. Second, an ML model was trained individually on partially synthetic data, in vivo data, and fully simulated data, to predict APT effect in rat brains bearing 9L tumors. Experiments on tissue-mimicking data suggest that the ML method using the partially synthetic data is accurate in predicting APT. In vivo experiments suggest that our method provides more accurate and robust prediction than the training using in vivo data and fully synthetic data. Partially synthetic CEST data can address the challenges in conventional ML methods. △ Less

Submitted 13 December, 2023; v1 submitted 2 November, 2023; originally announced November 2023.

Comments: Updated Supporting Information typos

Searching for Optimal Runtime Assurance via Reachability and Reinforcement Learning

Authors: Kristina Miller, Christopher K. Zeitler, William Shen, Kerianne Hobbs, Sayan Mitra, John Schierman, Mahesh Viswanathan

Abstract: A runtime assurance system (RTA) for a given plant enables the exercise of an untrusted or experimental controller while assuring safety with a backup (or safety) controller. The relevant computational design problem is to create a logic that assures safety by switching to the safety controller as needed, while maximizing some performance criteria, such as the utilization of the untrusted controll… ▽ More A runtime assurance system (RTA) for a given plant enables the exercise of an untrusted or experimental controller while assuring safety with a backup (or safety) controller. The relevant computational design problem is to create a logic that assures safety by switching to the safety controller as needed, while maximizing some performance criteria, such as the utilization of the untrusted controller. Existing RTA design strategies are well-known to be overly conservative and, in principle, can lead to safety violations. In this paper, we formulate the optimal RTA design problem and present a new approach for solving it. Our approach relies on reward sha** and reinforcement learning. It can guarantee safety and leverage machine learning technologies for scalability. We have implemented this algorithm and present experimental results comparing our approach with state-of-the-art reachability and simulation-based RTA approaches in a number of scenarios using aircraft models in 3D space with complex safety requirements. Our approach can guarantee safety while increasing utilization of the experimental controller over existing approaches. △ Less

Submitted 6 October, 2023; originally announced October 2023.

Deciding Differential Privacy of Online Algorithms with Multiple Variables

Authors: Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan, Bishnu Bhusal

Abstract: We consider the problem of checking the differential privacy of online randomized algorithms that process a stream of inputs and produce outputs corresponding to each input. This paper generalizes an automaton model called DiP automata (See arXiv:2104.14519) to describe such algorithms by allowing multiple real-valued storage variables. A DiP automaton is a parametric automaton whose behavior depe… ▽ More We consider the problem of checking the differential privacy of online randomized algorithms that process a stream of inputs and produce outputs corresponding to each input. This paper generalizes an automaton model called DiP automata (See arXiv:2104.14519) to describe such algorithms by allowing multiple real-valued storage variables. A DiP automaton is a parametric automaton whose behavior depends on the privacy budget $ε$. An automaton $A$ will be said to be differentially private if, for some $\mathfrak{D}$, the automaton is $\mathfrak{D}ε$-differentially private for all values of $ε>0$. We identify a precise characterization of the class of all differentially private DiP automata. We show that the problem of determining if a given DiP automaton belongs to this class is PSPACE-complete. Our PSPACE algorithm also computes a value for $\mathfrak{D}$ when the given automaton is differentially private. The algorithm has been implemented, and experiments demonstrating its effectiveness are presented. △ Less

Submitted 12 September, 2023; originally announced September 2023.

ACM Class: D.2.4; F.3.1

RTAEval: A framework for evaluating runtime assurance logic

Authors: Kristina Miller, Christopher K. Zeitler, William Shen, Mahesh Viswanathan, Sayan Mitra

Abstract: Runtime assurance (RTA) addresses the problem of kee** an autonomous system safe while using an untrusted (or experimental) controller. This can be done via logic that explicitly switches between the untrusted controller and a safety controller, or logic that filters the input provided by the untrusted controller. While several tools implement specific instances of RTAs, there is currently no fr… ▽ More Runtime assurance (RTA) addresses the problem of kee** an autonomous system safe while using an untrusted (or experimental) controller. This can be done via logic that explicitly switches between the untrusted controller and a safety controller, or logic that filters the input provided by the untrusted controller. While several tools implement specific instances of RTAs, there is currently no framework for evaluating different approaches. Given the importance of the RTA problem in building safe autonomous systems, an evaluation tool is needed. In this paper, we present the RTAEval framework as a low code framework that can be used to quickly evaluate different RTA logics for different types of agents in a variety of scenarios. RTAEval is designed to quickly create scenarios, run different RTA logics, and collect data that can be used to evaluate and visualize performance. In this paper, we describe different components of RTAEval and show how it can be used to create and evaluate scenarios involving multiple aircraft models. △ Less

Submitted 5 June, 2023; originally announced June 2023.

A fermionic path integral for exact enumeration of polygons on the simple cubic lattice

Authors: G. M. Viswanathan

Abstract: Enumerating polygons on regular lattices is a classic problem in rigorous statistical mechanics. The goal of enumerating polygons on the square lattice via fermionic path integration was achieved using a free-fermion quadratic action in the late 1970s. Given that polygon edges only link 2 vertices, it is considered plausible, if not natural, that an action of degree 2 in the Grassmann variables mi… ▽ More Enumerating polygons on regular lattices is a classic problem in rigorous statistical mechanics. The goal of enumerating polygons on the square lattice via fermionic path integration was achieved using a free-fermion quadratic action in the late 1970s. Given that polygon edges only link 2 vertices, it is considered plausible, if not natural, that an action of degree 2 in the Grassmann variables might suffice to enumerate lattice polygons in any dimension. Nevertheless, on nonplanar lattices the problem has remained open for more than four decades. Here we derive the Grassmann action for exact enumeration of polygons on the simple cubic lattice. Moreover, we prove that this action is not quadratic but quartic -- corresponding to a model of interacting fermions. △ Less

Submitted 7 June, 2023; v1 submitted 26 May, 2023; originally announced May 2023.

Comments: Submitted to Physical Review B

Sound Dynamic Deadlock Prediction in Linear Time

Authors: Hünkar Can Tunç, Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan

Abstract: Deadlocks are one of the most notorious concurrency bugs, and significant research has focused on detecting them efficiently. Dynamic predictive analyses work by observing concurrent executions, and reason about alternative interleavings that can witness concurrency bugs. Such techniques offer scalability and sound bug reports, and have emerged as an effective approach for concurrency bug detectio… ▽ More Deadlocks are one of the most notorious concurrency bugs, and significant research has focused on detecting them efficiently. Dynamic predictive analyses work by observing concurrent executions, and reason about alternative interleavings that can witness concurrency bugs. Such techniques offer scalability and sound bug reports, and have emerged as an effective approach for concurrency bug detection, such as data races. Effective dynamic deadlock prediction, however, has proven a challenging task, as no deadlock predictor currently meets the requirements of soundness, high-precision, and efficiency. In this paper, we first formally establish that this tradeoff is unavoidable, by showing that (a) sound and complete deadlock prediction is intractable, in general, and (b) even the seemingly simpler task of determining the presence of potential deadlocks, which often serve as unsound witnesses for actual predictable deadlocks, is intractable. The main contribution of this work is a new class of predictable deadlocks, called sync(hronization)-preserving deadlocks. Informally, these are deadlocks that can be predicted by reordering the observed execution while preserving the relative order of conflicting critical sections. We present two algorithms for sound deadlock prediction based on this notion. Our first algorithm SPDOffline detects all sync-preserving deadlocks, with running time that is linear per abstract deadlock pattern, a novel notion also introduced in this work. Our second algorithm SPDOnline predicts all sync-preserving deadlocks that involve two threads in a strictly online fashion, runs in overall linear time, and is better suited for a runtime monitoring setting. We implemented both our algorithms and evaluated their ability to perform offline and online deadlock-prediction on a large dataset of standard benchmarks. △ Less

Submitted 25 June, 2023; v1 submitted 7 April, 2023; originally announced April 2023.

Stack-Aware Hyperproperties

Authors: Ali Bajwa, Minjian Zhang, Rohit Chadha, Mahesh Viswanathan

Abstract: A hyperproperty relates executions of a program and is used to formalize security objectives such as confidentiality, non-interference, privacy, and anonymity. Formally, a hyperproperty is a collection of allowable sets of executions. A program violates a hyperproperty if the set of its executions is not in the collection specified by the hyperproperty. The logic HyperCTL^* has been proposed in th… ▽ More A hyperproperty relates executions of a program and is used to formalize security objectives such as confidentiality, non-interference, privacy, and anonymity. Formally, a hyperproperty is a collection of allowable sets of executions. A program violates a hyperproperty if the set of its executions is not in the collection specified by the hyperproperty. The logic HyperCTL^* has been proposed in the literature to formally specify and verify hyperproperties. The problem of checking whether a finite-state program satisfies a HyperCTL^* formula is known to be decidable. However, the problem turns out to be undecidable for procedural (recursive) programs. Surprisingly, we show that decidability can be restored if we consider restricted classes of hyperproperties, namely those that relate only those executions of a program which have the same call-stack access pattern. We call such hyperproperties, \emph{stack-aware hyperproperties.} Our decision procedure can be used as a proof method for establishing security objectives such as noninference for recursive programs, and also for refuting security objectives such as observational determinism. Further, if the call stack size is observable to the attacker, the decision procedure provides exact verification. △ Less

Submitted 26 January, 2023; originally announced January 2023.

ACM Class: D.2.4; F.4.1

Information parity on cortical functional brain networks increases under psychedelic influences

Authors: Aline Viol, Gandhi M. Viswanathan, Oleksandra Soldatkina, Fernanda Palhano-Fontes, Heloisa Onias, Draulio de Araujo, Philipp Hoevel

Abstract: The physical basis of consciousness is one of the most intriguing open questions that contemporary science aims to solve. By approaching the brain as an interactive information system, complex network theory has greatly contributed to understand brain process in different states of mind. We study an non-ordinary state of mind by comparing resting-state functional brain networks of individuals in t… ▽ More The physical basis of consciousness is one of the most intriguing open questions that contemporary science aims to solve. By approaching the brain as an interactive information system, complex network theory has greatly contributed to understand brain process in different states of mind. We study an non-ordinary state of mind by comparing resting-state functional brain networks of individuals in two different conditions: before and after the ingestion of the psychedelic brew Ayahuasca. In order to quantify the functional, statistical symmetries between brain region connectivity, we calculate the pairwise information parity of the functional brain networks. Unlike most of usual network quantification, which is done on a local or global scale, information parity quantifies the pairwise statistical similarities considering the entire network structure. We detect an increase in the average information parity on brain networks of individuals under psychedelic influences. Notably, the information parity between regions from the limbic system and frontal cortex is consistently higher for all the individuals while under the psychedelic influence. △ Less

Submitted 28 July, 2022; originally announced July 2022.

Comments: 9 pages 3 figures

What does it take to solve the 3D Ising model? Minimal necessary conditions for a valid solution

Authors: G. M. Viswanathan, M. A. G. Portillo, E. P. Raposo, M. G. E. da Luz

Abstract: Exact solution of the Ising model on the simple cubic lattice is one of the long-standing open problems in rigorous statistical mechanics. Indeed, it is generally believed that settling it would constitute a methodological breakthrough, fomenting great prospects for further application, similarly to what happened when Lars Onsager solved the two dimensional model eighty years ago. Hence, there hav… ▽ More Exact solution of the Ising model on the simple cubic lattice is one of the long-standing open problems in rigorous statistical mechanics. Indeed, it is generally believed that settling it would constitute a methodological breakthrough, fomenting great prospects for further application, similarly to what happened when Lars Onsager solved the two dimensional model eighty years ago. Hence, there have been many attempts to find analytic expressions for the exact partition function $Z$, but all such attempts have failed due to unavoidable conceptual or mathematical obstructions. Given the importance of this simple yet paradigmatic model, here we set out clear-cut criteria for any claimed exact expression for $Z$ to be minimally plausible. Specifically, we present six necessary -- but not sufficient -- conditions that $Z$ must satisfy. These criteria will allow very quick plausibility checks of future claims. As illustrative examples, we discuss previous mistaken ``solutions,'' unveiling their shortcomings. △ Less

Submitted 9 October, 2022; v1 submitted 24 May, 2022; originally announced May 2022.

Comments: 8 pages, minor corrections

A Tree Clock Data Structure for Causal Orderings in Concurrent Executions

Authors: Umang Mathur, Andreas Pavlogiannis, Hünkar Can Tunç, Mahesh Viswanathan

Abstract: Dynamic techniques are a scalable and effective way to analyze concurrent programs. Instead of analyzing all behaviors of a program, these techniques detect errors by focusing on a single program execution. Often a crucial step in these techniques is to define a causal ordering between events in the execution, which is then computed using vector clocks, a simple data structure that stores logical… ▽ More Dynamic techniques are a scalable and effective way to analyze concurrent programs. Instead of analyzing all behaviors of a program, these techniques detect errors by focusing on a single program execution. Often a crucial step in these techniques is to define a causal ordering between events in the execution, which is then computed using vector clocks, a simple data structure that stores logical times of threads. The two basic operations of vector clocks, namely join and copy, require $Θ(k)$ time, where $k$ is the number of threads. Thus they are a computational bottleneck when $k$ is large. In this work, we introduce tree clocks, a new data structure that replaces vector clocks for computing causal orderings in program executions. Joining and copying tree clocks takes time that is roughly proportional to the number of entries being modified, and hence the two operations do not suffer the a-priori $Θ(k)$ cost per application. We show that when used to compute the classic happens-before (HB) partial order, tree clocks are optimal, in the sense that no other data structure can lead to smaller asymptotic running time. Moreover, we demonstrate that tree clocks can be used to compute other partial orders, such as schedulable-happens-before (SHB) and the standard Mazurkiewicz (MAZ) partial order, and thus are a versatile data structure. Our experiments show that just by replacing vector clocks with tree clocks, the computation becomes from $2.02 \times$ faster (MAZ) to $2.66 \times$ (SHB) and $2.97 \times$ (HB) on average per benchmark. These results illustrate that tree clocks have the potential to become a standard data structure with wide applications in concurrent analyses. △ Less

Submitted 17 January, 2022; originally announced January 2022.

Numerical studies for an ab initio investigation into the Boltzmann prescription in statistical mechanics of large systems

Authors: V. Dossetti, G. M. Viswanathan, V. M. Kenkre

Abstract: We present numerical investigations into the question of the validity of the Boltzmann prescription in Statistical Mechanics for large systems, addressing the issue of whether extensivity of energy implies the extensivity of the Boltzmann entropy. The importance of the question stems from the fact that it is currently considered open by some investigators but quite settled by others. We report ab… ▽ More We present numerical investigations into the question of the validity of the Boltzmann prescription in Statistical Mechanics for large systems, addressing the issue of whether extensivity of energy implies the extensivity of the Boltzmann entropy. The importance of the question stems from the fact that it is currently considered open by some investigators but quite settled by others. We report ab initio results for gas-like Hamiltonian systems with long-range as well as short-range interactions, based on simulations that explicitly consider more than $2^{30} \approx 10^9$ states of the full Hilbert space. The basis of the technique is Monte Carlo algorithms. Despite the largeness of the numbers used, careful inspection shows that the systems studied are still too small to settle uniquely the issues raised. Therefore, the new approach outlined represents a first step in addressing on first principles the question of non-extensive statistical mechanics. General theoretical comments are also supplied to supplement the numerical investigations. △ Less

Submitted 6 January, 2022; originally announced January 2022.

Comments: 13 pages, 4 figures

Proof Blocks: Autogradable Scaffolding Activities for Learning to Write Proofs

Authors: Seth Poulsen, Mahesh Viswanathan, Geoffrey L. Herman, Matthew West

Abstract: Proof Blocks is a software tool which enables students to write proofs by dragging and drop** prewritten proof lines into the correct order. These proofs can be graded completely automatically, enabling students to receive rapid feedback on how they are doing with their proofs. When constructing a problem, the instructor specifies the dependency graph of the lines of the proof, so that any corre… ▽ More Proof Blocks is a software tool which enables students to write proofs by dragging and drop** prewritten proof lines into the correct order. These proofs can be graded completely automatically, enabling students to receive rapid feedback on how they are doing with their proofs. When constructing a problem, the instructor specifies the dependency graph of the lines of the proof, so that any correct arrangement of the lines can receive full credit. This innovation can improve assessment tools by increasing the types of questions we can ask students about proofs, and can give greater access to proof knowledge by increasing the amount that students can learn on their own with the help of a computer. △ Less

Submitted 4 May, 2022; v1 submitted 7 June, 2021; originally announced June 2021.

Journal ref: Proceedings of the 27th ACM Conference on Innovation and Technology in Computer Science Education Vol 1 (ITiCSE 2022)

Spectrum of the tight-binding model on Cayley Trees and comparison with Bethe Lattices

Authors: M. Ostilli, Claudionor G. Bezerra, G. M. Viswanathan

Abstract: There are few exactly solvable lattice models and even fewer solvable quantum lattice models. Here we address the problem of finding the spectrum of the tight-binding model (equivalently, the spectrum of the adjacency matrix) on Cayley trees. Recent approaches to the problem have relied on the similarity between Cayley tree and the Bethe lattice. Here, we avoid to make any ansatz related to the Be… ▽ More There are few exactly solvable lattice models and even fewer solvable quantum lattice models. Here we address the problem of finding the spectrum of the tight-binding model (equivalently, the spectrum of the adjacency matrix) on Cayley trees. Recent approaches to the problem have relied on the similarity between Cayley tree and the Bethe lattice. Here, we avoid to make any ansatz related to the Bethe lattice due to fundamental differences between the two lattices that persist even when taking the thermodynamic limit. Instead, we show that one can use a recursive procedure that starts from the boundary and then use the canonical basis to derive the complete spectrum of the tight-binding model on Cayley Trees. Our resulting algorithm is extremely efficient, as witnessed with remarkable large trees having hundred of shells. We also shows that, in the thermodynamic limit, the density of states is dramatically different from that of the Bethe lattice. △ Less

Submitted 18 March, 2022; v1 submitted 12 June, 2021; originally announced June 2021.

Comments: 17 pages, 5 figures

MSC Class: G.2.2; F.2.1

Journal ref: Phys. Rev. E 105, 034123 (2022)

Threshold-free estimation of entropy from a Pearson matrix

Authors: H. Felippe, A. Viol, D. B. de Araujo, M. G. E. da Luz, F. Palhano-Fontes, H. Onias, E. P. Raposo, G. M. Viswanathan

Abstract: There is demand in diverse fields for a reliable method of estimating the entropy associated with correlations. The estimation of a unique entropy directly from the Pearson correlation matrix has remained an open problem for more than half a century. All existing approaches lack generality insofar as they require thresholding choices that arbitrarily remove possibly important information. Here we… ▽ More There is demand in diverse fields for a reliable method of estimating the entropy associated with correlations. The estimation of a unique entropy directly from the Pearson correlation matrix has remained an open problem for more than half a century. All existing approaches lack generality insofar as they require thresholding choices that arbitrarily remove possibly important information. Here we propose an objective procedure for directly estimating a unique entropy of a general Pearson matrix. We show that upon rescaling the Pearson matrix satisfies all necessary conditions for an analog of the von Neumann entropy to be well defined. No thresholding is required. We demonstrate the method by estimating the entropy from neuroimaging time series of the human brain under the influence of a psychedelic. △ Less

Submitted 6 February, 2023; v1 submitted 9 June, 2021; originally announced June 2021.

Comments: 12 pages, 6 figures

Journal ref: EPL 141 31003 (2023)

On Linear Time Decidability of Differential Privacy for Programs with Unbounded Inputs

Authors: Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan

Abstract: We introduce an automata model for describing interesting classes of differential privacy mechanisms/algorithms that include known mechanisms from the literature. These automata can model algorithms whose inputs can be an unbounded sequence of real-valued query answers. We consider the problem of checking whether there exists a constant $d$ such that the algorithm described by these automata are… ▽ More We introduce an automata model for describing interesting classes of differential privacy mechanisms/algorithms that include known mechanisms from the literature. These automata can model algorithms whose inputs can be an unbounded sequence of real-valued query answers. We consider the problem of checking whether there exists a constant $d$ such that the algorithm described by these automata are $dε$-differentially private for all positive values of the privacy budget parameter $ε$. We show that this problem can be decided in time linear in the automaton's size by identifying a necessary and sufficient condition on the underlying graph of the automaton. This paper's results are the first decidability results known for algorithms with an unbounded number of query answers taking values from the set of reals. △ Less

Submitted 29 April, 2021; originally announced April 2021.

Comments: An extended abstract to be published in 36th Annual IEEE Symposium on Logic in Computer Science (LICS 2021)

The double hypergeometric series for the partition function of the 2D anisotropic Ising model

Authors: Gandhimohan M. Viswanathan

Abstract: In 1944 Lars Onsager published the exact partition function of the ferromagnetic Ising model on the infinite square lattice in terms of a definite integral. Only in the literature of the last decade, however, has it been recast in terms of special functions. Until now all known formulas for the partition function in terms of special functions have been restricted to the important special case of t… ▽ More In 1944 Lars Onsager published the exact partition function of the ferromagnetic Ising model on the infinite square lattice in terms of a definite integral. Only in the literature of the last decade, however, has it been recast in terms of special functions. Until now all known formulas for the partition function in terms of special functions have been restricted to the important special case of the isotropic Ising model with symmetric couplings. Indeed, the anisotropic model is more challenging because there are two couplings and hence two reduced temperatures, one for each of the two axes of the square lattice. Hence, standard special functions of one variable are inadequate to the task. Here, we reformulate the partition function of the anisotropic Ising model in terms of the Kampé de Fériet function, which is a double hypergeometric function in two variables that is more general than the Appell hypergeometric functions. Finally, we present hypergeometric formulas for the generating function of multipolygons of given length on the infinite square lattice, for isotropic as well as anisotropic edge weights. For the isotropic case, the results allow easy calculation, to arbitrary order, of the celebrated series found by Cyril Domb. △ Less

Submitted 26 June, 2021; v1 submitted 7 April, 2021; originally announced April 2021.

Comments: 13 pages, submitted for publication

Journal ref: J. Stat. Mech. (2021) 073104

Comment on "Inverse Square Lévy Walks are not Optimal Search Strategies for d $\geq$ 2" [Phys. Rev. Lett. 124, 080601 (2020)]

Authors: S. V. Buldyrev, E. P. Raposo, F. Bartumeus, S. Havlin, F. R. Rusch, M. G. E. da Luz, G. M. Viswanathan

Abstract: It is widely accepted that inverse square Lévy walks are optimal search strategies because they maximize the encounter rate with sparse, randomly distributed, replenishable targets when the search restarts in the vicinity of the previously visited target, which becomes revisitable again with high probability, i.e., non-destructive foraging [Nature 401, 911 (1999)]. The precise conditions for the v… ▽ More It is widely accepted that inverse square Lévy walks are optimal search strategies because they maximize the encounter rate with sparse, randomly distributed, replenishable targets when the search restarts in the vicinity of the previously visited target, which becomes revisitable again with high probability, i.e., non-destructive foraging [Nature 401, 911 (1999)]. The precise conditions for the validity of this Lévy flight foraging hypothesis (LFH) have been widely described in the literature [Phys. Life Rev. 14, 94 (2015)]. Nevertheless, three objecting claims to the LFH have been raised recently for $d \geq 2$: (i) the capture rate $η$ has linear dependence on the target density $ρ$ for all values of the Lévy index $α$; (ii) "the gain $η_{max}/η$ achieved by varying $α$ is bounded even in the limit $ρ\to 0 $" so that "tuning $α$ can only yield a marginal gain"; (iii) depending on the values of the radius of detection $a$, the restarting distance $l_c$ and the scale parameter $s$, the optimum is realized for a range of $α$ [Phys. Rev. Lett. 124, 080601 (2020)]. Here we answer each of these three criticisms in detail and show that claims (i)-(iii) do not actually invalidate the LFH. Our results and analyses restore the original result of the LFH for non-destructive foraging. △ Less

Submitted 22 March, 2021; v1 submitted 19 March, 2021; originally announced March 2021.

Journal ref: Physical Review Letters 126, 048901 (2021)

Deciding Accuracy of Differential Privacy Schemes

Authors: Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan

Abstract: Differential privacy is a mathematical framework for develo** statistical computations with provable guarantees of privacy and accuracy. In contrast to the privacy component of differential privacy, which has a clear mathematical and intuitive meaning, the accuracy component of differential privacy does not have a generally accepted definition; accuracy claims of differential privacy algorithms… ▽ More Differential privacy is a mathematical framework for develo** statistical computations with provable guarantees of privacy and accuracy. In contrast to the privacy component of differential privacy, which has a clear mathematical and intuitive meaning, the accuracy component of differential privacy does not have a generally accepted definition; accuracy claims of differential privacy algorithms vary from algorithm to algorithm and are not instantiations of a general definition. We identify program discontinuity as a common theme in existing \emph{ad hoc} definitions and introduce an alternative notion of accuracy parametrized by, what we call, {\distance} -- the {\distance} of an input $x$ w.r.t., a deterministic computation $f$ and a distance $d$, is the minimal distance $d(x,y)$ over all $y$ such that $f(y)\neq f(x)$. We show that our notion of accuracy subsumes the definition used in theoretical computer science, and captures known accuracy claims for differential privacy algorithms. In fact, our general notion of accuracy helps us prove better claims in some cases. Next, we study the decidability of accuracy. We first show that accuracy is in general undecidable. Then, we define a non-trivial class of probabilistic computations for which accuracy is decidable (unconditionally, or assuming Schanuel's conjecture). We implement our decision procedure and experimentally evaluate the effectiveness of our approach for generating proofs or counterexamples of accuracy for common algorithms from the literature. △ Less

Submitted 12 November, 2020; originally announced November 2020.

ACM Class: F.3.1

Optimal Prediction of Synchronization-Preserving Races

Authors: Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan

Abstract: Concurrent programs are notoriously hard to write correctly, as scheduling nondeterminism introduces subtle errors that are both hard to detect and to reproduce. The most common concurrency errors are (data) races, which occur when memory-conflicting actions are executed concurrently. Consequently, considerable effort has been made towards develo** efficient techniques for race detection. The mo… ▽ More Concurrent programs are notoriously hard to write correctly, as scheduling nondeterminism introduces subtle errors that are both hard to detect and to reproduce. The most common concurrency errors are (data) races, which occur when memory-conflicting actions are executed concurrently. Consequently, considerable effort has been made towards develo** efficient techniques for race detection. The most common approach is dynamic race prediction: given an observed, race-free trace $σ$ of a concurrent program, the task is to decide whether events of $σ$ can be correctly reordered to a trace $σ^*$ that witnesses a race hidden in $σ$. In this work we introduce the notion of sync(hronization)-preserving races. A sync-preserving race occurs in $σ$ when there is a witness $σ^*$ in which synchronization operations (e.g., acquisition and release of locks) appear in the same order as in $σ$. This is a broad definition that strictly subsumes the famous notion of happens-before races. Our main results are as follows. First, we develop a sound and complete algorithm for predicting sync-preserving races. For moderate values of parameters like the number of threads, the algorithm runs in $\widetilde{O}(\mathcal{N})$ time and space, where $\mathcal{N}$ is the length of the trace $σ$. Second, we show that the problem has a $Ω(\mathcal{N}/\log^2 \mathcal{N})$ space lower bound, and thus our algorithm is essentially time and space optimal. Third, we show that predicting races with even just a single reversal of two sync operations is $\operatorname{NP}$-complete and even $\operatorname{W}[1]$-hard when parameterized by the number of threads. Thus, sync-preservation characterizes exactly the tractability boundary of race prediction, and our algorithm is nearly optimal for the tractable side. △ Less

Submitted 30 October, 2020; originally announced October 2020.

Verifying Stochastic Hybrid Systems with Temporal Logic Specifications via Model Reduction

Authors: Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, Geir E. Dullerud

Abstract: We present a scalable methodology to verify stochastic hybrid systems. Using the Mori-Zwanzig reduction method, we construct a finite state Markov chain reduction of a given stochastic hybrid system and prove that this reduced Markov chain is approximately equivalent to the original system in a distributional sense. Approximate equivalence of the stochastic hybrid system and its Markov chain reduc… ▽ More We present a scalable methodology to verify stochastic hybrid systems. Using the Mori-Zwanzig reduction method, we construct a finite state Markov chain reduction of a given stochastic hybrid system and prove that this reduced Markov chain is approximately equivalent to the original system in a distributional sense. Approximate equivalence of the stochastic hybrid system and its Markov chain reduction means that analyzing the Markov chain with respect to a suitably strengthened property, allows us to conclude whether the original stochastic hybrid system meets its temporal logic specifications. We present the first statistical model checking algorithms to verify stochastic hybrid systems against correctness properties, expressed in the linear inequality linear temporal logic (iLTL) or the metric interval temporal logic (MITL). △ Less

Submitted 16 September, 2020; originally announced September 2020.

Eclipse timing variation of GK Vir: evidence of a possible Jupiter-like planet in a circumbinary orbit

Authors: Leonardo A. Almeida, Elielson S. Pereira, Gislene M. Borges, Augusto Damineli, Tatiana A. Michtchenko, Gandhi M. Viswanathan

Abstract: Eclipse timing variation analysis has become a powerful method to discover planets around binary systems. We applied this technique to investigate the eclipse times of GK Vir. This system is a post-common envelope binary with an orbital period of 8.26 h. Here, we present 10 new eclipse times obtained between 2013 and 2020. We calculated the O-C diagram using a linear ephemeris and verified a clear… ▽ More Eclipse timing variation analysis has become a powerful method to discover planets around binary systems. We applied this technique to investigate the eclipse times of GK Vir. This system is a post-common envelope binary with an orbital period of 8.26 h. Here, we present 10 new eclipse times obtained between 2013 and 2020. We calculated the O-C diagram using a linear ephemeris and verified a clear orbital period variation (OPV) with a cyclic behavior. We investigated if this variation could be explained by the Applegate mechanism, the apsidal motion, or the light travel time (LTT) effect. We found that the Applegate mechanism would hardly explain the OPV with its current theoretical description. We obtained using different approaches that the apsidal motion is a less likely explanation than the LTT effect. We showed that the LTT effect with one circumbinary body is the most likely cause for the OPV, which was reinforced by the orbital stability of the third body. The LTT best solution provided an orbital period of ~24 yr for the outer body. Under the assumption of coplanarity between the external body and the inner binary, we obtained a Jupiter-like planet around the GK Vir. In this scenario, the planet has one of the longest orbital periods, with a full observational baseline, discovered so far. However, as the observational baseline of GK Vir is smaller than twice the period found in the O-C diagram, the LTT solution must be taken as preliminary. △ Less

Submitted 8 September, 2020; originally announced September 2020.

Comments: 9 pages, 5 Figures, 3 tables. Published online by MNRAS on August 05, 2020

Journal ref: MNRAS 497 4022-4029 (2020)

The connection between Jackson and Hausdorff derivatives in the context of generalized statistical mechanics

Authors: Andre A. Marinho, G. M. Viswanathan, Francisco A. Brito, C. G. Bezerra

Abstract: In literature one can find many generalizations of the usual Leibniz derivative, such as Jackson derivative, Tsallis derivative and Hausdorff derivative. In this article we present a connection between Jackson derivative and recently proposed Hausdorff derivative. On one hand, the Hausdorff derivative has been previously associated with non-extensivity in systems presenting fractal aspects. On the… ▽ More In literature one can find many generalizations of the usual Leibniz derivative, such as Jackson derivative, Tsallis derivative and Hausdorff derivative. In this article we present a connection between Jackson derivative and recently proposed Hausdorff derivative. On one hand, the Hausdorff derivative has been previously associated with non-extensivity in systems presenting fractal aspects. On the other hand, the Jackson derivative has a solid mathematical basis because it is the $\overline{q}$-analog of the ordinary derivative and it also arises in quantum calculus. From a quantum deformed $\overline{q}$-algebra we obtain the Jackson derivative and then address the problem of $N$ non-interacting quantum oscillators. We perform an expansion in the quantum grand partition function from which we obtain a relationship between the parameter $\overline{q}$, related to Jackson derivative, and the parameters $ζ$ and $q$ related to Hausdorff derivative and Tsallis derivative, respectively. △ Less

Submitted 30 May, 2020; originally announced June 2020.

Comments: 12 pages

The Complexity of Dynamic Data Race Prediction

Authors: Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan

Abstract: Writing concurrent programs is notoriously hard due to scheduling non-determinism. The most common concurrency bugs are data races, which are accesses to a shared resource that can be executed concurrently. Dynamic data-race prediction is the most standard technique for detecting data races: given an observed, data-race-free trace $t$, the task is to determine whether $t$ can be reordered to a tra… ▽ More Writing concurrent programs is notoriously hard due to scheduling non-determinism. The most common concurrency bugs are data races, which are accesses to a shared resource that can be executed concurrently. Dynamic data-race prediction is the most standard technique for detecting data races: given an observed, data-race-free trace $t$, the task is to determine whether $t$ can be reordered to a trace $t^*$ that exposes a data-race. Although the problem has received significant practical attention for over three decades, its complexity has remained elusive. In this work, we address this lacuna, identifying sources of intractability and conditions under which the problem is efficiently solvable. Given a trace $t$ of size $n$ over $k$ threads, our main results are as follows. First, we establish a general $O(k\cdot n^{2\cdot (k-1)})$ upper-bound, as well as an $O(n^k)$ upper-bound when certain parameters of $t$ are constant. In addition, we show that the problem is NP-hard and even W[1]-hard parameterized by $k$, and thus unlikely to be fixed-parameter tractable. Second, we study the problem over acyclic communication topologies, such as server-clients hierarchies. We establish an $O(k^2\cdot d\cdot n^2\cdot \log n)$ upper-bound, where $d$ is the number of shared variables accessed in $t$. In addition, we show that even for traces with $k=2$ threads, the problem has no $O(n^{2-ε})$ algorithm under Orthogonal Vectors. Since any trace with 2 threads defines an acyclic topology, our upper-bound for this case is optimal wrt polynomial improvements for up to moderate values of $k$ and $d$. Finally, we study a distance-bounded version of the problem, where the task is to expose a data race by a witness trace that is similar to $t$. We develop an algorithm that works in $O(n)$ time when certain parameters of $t$ are constant. △ Less

Submitted 2 May, 2020; v1 submitted 30 April, 2020; originally announced April 2020.

Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning

Authors: Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, Geir E. Dullerud

Abstract: Probabilistic Computation Tree Logic (PCTL) is frequently used to formally specify control objectives such as probabilistic reachability and safety. In this work, we focus on model checking PCTL specifications statistically on Markov Decision Processes (MDPs) by sampling, e.g., checking whether there exists a feasible policy such that the probability of reaching certain goal states is greater than… ▽ More Probabilistic Computation Tree Logic (PCTL) is frequently used to formally specify control objectives such as probabilistic reachability and safety. In this work, we focus on model checking PCTL specifications statistically on Markov Decision Processes (MDPs) by sampling, e.g., checking whether there exists a feasible policy such that the probability of reaching certain goal states is greater than a threshold. We use reinforcement learning to search for such a feasible policy for PCTL specifications, and then develop a statistical model checking (SMC) method with provable guarantees on its error. Specifically, we first use upper-confidence-bound (UCB) based Q-learning to design an SMC algorithm for bounded-time PCTL specifications, and then extend this algorithm to unbounded-time specifications by identifying a proper truncation time by checking the PCTL specification and its negation at the same time. Finally, we evaluate the proposed method on case studies. △ Less

Submitted 21 April, 2020; v1 submitted 1 April, 2020; originally announced April 2020.

Atomicity Checking in Linear Time using Vector Clocks

Authors: Umang Mathur, Mahesh Viswanathan

Abstract: Multi-threaded programs are challenging to write. Developers often need to reason about a prohibitively large number of thread interleavings to reason about the behavior of software. A non-interference property like atomicity can reduce this interleaving space by ensuring that any execution is equivalent to an execution where all atomic blocks are executed serially. We consider the well studied no… ▽ More Multi-threaded programs are challenging to write. Developers often need to reason about a prohibitively large number of thread interleavings to reason about the behavior of software. A non-interference property like atomicity can reduce this interleaving space by ensuring that any execution is equivalent to an execution where all atomic blocks are executed serially. We consider the well studied notion of conflict serializability for dynamically checking atomicity. Existing algorithms detect violations of conflict serializability by detecting cycles in a graph of transactions observed in a given execution. The number of edges in such a graph can grow quadratically with the length of the trace making the analysis not scalable. In this paper, we present AeroDrome, a novel single pass linear time algorithm that uses vector clocks to detect violations of conflict serializability in an online setting. Experiments show that AeroDrome scales to traces with a large number of events with significant speedup. △ Less

Submitted 17 October, 2020; v1 submitted 14 January, 2020; originally announced January 2020.

What's Decidable About Program Verification Modulo Axioms?

Authors: Umang Mathur, P. Madhusudan, Mahesh Viswanathan

Abstract: We consider the decidability of the verification problem of programs \emph{modulo axioms} --- that is, verifying whether programs satisfy their assertions, when the functions and relations it uses are assumed to interpreted by arbitrary functions and relations that satisfy a set of first-order axioms. Unfortunately, verification of entirely uninterpreted programs (with the empty set of axioms) is… ▽ More We consider the decidability of the verification problem of programs \emph{modulo axioms} --- that is, verifying whether programs satisfy their assertions, when the functions and relations it uses are assumed to interpreted by arbitrary functions and relations that satisfy a set of first-order axioms. Unfortunately, verification of entirely uninterpreted programs (with the empty set of axioms) is already undecidable. A recent work introduced a subclass of \emph{coherent} uninterpreted programs, and showed that they admit decidable verification \cite{coherence2019}. We undertake a systematic study of various natural axioms for relations and functions, and study the decidability of the coherent verification problem. Axioms include relations being reflexive, symmetric, transitive, or total order relations, %and their combinations, functions restricted to being associative, idempotent or commutative, and combinations of such axioms as well. Our comprehensive results unearth a rich landscape that shows that though several axiom classes admit decidability for coherent programs, coherence is not a panacea as several others continue to be undecidable. △ Less

Submitted 28 October, 2019; v1 submitted 23 October, 2019; originally announced October 2019.

Decidable Synthesis of Programs with Uninterpreted Functions

Authors: Paul Krogmeier, Umang Mathur, Adithya Murali, P. Madhusudan, Mahesh Viswanathan

Abstract: We identify a decidable synthesis problem for a class of programs of unbounded size with conditionals and iteration that work over infinite data domains. The programs in our class use uninterpreted functions and relations, and abide by a restriction called coherence that was recently identified to yield decidable verification. We formulate a powerful grammar-restricted (syntax-guided) synthesis pr… ▽ More We identify a decidable synthesis problem for a class of programs of unbounded size with conditionals and iteration that work over infinite data domains. The programs in our class use uninterpreted functions and relations, and abide by a restriction called coherence that was recently identified to yield decidable verification. We formulate a powerful grammar-restricted (syntax-guided) synthesis problem for coherent uninterpreted programs, and we show the problem to be decidable, identify its precise complexity, and also study several variants of the problem. △ Less

Submitted 22 July, 2020; v1 submitted 21 October, 2019; originally announced October 2019.

Revisiting MITL to Fix Decision Procedures

Authors: Nima Roohi, Mahesh Viswanathan

Abstract: Metric Interval Temporal Logic (MITL) is a well studied real-time, temporal logic that has decidable satisfiability and model checking problems. The decision procedures for MITL rely on the automata theoretic approach, where logic formulas are translated into equivalent timed automata. Since timed automata are not closed under complementation, decision procedures for MITL first convert a formula i… ▽ More Metric Interval Temporal Logic (MITL) is a well studied real-time, temporal logic that has decidable satisfiability and model checking problems. The decision procedures for MITL rely on the automata theoretic approach, where logic formulas are translated into equivalent timed automata. Since timed automata are not closed under complementation, decision procedures for MITL first convert a formula into negated normal form before translating to a timed automaton. We show that, unfortunately, these 20-year-old procedures are incorrect, because they rely on an incorrect semantics of the R operator. We present the right semantics of R and give new, correct decision procedures for MITL. We show that both satisfiability and model checking for MITL are EXPSPACE-complete, as was previously claimed. We also identify a fragment of MITL that we call MITL_{WI} that is richer than MITL_{0,\infty}, for which we show that both satisfiability and model checking are PSPACE-complete. Many of our results have been formally proved in PVS. △ Less

Submitted 9 October, 2019; originally announced October 2019.

Comments: Presented at the 19th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'18)

Deciding Differential Privacy for Programs with Finite Inputs and Outputs

Authors: Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan

Abstract: Differential privacy is a de facto standard for statistical computations over databases that contain private data. The strength of differential privacy lies in a rigorous mathematical definition that guarantees individual privacy and yet allows for accurate statistical results. Thanks to its mathematical definition, differential privacy is also a natural target for formal analysis. A broad line of… ▽ More Differential privacy is a de facto standard for statistical computations over databases that contain private data. The strength of differential privacy lies in a rigorous mathematical definition that guarantees individual privacy and yet allows for accurate statistical results. Thanks to its mathematical definition, differential privacy is also a natural target for formal analysis. A broad line of work uses logical methods for proving privacy. However, these methods are not complete, and only partially automated. A recent and complementary line of work uses statistical methods for finding privacy violations. However, the methods only provide statistical guarantees (but no proofs). We propose the first decision procedure for checking the differential privacy of a non-trivial class of probabilistic computations. Our procedure takes as input a program P parametrized by a privacy budget $ε$, and either proves differential privacy for all possible values of $ε$ or generates a counterexample. In addition, our procedure applies both to $ε$-differential privacy and $(ε,δ)$-differential privacy. Technically, the decision procedure is based on a novel and judicious encoding of the semantics of programs in our class into a decidable fragment of the first-order theory of the reals with exponentiation. We implement our procedure and use it for (dis)proving privacy bounds for many well-known examples, including randomized response, histogram, report noisy max and sparse vector. △ Less

Submitted 1 May, 2020; v1 submitted 9 October, 2019; originally announced October 2019.

Deciding Memory Safety for Single-Pass Heap-Manipulating Programs

Authors: Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, Mahesh Viswanathan

Abstract: We investigate the decidability of automatic program verification for programs that manipulate heaps, and in particular, decision procedures for proving memory safety for them. We extend recent work that identified a decidable subclass of uninterpreted programs to a class of alias-aware programs that can update maps. We apply this theory to develop verification algorithms for memory safety--- dete… ▽ More We investigate the decidability of automatic program verification for programs that manipulate heaps, and in particular, decision procedures for proving memory safety for them. We extend recent work that identified a decidable subclass of uninterpreted programs to a class of alias-aware programs that can update maps. We apply this theory to develop verification algorithms for memory safety--- determining if a heap-manipulating program that allocates and frees memory locations and manipulates heap pointers does not dereference an unallocated memory location. We show that this problem is decidable when the initial allocated heap forms a forest data-structure and when programs are streaming-coherent, which intuitively restricts programs to make a single pass over a data-structure. Our experimental evaluation on a set of library routines that manipulate forest data-structures shows that common single-pass algorithms on data-structures often fall in the decidable class, and that our decision procedure is efficient in verifying them. △ Less

Submitted 31 December, 2019; v1 submitted 29 June, 2019; originally announced July 2019.

Comments: StreamVerif tool for automata-based verification of uninterpreted programs can be found at https://github.com/umangm/streamverif

Journal ref: Proceedings of the ACM on Programming Languages Vol. 4, Issue POPL, Article 35 (December 2019)

Decidable Verification of Uninterpreted Programs

Authors: Umang Mathur, P. Madhusudan, Mahesh Viswanathan

Abstract: We study the problem of completely automatically verifying uninterpreted programs---programs that work over arbitrary data models that provide an interpretation for the constants, functions and relations the program uses. The verification problem asks whether a given program satisfies a postcondition written using quantifier-free formulas with equality on the final state, with no loop invariants,… ▽ More We study the problem of completely automatically verifying uninterpreted programs---programs that work over arbitrary data models that provide an interpretation for the constants, functions and relations the program uses. The verification problem asks whether a given program satisfies a postcondition written using quantifier-free formulas with equality on the final state, with no loop invariants, contracts, etc. being provided. We show that this problem is undecidable in general. The main contribution of this paper is a subclass of programs, called coherent programs that admits decidable verification, and can be decided in PSPACE. We then extend this class of programs to classes of programs that are $k$-coherent, where $k \in \mathbb{N}$, obtained by (automatically) adding $k$ ghost variables and assignments that make them coherent. We also extend the decidability result to programs with recursive function calls and prove several undecidability results that show why our restrictions to obtain decidability seem necessary. △ Less

Submitted 26 August, 2020; v1 submitted 31 October, 2018; originally announced November 2018.

Characterizing complex networks using Entropy-degree diagrams: unveiling changes in functional brain connectivity induced by Ayahuasca

Authors: A. Viol, Fernanda Palhano-Fontes, Heloisa Onias, Draulio B. de Araujo, Philipp Hövel, G. M. Viswanathan

Abstract: Open problems abound in the theory of complex networks, which has found successful application to diverse fields of science. With the aim of further advancing the understanding of the brain's functional connectivity, we propose to evaluate a network metric which we term the geodesic entropy. This entropy, in a way that can be made precise, quantifies the Shannon entropy of the distance distributio… ▽ More Open problems abound in the theory of complex networks, which has found successful application to diverse fields of science. With the aim of further advancing the understanding of the brain's functional connectivity, we propose to evaluate a network metric which we term the geodesic entropy. This entropy, in a way that can be made precise, quantifies the Shannon entropy of the distance distribution to a specific node from all other nodes. Measurements of geodesic entropy allow for the characterization of the structural information of a network that takes into account the distinct role of each node into the network topology. The measurement and characterization of this structural information has the potential to greatly improve our understanding of sustained activity and other emergent behaviors in networks, such as self-organized criticality sometimes seen in such contexts. We apply these concepts and methods to study the effects of how the psychedelic Ayahuasca affects the functional connectivity of the human brain. We show that the geodesic entropy is able to differentiate the functional networks of the human brain in two different states of consciousness in the resting state: (i) the ordinary waking state and (ii) a state altered by ingestion of the Ayahuasca. The entropy of the nodes of brain networks from subjects under the influence of Ayahuasca diverge significantly from those of the ordinary waking state. The functional brain networks from subjects in the altered state have, on average, a larger geodesic entropy compared to the ordinary state. We conclude that geodesic entropy is a useful tool for analyzing complex networks and discuss how and why it may bring even further valuable insights into the study of the human brain and other empirical networks. △ Less

Submitted 26 September, 2018; originally announced September 2018.

What Happens - After the First Race? Enhancing the Predictive Power of Happens - Before Based Dynamic Race Detection

Authors: Umang Mathur, Dileep Kini, Mahesh Viswanathan

Abstract: Dynamic race detection is the problem of determining if an observed program execution reveals the presence of a data race in a program. The classical approach to solving this problem is to detect if there is a pair of conflicting memory accesses that are unordered by Lamport's happens-before (HB) relation. HB based race detection is known to not report false positives, i.e., it is sound. However,… ▽ More Dynamic race detection is the problem of determining if an observed program execution reveals the presence of a data race in a program. The classical approach to solving this problem is to detect if there is a pair of conflicting memory accesses that are unordered by Lamport's happens-before (HB) relation. HB based race detection is known to not report false positives, i.e., it is sound. However, the soundness guarantee of HB only promises that the first pair of unordered, conflicting events is a schedulable data race. That is, there can be pairs of HB-unordered conflicting data accesses that are not schedulable races because there is no reordering of the events of the execution, where the events in race can be executed immediately after each other. We introduce a new partial order, called schedulable happens-before (SHB) that exactly characterizes the pairs of schedulable data races --- every pair of conflicting data accesses that are identified by SHB can be scheduled, and every HB-race that can be scheduled is identified by SHB. Thus, the SHB partial order is truly sound. We present a linear time, vector clock algorithm to detect schedulable races using SHB. Our experiments demonstrate the value of our algorithm for dynamic race detection --- SHB incurs only little performance overhead and can scale to executions from real-world software applications without compromising soundness. △ Less

Submitted 1 August, 2018; originally announced August 2018.

Data Race Detection on Compressed Traces

Authors: Dileep Kini, Umang Mathur, Mahesh Viswanathan

Abstract: We consider the problem of detecting data races in program traces that have been compressed using straight line programs (SLP), which are special context-free grammars that generate exactly one string, namely the trace that they represent. We consider two classical approaches to race detection --- using the happens-before relation and the lockset discipline. We present algorithms for both these me… ▽ More We consider the problem of detecting data races in program traces that have been compressed using straight line programs (SLP), which are special context-free grammars that generate exactly one string, namely the trace that they represent. We consider two classical approaches to race detection --- using the happens-before relation and the lockset discipline. We present algorithms for both these methods that run in time that is linear in the size of the compressed, SLP representation. Typical program executions almost always exhibit patterns that lead to significant compression. Thus, our algorithms are expected to result in large speedups when compared with analyzing the uncompressed trace. Our experimental evaluation of these new algorithms on standard benchmarks confirms this observation. △ Less

Submitted 23 July, 2018; originally announced July 2018.

A Decidable Fragment of Second Order Logic With Applications to Synthesis

Authors: P. Madhusudan, Umang Mathur, Shambwaditya Saha, Mahesh Viswanathan

Abstract: We propose a fragment of many-sorted second order logic called EQSMT and show that checking satisfiability of sentences in this fragment is decidable. EQSMT formulae have an $\exists^*\forall^*$ quantifier prefix (over variables, functions and relations) making EQSMT conducive for modeling synthesis problems. Moreover, EQSMT allows reasoning using a combination of background theories provided that… ▽ More We propose a fragment of many-sorted second order logic called EQSMT and show that checking satisfiability of sentences in this fragment is decidable. EQSMT formulae have an $\exists^*\forall^*$ quantifier prefix (over variables, functions and relations) making EQSMT conducive for modeling synthesis problems. Moreover, EQSMT allows reasoning using a combination of background theories provided that they have a decidable satisfiability problem for the $\exists^*\forall^*$ FO-fragment (e.g., linear arithmetic). Our decision procedure reduces the satisfiability of EQSMT formulae to satisfiability queries of $\exists^*\forall^*$ formulae of each individual background theory, allowing us to use existing efficient SMT solvers supporting $\exists^*\forall^*$ reasoning for these theories; hence our procedure can be seen as effectively quantified SMT (EQSMT) reasoning. Errata: We have modified the transformation step-2 (page 9) to correct for a slight error. Also, the description above Theorem 10 is different from the published version. △ Less

Submitted 27 September, 2018; v1 submitted 14 December, 2017; originally announced December 2017.

Journal ref: 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), http://drops.dagstuhl.de/opus/volltexte/2018/9698

Correspondence between spanning trees and the Ising model on a square lattice

Authors: G. M. Viswanathan

Abstract: An important problem in statistical physics concerns the fascinating connections between partition functions of lattice models studied in equilibrium statistical mechanics on the one hand and graph theoretical enumeration problems on the other hand. We investigate the nature of the relationship between the number of spanning trees and the partition function of the Ising model on the square lattice… ▽ More An important problem in statistical physics concerns the fascinating connections between partition functions of lattice models studied in equilibrium statistical mechanics on the one hand and graph theoretical enumeration problems on the other hand. We investigate the nature of the relationship between the number of spanning trees and the partition function of the Ising model on the square lattice. The spanning tree generating function $T(z)$ gives the spanning tree constant when evaluated at $z=1$, while giving he lattice green function when differentiated. It is known that for the infinite square lattice the partition function $Z(K)$ of the Ising model evaluated at the critical temperature $K=K_c$ is related to $T(1)$. Here we show that this idea in fact generalizes to all real temperatures. We prove that $ ( Z(K) {\rm sech~} 2K ~\!)^2 = k \exp\big[ T(k) \big] $, where $k= 2 \tanh(2K) {\rm sech}(2K)$. The identical Mahler measure connects the two seemingly disparate quantities $T(z)$ and $Z(K)$. In turn, the Mahler measure is determined by the random walk structure function. Finally, we show that the the above correspondence does not generalize in a straightforward manner to non-planar lattices. △ Less

Submitted 6 May, 2020; v1 submitted 2 June, 2017; originally announced June 2017.

Comments: Subm. to Phys. Rev. E

The complex social network of surnames: A comparison between Brazil and Portugal

Authors: G. D. Ferreira, G. M. Viswanathan, L. R. da Silva, H. J. Herrmann

Abstract: We present a study of social networks based on the analysis of Brazilian and Portuguese family names (surnames). We construct networks whose nodes are names of families and whose edges represent parental relations between two families. From these networks we extract the connectivity distribution, clustering coefficient, shortest path and centrality. We find that the connectivity distribution follo… ▽ More We present a study of social networks based on the analysis of Brazilian and Portuguese family names (surnames). We construct networks whose nodes are names of families and whose edges represent parental relations between two families. From these networks we extract the connectivity distribution, clustering coefficient, shortest path and centrality. We find that the connectivity distribution follows an approximate power law. We associate the number of hubs, centrality and entropy to the degree of miscegenation in the societies in both countries. Our results show that Portuguese society has a higher miscegenation degree than Brazilian society. All networks analyzed lead to approximate inverse square power laws in the degree distribution. We conclude that the thermodynamic limit is reached for small networks (3 or 4 thousand nodes). The assortative mixing of all networks is negative, showing that the more connected vertices are connected to vertices with lower connectivity. Finally, the network of surnames presents some small world characteristics. △ Less

Submitted 12 May, 2017; originally announced May 2017.

Comments: 13 pages, 5 figures

Dynamic Race Prediction in Linear Time

Authors: Dileep Kini, Umang Mathur, Mahesh Viswanathan

Abstract: Writing reliable concurrent software remains a huge challenge for today's programmers. Programmers rarely reason about their code by explicitly considering different possible inter-leavings of its execution. We consider the problem of detecting data races from individual executions in a sound manner. The classical approach to solving this problem has been to use Lamport's happens-before (HB) relat… ▽ More Writing reliable concurrent software remains a huge challenge for today's programmers. Programmers rarely reason about their code by explicitly considering different possible inter-leavings of its execution. We consider the problem of detecting data races from individual executions in a sound manner. The classical approach to solving this problem has been to use Lamport's happens-before (HB) relation. Until now HB remains the only approach that runs in linear time. Previous efforts in improving over HB such as causally-precedes (CP) and maximal causal models fall short due to the fact that they are not implementable efficiently and hence have to compromise on their race detecting ability by limiting their techniques to bounded sized fragments of the execution. We present a new relation weak-causally-precedes (WCP) that is provably better than CP in terms of being able to detect more races, while still remaining sound. Moreover it admits a linear time algorithm which works on the entire execution without having to fragment it. △ Less

Submitted 16 April, 2017; v1 submitted 7 April, 2017; originally announced April 2017.

Comments: 22 pages, 8 figures, 1 algorithm, 1 table

ACM Class: D.2.5; D.2.4

DRYVR:Data-driven verification and compositional reasoning for automotive systems

Authors: Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan

Abstract: We present the DRYVR framework for verifying hybrid control systems that are described by a combination of a black-box simulator for trajectories and a white-box transition graph specifying mode switches. The framework includes (a) a probabilistic algorithm for learning sensitivity of the continuous trajectories from simulation data, (b) a bounded reachability analysis algorithm that uses the lear… ▽ More We present the DRYVR framework for verifying hybrid control systems that are described by a combination of a black-box simulator for trajectories and a white-box transition graph specifying mode switches. The framework includes (a) a probabilistic algorithm for learning sensitivity of the continuous trajectories from simulation data, (b) a bounded reachability analysis algorithm that uses the learned sensitivity, and (c) reasoning techniques based on simulation relations and sequential composition, that enable verification of complex systems under long switching sequences, from the reachability analysis of a simpler system under shorter sequences. We demonstrate the utility of the framework by verifying a suite of automotive benchmarks that include powertrain control, automatic transmission, and several autonomous and ADAS features like automatic emergency braking, lane-merge, and auto-passing controllers. △ Less

Submitted 22 February, 2017; originally announced February 2017.

Comments: 25 pages, 3 figures

Shannon entropy of brain functional complex networks under the influence of the psychedelic Ayahuasca

Authors: A. Viol, Fernanda Palhano-Fontes, Heloisa Onias, Draulio B. de Araujo, G. M. Viswanathan

Abstract: The entropic brain hypothesis holds that the key facts concerning psychedelics are partially explained in terms of increased entropy of the brain's functional connectivity. Ayahuasca is a psychedelic beverage of Amazonian indigenous origin with legal status in Brazil in religious and scientific settings. In this context, we use tools and concepts from the theory of complex networks to analyze rest… ▽ More The entropic brain hypothesis holds that the key facts concerning psychedelics are partially explained in terms of increased entropy of the brain's functional connectivity. Ayahuasca is a psychedelic beverage of Amazonian indigenous origin with legal status in Brazil in religious and scientific settings. In this context, we use tools and concepts from the theory of complex networks to analyze resting state fMRI data of the brains of human subjects under two distinct conditions: (i) under ordinary waking state and (ii) in an altered state of consciousness induced by ingestion of Ayahuasca. We report an increase in the Shannon entropy of the degree distribution of the networks subsequent to Ayahuasca ingestion. We also find increased local and decreased global network integration. Our results are broadly consistent with the entropic brain hypothesis. Finally, we discuss our findings in the context of descriptions of "mind-expansion" frequently seen in self-reports of users of psychedelic drugs. △ Less

Submitted 1 November, 2016; originally announced November 2016.

Comments: 27 pages, 6 figures

Journal ref: Scientific Reports 7: 7388,2017

Information entropy of classical versus explosive percolation

Authors: T. M. Vieira, G. M. Viswanathan, L. R. da Silva

Abstract: We study the Shannon entropy of the cluster size distribution in classical as well as explosive percolation, in order to estimate the uncertainty in the sizes of randomly chosen clusters. At the critical point the cluster size distribution is a power-law, i.e. there are clusters of all sizes, so one expects the information entropy to attain a maximum. As expected, our results show that the entropy… ▽ More We study the Shannon entropy of the cluster size distribution in classical as well as explosive percolation, in order to estimate the uncertainty in the sizes of randomly chosen clusters. At the critical point the cluster size distribution is a power-law, i.e. there are clusters of all sizes, so one expects the information entropy to attain a maximum. As expected, our results show that the entropy attains a maximum at this point for classical percolation. Surprisingly, for explosive percolation the maximum entropy does not match the critical point. Moreover, we show that it is possible determine the critical point without using the conventional order parameter, just analysing the entropy's derivatives. △ Less

Submitted 14 August, 2015; v1 submitted 21 November, 2014; originally announced November 2014.

Comments: 6 pages, 6 figures

The hypergeometric series for the partition function of the 2-D Ising model

Authors: G. M. Viswanathan

Abstract: In 1944 Onsager published the formula for the partition function of the Ising model for the infinite square lattice. He was able to express the internal energy in terms of a special function, but he left the free energy as a definite integral. Seven decades later, the partition function and free energy have yet to be written in closed form, even with the aid of special functions. Here we evaluate… ▽ More In 1944 Onsager published the formula for the partition function of the Ising model for the infinite square lattice. He was able to express the internal energy in terms of a special function, but he left the free energy as a definite integral. Seven decades later, the partition function and free energy have yet to be written in closed form, even with the aid of special functions. Here we evaluate the definite integral explicitly, using hypergeometric series. Let $β$ denote the reciprocal temperature, $J$ the coupling and $f$ the free energy per spin. We prove that $-βf = \ln(2 \cosh 2K) - κ^2\, {}_4F_3 [1,1,\tfrac{3}{2},\tfrac{3}{2};\ 2,2,2 ;\ 16 κ^2 ] $, where $_p F_q$ is the generalized hypergeometric function, $K=βJ$, and $2κ= {\rm tanh} 2K {\rm sech} 2K$. △ Less

Submitted 24 July, 2015; v1 submitted 10 November, 2014; originally announced November 2014.

Comments: Final version as published in JSTAT

Journal ref: J. Stat. Mech. (2015) P07004

How to efficiently destroy a network with limited information

Authors: T. M. Vieira, G. M. Viswanathan, L. R. da Silva

Abstract: We address the general problem of how best to attack and destroy a network by node removal, given limited or no prior information about the edges. We consider a family of strategies in which nodes are randomly chosen, but not removed. Instead, a random acquaintance (i.e., a first neighbour) of the chosen node is removed from the network. By assigning an informal cost to the information about the n… ▽ More We address the general problem of how best to attack and destroy a network by node removal, given limited or no prior information about the edges. We consider a family of strategies in which nodes are randomly chosen, but not removed. Instead, a random acquaintance (i.e., a first neighbour) of the chosen node is removed from the network. By assigning an informal cost to the information about the network structure, we show using cost-benefit analysis that acquaintance removal is the optimal strategy to destroy networks efficiently. △ Less

Submitted 10 November, 2014; originally announced November 2014.

Comments: 10 pages, 3 figures

Activity, diffusion, and correlations in a two-dimensional conserved stochastic sandpile

Authors: Sharon Dantas da Cunha, Luciano Rodrigues da Silva, Gandhimohan M. Viswanathan, Ronald Dickman

Abstract: We perform large-scale simulations of a two-dimensional restricted-height conserved stochastic sandpile, focusing on particle diffusion and mobility, and spatial correlations. Quasistationary (QS) simulations yield the critical particle density to high precision [$p_c = 0.7112687(2)$], and show that the diffusion constant scales in the same manner as the activity density, as found previously in th… ▽ More We perform large-scale simulations of a two-dimensional restricted-height conserved stochastic sandpile, focusing on particle diffusion and mobility, and spatial correlations. Quasistationary (QS) simulations yield the critical particle density to high precision [$p_c = 0.7112687(2)$], and show that the diffusion constant scales in the same manner as the activity density, as found previously in the one-dimensional case. Short-time scaling is characterized by subdiffusive behavior (mean-square displacement $\sim t^γ$ with $γ< 1$), which is easily understood as a consequence of the initial decay of activity, $ρ(t) \sim t^{-δ}$, with $γ= 1- δ$. We verify that at criticality, the activity correlation function $C(r) \sim r^{-β/ν_\perp}$, as expected at an absorbing-state phase transition. Our results for critical exponents are consistent with, and somewhat more precise than, predictions derived from the Langevin equation for stochastic sandpiles in two dimensions. △ Less

Submitted 5 May, 2014; originally announced May 2014.

Comments: 14 pages; 18 figures

Reachability under Contextual Locking

Authors: Remi Bonnet, Rohit Chadha, Mahesh Viswanathan, P. Madhusudan

Abstract: The pairwise reachability problem for a multi-threaded program asks, given control locations in two threads, whether they can be simultaneously reached in an execution of the program. The problem is important for static analysis and is used to detect statements that are concurrently enabled. This problem is in general undecidable even when data is abstracted and when the threads (with recursion)… ▽ More The pairwise reachability problem for a multi-threaded program asks, given control locations in two threads, whether they can be simultaneously reached in an execution of the program. The problem is important for static analysis and is used to detect statements that are concurrently enabled. This problem is in general undecidable even when data is abstracted and when the threads (with recursion) synchronize only using a finite set of locks. Popular programming paradigms that limit the lock usage patterns have been identified under which the pairwise reachability problem becomes decidable. In this paper, we consider a new natural programming paradigm, called contextual locking, which ties the lock usage to calling patterns in each thread: we assume that locks are released in the same context that they were acquired and that every lock acquired by a thread in a procedure call is released before the procedure returns. Our main result is that the pairwise reachability problem is polynomial-time decidable for this new programming paradigm as well. The problem becomes undecidable if the locks are reentrant; reentrant locking is a \emph{recursive locking} mechanism which allows a thread in a multi-threaded program to acquire the reentrant lock multiple times. △ Less

Submitted 20 September, 2013; v1 submitted 10 August, 2013; originally announced August 2013.

Comments: A preliminary version appears in TACAS 2012

Journal ref: Logical Methods in Computer Science, Volume 9, Issue 3 (September 17, 2013) lmcs:762

Power of Randomization in Automata on Infinite Strings

Authors: Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan

Abstract: Probabilistic Büchi Automata (PBA) are randomized, finite state automata that process input strings of infinite length. Based on the threshold chosen for the acceptance probability, different classes of languages can be defined. In this paper, we present a number of results that clarify the power of such machines and properties of the languages they define. The broad themes we focus on are as fol… ▽ More Probabilistic Büchi Automata (PBA) are randomized, finite state automata that process input strings of infinite length. Based on the threshold chosen for the acceptance probability, different classes of languages can be defined. In this paper, we present a number of results that clarify the power of such machines and properties of the languages they define. The broad themes we focus on are as follows. We present results on the decidability and precise complexity of the emptiness, universality and language containment problems for such machines, thus answering questions central to the use of these models in formal verification. Next, we characterize the languages recognized by PBAs topologically, demonstrating that though general PBAs can recognize languages that are not regular, topologically the languages are as simple as ω-regular languages. Finally, we introduce Hierarchical PBAs, which are syntactically restricted forms of PBAs that are tractable and capture exactly the class of ω-regular languages. △ Less

Submitted 28 September, 2011; v1 submitted 12 September, 2011; originally announced September 2011.

ACM Class: F.4.3,D.2.4,F.1.1,F.1.2

Journal ref: Logical Methods in Computer Science, Volume 7, Issue 3 (September 29, 2011) lmcs:948

Influence of lattice distortion on the Curie temperature and spin-phonon coupling in LaMn$_{0.5}$Co$_{0.5}$O$_{3}$

Authors: M. Viswanathan, P. S. Anil Kumar, Venkata Srinu Bhadram, Chandrabhas Narayana, A. K. Bera, S. M. Yusuf

Abstract: Two distinct ferromagnetic phases of LaMn$_{0.5}$Co$_{0.5}$O$_{3}$ having monoclinic structure with distinct physical properties have been studied. The ferromagnetic ordering temperature $\textit{T}_{c}$ is found to be different for both the phases. The origin of such contrasting characteristics is assigned to the changes in the distance(s) and angle(s) between Mn - O - Co resulting from distortio… ▽ More Two distinct ferromagnetic phases of LaMn$_{0.5}$Co$_{0.5}$O$_{3}$ having monoclinic structure with distinct physical properties have been studied. The ferromagnetic ordering temperature $\textit{T}_{c}$ is found to be different for both the phases. The origin of such contrasting characteristics is assigned to the changes in the distance(s) and angle(s) between Mn - O - Co resulting from distortions observed from neutron diffraction studies. Investigations on the temperature dependent Raman spectroscopy provide evidence for such structural characteristics, which affects the exchange interaction. The difference in B-site ordering which is evident from the neutron diffraction is also responsible for the difference in $\textit{T}_{c}$. Raman scattering suggests the presence of spin-phonon coupling for both the phases around the $\textit{T}_{c}$. Electrical transport properties of both the phases have been investigated based on the lattice distortion. △ Less

Submitted 7 September, 2010; originally announced September 2010.

Comments: 9 figures

Journal ref: J. Phys.: Condens. Matter 22, 346006 (2010)

A Solvability criterion for Navier-Stokes equations in high dimensions

Authors: T. M. Viswanathan, G. M. Viswanathan

Abstract: We define the Ladyzhenskaya-Lions exponent $α_{\rm {\tiny \sc l}} (n)=({2+n})/4$ for Navier-Stokes equations with dissipation $-(-Δ)^α$ in ${\Bbb R}^n$, for all $n\geq 2$. We review the proof of strong global solvability when $α\geq α_{\rm {\tiny \sc l}} (n)$, given smooth initial data. If the corresponding Euler equations for $n>2$ were to allow uncontrolled growth of the enstrophy… ▽ More We define the Ladyzhenskaya-Lions exponent $α_{\rm {\tiny \sc l}} (n)=({2+n})/4$ for Navier-Stokes equations with dissipation $-(-Δ)^α$ in ${\Bbb R}^n$, for all $n\geq 2$. We review the proof of strong global solvability when $α\geq α_{\rm {\tiny \sc l}} (n)$, given smooth initial data. If the corresponding Euler equations for $n>2$ were to allow uncontrolled growth of the enstrophy ${1\over 2} \|\nabla u \|^2_{L^2}$, then no globally controlled coercive quantity is currently known to exist that can regularize solutions of the Navier-Stokes equations for $α<α_{\rm {\tiny \sc l}} (n)$. The energy is critical under scale transformations only for $α=α_{\rm {\tiny \sc l}} (n)$. △ Less

Submitted 16 October, 2009; v1 submitted 24 July, 2009; originally announced July 2009.

Comments: Fixed references, priority etc

Spontaneous symmetry breaking and finite time singularities in $d$-dimensional incompressible flow with fractional dissipation

Authors: G. M. Viswanathan, T. M. Viswanathan

Abstract: We investigate the formation of singularities in the incompressible Navier-Stokes equations in $d\geq 2$ dimensions with a fractional Laplacian $|\nabla |^α$. We derive analytically a sufficient but not necessary condition for solutions to remain always smooth and show that finite time singularities cannot form for $α\geq α_c= 1+d/2$. Moreover, initial singularities become unstable for $α>α_c$. We investigate the formation of singularities in the incompressible Navier-Stokes equations in $d\geq 2$ dimensions with a fractional Laplacian $|\nabla |^α$. We derive analytically a sufficient but not necessary condition for solutions to remain always smooth and show that finite time singularities cannot form for $α\geq α_c= 1+d/2$. Moreover, initial singularities become unstable for $α>α_c$. △ Less

Submitted 9 July, 2008; originally announced July 2008.

Comments: 5 pages