-
Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties
Authors:
S. Akshay,
Krishnendu Chatterjee,
Tobias Meggendorfer,
Đorđe Žikelić
Abstract:
Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty. Often they are viewed as state transformers with planning objectives defined with respect to paths over MDP states. An increasingly popular alternative is to view them as distribution transformers, giving rise to a sequence of probability distributions over MDP states. For instance, reachabil…
▽ More
Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty. Often they are viewed as state transformers with planning objectives defined with respect to paths over MDP states. An increasingly popular alternative is to view them as distribution transformers, giving rise to a sequence of probability distributions over MDP states. For instance, reachability and safety properties in modeling robot swarms or chemical reaction networks are naturally defined in terms of probability distributions over states. Verifying such distributional properties is known to be hard and often beyond the reach of classical state-based verification techniques.
In this work, we consider the problems of certified policy (i.e. controller) verification and synthesis in MDPs under distributional reach-avoidance specifications. By certified we mean that, along with a policy, we also aim to synthesize a (checkable) certificate ensuring that the MDP indeed satisfies the property. Thus, given the target set of distributions and an unsafe set of distributions over MDP states, our goal is to either synthesize a certificate for a given policy or synthesize a policy along with a certificate, proving that the target distribution can be reached while avoiding unsafe distributions. To solve this problem, we introduce the novel notion of distributional reach-avoid certificates and present automated procedures for (1) synthesizing a certificate for a given policy, and (2) synthesizing a policy together with the certificate, both providing formal guarantees on certificate correctness. Our experimental evaluation demonstrates the ability of our method to solve several non-trivial examples, including a multi-agent robot-swarm model, to synthesize certified policies and to certify existing policies.
△ Less
Submitted 7 May, 2024;
originally announced May 2024.
-
On Dependent Variables in Reactive Synthesis
Authors:
S. Akshay,
Eliyahu Basa,
Supratik Chakraborty,
Dror Fried
Abstract:
Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step for every sequence of inputs, such that the LTL formula is satisfied. In this paper, we investigate the notion of dependent variables in the context of reactive synthesis. Inspired by successful pre-p…
▽ More
Given a Linear Temporal Logic (LTL) formula over input and output variables, reactive synthesis requires us to design a deterministic Mealy machine that gives the values of outputs at every time step for every sequence of inputs, such that the LTL formula is satisfied. In this paper, we investigate the notion of dependent variables in the context of reactive synthesis. Inspired by successful pre-processing steps in Boolean functional synthesis, we define dependent variables as output variables that are uniquely assigned, given an assignment, to all other variables and the history so far. We describe an automata-based approach for finding a set of dependent variables. Using this, we show that dependent variables are surprisingly common in reactive synthesis benchmarks. Next, we develop a novel synthesis framework that exploits dependent variables to construct an overall synthesis solution. By implementing this framework using the widely used library Spot, we show that reactive synthesis using dependent variables can solve some problems beyond the reach of several existing techniques. Further, among benchmarks with dependent variables, if the number of non-dependent variables is low (at most 3 in our experiments), our method is able outperform all state-of-the-art tools for synthesis.
△ Less
Submitted 20 January, 2024;
originally announced January 2024.
-
Auditable Algorithms for Approximate Model Counting
Authors:
Kuldeep S. Meel,
Supratik Chakraborty,
S. Akshay
Abstract:
Model counting, or counting the satisfying assignments of a Boolean formula, is a fundamental problem with diverse applications. Given #P-hardness of the problem, develo** algorithms for approximate counting is an important research area. Building on the practical success of SAT-solvers, the focus has recently shifted from theory to practical implementations of approximate counting algorithms. T…
▽ More
Model counting, or counting the satisfying assignments of a Boolean formula, is a fundamental problem with diverse applications. Given #P-hardness of the problem, develo** algorithms for approximate counting is an important research area. Building on the practical success of SAT-solvers, the focus has recently shifted from theory to practical implementations of approximate counting algorithms. This has brought to focus new challenges, such as the design of auditable approximate counters that not only provide an approximation of the model count, but also a certificate that a verifier with limited computational power can use to check if the count is indeed within the promised bounds of approximation.
Towards generating certificates, we start by examining the best-known deterministic approximate counting algorithm that uses polynomially many calls to a $Σ_2^P$ oracle. We show that this can be audited via a $Σ_2^P$ oracle with the query constructed over $n^2 \log^2 n$ variables, where the original formula has $n$ variables. Since $n$ is often large, we ask if the count of variables in the certificate can be reduced -- a crucial question for potential implementation. We show that this is indeed possible with a tradeoff in the counting algorithm's complexity. Specifically, we develop new deterministic approximate counting algorithms that invoke a $Σ_3^P$ oracle, but can be certified using a $Σ_2^P$ oracle using certificates on far fewer variables: our final algorithm uses only $n \log n$ variables. Our study demonstrates that one can simplify auditing significantly if we allow the counting algorithm to access a slightly more powerful oracle. This shows for the first time how audit complexity can be traded for complexity of approximate counting.
△ Less
Submitted 19 December, 2023;
originally announced December 2023.
-
A Few-Shot Approach to Dysarthric Speech Intelligibility Level Classification Using Transformers
Authors:
Paleti Nikhil Chowdary,
Vadlapudi Sai Aravind,
Gorantla V N S L Vishnu Vardhan,
Menta Sai Akshay,
Menta Sai Aashish,
Jyothish Lal. G
Abstract:
Dysarthria is a speech disorder that hinders communication due to difficulties in articulating words. Detection of dysarthria is important for several reasons as it can be used to develop a treatment plan and help improve a person's quality of life and ability to communicate effectively. Much of the literature focused on improving ASR systems for dysarthric speech. The objective of the current wor…
▽ More
Dysarthria is a speech disorder that hinders communication due to difficulties in articulating words. Detection of dysarthria is important for several reasons as it can be used to develop a treatment plan and help improve a person's quality of life and ability to communicate effectively. Much of the literature focused on improving ASR systems for dysarthric speech. The objective of the current work is to develop models that can accurately classify the presence of dysarthria and also give information about the intelligibility level using limited data by employing a few-shot approach using a transformer model. This work also aims to tackle the data leakage that is present in previous studies. Our whisper-large-v2 transformer model trained on a subset of the UASpeech dataset containing medium intelligibility level patients achieved an accuracy of 85%, precision of 0.92, recall of 0.8 F1-score of 0.85, and specificity of 0.91. Experimental results also demonstrate that the model trained using the 'words' dataset performed better compared to the model trained on the 'letters' and 'digits' dataset. Moreover, the multiclass model achieved an accuracy of 67%.
△ Less
Submitted 17 September, 2023;
originally announced September 2023.
-
Enhancing Knee Osteoarthritis severity level classification using diffusion augmented images
Authors:
Paleti Nikhil Chowdary,
Gorantla V N S L Vishnu Vardhan,
Menta Sai Akshay,
Menta Sai Aashish,
Vadlapudi Sai Aravind,
Garapati Venkata Krishna Rayalu,
Aswathy P
Abstract:
This research paper explores the classification of knee osteoarthritis (OA) severity levels using advanced computer vision models and augmentation techniques. The study investigates the effectiveness of data preprocessing, including Contrast-Limited Adaptive Histogram Equalization (CLAHE), and data augmentation using diffusion models. Three experiments were conducted: training models on the origin…
▽ More
This research paper explores the classification of knee osteoarthritis (OA) severity levels using advanced computer vision models and augmentation techniques. The study investigates the effectiveness of data preprocessing, including Contrast-Limited Adaptive Histogram Equalization (CLAHE), and data augmentation using diffusion models. Three experiments were conducted: training models on the original dataset, training models on the preprocessed dataset, and training models on the augmented dataset. The results show that data preprocessing and augmentation significantly improve the accuracy of the models. The EfficientNetB3 model achieved the highest accuracy of 84\% on the augmented dataset. Additionally, attention visualization techniques, such as Grad-CAM, are utilized to provide detailed attention maps, enhancing the understanding and trustworthiness of the models. These findings highlight the potential of combining advanced models with augmented data and attention visualization for accurate knee OA severity classification.
△ Less
Submitted 17 September, 2023;
originally announced September 2023.
-
A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation
Authors:
S Akshay,
Paul Gastin,
R Govind,
Aniruddha R Joshi,
B Srivathsan
Abstract:
In this paper, we consider a model of generalized timed automata (GTA) with two kinds of clocks, history and future, that can express many timed features succinctly, including timed automata, event-clock automata with and without diagonal constraints, and automata with timers. Our main contribution is a new simulation-based zone algorithm for checking reachability in this unified model. While such…
▽ More
In this paper, we consider a model of generalized timed automata (GTA) with two kinds of clocks, history and future, that can express many timed features succinctly, including timed automata, event-clock automata with and without diagonal constraints, and automata with timers. Our main contribution is a new simulation-based zone algorithm for checking reachability in this unified model. While such algorithms are known to exist for timed automata, and have recently been shown for event-clock automata without diagonal constraints, this is the first result that can handle event-clock automata with diagonal constraints and automata with timers. We also provide a prototype implementation for our model and show experimental results on several benchmarks. To the best of our knowledge, this is the first effective implementation not just for our unified model, but even just for automata with timers or for event-clock automata (with predicting clocks) without going through a costly translation via timed automata. Last but not least, beyond being interesting in their own right, generalized timed automata can be used for model-checking event-clock specifications over timed automata models.
△ Less
Submitted 28 May, 2023;
originally announced May 2023.
-
MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives
Authors:
S. Akshay,
Krishnendu Chatterjee,
Tobias Meggendorfer,
Đorđe Žikelić
Abstract:
Markov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpoint to reason about trajectories of distributions, basic reachability and safety problems are known to be computationally intractable (i.e., Skolem-hard) to solve in such models. Further, we show that even for simple examples of MDPs, strategies for safety objecti…
▽ More
Markov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpoint to reason about trajectories of distributions, basic reachability and safety problems are known to be computationally intractable (i.e., Skolem-hard) to solve in such models. Further, we show that even for simple examples of MDPs, strategies for safety objectives over distributions can require infinite memory and randomization.
In light of this, we present a novel overapproximation approach to synthesize strategies in an MDP, such that a safety objective over the distributions is met. More precisely, we develop a new framework for template-based synthesis of certificates as affine distributional and inductive invariants for safety objectives in MDPs. We provide two algorithms within this framework. One can only synthesize memoryless strategies, but has relative completeness guarantees, while the other can synthesize general strategies. The runtime complexity of both algorithms is in PSPACE. We implement these algorithms and show that they can solve several non-trivial examples.
△ Less
Submitted 26 May, 2023;
originally announced May 2023.
-
On Robustness for the Skolem, Positivity and Ultimate Positivity Problems
Authors:
S. Akshay,
Hugo Bazille,
Blaise Genest,
Mihir Vahanwala
Abstract:
The Skolem problem is a long-standing open problem in linear dynamical systems: can a linear recurrence sequence (LRS) ever reach 0 from a given initial configuration? Similarly, the positivity problem asks whether the LRS stays positive from an initial configuration. Deciding Skolem (or positivity) has been open for half a century: the best known decidability results are for LRS with special prop…
▽ More
The Skolem problem is a long-standing open problem in linear dynamical systems: can a linear recurrence sequence (LRS) ever reach 0 from a given initial configuration? Similarly, the positivity problem asks whether the LRS stays positive from an initial configuration. Deciding Skolem (or positivity) has been open for half a century: the best known decidability results are for LRS with special properties (e.g., low order recurrences). But these problems are easier for "uninitialized" variants, where the initial configuration is not fixed but can vary arbitrarily: checking if there is an initial configuration from which the LRS stays positive can be decided in polynomial time (Tiwari in 2004, Braverman in 2006). In this paper, we consider problems that lie between the initialized and uninitialized variants. More precisely, we ask if 0 (resp. negative numbers) can be avoided from every initial configuration in a neighborhood of a given initial configuration. This can be considered as a robust variant of the Skolem (resp. positivity) problem. We show that these problems lie at the frontier of decidability: if the neighbourhood is given as part of the input, then robust Skolem and robust positivity are Diophantine hard, i.e., solving either would entail major breakthroughs in Diophantine approximations, as happens for (non-robust) positivity. However, if one asks whether such a neighbourhood exists, then the problems turn out to be decidable with PSPACE complexity. Our techniques also allow us to tackle robustness for ultimate positivity, which asks whether there is a bound on the number of steps after which the LRS remains positive. There are two variants depending on whether we ask for a "uniform" bound on this number of steps. For the non-uniform variant, when the neighbourhood is open, the problem turns out to be tractable, even when the neighbourhood is given as input.
△ Less
Submitted 4 June, 2024; v1 submitted 4 November, 2022;
originally announced November 2022.
-
Simulations for Event-Clock Automata
Authors:
S Akshay,
Paul Gastin,
R Govind,
B Srivathsan
Abstract:
Event-clock automata (ECA) are a well-known semantic subclass of timed automata (TA) which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for checking non-emptiness of event-clock automata. As ECAs contain special prophecy clocks that guess and maintain t…
▽ More
Event-clock automata (ECA) are a well-known semantic subclass of timed automata (TA) which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for checking non-emptiness of event-clock automata. As ECAs contain special prophecy clocks that guess and maintain the time to the next occurrence of specific events, they cannot be seen as a syntactic subclass of TA. Therefore, implementations for TA cannot be directly used for ECAs, and moreover the translation of an ECA to a semantically equivalent TA is expensive. Another reason for the lack of ECA implementations is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied by Geeraerts et al. in 2011, where the authors proposed a zone enumeration procedure that uses zone extrapolations for finiteness. In this article, we propose a different zone-based algorithm to solve the reachability problem for event-clock automata, using simulations for finiteness. A surprising consequence of our result is that for event-predicting automata, the subclass of event-clock automata that only use prophecy clocks, we obtain finiteness even without any simulations. For general event-clock automata, our new algorithm exploits the G-simulation framework, which is the coarsest known simulation relation in timed automata literature, and has been recently used for advances in other extensions of timed automata.
△ Less
Submitted 1 July, 2024; v1 submitted 6 July, 2022;
originally announced July 2022.
-
On eventual non-negativity and positivity for the weighted sum of powers of matrices
Authors:
S Akshay,
Supratik Chakraborty,
Debtanu Pal
Abstract:
The long run behaviour of linear dynamical systems is often studied by looking at eventual properties of matrices and recurrences that underlie the system. A basic problem that lies at the core of many questions in this setting is the following: given a set of pairs of rational weights and matrices {(w_1 , A_1 ), . . . , (w_m , A_m )}, we ask if the weighted sum of powers of these matrices is even…
▽ More
The long run behaviour of linear dynamical systems is often studied by looking at eventual properties of matrices and recurrences that underlie the system. A basic problem that lies at the core of many questions in this setting is the following: given a set of pairs of rational weights and matrices {(w_1 , A_1 ), . . . , (w_m , A_m )}, we ask if the weighted sum of powers of these matrices is eventually non-negative P (resp. n positive), i.e., does there exist an integer N s.t for all n greater than N , (w_1 A_1^n + ... + w_m A_m^n) is atmost 0 (resp. greater than 0). The restricted setting when m = w_1 = 1, results in so-called eventually non-negative (or eventually positive) matrices, which enjoy nice spectral properties and have been well-studied in control theory. More applications arise in varied contexts, ranging from program verification to partially observable and multi-modal systems.
Our goal is to investigate this problem and its link to linear recurrence sequences. Our first result is that for m at least 2, the problem is as hard as the ultimate positivity of linear recurrences, a long standing open question (known to be coNP-hard). Our second result is a reduction in the other direction showing that for any m at least 1, the problem reduces to ultimate positivity of linear recurrences. This shows precise upper bounds for several subclasses of matrices by exploiting known results on linear recurrence sequences. Our third main result is a novel reduction technique for a large class of problems (including those mentioned above) over rational diagonalizable matrices to the corresponding problem over simple real-algebraic matrices. This yields effective decision procedures for diagonalizable matrices.
△ Less
Submitted 18 May, 2022;
originally announced May 2022.
-
Synthesizing Pareto-Optimal Interpretations for Black-Box Models
Authors:
Hazem Torfah,
Shetal Shah,
Supratik Chakraborty,
S. Akshay,
Sanjit A. Seshia
Abstract:
We present a new multi-objective optimization approach for synthesizing interpretations that "explain" the behavior of black-box machine learning models. Constructing human-understandable interpretations for black-box models often requires balancing conflicting objectives. A simple interpretation may be easier to understand for humans while being less precise in its predictions vis-a-vis a complex…
▽ More
We present a new multi-objective optimization approach for synthesizing interpretations that "explain" the behavior of black-box machine learning models. Constructing human-understandable interpretations for black-box models often requires balancing conflicting objectives. A simple interpretation may be easier to understand for humans while being less precise in its predictions vis-a-vis a complex interpretation. Existing methods for synthesizing interpretations use a single objective function and are often optimized for a single class of interpretations. In contrast, we provide a more general and multi-objective synthesis framework that allows users to choose (1) the class of syntactic templates from which an interpretation should be synthesized, and (2) quantitative measures on both the correctness and explainability of an interpretation. For a given black-box, our approach yields a set of Pareto-optimal interpretations with respect to the correctness and explainability measures. We show that the underlying multi-objective optimization problem can be solved via a reduction to quantitative constraint solving, such as weighted maximum satisfiability. To demonstrate the benefits of our approach, we have applied it to synthesize interpretations for black-box neural-network classifiers. Our experiments show that there often exists a rich and varied set of choices for interpretations that are missed by existing approaches.
△ Less
Submitted 16 August, 2021;
originally announced August 2021.
-
Fast zone-based algorithms for reachability in pushdown timed automata
Authors:
S. Akshay,
Paul Gastin,
Karthik R Prakash
Abstract:
Given the versatility of timed automata a huge body of work has evolved that considers extensions of timed automata. One extension that has received a lot of interest is timed automata with a, possibly unbounded, stack, also called the pushdown timed automata (PDTA) model. While different algorithms have been given for reachability in different variants of this model, most of these results are pur…
▽ More
Given the versatility of timed automata a huge body of work has evolved that considers extensions of timed automata. One extension that has received a lot of interest is timed automata with a, possibly unbounded, stack, also called the pushdown timed automata (PDTA) model. While different algorithms have been given for reachability in different variants of this model, most of these results are purely theoretical and do not give rise to efficient implementations. One main reason for this is that none of these algorithms (and the implementations that exist) use the so-called zone-based abstraction, but rely either on the region-abstraction or other approaches, which are significantly harder to implement.
In this paper, we show that a naive extension of the zone based reachability algorithm for the control state reachability problem of timed automata is not sound in the presence of a stack. To understand this better we give an inductive rule based view of the zone reachability algorithm for timed automata. This alternate view allows us to analyze and adapt the rules to also work for pushdown timed automata. We obtain the first zone-based algorithm for PDTA which is terminating, sound and complete. We implement our algorithm in the tool TChecker and perform experiments to show its efficacy, thus leading the way for more practical approaches to the verification of pushdown timed systems.
△ Less
Submitted 19 July, 2021; v1 submitted 28 May, 2021;
originally announced May 2021.
-
A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis
Authors:
Preey Shah,
Aman Bansal,
S. Akshay,
Supratik Chakraborty
Abstract:
Boolean Skolem function synthesis concerns synthesizing outputs as Boolean functions of inputs such that a relational specification between inputs and outputs is satisfied. This problem, also known as Boolean functional synthesis, has several applications, including design of safe controllers for autonomous systems, certified QBF solving, cryptanalysis etc. Recently, complexity theoretic hardness…
▽ More
Boolean Skolem function synthesis concerns synthesizing outputs as Boolean functions of inputs such that a relational specification between inputs and outputs is satisfied. This problem, also known as Boolean functional synthesis, has several applications, including design of safe controllers for autonomous systems, certified QBF solving, cryptanalysis etc. Recently, complexity theoretic hardness results have been shown for the problem, although several algorithms proposed in the literature are known to work well in practice. This dichotomy between theoretical hardness and practical efficacy has motivated the research into normal forms or representations of input specifications that permit efficient synthesis, thus explaining perhaps the efficacy of these algorithms.
In this paper we go one step beyond this and ask if there exists a normal form representation that can in fact precisely characterize "efficient" synthesis. We present a normal form called SAUNF that precisely characterizes tractable synthesis in the following sense: a specification is polynomial time synthesizable iff it can be compiled to SAUNF in polynomial time. Additionally, a specification admits a polynomial-sized functional solution iff there exists a semantically equivalent polynomial-sized SAUNF representation. SAUNF is exponentially more succinct than well-established normal forms like BDDs and DNNFs, used in the context of AI problems, and strictly subsumes other more recently proposed forms like SynNNF. It enjoys compositional properties that are similar to those of DNNF. Thus, SAUNF provides the right trade-off in knowledge representation for Boolean functional synthesis.
△ Less
Submitted 28 June, 2021; v1 submitted 29 April, 2021;
originally announced April 2021.
-
On synthesizing Skolem functions for first order logic formulae
Authors:
S. Akshay,
Supratik Chakraborty
Abstract:
Skolem functions play a central role in the study of first order logic, both from theoretical and practical perspectives. While every Skolemized formula in first-order logic makes use of Skolem constants and/or functions, not all such Skolem constants and/or functions admit effectively computable interpretations. Indeed, the question of whether there exists an effectively computable interpretation…
▽ More
Skolem functions play a central role in the study of first order logic, both from theoretical and practical perspectives. While every Skolemized formula in first-order logic makes use of Skolem constants and/or functions, not all such Skolem constants and/or functions admit effectively computable interpretations. Indeed, the question of whether there exists an effectively computable interpretation of a Skolem function, and if so, how to automatically synthesize it, is fundamental to their use in several applications, such as planning, strategy synthesis, program synthesis etc.
In this paper, we investigate the computability of Skolem functions and their automated synthesis in the full generality of first order logic. We first show a strong negative result, that even under mild assumptions on the vocabulary, it is impossible to obtain computable interpretations of Skolem functions. We then show a positive result, providing a precise characterization of first-order theories that admit effective interpretations of Skolem functions, and also present algorithms to automatically synthesize such interpretations. We discuss applications of our characterization as well as complexity bounds for Skolem functions (interpreted as Turing machines).
△ Less
Submitted 4 August, 2022; v1 submitted 15 February, 2021;
originally announced February 2021.
-
Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice
Authors:
Kuldeep S. Meel,
S. Akshay
Abstract:
Given a CNF formula F on n variables, the problem of model counting or #SAT is to compute the number of satisfying assignments of F . Model counting is a fundamental but hard problem in computer science with varied applications. Recent years have witnessed a surge of effort towards develo** efficient algorithmic techniques that combine the classical 2-universal hashing with the remarkable progre…
▽ More
Given a CNF formula F on n variables, the problem of model counting or #SAT is to compute the number of satisfying assignments of F . Model counting is a fundamental but hard problem in computer science with varied applications. Recent years have witnessed a surge of effort towards develo** efficient algorithmic techniques that combine the classical 2-universal hashing with the remarkable progress in SAT solving over the past decade. These techniques augment the CNF formula F with random XOR constraints and invoke an NP oracle repeatedly on the resultant CNF-XOR formulas. In practice, calls to the NP oracle calls are replaced a SAT solver whose runtime performance is adversely affected by size of XOR constraints. The standard construction of 2-universal hash functions chooses every variable with probability p = 1/2 leading to XOR constraints of size n/2 in expectation. Consequently, the challenge is to design sparse hash functions where variables can be chosen with smaller probability and lead to smaller sized XOR constraints.
In this paper, we address this challenge from theoretical and practical perspectives. First, we formalize a relaxation of universal hashing, called concentrated hashing and establish a novel and beautiful connection between concentration measures of these hash functions and isoperimetric inequalities on boolean hypercubes. This allows us to obtain (log m) tight bounds on variance and dispersion index and show that p = O( log(m)/m ) suffices for design of sparse hash functions from {0, 1}^n to {0, 1}^m. We then use sparse hash functions belonging to this concentrated hash family to develop new approximate counting algorithms. A comprehensive experimental evaluation of our algorithm on 1893 benchmarks demonstrates that usage of sparse hash functions can lead to significant speedups.
△ Less
Submitted 30 April, 2020;
originally announced April 2020.
-
Revisiting Underapproximate Reachability for Multipushdown Systems
Authors:
S. Akshay,
Paul Gastin,
S Krishna,
Sparsa Roychowdhury
Abstract:
Boolean programs with multiple recursive threads can be captured as pushdown automata with multiple stacks. This model is Turing complete, and hence, one is often interested in analyzing a restricted class that still captures useful behaviors. In this paper, we propose a new class of bounded under approximations for multi-pushdown systems, which subsumes most existing classes. We develop an effici…
▽ More
Boolean programs with multiple recursive threads can be captured as pushdown automata with multiple stacks. This model is Turing complete, and hence, one is often interested in analyzing a restricted class that still captures useful behaviors. In this paper, we propose a new class of bounded under approximations for multi-pushdown systems, which subsumes most existing classes. We develop an efficient algorithm for solving the under-approximate reachability problem, which is based on efficient fix-point computations. We implement it in our tool BHIM and illustrate its applicability by generating a set of relevant benchmarks and examining its performance. As an additional takeaway, BHIM solves the binary reachability problem in pushdown automata. To show the versatility of our approach, we then extend our algorithm to the timed setting and provide the first implementation that can handle timed multi-pushdown automata with closed guards.
△ Less
Submitted 5 May, 2020; v1 submitted 14 February, 2020;
originally announced February 2020.
-
Knowledge Compilation for Boolean Functional Synthesis
Authors:
S. Akshay,
Jatin Arora,
Supratik Chakraborty,
S. Krishna,
Divya Raghunathan,
Shetal Shah
Abstract:
Given a Boolean formula F(X,Y), where X is a vector of outputs and Y is a vector of inputs, the Boolean functional synthesis problem requires us to compute a Skolem function vector G(Y)for X such that F(G(Y),Y) holds whenever \exists X F(X,Y) holds. In this paper, we investigate the relation between the representation of the specification F(X,Y) and the complexity of synthesis. We introduce a new…
▽ More
Given a Boolean formula F(X,Y), where X is a vector of outputs and Y is a vector of inputs, the Boolean functional synthesis problem requires us to compute a Skolem function vector G(Y)for X such that F(G(Y),Y) holds whenever \exists X F(X,Y) holds. In this paper, we investigate the relation between the representation of the specification F(X,Y) and the complexity of synthesis. We introduce a new normal form for Boolean formulas, called SynNNF, that guarantees polynomial-time synthesis and also polynomial-time existential quantification for some order of quantification of variables. We show that several normal forms studied in the knowledge compilation literature are subsumed by SynNNF, although SynNNFcan be super-polynomially more succinct than them. Motivated by these results, we propose an algorithm to convert a specification in CNF to SynNNF, with the intent of solving the Boolean functional synthesis problem. Experiments with a prototype implementation show that this approach solves several benchmarks beyond the reach of state-of-the-art tools.
△ Less
Submitted 17 August, 2019;
originally announced August 2019.
-
Timed Systems through the Lens of Logic
Authors:
S. Akshay,
Paul Gastin,
Vincent Juge,
Shankara Narayanan Krishna
Abstract:
In this paper, we analyze timed systems with data structures, using a rich interplay of logic and properties of graphs. We start by describing behaviors of timed systems using graphs with timing constraints. Such a graph is called realizable if we can assign time-stamps to nodes or events so that they are consistent with the timing constraints. The logical definability of several graph properties…
▽ More
In this paper, we analyze timed systems with data structures, using a rich interplay of logic and properties of graphs. We start by describing behaviors of timed systems using graphs with timing constraints. Such a graph is called realizable if we can assign time-stamps to nodes or events so that they are consistent with the timing constraints. The logical definability of several graph properties has been a challenging problem, and we show, using a highly non-trivial argument, that the realizability property for collections of graphs with strict timing constraints is logically definable in a class of propositional dynamic logic (EQ-ICPDL), which is strictly contained in MSO. Using this result, we propose a novel, algorithmically efficient and uniform proof technique for the analysis of timed systems enriched with auxiliary data structures, like stacks and queues. Our technique unravels new results (for emptiness checking as well as model checking) for timed systems with richer features than considered so far, while also recovering existing results.
△ Less
Submitted 27 April, 2019; v1 submitted 9 March, 2019;
originally announced March 2019.
-
Continuous Reachability for Unordered Data Petri nets is in PTime
Authors:
Utkarsh Gupta,
Preey Shah,
S. Akshay,
Piotr Hofman
Abstract:
Unordered data Petri nets (UDPN) are an extension of classical Petri nets with tokens that carry data from an infinite domain and where transitions may check equality and disequality of tokens. UDPN are well-structured, so the coverability and termination problems are decidable, but with higher complexity than for Petri nets. On the other hand, the problem of reachability for UDPN is surprisingly…
▽ More
Unordered data Petri nets (UDPN) are an extension of classical Petri nets with tokens that carry data from an infinite domain and where transitions may check equality and disequality of tokens. UDPN are well-structured, so the coverability and termination problems are decidable, but with higher complexity than for Petri nets. On the other hand, the problem of reachability for UDPN is surprisingly complex, and its decidability status remains open. In this paper, we consider the continuous reachability problem for UDPN, which can be seen as an over-approximation of the reachability problem. Our main result is a characterization of continuous reachability for UDPN and polynomial time algorithm for solving it. This is a consequence of a combinatorial argument, which shows that if continuous reachability holds then there exists a run using only polynomially many data values.
△ Less
Submitted 14 February, 2019;
originally announced February 2019.
-
Distribution-based objectives for Markov Decision Processes
Authors:
S. Akshay,
Blaise Genest,
Nikhil Vyas
Abstract:
We consider distribution-based objectives for Markov Decision Processes (MDP). This class of objectives gives rise to an interesting trade-off between full and partial information. As in full observation, the strategy in the MDP can depend on the state of the system, but similar to partial information, the strategy needs to account for all the states at the same time. In this paper, we focus on tw…
▽ More
We consider distribution-based objectives for Markov Decision Processes (MDP). This class of objectives gives rise to an interesting trade-off between full and partial information. As in full observation, the strategy in the MDP can depend on the state of the system, but similar to partial information, the strategy needs to account for all the states at the same time. In this paper, we focus on two safety problems that arise naturally in this context, namely, existential and universal safety. Given an MDP A and a closed and convex polytope H of probability distributions over the states of A, the existential safety problem asks whether there exists some distribution d in H and a strategy of A, such that starting from d and repeatedly applying this strategy keeps the distribution forever in H. The universal safety problem asks whether for all distributions in H, there exists such a strategy of A which keeps the distribution forever in H. We prove that both problems are decidable, with tight complexity bounds: we show that existential safety is PTIME-complete, while universal safety is co-NP-complete. Further, we compare these results with existential and universal safety problems for Rabin's probabilistic finite-state automata (PFA), the subclass of Partially Observable MDPs which have zero observation. Compared to MDPs, strategies of PFAs are not state-dependent. In sharp contrast to the PTIME result, we show that existential safety for PFAs is undecidable, with H having closed and open boundaries. On the other hand, it turns out that the universal safety for PFAs is decidable in EXPTIME, with a co-NP lower bound. Finally, we show that an alternate representation of the input polytope allows us to improve the complexity of universal safety for MDPs and PFAs.
△ Less
Submitted 25 April, 2018;
originally announced April 2018.
-
What's hard about Boolean Functional Synthesis
Authors:
S. Akshay,
Supratik Chakraborty,
Shubham Goel,
Sumith Kulal,
Shetal Shah
Abstract:
Given a relational specification between Boolean inputs and outputs, the goal of Boolean functional synthesis is to synthesize each output as a function of the inputs such that the specification is met. In this paper, we first show that unless some hard conjectures in complexity theory are falsified, Boolean functional synthesis must necessarily generate exponential-sized Skolem functions, thereby…
▽ More
Given a relational specification between Boolean inputs and outputs, the goal of Boolean functional synthesis is to synthesize each output as a function of the inputs such that the specification is met. In this paper, we first show that unless some hard conjectures in complexity theory are falsified, Boolean functional synthesis must necessarily generate exponential-sized Skolem functions, thereby requiring exponential time, in the worst-case. Given this inherent hardness, what does one do to solve the problem? We present a two-phase algorithm for Boolean functional synthesis, where the first phase is efficient both in terms of time and sizes of synthesized functions, and solves an overwhelming majority of benchmarks. To explain this surprisingly good performance, we provide a sufficient condition under which the first phase must produce exact correct answers. When this condition fails, the second phase builds upon the result of the first phase, possibly requiring exponential time and generating exponential-sized functions in the worst-case. Detailed experimental evaluation shows our algorithm to perform better than state-of-the-art techniques for a majority of benchmarks.
△ Less
Submitted 18 May, 2018; v1 submitted 16 April, 2018;
originally announced April 2018.
-
Towards an Efficient Tree Automata based technique for Timed Systems
Authors:
S. Akshay,
Paul Gastin,
Shankara Narayanan Krishna,
Ilias Sarkar
Abstract:
The focus of this paper is the analysis of real-time systems with recursion, through the development of good theoretical techniques which are implementable. Time is modeled using clock variables, and recursion using stacks. Our technique consists of modeling the behaviours of the timed system as graphs, and interpreting these graphs on tree terms by showing a bound on their tree-width. We then bui…
▽ More
The focus of this paper is the analysis of real-time systems with recursion, through the development of good theoretical techniques which are implementable. Time is modeled using clock variables, and recursion using stacks. Our technique consists of modeling the behaviours of the timed system as graphs, and interpreting these graphs on tree terms by showing a bound on their tree-width. We then build a tree automaton that accepts exactly those tree terms that describe realizable runs of the timed system. The emptiness of the timed system thus boils down to emptiness of a finite tree automaton that accepts these tree terms. This approach helps us in obtaining an optimal complexity, not just in theory (as done in earlier work), but also in going towards an efficient implementation of our technique. To do this, we make several improvements in the theory and exploit these to build a first prototype tool that can analyze timed systems with recursion.
△ Less
Submitted 8 July, 2017;
originally announced July 2017.
-
On Petri Nets with Hierarchical Special Arcs
Authors:
S. Akshay,
Supratik Chakraborty,
Ankush Das,
Vishal Jagannath,
Sai Sandeep
Abstract:
We investigate the decidability of termination, reachability, coverability and deadlock-freeness of Petri nets endowed with a hierarchy on places, and with inhibitor arcs, reset arcs and transfer arcs that respect this hierarchy. We also investigate what happens when we have a mix of these special arcs, some of which respect the hierarchy, while others do not. We settle the decidability status of…
▽ More
We investigate the decidability of termination, reachability, coverability and deadlock-freeness of Petri nets endowed with a hierarchy on places, and with inhibitor arcs, reset arcs and transfer arcs that respect this hierarchy. We also investigate what happens when we have a mix of these special arcs, some of which respect the hierarchy, while others do not. We settle the decidability status of the above four problems for all combinations of hierarchy, inhibitor, reset and transfer arcs, except the termination problem for two combinations. For both these combinations, we show that the termination problem is as hard as deciding positivity for linear recurrent sequences -- a long-standing open problem.
△ Less
Submitted 4 July, 2017;
originally announced July 2017.
-
Towards Parallel Boolean Functional Synthesis
Authors:
S. Akshay,
Supratik Chakraborty,
Ajith K. John,
Shetal Shah
Abstract:
Given a relational specification R(X, Y), where X and Y are sequences of input and output variables, we wish to synthesize each output as a function of the inputs such that the specification holds. This is called the Boolean functional synthesis problem and has applications in several areas. In this paper, we present the first parallel approach for solving this problem, using compositional and CEG…
▽ More
Given a relational specification R(X, Y), where X and Y are sequences of input and output variables, we wish to synthesize each output as a function of the inputs such that the specification holds. This is called the Boolean functional synthesis problem and has applications in several areas. In this paper, we present the first parallel approach for solving this problem, using compositional and CEGAR-style reasoning as key building blocks. We show by means of extensive experiments that our approach outperforms existing tools on a large class of benchmarks.
△ Less
Submitted 4 March, 2017;
originally announced March 2017.
-
Stochastic Timed Games Revisited
Authors:
S Akshay,
Patricia Bouyer,
Shankara Narayanan Krishna,
Lakshmi Manasa,
Ashutosh Trivedi
Abstract:
Stochastic timed games (STGs), introduced by Bouyer and Forejt, naturally generalize both continuous-time Markov chains and timed automata by providing a partition of the locations between those controlled by two players (Player Box and Player Diamond) with competing objectives and those governed by stochastic laws. Depending on the number of players---$2$, $1$, or $0$---subclasses of stochastic t…
▽ More
Stochastic timed games (STGs), introduced by Bouyer and Forejt, naturally generalize both continuous-time Markov chains and timed automata by providing a partition of the locations between those controlled by two players (Player Box and Player Diamond) with competing objectives and those governed by stochastic laws. Depending on the number of players---$2$, $1$, or $0$---subclasses of stochastic timed games are often classified as $2\frac{1}{2}$-player, $1\frac{1}{2}$-player, and $\frac{1}{2}$-player games where the $\frac{1}{2}$ symbolizes the presence of the stochastic "nature" player. For STGs with reachability objectives it is known that $1\frac{1}{2}$-player one-clock STGs are decidable for qualitative objectives, and that $2\frac{1}{2}$-player three-clock STGs are undecidable for quantitative reachability objectives. This paper further refines the gap in this decidability spectrum. We show that quantitative reachability objectives are already undecidable for $1\frac{1}{2}$ player four-clock STGs, and even under the time-bounded restriction for $2\frac{1}{2}$-player five-clock STGs. We also obtain a class of $1\frac{1}{2}$, $2\frac{1}{2}$ player STGs for which the quantitative reachability problem is decidable.
△ Less
Submitted 19 July, 2016;
originally announced July 2016.
-
Analyzing Timed Systems Using Tree Automata
Authors:
S. Akshay,
Paul Gastin,
Shankara Narayanan Krishna
Abstract:
Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The m…
▽ More
Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. When a family of graphs has bounded tree-width, they can be interpreted in trees and MSO-definable properties of such graphs can be checked using tree automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions).
△ Less
Submitted 8 May, 2018; v1 submitted 28 April, 2016;
originally announced April 2016.
-
Skolem Functions for Factored Formulas
Authors:
Ajith K. John,
Shetal Shah,
Supratik Chakraborty,
Ashutosh Trivedi,
S. Akshay
Abstract:
Given a propositional formula F(x,y), a Skolem function for x is a function Ψ(y), such that substituting Ψ(y) for x in F gives a formula semantically equivalent to \exists F. Automatically generating Skolem functions is of significant interest in several applications including certified QBF solving, finding strategies of players in games, synthesising circuits and bit-vector programs from specific…
▽ More
Given a propositional formula F(x,y), a Skolem function for x is a function Ψ(y), such that substituting Ψ(y) for x in F gives a formula semantically equivalent to \exists F. Automatically generating Skolem functions is of significant interest in several applications including certified QBF solving, finding strategies of players in games, synthesising circuits and bit-vector programs from specifications, disjunctive decomposition of sequential circuits etc. In many such applications, F is given as a conjunction of factors, each of which depends on a small subset of variables. Existing algorithms for Skolem function generation ignore any such factored form and treat F as a monolithic function. This presents scalability hurdles in medium to large problem instances. In this paper, we argue that exploiting the factored form of F can give significant performance improvements in practice when computing Skolem functions. We present a new CEGAR style algorithm for generating Skolem functions from factored propositional formulas. In contrast to earlier work, our algorithm neither requires a proof of QBF satisfiability nor uses composition of monolithic conjunctions of factors. We show experimentally that our algorithm generates smaller Skolem functions and outperforms state-of-the-art approaches on several large benchmarks.
△ Less
Submitted 23 September, 2015; v1 submitted 22 August, 2015;
originally announced August 2015.
-
Fermi-Bose cubic couplings in light-cone field theories
Authors:
Y. S. Akshay,
Sudarshan Ananth
Abstract:
We derive light-cone cubic interaction vertices involving fermions and bosons of arbitrary spin by demanding closure of the Poincaré algebra. We derive the three-point scattering amplitude corresponding to these interaction vertices and find that they possess interesting factorization properties, identical to the case of three boson scattering.
We derive light-cone cubic interaction vertices involving fermions and bosons of arbitrary spin by demanding closure of the Poincaré algebra. We derive the three-point scattering amplitude corresponding to these interaction vertices and find that they possess interesting factorization properties, identical to the case of three boson scattering.
△ Less
Submitted 3 April, 2015;
originally announced April 2015.
-
Coarse-grain Molecular Dynamics Study of Fullerene Transport across a Cell Membrane
Authors:
Sridhar Akshay,
Bharath Srikanth,
Amit Kumar,
Ashok Kumar Dasmahapatra
Abstract:
The study of the ability of drug molecules to enter cells through the membrane is of vital importance in the field of drug delivery. In cases where the transport of the drug molecules through the membrane is not easily accomplishable, other carrier molecules are used. Spherical fullerene molecules have been postulated as potential carriers of highly hydrophilic drugs across the plasma membrane. He…
▽ More
The study of the ability of drug molecules to enter cells through the membrane is of vital importance in the field of drug delivery. In cases where the transport of the drug molecules through the membrane is not easily accomplishable, other carrier molecules are used. Spherical fullerene molecules have been postulated as potential carriers of highly hydrophilic drugs across the plasma membrane. Here we report the coarse-grain molecular dynamics study of the translocation of C60 fullerene and its derivatives across a cell membrane modeled as a 1, 2-distearoyl-sn-glycero-3-phosphocholine (DSPC) bilayer. Simulation results indicate that pristine fullerene molecules enter the bilayer quickly and reside within it. The addition of polar functionalized groups makes the fullerenes less likely to reside within the bilayer but increases their residence time in bulk water. Addition of polar functional groups to one half of the fullerene surface, in effect creating a Janus particle, offers the most promise in develo** fullerene models that can achieve complete translocation through the membrane bilayer.
△ Less
Submitted 14 March, 2015;
originally announced March 2015.
-
Efficient Support of Big Data Storage Systems on the Cloud
Authors:
Akshay MS,
Suhas Mohan,
Vincent Kuri,
Dinkar Sitaram,
H. L. Phalachandra
Abstract:
Due to its advantages over traditional data centers, there has been a rapid growth in the usage of cloud infrastructures. These include public clouds (e.g., Amazon EC2), or private clouds, such as clouds deployed using OpenStack. A common factor in many of the well known infrastructures, for example OpenStack and CloudStack, is that networked storage is used for storage of persistent data. However…
▽ More
Due to its advantages over traditional data centers, there has been a rapid growth in the usage of cloud infrastructures. These include public clouds (e.g., Amazon EC2), or private clouds, such as clouds deployed using OpenStack. A common factor in many of the well known infrastructures, for example OpenStack and CloudStack, is that networked storage is used for storage of persistent data. However, traditional Big Data systems, including Hadoop, store data in commodity local storage for reasons of high performance and low cost. We present an architecture for supporting Hadoop on Openstack using local storage. Subsequently, we use benchmarks on Openstack and Amazon to show that for supporting Hadoop, local storage has better performance and lower cost. We conclude that cloud systems should support local storage for persistent data (in addition to networked storage) so as to provide efficient support for Hadoop and other Big Data systems
△ Less
Submitted 27 November, 2014;
originally announced November 2014.
-
Factorization of cubic vertices involving three different higher spin fields
Authors:
Y. S. Akshay,
Sudarshan Ananth
Abstract:
We derive a class of cubic interaction vertices for three higher spin fields, with integer spins $λ_1$, $λ_2$, $λ_3$, by closing commutators of the Poincaré algebra in four-dimensional flat spacetime. We find that these vertices exhibit an interesting factorization property which allows us to identify off-shell perturbative relations between them.
We derive a class of cubic interaction vertices for three higher spin fields, with integer spins $λ_1$, $λ_2$, $λ_3$, by closing commutators of the Poincaré algebra in four-dimensional flat spacetime. We find that these vertices exhibit an interesting factorization property which allows us to identify off-shell perturbative relations between them.
△ Less
Submitted 27 August, 2014; v1 submitted 9 April, 2014;
originally announced April 2014.
-
Light-cone gravity in AdS$_{4}$
Authors:
Y. S. Akshay,
Sudarshan Ananth,
Mahendra Mali
Abstract:
We obtain a closed form expression for the Action describing pure gravity, in light-cone gauge, in a four-dimensional Anti de Sitter background. We perform a perturbative expansion of this closed form result to extract the cubic interaction vertex in this gauge.
We obtain a closed form expression for the Action describing pure gravity, in light-cone gauge, in a four-dimensional Anti de Sitter background. We perform a perturbative expansion of this closed form result to extract the cubic interaction vertex in this gauge.
△ Less
Submitted 23 January, 2014;
originally announced January 2014.
-
Cubic interaction vertices in higher spin theories
Authors:
Y. S. Akshay,
Sudarshan Ananth
Abstract:
Based purely on symmetry considerations, we derive the following result: in momentum space, the coefficient of the cubic interaction vertex for a spin $λ$ field is equal to the corresponding Yang-Mills (spin 1) coefficient, raised to the power $λ$. This result is valid for all $λ$ for Lagrangians that contain a cubic interaction vertex of the form $λ$-$λ$-$λ$, in four-dimensional flat spacetime. F…
▽ More
Based purely on symmetry considerations, we derive the following result: in momentum space, the coefficient of the cubic interaction vertex for a spin $λ$ field is equal to the corresponding Yang-Mills (spin 1) coefficient, raised to the power $λ$. This result is valid for all $λ$ for Lagrangians that contain a cubic interaction vertex of the form $λ$-$λ$-$λ$, in four-dimensional flat spacetime. For $λ=3$, we present an additional derivation of this result.
△ Less
Submitted 17 April, 2014; v1 submitted 30 April, 2013;
originally announced April 2013.
