7 citations · 27 across the 17 of their papers we have counts for
22 papers
A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation
S Akshay, Paul Gastin, R Govind +2
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 time…
MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives
S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer +1
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 distribu…
On Robustness for the Skolem, Positivity and Ultimate Positivity Problems
S. Akshay, Hugo Bazille, Blaise Genest +1
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, t…
Simulations for Event-Clock Automata
S Akshay, Paul Gastin, R Govind +1
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 usef…
On eventual non-negativity and positivity for the weighted sum of powers of matrices
S Akshay, Supratik Chakraborty, Debtanu Pal
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 lie…
Synthesizing Pareto-Optimal Interpretations for Black-Box Models
Hazem Torfah, Shetal Shah, Supratik Chakraborty +2
We present a new multi-objective optimization approach for synthesizing interpretations that "explain" the behavior of black-box machine learning models. Constructing human-underst…
Fast zone-based algorithms for reachability in pushdown timed automata
S. Akshay, Paul Gastin, Karthik R Prakash
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 auto…
A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis
Preey Shah, Aman Bansal, S. Akshay +1
Boolean Skolem function synthesis concerns synthesizing outputs as Boolean functions of inputs such that a relational specification between inputs and outputs is satisfied. This pr…
On synthesizing Skolem functions for first order logic formulae
S. Akshay, Supratik Chakraborty
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…
Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice
Kuldeep S. Meel, S. Akshay
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 probl…
Revisiting Underapproximate Reachability for Multipushdown Systems
S. Akshay, Paul Gastin, S Krishna +1
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 ana…
Knowledge Compilation for Boolean Functional Synthesis
S. Akshay, Jatin Arora, Supratik Chakraborty +3
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…
Timed Systems through the Lens of Logic
S. Akshay, Paul Gastin, Vincent Juge +1
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 grap…
Continuous Reachability for Unordered Data Petri nets is in PTime
Utkarsh Gupta, Preey Shah, S. Akshay +1
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 disequali…
What's hard about Boolean Functional Synthesis
S. Akshay, Supratik Chakraborty, Shubham Goel +2
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…
Distribution-based objectives for Markov Decision Processes
S. Akshay, Blaise Genest, Nikhil Vyas
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.…
Towards an Efficient Tree Automata based technique for Timed Systems
S. Akshay, Paul Gastin, Shankara Narayanan Krishna +1
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 c…
On Petri Nets with Hierarchical Special Arcs
S. Akshay, Supratik Chakraborty, Ankush Das +2
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 ar…
Towards Parallel Boolean Functional Synthesis
S. Akshay, Supratik Chakraborty, Ajith K. John +1
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 spe…
Stochastic Timed Games Revisited
S Akshay, Patricia Bouyer, Shankara Narayanan Krishna +2
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…
Analyzing Timed Systems Using Tree Automata
S. Akshay, Paul Gastin, Shankara Narayanan Krishna
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 (u…
Skolem Functions for Factored Formulas
Ajith K. John, Shetal Shah, Supratik Chakraborty +2
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. Autom…