• Home
• Publications
• Teaching
• Activities
• Talks
• Misc

Book Chapters

S. Akshay and S. Chakraborty,
Synthesizing Skolem functions: A view from theory and practice
In Handbook of Logical Thought in India, eds. Sundar Sarukkai and Mihir K. Chakraborty, Springer, July 2022. Preprint | Springer link

Edited Volumes

• Akash Lal, S. Akshay, Saket Saurabh, Sandeep Sen,
  36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, 2016, Chennai, India.
  LIPIcs Vol. 65, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2016, ISBN 978-3-95977-027-9. Open Access Online

Journal Articles

• S. Akshay, P. Gastin, R. Govind, B. Srivathsan,
  Simulations for Event Clock Automata.
  In Logical Methods in Computer Science, Volume 20(2:10), 2024. (A preliminary version appeared at CONCUR'23.)


• S. Akshay, H. Bazille, B. Genest, M. Vahanwala.
  On Robustness for the Skolem, Positivity and Ultimate Positivity Problems.
  In Logical Methods in Computer Science, Volume 20(2:11), 2024. pdf (A preliminary version appeared at STACS'22.)


• S. Akshay, S. Chakraborty, S. Shah.
  Tractable Representations for Boolean Functional Synthesis,
  In Annals of Mathematics and Artificial Intelligence (AMAI), 2023, Springer online .


• S. Akshay, S. Chakraborty, S. Goel , S. Kulal, S. Shah.
  Boolean Functional Synthesis: Hardness and Practical Algorithms,
  In Formal Methods in System Design, Vol 57(1), pages 53--86, 2021. (Published online in Oct 2020 at Springer online.)


• S. Akshay, L. Helouet, R. Phawade.
  Combining Free Choice and Time in Petri Nets
  In Journal of Logical and Algebraic Methods in Programming, Volume 110, 100426, January 2020. (A preliminary version appeared at TIME'16.)


• S. Akshay, P. Gastin, S. Krishna.
  Analyzing Timed Systems Using Tree Automata.
  In Logical Methods in Computer Science, Volume 14 (2:8), pages 1-35, 2018. pdf (A preliminary version appeared at CONCUR'16.)


• S. Akshay, L. Helouet, C. Jard, P.-A. Reynier.
  Robustness of time Petri nets under guard enlargement.
  In Fundamenta Informaticae, volume 143, number 3-4, pages 207--234, 2016. (A preliminary version appeared at RP'12.)


• S. Akshay, T. Antonopoulos, J. Ouaknine, J. Worrell.
  Reachability problems for Markov chains.
  In Information Processing Letters, Elsevier, Volume 115, Number 2, Pages 155-158, 2015. pdf


• S. Akshay, P. Gastin, M. Mukund, K. Narayan Kumar.
  Checking conformance for time-constrained scenario-based specifications.
  In Theoretical Computer Science, Elsevier, 2015. online version (Preliminary versions of some results appeared in CONCUR'07 and FSTTCS'10.)


• M. Agrawal, S. Akshay, B. Genest, P. S. Thiagarajan.
  Approximate verification of the symbolic dynamics of Markov chains.
  In Journal of the ACM, Volume 62, Number 1, Article 2, 2015. pdf (A preliminary version appeared at LICS'12.)


• S. Akshay, B. Bollig, P. Gastin, M. Mukund, K. Narayan Kumar.
  Distributed timed automata with independently evolving clocks.
  In Fundamenta Informaticae, IOS Press, Volume 130, Number 4, Pages 377-407, 2014. pdf (A preliminary version appeared at CONCUR'08.)


• S. Akshay, B. Bollig, P. Gastin.
  Event-clock Message Passing Automata: A logical characterization and an emptiness checking algorithm.
  In Formal Methods in Systems Design, Springer, Volume 42, Number 3, Pages 262-300, 2013. (A preliminary version appeared at FSTTCS'07.)
  
  
• S. K. Palaniappan, S. Akshay, B. Liu, B. Genest, P. S. Thiagarajan.
  A hybrid factored frontier algorithm for dynamic Bayesian networks with a biopathway application.
  In IEEE/ACM Transactions on Computational Biology and Bioinformatics, IEEE Computer Society Press, Volume 9, Number 5, Pages 1352-1365, 2012. pdf (A preliminary version appeared at CMSB'11.)


• S. Akshay, B. Genest, L. Helouet. S. Yang.
  Regular sets of representatives for Time-Constrained MSC Graphs.
  In Information Processing Letters, Elsevier, Volume 112, Issues 14-15, 15 August Pages 592-598, 2012. pdf

Conference Papers

• S. Akshay, P. Gastin, R. Govind, B. Srivathsan.
  MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm.
  In the proceedings of the the 35th International Conference on Concurrency Theory, {CONCUR} 2024, September 9-13, 2024, Canada, LIPIcs Vol. 311, pp. 5:1--5:19. pdf (arXiv version)


• S. Akshay, T. Meggendorfer, P. S. Thiagarajan
  Causally Deterministic Markov Decision Processes. S. Akshay, T. Meggendorfer and P. S. Thiagarajan.
  In proceedings of the 35th International Conference on Concurrency Theory, {CONCUR} 2024, September 9-13, 2024, Canada, LIPIcs Vol. 311, pp. 6:1--6:22. pdf


• S. Akshay, S. Chakraborty, A. K. Goharshady, R. Govind, H. J. Motwani, S. T. Varanasi.
  Practical Approximate Quantifier Elimination for Non-linear Real Arithmetic.
  In proceedings of the 26th International Symposium on Formal Methods (FM 2024), September 9-13 2024, Italy, LNCS Springer Volume 14933, pp 111--130.
• 
  
• S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic,
  Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance Properties.
  In proceedings of the 33rd International Joint Conference on Artificial Intelligence (IJCAI 2024), Main Track, August 3-9 2024, South Korea, pp 3--12. pdf (arXiv version)


• S. Akshay, S. Chakraborty, A. K. Goharshady, R. Govind, H. J. Motwani, S. T. Varanasi.
  Automated Synthesis of Decision Lists for Polynomial Specifications over Integers.
  In proceedings of the 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2024), pg 484-502, May 2024. pdf


• S. Akshay, E. Basa, D. Fried, S. Chakraborty.
  On Dependent Variables in Reactive Synthesis.
  In proceedings, Part I, of the 30th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2024), April 2024, Luxembourg. LNCS Springer Volume 14570, pp 123--143. pdf
• 
  
• K. S. Meel ® S. Chakraborty ® S. Akshay.
  Auditable Algorithms for Approximate Model Counting.
  In proceedings of the 38th Annual AAAI Conference on Artificial Intelligence (AAAI 2024), Volume 38(9), pg 10654-10661, February 2024. pdf


• M. Afzal, A. Gupta, S. Akshay.
  Using counterexamples to improve Robustness Verification in Neural Networks.
  In proceedings, Part I, of the 21st International Symposium on Automated Technology for Verification and Analysis (ATVA 2023), October 24-27 2023, Singapore, LNCS Springer Volume 14215, pp 422–443. pdf


• H. Torfah, A. Joshi, S. Shah, S. Akshay, S. Chakraborty, S. A. Seshia.
  Learning Monitor Ensembles for Operational Design Domains.
  In proceedings on the 22nd International Conference on Runtime Verification (RV 2023), October 3-6 2023, Greece. LNCS Springer Volume 14245, pp 271-290. pdf


• S. Akshay, P. Gastin, R. Govind, A. Joshi, B. Srivathsan,
  A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation.
  In proceedings, Part III, of the 35th International Conference on Computer Aided Verification (CAV 2023), July 17-22, 2023, Paris, France, LNCS Springer Volume 13966, pp 86-112. pdf (arXiv version)


• S. Akshay, S. Chakraborty, S. Jain
  Counter-Example Guided Knowledge Compilation for Boolean Functional Synthesis.
  In proceedings, Part I, of the 35th International Conference on Computer Aided Verification (CAV 2023), July 17-22, 2023, Paris, France, LNCS Springer Volume 13964, pp 367-389.


• S. Akshay, K. Chatterjee, T. Meggendorfer, D. Zikelic,
  MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives.
  In proceedings, Part I, of the 35th International Conference on Computer Aided Verification (CAV 2023), July 17-22, 2023, Paris, France, LNCS Springer Volume 13964, pp 266-288. Online | pdf (arXiv version)


• S. Akshay, P. Gastin, R. Govind, B. Srivathsan,
  Simulations for event-clock automata.
  In the proceedings of the International Conference on Concurrency Theory (CONCUR 2022), September 2022, Warsaw, Poland. LIPIcs Vol. 243, pp. 13:1-13:18. pdf (arXiv version)


• S. Akshay, S. Chakraborty, D. Pal,
  On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices.
  In the proceedings of the 11th International Joint Conference on Automated Reasoning (IJCAR 2022), Part of FLOC 2022, Israel. LNCS Springer Volume 13385, pp 671-690.


• S. Chakraborty and S. Akshay
  On synthesizing Skolem functions for First Order Logic.
  In proceedings of the 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022), Aug 22-26 2022, Vienna, Austria, LIPIcs Vol. 241, pp 30:1-30:15. Open access online

S. Akshay, H. Bazille, B. Genest, M. Vahanwala.
On robustness for the Skolem and positivity problems.
In proceedings of the 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022), March 15-18, 2022, Marseille, France, pp 5:1--5:20. Open Access Online

S. Akshay, P. Gastin, K. R. Prakash.
Fast zone-based algorithms for reachability in pushdown timed automata.
In proceedings, Part 1, of the 33rd International Conference on Computer Aided Verification (CAV 2021), Virtual Event, July 20-23, 2021. LNCS Springer Volume 12759, pp 619-642. Online | pdf (arXiv version)

H. Torfah, S. Shah, S. Chakraborty, S. Akshay, S. A. Seshia.
Synthesizing Pareto-Optimal Interpretations for Black-Box Models.
In proceedings of the 21st International Conference on Formal Methods in Computer-Aided Design (FMCAD 2021), pages 152-162, Oct 2021. pdf (arXiv version)

P. Shah, A. Bansal, S. Akshay, S. Chakraborty.
A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis.
In proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021), July 2021, pp. 1--13. pdf (arXiv version)

S. Akshay, B. Genest, L. Helouet, S. Krishna, S. Roychowdhary.
Resilience in Timed Systems
In Proceedings of the 41st International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021), December, 2021, Online. Leibniz International Proceedings in Informatics, LiPIcs, Dagstuhl, 33:1-33:22, 2021. Open Access online

K. S. Meel ® S. Akshay.
Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice.
In proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), Saarbrucken, Germany, 2020, pp. 728-741. pdf

S. Akshay, P. Gastin, S. Krishna, S. Roychowdhary.
Revisiting Underapproximate Reachability for Multipushdown Systems.
In proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, pp. 387-404. pdf (arXiv version)

S. Akshay, L. Helouet, B. Genest, S. Mital.
Timed Negotiations.
In proceedings of the 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020), held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, pp. 37-56. pdf

S. Akshay, N. Balaji, A. Murhekar, R. Varma, N. Vyas.
Near-optimal complexity bounds for fragments of the Skolem Problem.
In proceedings of the 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020), Montpellier, March 10 - 13, 2020, 37:1-37:18. Open Access Online

S. Akshay, H. Bazille, E. Fabre, B. Genest,
Classification Among Hidden Markov Models.
In Proceedings of the 39th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019), December, 2019, Mumbai, India. Leibniz International Proceedings in Informatics, LiPIcs, Dagstuhl, 29:1-29:14, 2019. Open Access online

S. Akshay, J. Arora, S. Chakraborty, S. Krishna, D. Raghunathan, S. Shah.
Knowledge Compilation for Boolean Functional Synthesis.
In the proceedings of the 19th conference on Formal Methods in Computer-Aided Design (FMCAD 2019), Oct 22-25 2019, California, USA. pdf (arXiv version)

S. Akshay, S. Basu, S. Chakraborty, R. Sundararajan, P. Venkatraman.
Functional significance checking in noisy gene regulatory networks
In the proceedings of the 25th International Conference on Principles and Practice of Constraint Programming (CP 2019), Sept 30 - Oct 4 2019, Stamford, CT, U.S. pdf

S. Akshay, P. Gastin, S. Krishna, V. Juge.
Timed Systems through the Lens of Logic.
In the proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019), June 24-27 2019, Vancouver, Canada. pdf (arXiv version)

Utkarsh Gupta, Preey Shah, S. Akshay, Piotrek Hofman.
Continuous Reachability for Unordered Data Petri Nets is in PTime
In the proceedings of the 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2019), Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, LNCS Springer Volume 11425, pp.260-276. pdf (arXiv version)

S. Akshay, B. Genest, N. Vyas.
Distribution-based objectives for Markov Decision Processes
In the proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), Held as Part of Federated Logic Conference, Floc 2018, July 9-12 2018, Oxford, UK. ACM pp. 36-45. pdf (arXiv version)

S. Akshay, S. Chakraborty, S. Goel , S. Kulal, S. Shah.
What's hard about boolean functional synthesis
In the proceedings, Part 1, of the 30th International Conference on Computer Aided Verification (CAV 2018), Held as Part of Federated Logic Conference, FloC 2018, July 14-17 2018, Oxford, UK. LNCS Springer Volume 10981, pp 251-269. pdf (arXiv version)

S. Akshay, N. Balaji, N. Vyas.
Complexity of restricted variants of Skolem and related problems.
In the proceedings of 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017) August 21-25, 2017, Aalborg, Denmark. LIPIcs Vol. 83, pp. 78:1-78:14.

S. Akshay, S. Chakraborty, A. Das, V. Jagannath, S. Sandeep.
On Petri Nets with Hierarchical Special Arcs.
In the proceedings of the International Conference on Concurrency Theory (CONCUR 2017), September 2017, Berlin, Germany. LIPIcs Vol. 85, pp. 40:1-40:17. pdf (arXiv version)

S. Akshay, P. Gastin, S. Krishna, I. Sarkar.
Towards an Efficient Tree Automata based technique for Timed Systems.
In the proceedings of the International Conference on Concurrency Theory (CONCUR 2017), September 2017, Berlin, Germany. LIPIcs 85, pp. 39:1-39:15 pdf (arXiv version)

S. Akshay, S. Chakraborty, A. John, S. Shah.
Towards Parallel Boolean Functional Synthesis
In the proceedings of Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, {TACAS} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, LNCS vol 10205, pp.337-353. pdf (arXiv version)

S. Akshay, L. Helouet, R. Phawade.
Combining Free Choice and Time in Petri Nets
In the proceedings of the 23rd International Symposium on Temporal Representation and Reasoning, {TIME} 2016, Denmark, October 17-19, 2016, {IEEE} Computer Society, pp. 120-129.

S. Akshay, P. Gastin, S. Krishna.
Analyzing Timed Systems Using Tree Automata.
In the proceedings of the 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Quebec City, Canada. LIPIcs Vol. 59. pp. 27:1 - 27:14 pdf (arxiv version)

S. Akshay, P. Bouyer, S. Krishna, L. Manasa, A. Trivedi.
Stochastic Timed Games Revisited.
In the proceedings of the 41st International Symposium on Mathematical Foundations of Computer Science, MFCS 2016, August 22-26, 2016 - Krakow, Poland. LIPIcs Vol. 58. pp. 8:1-8:14.

S. Akshay, B. Genest, L. Helouet.
Decidable Classes of Unbounded Petri Nets with Time and Urgency.
In proceedings of the 37th International Conference on Application and Theory of Petri Nets (PETRI NETS), June 2016, Torun, Poland. Springer LNCS 9698, pp. 301 - 322. pdf (report)

S. Akshay, B. Genest, B. Karelovic, N. Vyas.
On Regularity of unary Probabilistic Automata
In proceedings of the 33rd Symposium on Theoretical Aspects of Computer Science (STACS), Feb 2016, Orleans, France. LIPIcs Vol. 47, pp. 8:1 - 8:14. pdf (report)

A. John, S. Shah, S. Chakraborty, A. Trivedi, S. Akshay.
Skolem Functions for Factored Formulas
In proceedings of the 15th Conference on Formal Methods in Computer-Aided Design (FMCAD), Sep 2015, Austin, Texas, USA. pp. 73-80. pdf (full version)

S. Akshay, L. Helouet, M. Mukund.
Sessions with an unbounded number of agents.
In proceedings of the 14th International Conference on Application of Concurrency to System Design (ACSD), 2014, Tunis La Marsa, Tunisia. IEEE Computer Society, pp. 166-174.

S. Akshay, I. Dinca, B. Genest, A. Stefanescu.
Implementing realistic asynchronous automata.
In proceedings of the 33rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2013, Guwahati, India. Leibniz International Proceedings in Informatics, LiPIcs, Dagstuhl, vol. 24, pp. 213-224. pdf | report

S. Akshay, N. Bertrand, S. Haddad, L. Helouet.
The steady-state control problem for Markov decision processes.
In proceedings of the 10th International Conference on Quantitative Evaluation of Systems (QEST), 2013, Buenos Aires, Argentina. Springer LNCS, pp. 290-304.

M. Agrawal, S. Akshay, B. Genest, P. S. Thiagarajan.
Approximate verification of the symbolic dynamics of Markov chains.
In proceedings of the 27th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS), 2012, Dubrovnik, Croatia. IEEE Computer Society Press, pp. 55-64. pdf

---

S. Akshay, L. Helouet, C. Jard, D. Lime, O. H. Roux.
Robustness of time Petri nets under architectural constraints.
In proceedings of the 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 2012, London, UK. Springer LNCS 7595, pp. 11-26.

S. Akshay, L. Helouet, C. Jard, P.-A. Reynier.
Robustness of time Petri nets under guard enlargement.
In proceedings of the 6th International Workshop on Reachability Problems (RP), 2012, Bordeaux, France. Springer LNCS 7550, pp. 92-106.

S. Akshay, B. Genest, L. Helouet, S. Yang.
Symbolically bounding the drift in time-constrained MSC graphs.
In proceedings of the 9th International Colloquium on Theoretical Aspects of Computing (ICTAC), 2012, Bangalore, India. Springer LNCS 7521, pp. 1-15. pdf (Technical report)

S. K. Palaniappan, S. Akshay, B. Genest, P. S. Thiagarajan.
A hybrid factored frontier algorithm for dynamic Bayesian network models of biopathways.
In proceedings of the 9th International Conference on Computational Methods in Systems Biology (CMSB), 2011, Paris, France. ACM 2011, pp.35-44. pdf

---

S. Akshay, P. Gastin, M. Mukund, K. Narayan Kumar.
Model checking time-constrained scenario-based specifications.
In proceedings of the 30th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2010, Chennai, India. Leibniz International Proceedings in Informatics, LiPIcs, Dagstuhl, vol. 8, pp. 204-215. pdf | Report

---

S. Akshay, B. Bollig, P. Gastin, M. Mukund, K. Narayan Kumar.
Distributed timed automata with independently evolving clocks.
In proceedings of the 19th International Conference on Concurrency Theory (CONCUR), 2008, Toronto, Canada. Springer LNCS 5201, pp. 82-97. pdf

---

S. Akshay, M. Mukund, K. Narayan Kumar.
Checking coverage for infinite collections of timed scenarios.
In proceedings of the 18th International Conference on Concurrency Theory (CONCUR), 2007, Lisbon, Portugal. Springer LNCS 4703, pp. 181-196. pdf

---

S. Akshay, B. Bollig, P. Gastin,
Automata and logics for timed message sequence charts.
In proceedings of the 27th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2007, New Delhi, India. Springer LNCS 4855, pp. 290-302. pdf

---

Thesis

• S. Akshay
  Specification and verification of timed and communicating systems
  Doctoral Thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2010.