Vinayak S. Prabhu

Ph.D. University of California at Berkeley
EMail

Assistant Professor
Department of Computer Science
Colorado State University

Office: CSB 446

Research Areas

Formal Methods for Verification and Synthesis.
Formal Verification and Model Checking; Temporal logics.
Embedded and Cyber-Physical Systems (CPS).
Models of computation.
Robustness issues in CPS; Conformance checking.
Modelling and analysis of concurrent reactive systems; Testing and debugging.
Control of timed, hybrid and discrete-event systems.
Multi-agent and autonomous systems.

The goal of my research is to synthesize tools and algorithms to aid the development of reliable embedded and cyber-physical systems and devices, using techniques from formal methods (automata theory, logic), control theory, machine learning, and software analysis. My work deals with both theoretic and applied aspects, building on collaborations with researchers and industrial research labs from the US and from Europe.

Prospective Students: Funded positions available. Information

Teaching

Spring 2020: Foundations of Cyber-Physical Systems (CS 522)
Fall 2019: Automata, Logic, and Computation (CS 480A4)
Spring 2019: Foundations of Cyber-Physical Systems (CS 581A4)
Fall 2018: Introduction to Analysis of Algorithms (CS 420)
Spring 2018: Foundations of Cyber-Physical Systems (CS 581A4)

Program Committees

21st ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2018)

20th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2017)

Publications

DBLP database | Journal publications

Jyotirmoy V. Deshmukh, Xiaoqing Jin, Rupak Majumdar and Vinayak S. Prabhu, Parameter fault localization for debugging and performance optimization of control software. .Proceedings of the 9th ACM/IEEE International Conference on Cyber-Physical Systems, (ICCPS) 2018, pp. 230--231.

Jyotirmoy V. Deshmukh, Marko Horvat, Xiaoqing Jin, Rupak Majumdar and Vinayak S. Prabhu, Testing Cyber-Physical Systems through Bayesian Optimization . Transactions on Embedded Computing Systems (TECS), ESWEEK special issue for articles presented in the 2017 ACM SIGBED International Conference on Embedded Software (EMSOFT), vol 16(5s) ACM 2017, pp. 170:1--170:18.

Rayna Dimitrova, Ivan Gavran, Rupak Majumdar, Vinayak S. Prabhu and Sadegh Soudjani, The robot routing problem for collecting aggregate stochastic rewards. Proceedings of the 28th International Conference on Concurrency Theory (CONCUR), 2017, pp. 13:1--13:17.

Jyotirmoy V. Deshmukh, Rupak Majumdar and Vinayak S. Prabhu, Quantifying conformance using the Skorokhod metric. Formal Methods in System Design. Vol 50 (2-3), Springer 2017, pp. 168--206.

Samira S. Farahani, Rupak Majumdar, Vinayak S. Prabhu and Sadegh Soudjani, Shrinking horizon Model Predictive Control with chance-constrained Signal Temporal Logic specifications. Proceedings of the 2017 American Control Conference (ACC), IEEE 2017, pp. 1740-1746.

Rayna Dimitrova, Rupak Majumdar, and Vinayak S. Prabhu, Causality analysis for concurrent reactive systems. Draft.

Rupak Majumdar, and Vinayak S. Prabhu, Computing distances between reach flowpipes. Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control (HSCC), ACM 2016, pp. 267-276.

Jyotirmoy V. Deshmukh, Rupak Majumdar, and Vinayak S. Prabhu, Quantifying conformance using the Skorokhod metric. Proceedings of the 27th International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science 9207, Springer 2015, pp. 234-250 (Volume 2).

Rupak Majumdar, and Vinayak S. Prabhu, Computing the Skorokhod distance between polygonal traces. [Technical report] Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC), ACM 2015, pp. 199-208.

Krishnendu Chatterjee, and Vinayak S. Prabhu, Quantitative temporal simulation and refinement distances for timed systems. Transactions on Automatic Control, IEEE, 60(9), 2015, pp. 2291-2306.

Krishnendu Chatterjee, and Vinayak S. Prabhu, Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems. Information and Computation, Elsevier, 228 (2013), pp. 83-119.

Krishnendu Chatterjee, and Vinayak S. Prabhu, Quantitative timed simulation functions and refinement metrics for real-time systems. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC), ACM 2013, pp. 273-282.

Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu, Finite automata with time-delay blocks. Proceedings of the 10th International Conference on Embedded Software (EMSOFT), ACM 2012, pp. 43-52.

Mangal Kothari, Jose Pinto, Vinayak S. Prabhu, Pedro Ribeiro, Joao Borges de Sousa, and P.B. Sujit, Robust Mission Planning for Underwater Applications: Issues and Challenges. Proceedings of the 3rd IFAC Workshop on Navigation, Guidance and Control of Underwater Vehicles (NGCUV), IFAC 2012, pp. 223-229.

Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu, Timed parity games: Complexity and robustness. Journal of Logical Methods in Computer Science, 7(4) (2011), pp. 1-55.

Krishnendu Chatterjee, and Vinayak S. Prabhu, Synthesis of memory efficient real-time controllers for safety objectives. Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC), ACM 2011, pp. 221-230.

Andrew G. West, Adam J. Aviv, Jian Chang, Vinayak S. Prabhu, Matt Blaze, Sampath Kannan, Insup Lee, Jonathan M. Smith, and Oleg Sokolsky, QuanTM: A quantitative trust management system. Proceedings of the Second European Workshop on System Security (EuroSec), ACM 2009, pp. 28-35.

Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu, Timed parity games: Complexity and robustness. Proceedings of the Sixth International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Lecture Notes in Computer Science 5215, Springer-Verlag, 2008, pp. 124-140.

Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu, Trading infinite memory for uniform randomness in timed games. Proceedings of the 11th International Conference on Hybrid Systems: Computation and Control (HSCC), Lecture Notes in Computer Science 4981, Springer-Verlag, 2008, pp. 87-100.

Thomas Brihay, Thomas A. Henzinger, and Vinayak S. Prabhu, and Jean-Francois Raskin, Minimum-time reachability in timed games. Proceedings of the 34th International Colloquium on Automata, Languages, and Programming (ICALP), Lecture Notes in Computer Science 4596, Springer-Verlag, 2007, pp. 825-837.

Thomas A. Henzinger, and Vinayak S. Prabhu, Timed alternating-time temporal logic. Proceedings of the Fourth International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Lecture Notes in Computer Science 4202, Springer-Verlag, 2006, pp. 1-17.

Thomas A. Henzinger, Rupak Majumdar, and Vinayak S. Prabhu, Quantifying similarities between timed systems. Proceedings of the Third International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Lecture Notes in Computer Science 3829, Springer-Verlag, 2005, pp. 226-241.

Thomas A. Henzinger, Marius Minea, and Vinayak S. Prabhu, Assume-guarantee reasoning for hierarchical hybrid systems. Proceedings of the Fourth International Workshop on Hybrid Systems: Computation and Control (HSCC), Lecture Notes in Computer Science 2034, Springer-Verlag, 2001, pp. 275-290.

Software

Tool (C++) for computing the Skorokhod distance between two continuous-time traces (given as sampled time-points) based on the work in [CAV 2015], [FMSD 2017]. Available at Github