I am an assistant professor in the Department of Computer Science at the University of Colorado Boulder. I am affilited with the Programming Languages and Verification Group and the Theory Group at the University of Colorado Boulder.
▲

Ashutosh Trivedi
Email: ashutosh.trivedi @ colorado.edu “ My research focuses on applying rigorous mathematical reasoning techniques to design and analyze safe and secure cyberphysical systems (CPS) with guaranteed performance. I investigate foundational issues (decidability and complexity) related to modeling and analysis of CPS as well as practically focused tools that can be used by practitioners to analyze large systems at scale. ” 
News.
 I am teaching CSCI 7000 (Automata for Verification, Synthesis, and Learning) this semester (Fall 2019).
 I gave a tutorial on Reinforcement Learning and Formal Requirements at NSV@CAV 2019 and at SNR 2019@CPSWeek.
 Our paper Quantitative Mitigation of Timing Side Channels is accepted for CAV 2019.
 Our paper On Timed ScopeBounded ContextSensitive Languages is accepted for DLT 2019.
 Our paper Expected ReachabilityPrice Games is accepted for FORMATS 2019.
 Our paper OmegaRegular Objectives in ModelFree Reinforcement Learning is accepted for TACAS 2019.
 Our paper TypeDirected Bounding of Collections in Reactive Programs is accepted for VMCAI 2019.
Students.
 Devendra Bhave (PhD, coadvised with Krishna S., since 2013)
 Juraj Culak (PhD, since 2017)
 Taylor Dohmen (PhD, since 2018
 John Komp (PhD, since 2018)
 Tianhan Lu (PhD, coadvised with Evan Chang, since 2015)
 John Paul Martin Jr. (PhD, since 2018)
 Saeid TizpazNiari (PhD, coadvised with Pavol Cerny, since 2015)
Current Research.
Keywords: Formal Methods, Game Theory, LearningEnabled CyberPhysical Systems, Automata Theory and LogicI am actively working on the following research projects:
 Formal Requirements in Reinforcement Learning.
Reinforcement learning is an approach to controller synthesis where
agents rely on reward signals to choose actions in order to satisfy
the requirements implicit in reward signals. Oftentimes nonexperts
have to come up with the requirements and their translation to rewards
under significant time pressure, even though manual translation is
time consuming and error prone. For safetycritical applications of
reinforcement learning a rigorous design methodology is needed and, in
particular, a principled approach to requirement specification and to
the translation of objectives into the form required by reinforcement
learning algorithms.
Formal logic provides a foundation for the rigorous and unambiguous requirement
specification of learning objectives. However, reinforcement
learning algorithms require requirements to be expressed as
scalar reward signals. We discuss a recent technique, called
limitreachability, that bridges this gap by faithfully
translating logicbased requirements into the scalar reward
form needed in modelfree reinforcement learning. This
technique enables the synthesis of controllers that maximize
the probability to satisfy given logical requirements using
offtheshelf, modelfree reinforcement learning algorithms.
Related publications : [1], [2].
 Space/Time Analaysis for Cybersecurity.
The goal of this DARPAsponsored project is to develop new program analysis
techniques to allow analysts to discover Java applications with exploitable
security vulnerabilities such as availability
(denialofservice) and confidentiality (sidechannels) vulnerabilities due to space and time usage
of the programs.
In identifying availability and confidentiality
problems, our focus is to minimize both false positives and false negatives.
In addition, it is often desirable that every identified vulnerability is
presented with sufficient evidence towards an exploit of
the vulnerability. In the case of availability problems, such evidence should
be in the form of an input that triggers excessive resource usage, while for
confidentiality problems, such evidence may a be pair of inputs that result in
differential resource usage.
I am particularly interested in combining static analysis techniques with
runtime analysis to pinpoint program vulnerabilities.
In one of our recent publications [1], we present a new runtime analysis
technique for debugging Java bytecode to uncover potential causes for
sidechannels in time.
Related publications: [1], [2].
 Theory of Stochastic Hybrid Structures.
The problem of mathematically modeling CPS is fundamental to analyzing their
safety and security properties. However, CPS integrate many different
aspects including timecriticality, nondeterminism,
presence of multiple
rational agents, rich continuous dynamics, stochastic behavior, and
higherlevel programming constructs such as heaps and recursion. This poses
a fundamental challenge: a rich combination of these features yields models
that are too complex to reason about. In this project I study several useful
restrictions to these models to characterize the
decidability/undecidability frontier as well as exact computational
complexity of various verification and synthesis related questions.
Parts of this projects were sponsored by a LiverpoolIndia fellowship,
an IIT Bombay seedgrant, and the Indofrench project AVeRTS.
Related publications : [1], [2], [3], [4], and [5].
 Theory of Streaming String Transducers.
The beautiful theory of regular languages is the cornerstone of theoretical
computer science and formal language theory. The perfect harmony among the
languages of finite words definable using
abstract machines (deterministic
finite automata), algebra (regular expressions and finite monoids), and logic (monadic
secondorder logic) did set the stage for the generalizations of the
theory to the theory of regular languages of infinite words,
trees, and partial orders.
Alur and Cerny have proposed a model of transducers, called
streaming string transducers, that for regular transformations seems
to be as appealing model as deterministic finite automata for regular languages.
The goal of this project is to study theoretical properties of streaming string
transducers and their applications in verification of CPS.
This project has been supported by the NSF Expeditions in Computing award
1138996 and an IITB seedgrant.
Related publications : [1], [2], [3], and [4].
Selected Publications.

Discriminating Traces with Time
Saeid TizpazNiari, Pavol Cerny, BorYuh Evan Chang, Sriram Sankaranarayanan, and Ashutosh Trivedi
In Proc. of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017).

MeanPayoff Games on Timed Automata .
Shibashis Guha, Marcin Jurdzinski, Krishna S. and Ashutosh Trivedi.
In Proc. of Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016.

Symmetric Strategy Improvment .
Sven Schewe, Ashutosh Trivedi, Thomas Varghese.
In Proc. of the 42nd International Colloquium on Automata, Languages, and Programming (ICALP 2015).

Regular Transformations of Infinite
Strings.
Rajeev Alur, Emmanuel Filiot, and Ashutosh Trivedi.
Proceedings of the 27th Annual IEEE/ACM Symposium on Logic in Computer Science, LICS 2012.

Optimal Scheduling for ConstantRate
MultiMode System.
Rajeev Alur, Ashutosh Trivedi, and Dominik Wojtczak.
Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control, HSCC 2012.
Best paper award, HSCC, CPS Week 2012.

Recursive Timed Automata.
Ashutosh Trivedi and Dominik Wojtczak.
Proceedings of 8th International Symposium on Automated Technology for Verification and Analysis, ATVA 2010.

ReachabilityTime Games on Timed Automata
[Full
version].
Marcin Jurdzinski and Ashutosh Trivedi.
Proceedings of 34th International Colloquium on Automata, Languages and Programming, ICALP 2007.