Murray Wiki - User contributions [en]

Liren Yang, 5-6 Feb 2020

2020-02-03T19:33:16Z

Tmphan: /* Schedule */

Liren Yang is a PhD student at U. Michigan who has recently defended his thesis on correct-by-construction fault-tolerant control synthesis. He will visit Caltech on 5-6 Feb. Sign up here if you would lik to meet with him (use your Caltech credentials).

=== Schedule ===

5 Feb (Wed)
* 2:00p: NCS group meeting
* 3:00p: CDS tea
* 3:30p: Chuchu
* 4:15p: Karena
* 5:00p: Informal seminar - 121 Annenberg
* 6:00p: Dinner with Richard + students (add your name here if you want to go): Apurva

6 Feb (Thu)
* 9:15a: Richard Murray, 109 Steele Lab
* 10:00a: Apurva, Pick up from Richard’s office. Meeting location: CDS Library
* 10:45a: Yuxiao
* 11:30a: Sumanth
* 12:15p: Lunch
* 1:15p: Open
* 2:00p: Tung
* 2:45p: Josefine
* 3:30p: Done for the day

=== Talk ===

Correct-by-construction fault-tolerant control of complex dynamical systems

Correct-by-construction control synthesis methods can be used to algorithmically design controllers that render dynamical systems to satisfy complex tasks specified by formal languages. However, there is a gap between such techniques and real applications, especially when the systems experience faults, such as physical component failures and extreme operating conditions. Moreover, it is conservative and computationally expensive to apply such techniques developed for pure discrete systems directly to continuous-state dynamical systems. In this talk, I will present our work tackling these challenges. First, I will briefly mention our work on guaranteed fault-detection with linear temporal logic (LTL) constraints, and a hierarchical abstraction-based fault-tolerant controller synthesis approach. Then, regarding the first issue, I will focus on how to construct abstractions for systems with complex but structured dynamics. In particular, we leverage a special system structural property called mixed monotonicity to ease abstraction computation, and to develop synthesis techniques to incorporate this property. The presented methodology will be illustrated on a fuel cell thermal-power management problem.

Group Schedule, Fall 2019

2019-10-10T22:00:01Z

Tmphan: /* Week 8: 18-22 Nov */

Group Schedule, Fall 2019

2019-10-10T21:59:52Z

Tmphan: /* Week 6: 4-8 Nov */

CS 142, Fall 2019

2019-10-08T03:05:11Z

Tmphan: /* Teaching assistants */

{| width=100%
|-
| colspan=2 align=center |
Distributed Computing__NOTOC__
|- valign=top
| width=50% |
=== Instructors ===
* Richard Murray (CMS)
* Mani Chandy (CMS)
* Lectures: MW, 9-10 am, 213 Annenberg
* Office hours: by appointment
| width=50% |
=== Teaching assistants ===
* Prithvi Akella (ME), Tung Phan (ME)
* Problem solving sessions: Fri, 9 am, 213 Annenberg
* Office hours: Mon, 5-6 pm and Tue, 5-7 pm; 243 Annenberg
* Online resources: [https://piazza.com/caltech/fall2019/cs142 Piazza]] (Q&A forum), [https://courses.caltech.edu/course/view.php?id=3539 Moodle] (HW submission)
|}
<hr>
{| width=100%
|- valign=top
| width=50% |

=== Course description ===
CS 142. Distributed Computing. 9 units (3-0-6); first term. Prerequisites: CS 24, CS 38. Fundamental concepts for the design and analysis of distributed systems and algorithms, including reasoning about distributed programs, handling the lack of global time and global state, achieving distributed consensus in the presence of faults and asynchrony, and designing fault-tolerance for distributed systems. Review of state-of-the-art distributed systems, particularly cloud computing systems. Instructor: Murray/Chandy.
| width=50% |
=== Course announcements ===
* 2 Oct 2019: HW #1 has been posted; due 9 Oct (Wed) at 2 pm
* 29 Sep 2019: Monday lecture posted + Piazza signups created (if you didn't get added, sign up using the link above)
* 21 Sep 2019: web site under construction; use with care
|}

== Course syllabus and schedule ==

=== Lecture Schedule ===

{| class="mw-collapsible wikitable" border=1 cellpadding=5
|-
| '''Date'''
| '''Topic'''
| '''Reading/Homework'''
|- valign=top
| W1 (30 Sep)
|
* Motivation, course admin
* Logic and computation
* Propositional logic, guarded command programs
|
* Sivilotti, Chapters 1 and 2
* {{CS 142 pdf|fa19|hw1-fa19.pdf|HW #1}} due on 9 Oct
* {{CS 142 pdf|fa19|L1-1_intro-30Sep2019.pdf|Mon lecture slides}}
* {{CS 142 pdf|fa19|L1-2_computation-02Oct2019.pdf|Wed lecture slides}}
* {{CS 142 pdf|fa19|L1-3_predicates-04Oct2019.pdf| Fri recitation slides}}
|- valign=top
| W2 (7 Oct)
| rowspan=2 |
* Specifications and proofs
* Program properties (invariants, safety, liveness)
* Simple examples and proofs of correctness
|
* Sivilotti, Chapters 3 and 4
* HW #2 due on 16 Oct
* {{CS 142 pdf|fa19|L2-1_reasoning-07Oct2019.pdf|Mon lecture slides}}

|- valign=top
| W3 (14 Oct)
|
* HW #3 due on 23 Oct

|- valign=top
| W4 (21 Oct)
|
* Time, clocks
* Gossip algorithms
|
* Sivilotti, Chapter 5 and 6
* HW #4 due on 30 Oct

|- valign=top
| W5 (28 Oct)
|
* Mutual exclusion
||
* Midterm office hours: TBD

* Sivilotti, Chapter 7
* Midterm: out 30 Oct, due 5 Nov

|- valign=top
| W6 (4 Nov) KMC
|
* Specifications, refinement, dining philosophers
|
* Sivilotti, Chapter 8
* Chandy and Misra, Ch 7 & 12|
* HW #5 due on 13 Nov

|- valign=top
| W7 (11 Nov)
|
* Snapshots
|
* Sivilotti, Chapter 9
* HW #6 due on 20 Nov

|- valign=top
| W8 (18 Nov) KMC
| rowspan=2 |
* Byzantine agreement and the PAXOS algorithm
| rowspan=2 |
* Sivilotti, Ch 12
* Paxos Made Simple (Lamport, 2001)
* HW #7 due on 27 Nov

* No class on 27 Nov (Wed)
|- valign=top
| W9 (25 Nov)
|- valign=top
| W10 (2 Dec)
|
* Distributed consensus and distributed ledger
|
* Modified office hours: TBD


* Bitcoin: A Peer-to-Peer Electronic Cash System
* Bitcoin and Cryptocurrency Technologies, Narayanan et al, 2017. Chapter 2
* HW #8 due on 3 Dec (Sun)

* Final: out 6 Dec, due 13 Dec @ 2 pm
|}

=== Grading ===
The final grade will be based on homework sets, a midterm exam, and a final exam:
* Homework (50%): Homework sets will be handed out weekly and due on Wednesdays by 2 pm (submitted via Moodle). Each student is allowed up to two extensions of no more than 2 days each over the course of the term. Homework turned in after Friday at 2 pm or after the two extensions are exhausted will not be accepted without a note from the health center or the Dean.
* Midterm exam (20%): A midterm exam will be handed out at the beginning of midterms period (25 Oct) and due at the end of the midterm examination period (1 Nov). The midterm exam will be open book (textbook and course notes OK: access to the Internet is not allowed).
* Final exam (30%): The final exam will be handed out on the last day of class (1 Dec) and due at the end of finals week. The final exam will be open book (textbook and course notes OK: access to the Internet is not allowed).

=== Collaboration Policy ===
* Collaboration on homework assignments is encouraged. You may consult outside reference materials, other students, the TA, or the instructor, but you cannot consult homework solutions from prior years and you must cite any use of material from outside references. All solutions that are handed in should be written up individually and should reflect your own understanding of the subject matter at the time of writing.
* No collaboration is allowed on the midterm or final exams.

=== Course Text and References ===
The primary course text is
* P. Sivilotti, {{CS 142 pdf|fa19|sivilotti-distributed_systems.pdf|Introduction to Distributed Systems}}, Course notes, 2007.
The following additional references may also be useful:
* K.M. Chandy and J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, 1988

[[Category:Courses]]

Kristin Rozier, May 2019

2019-05-13T18:15:23Z

Tmphan:

Kristin Rozier will visit Caltech on 17 May (Fri). Kristin is an Assistant Professor at Iowa State University, in the Aerospace Engineering and Computer Science Departments. Previous to that, she spent three semesters at the University of Cincinnati (2015-2016) and 14 years as a Research Scientist at NASA, holding civil service positions at NASA Ames Research Center (2008-2014) and NASA Langley Research Center (2001-2008).

=== Schedule ===

* 10 am: Open (if needed)
* 10:45 am: Seminar setup
* 11:00 am: Seminar
* 12:00 pm: Lunch with Richard
* 1:15 pm: Tung Phan (Steele library)
* 2:00 pm: Open
* 2:45 pm: Open
* 3:30 pm: Open (if needed)
* 4:15 pm: Open (if needed)
* 5:00 pm: Done for the day

=== Seminar abstract ===

From Unmanned Aerial Systems to Robonaut2: On-board Runtime Reasoning in Air and Space

Kristin Rozier
Iowa State University

Runtime Verification (RV) has become critical to the deployment of a wide range of systems, including aircraft, spacecraft, satellites, rovers, and robots. The most useful, important, and safety-critical jobs will require these systems to operate both intelligently and autonomously, with the ability to sense and respond to both nominal and off-nominal conditions. It is essential that we enable reasoning sufficient to react to challenging environments and detect critical failures on-board, in real time, to enable mitigation triggering. We are challenged by the constraints of real-life embedded operation that limit the system instrumentation, space, timing, power, weight, cost, and other operating conditions of on-board, runtime verification. While the research area of RV is vast, there is a dearth of RV tools that can operate within these constraints, and without violating, e.g., FAA rules for flight certification.

The Realizable, Responsive, Unobtrusive Unit (R2U2) analyzes specifications that combine temporal logics with probabilistic reasoning to provide formal assurances during runtime, enabling self-assessment of critical systems. This presentation overviews the achievements of the three-year NASA Early Career Faculty proposal, "Multi-Platform, Multi-Architecture Runtime Verification of Autonomous Space Systems." We discuss the unique design of R2U2 and demo R2U2 on-board Robonaut2, disambiguation emergent faults in the knee joint. We highlight on-going work in predictive and adaptable runtime verification, including adaptations for other platforms, and seek future collaborations with JPL missions.

Kristin Rozier, May 2019

2019-05-13T18:14:49Z

Tmphan: /* Schedule */

Kristin Rozier will visit Caltech on 17 May (Fri). Kristin is an Assistant Professor at Iowa State University, in the Aerospace Engineering and Computer Science Departments. Previous to that, she spent three semesters at the University of Cincinnati (2015-2016) and 14 years as a Research Scientist at NASA, holding civil service positions at NASA Ames Research Center (2008-2014) and NASA Langley Research Center (2001-2008).

=== Schedule ===

* 10 am: Open (if needed)
* 10:45 am: Seminar setup
* 11:00 am: Seminar
* 12:00 pm: Lunch with Richard
* 1:15 pm: Tung (Steele library)
* 2:00 pm: Open
* 2:45 pm: Open
* 3:30 pm: Open (if needed)
* 4:15 pm: Open (if needed)
* 5:00 pm: Done for the day

=== Seminar abstract ===

From Unmanned Aerial Systems to Robonaut2: On-board Runtime Reasoning in Air and Space

Kristin Rozier
Iowa State University

Runtime Verification (RV) has become critical to the deployment of a wide range of systems, including aircraft, spacecraft, satellites, rovers, and robots. The most useful, important, and safety-critical jobs will require these systems to operate both intelligently and autonomously, with the ability to sense and respond to both nominal and off-nominal conditions. It is essential that we enable reasoning sufficient to react to challenging environments and detect critical failures on-board, in real time, to enable mitigation triggering. We are challenged by the constraints of real-life embedded operation that limit the system instrumentation, space, timing, power, weight, cost, and other operating conditions of on-board, runtime verification. While the research area of RV is vast, there is a dearth of RV tools that can operate within these constraints, and without violating, e.g., FAA rules for flight certification.

The Realizable, Responsive, Unobtrusive Unit (R2U2) analyzes specifications that combine temporal logics with probabilistic reasoning to provide formal assurances during runtime, enabling self-assessment of critical systems. This presentation overviews the achievements of the three-year NASA Early Career Faculty proposal, "Multi-Platform, Multi-Architecture Runtime Verification of Autonomous Space Systems." We discuss the unique design of R2U2 and demo R2U2 on-board Robonaut2, disambiguation emergent faults in the knee joint. We highlight on-going work in predictive and adaptable runtime verification, including adaptations for other platforms, and seek future collaborations with JPL missions.

Elahe Aghapour, Feb 2019

2019-02-19T21:09:03Z

Tmphan: /* 19 Feb 2019 (Tue) */

Elahe Aghapour is a Ph.D. student at University of California, Riverside, working with Prof. Jay A. Farrell. Her work is focused was on autonomous vehicle control, divided in three sub-projects, a) Risk-averse performance specified state estimation which is an optimization based approach to select a subset of good measurements when measurements may be affected by outliers, b) system identification and data driven method for human action prediction using behavioral approach, and c) mixed sample rate nonlinear smoothing.

=== 19 Feb 2019 (Tue) ===

* ~8:45 am: arrival
* 9 am: seminar, 115 Gates-Thomas
* 10 am: Tung and Karena?
* 11a: Aaron, Gates-Thomas
* 11:30: Richard, 107 Steele
* 12p: lunch with Yuxiao and Reza (meet at Richard's office)
* 1:15p: Tung (115 Gates Thomas)
* 2:00p: Richard C. (205 Gates Thomas)
* 2:45p: Yuxiao and Reza
* 3:30p: AmberLab (B121 in Gates-Thomas)
* 4p: final meeting with Richard
* 4:30p: done for the day

Ather Gattami, Feb 2019

2019-02-17T21:06:46Z

Tmphan:

Ather Gattami will visit Caltech on 19-20 Feb. Ather is a senior AI expert at RISE (Research Institutes of Sweden) AI. His research interests are within the mathematical foundations of Machine Learning in general and Deep Learning in particular, Reinforcement Learning, learning in dynamical systems and games, and low rank matrix approximation and completion problems, with applications to recommender systems, anomaly detection, predictive maintenance, and Natural Language.

=== Schedule ===

Tuesday, 19 Feb 2019:
* 12 pm: Lunch with Richard (meet at 107 Steele)
* 1:30 pm: open
* 2:15 pm: open
* 3:00 pm: open
* 3:45 pm: open
* 4:30 pm: open
* 5:15 pm: done for the day

Wednesday, 20 Feb 2019:
* 11 am: Seminar (abstract below)
* 12 pm: Lunch (TBD)
* 1:30 pm: Tung (Steele library)
* 2:15 pm: open
* 3:00 pm: Richard C.
* 3:45 pm: open
* 4:30 pm: open
* 5:15 pm: done for the day

=== Talk info ===

Reinforcement Learning for Constrained and Multi-Objective Markov Decision Processes 
Ather Gattami, PhD 
Wednesday, February 20, 11am 
Annenberg 243 

We consider the problem of optimization and learning for constrained and multi-objective Markov decision processes, for both discounted rewards and expected average rewards. We formulate the problems as zero-sum games where one player (the agent) solves a Markov decision problem and its opponent solves a bandit optimization problem, which we here call Markov-Bandit games. We extend $Q$-learning to solve Markov-Bandit games and show that our new $Q$-learning algorithms converge to the optimal solutions of the zero-sum Markov-Bandit games, and hence converge to the optimal solutions of the constrained and multi-objective Markov decision problems. We provide a numerical example where we calculate the optimal policies and show by simulations that the algorithm converges to the calculated optimal policies. To the best of our knowledge, this is the first time learning algorithms guarantee convergence to optimal stationary policies for the constrained MDP problem with discounted and expected average rewards, respectively.

Ather Gattami, Feb 2019

2019-02-16T20:09:11Z

Tmphan:

Ather Gattami will visit Caltech on 19-20 Feb. Ather is a senior AI expert at RISE (Research Institutes of Sweden) AI. His research interests are within the mathematical foundations of Machine Learning in general and Deep Learning in particular, Reinforcement Learning, learning in dynamical systems and games, and low rank matrix approximation and completion problems, with applications to recommender systems, anomaly detection, predictive maintenance, and Natural Language.

=== Schedule ===

Tuesday, 19 Feb 2019:
* 12 pm: Lunch with Richard (meet at 107 Steele)
* 1:30 pm: open
* 2:15 pm: open
* 3:00 pm: open
* 3:45 pm: open
* 4:30 pm: open
* 5:15 pm: done for the day

Wednesday, 20 Feb 2019:
* 11 am: Seminar (abstract below)
* 12 pm: Lunch (TBD)
* 1:30 pm: Tung
* 2:15 pm: open
* 3:00 pm: open
* 3:45 pm: open
* 4:30 pm: open
* 5:15 pm: done for the day

=== Talk info ===

Reinforcement Learning for Constrained and Multi-Objective Markov Decision Processes 
Ather Gattami, PhD 
Wednesday, February 20, 11am 
Annenberg 243 

We consider the problem of optimization and learning for constrained and multi-objective Markov decision processes, for both discounted rewards and expected average rewards. We formulate the problems as zero-sum games where one player (the agent) solves a Markov decision problem and its opponent solves a bandit optimization problem, which we here call Markov-Bandit games. We extend $Q$-learning to solve Markov-Bandit games and show that our new $Q$-learning algorithms converge to the optimal solutions of the zero-sum Markov-Bandit games, and hence converge to the optimal solutions of the constrained and multi-objective Markov decision problems. We provide a numerical example where we calculate the optimal policies and show by simulations that the algorithm converges to the calculated optimal policies. To the best of our knowledge, this is the first time learning algorithms guarantee convergence to optimal stationary policies for the constrained MDP problem with discounted and expected average rewards, respectively.

Daniel Fremont, Sep 2018

2018-09-17T17:11:11Z

Tmphan: /* Agenda */

Daniel Fremont, a PhD student at UC Berkeley working with Sanjit Seshia, will visit Caltech on 21 Sep. Sign of for a time to meet with him below.

=== Agenda ===
* ~10:30-10:45 am: arrive at Caltech; meet in Jin Ge's office ()
* 11 am: seminar in 121 ANB
* 12 pm: Lunch with Jin, X, Y, Z (sign up if you want to join)
* 1:30 pm: Jin, Ann 337
* 2:15 pm: Tung, Steele library
* 3:00 pm: Open (replace with your name and location)
* 3:45 pm: Open (replace with your name and location)
* 4:30 pm: Open, if needed (replace with your name and location)
* 5:15 pm: done for the day

=== Seminar ===

Algorithmic Improvisation 
Daniel Fremont, UC Berkeley 

21 Sep 2018, 11 am 
121 Annenberg

Algorithmic Improvisation is a framework for automatically synthesizing systems with random but controllable behavior. It can be used in a wide variety of applications where randomness can provide variety, robustness, or unpredictability but safety guarantees or other properties must be ensured. These include software fuzz testing, robotic surveillance, machine music improvisation, randomized control of systems mimicking human behavior, and generation of synthetic data sets to train and test machine learning algorithms. In this talk, I will discuss both the theory of algorithmic improvisation and its practical applications. I will define the underlying formal language-theoretic problem, “control improvisation”, analyze its complexity and give efficient algorithms to solve it. I will describe in detail two applications: planning randomized patrol routes for surveillance robots, and generating random scenes of traffic to improve the reliability of neural networks used for autonomous driving. The latter application involves the design of a domain-specific probabilistic programming language to specify traffic and other scenarios.

Daniel Fremont is a PhD student in the Group in Logic and the Methodology of Science at UC Berkeley, working with Sanjit Seshia. He received a B.S. degree in Mathematics and Physics from MIT in 2013. His research is generally in the area of formal methods, focusing on the problems of counting and uniform generation of solutions to Boolean formulas. This includes developing practical algorithms to solve these problems, as well as finding new applications to the construction, verification, and testing of software, hardware, and cyber-physical systems.

Ben Richards, 20 Apr 2018

2018-04-17T15:35:58Z

Tmphan:

Ben Richards will visit Caltech on 20 Apr (Fri). Ben is an engineer for General Motors' North Hollywood Advanced Design Center who is interested in learning more about Caltech and our work on the VeHiCaL project.

Schedule:

* 2:00: Richard, 109 Steele Lab
* 2:45: Jin
* 3:30: Sumanth
* 4:15: Tung
* 5:00: Karena

Ben Richards, 20 Apr 2018

2018-04-17T05:25:11Z

Tmphan:

SURF discussions, Jan 2018

2018-01-23T01:43:27Z

Tmphan: /* 24 Jan (Wed) */

Slots for talking with applicants and co-mentors about SURF projects. Please sign up for one of the slots below. All times are PST. __NOTOC__

In preparation for our conversation, please do the following:
* SURF students should work with their co-mentors to find a time the meeting/Skype call. (For Skype calls, co-mentors should initiate.)
* Please make sure you have read the material in the description of your project, so that you are prepared to talk about what the project is about and we can narrow in on the key ideas that will be the basis of your proposal
* Please take a look at the [[SURF GOTChA chart]] page, which is the format that we will use for the first iteration of your project proposal.

{| border=1
|- valign=top
| width=30% |
==== 23 Jan (Tue) ====
* 1:00 pm PST: open
<hr>
* 4:00 pm PST: Andrey/ Sanjana
* 4:30 pm PST: open
<hr>
* 6:00 pm PST: Andy/Emanuel
* 6:30 pm PST: open
| width=30% |

==== 24 Jan (Wed) ====
* 7:30 am PST: William/Sannat
* 8:00 am PST: Rory/Elin
<hr>
*12:15 pm PST: Filip / Jin
*12:45 pm PST: open (if needed)
<hr>
* 4:30 pm PST: Reed / Leah
* 5:00 pm PST: open
* 5:30 pm PST: Steve & Tung
|}

The agenda for the phone call is (roughly):

# Description of the basic idea behind the project (based on applicant's understanding)
# Discussion about approaches, things to read, variations to consider, etc
# Discussion of the format of the proposal
# Questions and discussion about the process

SURF discussions, Jan 2018

2018-01-22T21:19:01Z

Tmphan: /* 24 Jan (Wed) */

Slots for talking with applicants and co-mentors about SURF projects. Please sign up for one of the slots below. All times are PST. __NOTOC__

In preparation for our conversation, please do the following:
* SURF students should work with their co-mentors to find a time the meeting/Skype call. (For Skype calls, co-mentors should initiate.)
* Please make sure you have read the material in the description of your project, so that you are prepared to talk about what the project is about and we can narrow in on the key ideas that will be the basis of your proposal
* Please take a look at the [[SURF GOTChA chart]] page, which is the format that we will use for the first iteration of your project proposal.

{| border=1
|- valign=top
| width=30% |
==== 23 Jan (Tue) ====
* 1:00 pm PST: open
<hr>
* 4:00 pm PST: Andrey/ Sanjana
* 4:30 pm PST: open
<hr>
* 6:00 pm PST: Andy/Emanuel
* 6:30 pm PST: open
| width=30% |

==== 24 Jan (Wed) ====
* 7:30 am PST: William/Sannat
* 8:00 am PST: Rory/Elin
<hr>
*12:15 pm PST: Filip / Jin
*12:45 pm PST: open (if needed)
<hr>
* 4:30 pm PST: Reed / Leah
* 5:00 pm PST: Steve & Tung
* 5:30 pm PST: open
|}

The agenda for the phone call is (roughly):

# Description of the basic idea behind the project (based on applicant's understanding)
# Discussion about approaches, things to read, variations to consider, etc
# Discussion of the format of the proposal
# Questions and discussion about the process

SURF discussions, Jan 2018

2018-01-22T05:50:50Z

Tmphan: /* 24 Jan (Wed) */

Slots for talking with applicants and co-mentors about SURF projects. Please sign up for one of the slots below. All times are PST. __NOTOC__

In preparation for our conversation, please do the following:
* SURF students should work with their co-mentors to find a time the meeting/Skype call. (For Skype calls, co-mentors should initiate.)
* Please make sure you have read the material in the description of your project, so that you are prepared to talk about what the project is about and we can narrow in on the key ideas that will be the basis of your proposal
* Please take a look at the [[SURF GOTChA chart]] page, which is the format that we will use for the first iteration of your project proposal.

{| border=1
|- valign=top
| width=30% |
==== 23 Jan (Tue) ====
* 12:00 pm PST: open
* 12:30 pm PST: open
* 1:00 pm PST: open
<hr>
* 4:00 pm PST: open
* 4:30 pm PST: open
<hr>
* 6:00 pm PST: open
* 6:30 pm PST: open
| width=30% |

==== 24 Jan (Wed) ====
* 7:30 am PST: open (hold for India/Europe)
* 8:00 am PST: open (hold for India/Europe)
<hr>
*12:15 pm PST: open (if needed)
*12:45 pm PST: open (if needed)
<hr>
* 4:30 pm PST: Tung
* 5:00 pm PST: open
* 5:30 pm PST: open
|}

The agenda for the phone call is (roughly):

# Description of the basic idea behind the project (based on applicant's understanding)
# Discussion about approaches, things to read, variations to consider, etc
# Discussion of the format of the proposal
# Questions and discussion about the process

SURF 2018: Contract-based Design of Control Systems

2017-12-19T07:00:13Z

Tmphan:

'''[[SURF 2018|2018 SURF]]: project description'''
* Mentor: Richard M. Murray
* Co-mentor: Tung Phan

==Description==

As systems grow in scale and complexity, a modular approach to design becomes mandatory. With this comes the question of generating specifications for implementing submodules such that when these are reassembled at the end of the design process, a complete system that designers originally had in mind will emerge. Despite the existence of various theories and tools that support "local" design of submodules from many subfields of computer science and engineering, studies into interactions between these are still lacking. A contract-based methodology for system design like the one proposed in [1] is an attractive step in the direction of developing a mathematical design and specification framework.

In this project, we will investigate methods for integrating design implementations from different domains into a unified platform in a correct-by-construction manner. In particular, we allow the student to either choose to

[[File:AVP.png|500px|right]]

1. Study how to write formal specifications for contracts and implement algorithms that perform mathematical operations on contracts with the goal of automated contract synthesis, contract refinement and error recovery in mind. It is recommended that students willing to contribute to this version of the project have a basic knowledge of formal methods (see [3] for a quick introduction to the specification language TLA+) and automata theory (it might be helpful to have a look at [4]).

2. Find a design scenario of interest to which our contract framework applies and demonstrate how they can be implemented. Some examples are autonomous valet parking service with non-cooperative human drivers, supervisory controller to vehicle communication subsystems. For a more concrete example, see [2]. Students interested in this version of the project should have a good knowledge of control theory. Experience with implementing controllers and generating simulations is highly valued.

Both versions require programming experience. The student is expected to know Python or to have enough programming experience to learn it in a short time.
[[File:AVP_contracts.png|500px|left]]

==References==

[1] Albert Benveniste, Benoit Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, et al.. Contracts for System Design. [Research Report] RR-8147, INRIA. 2012, pp.65. 〈hal-00757488〉

[2] P. Nuzzo, H. Xu, N. Ozay, J. B. Finn, A. L. Sangiovanni-Vincentelli, R. M. Murray, A. Donze, S. A. Seshia. A Contract-Based Methodology for Aircraft Electric Power System Design. IEEE Access, 2014. DOI 10.1109/ACCESS.2013.2295764

[3] https://www.learntla.com/introduction/

[4] Raclet, Jean-Baptiste, et al. "A modal interface theory for component-based design." Fundamenta Informaticae 108.1-2 (2011): 119-149.

SURF 2018: Contract-based Design of Control Systems

2017-12-19T06:55:51Z

Tmphan: /* Description */

'''[[SURF 2018|2018 SURF]]: project description'''
* Mentor: Richard M. Murray
* Co-mentor: Tung Phan

==Description==

As systems grow in scale and complexity, a modular approach to design becomes mandatory. With this comes the question of generating specifications for implementing submodules such that when these are reassembled at the end of the design process, a complete system that designers originally had in mind will emerge. Despite the existence of various theories and tools that support "local" design of submodules from many subfields of computer science and engineering, studies into interactions between these are still lacking. A contract-based methodology for system design like the one proposed in [1] is an attractive step in the direction of developing a mathematical design and specification framework.

In this project, we will investigate methods for integrating design implementations from different domains into a unified platform in a correct-by-construction manner. In particular, we allow the student to either choose to

[[File:AVP.png|500px|right]]

1. Study how to write formal specifications for contracts and implement algorithms that perform mathematical operations on contracts with the goal of automated contract synthesis, contract refinement and error recovery in mind. It is recommended that students willing to contribute to this version of the project have a basic knowledge of formal methods (see [3] for a quick introduction to the specification language TLA+) and automata theory ([4] might be useful).

2. Find a design scenario of interest to which our contract framework applies and demonstrate how they can be implemented. Some examples are autonomous valet parking service with non-cooperative human drivers, supervisory controller to vehicle communication subsystems. For a more concrete example, see [2]. Students interested in this version of the project should have a good knowledge of control theory. Experience with implementing controllers and generating simulations is highly valued.

Both versions require programming experience. The student is expected to know Python or to have enough programming experience to learn it in a short time.
[[File:AVP_contracts.png|500px|left]]

==References==

[1] Albert Benveniste, Benoit Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, et al.. Contracts for System Design. [Research Report] RR-8147, INRIA. 2012, pp.65. 〈hal-00757488〉

[2] P. Nuzzo, H. Xu, N. Ozay, J. B. Finn, A. L. Sangiovanni-Vincentelli, R. M. Murray, A. Donze, S. A. Seshia. A Contract-Based Methodology for Aircraft Electric Power System Design. IEEE Access, 2014. DOI 10.1109/ACCESS.2013.2295764

[3] https://www.learntla.com/introduction/

[4] Raclet, Jean-Baptiste, et al. "A modal interface theory for component-based design." Fundamenta Informaticae 108.1-2 (2011): 119-149.

SURF 2018: Contract-based Design of Control Systems

2017-12-19T06:54:44Z

Tmphan: /* References */

'''[[SURF 2018|2018 SURF]]: project description'''
* Mentor: Richard M. Murray
* Co-mentor: Tung Phan

==Description==

As systems grow in scale and complexity, a modular approach to design becomes mandatory. With this comes the question of generating specifications for implementing submodules such that when these are reassembled at the end of the design process, a complete system that designers originally had in mind will emerge. Despite the existence of various theories and tools that support "local" design of submodules from many subfields of computer science and engineering, studies into interactions between these are still lacking. A contract-based methodology for system design like the one proposed in [1] is an attractive step in the direction of developing a mathematical design and specification framework.

In this project, we will investigate methods for integrating design implementations from different domains into a unified platform in a correct-by-construction manner. In particular, we allow the student to either choose to

[[File:AVP.png|500px|right]]

1. Study how to write formal specifications for contracts and implement algorithms that perform mathematical operations on contracts with the goal of automated contract synthesis, contract refinement and error recovery in mind. It is recommended that students willing to contribute to this version of the project have a basic knowledge of formal methods (see [3] for a quick introduction to the specification language TLA+) and automata theory.

2. Find a design scenario of interest to which our contract framework applies and demonstrate how they can be implemented. Some examples are autonomous valet parking service with non-cooperative human drivers, supervisory controller to vehicle communication subsystems. For a more concrete example, see [2]. Students interested in this version of the project should have a good knowledge of control theory. Experience with implementing controllers and generating simulations is highly valued.

Both versions require programming experience. The student is expected to know Python or to have enough programming experience to learn it in a short time.
[[File:AVP_contracts.png|500px|left]]

==References==

[1] Albert Benveniste, Benoit Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, et al.. Contracts for System Design. [Research Report] RR-8147, INRIA. 2012, pp.65. 〈hal-00757488〉

[2] P. Nuzzo, H. Xu, N. Ozay, J. B. Finn, A. L. Sangiovanni-Vincentelli, R. M. Murray, A. Donze, S. A. Seshia. A Contract-Based Methodology for Aircraft Electric Power System Design. IEEE Access, 2014. DOI 10.1109/ACCESS.2013.2295764

[3] https://www.learntla.com/introduction/

[4] Raclet, Jean-Baptiste, et al. "A modal interface theory for component-based design." Fundamenta Informaticae 108.1-2 (2011): 119-149.

SURF 2018: Contract-based Design of Control Systems

2017-12-08T20:31:24Z

Tmphan:

'''[[SURF 2018|2018 SURF]]: project description'''
* Mentor: Richard M. Murray
* Co-mentor: Tung Phan

==Description==

As systems grow in scale and complexity, a modular approach to design becomes mandatory. With this comes the question of generating specifications for implementing submodules such that when these are reassembled at the end of the design process, a complete system that designers originally had in mind will emerge. Despite the existence of various theories and tools that support "local" design of submodules from many subfields of computer science and engineering, studies into interactions between these are still lacking. A contract-based methodology for system design like the one proposed in [1] is an attractive step in the direction of developing a mathematical design and specification framework.

In this project, we will investigate methods for integrating design implementations from different domains into a unified platform in a correct-by-construction manner. In particular, we allow the student to either choose to

[[File:AVP.png|500px|right]]

1. Study how to write formal specifications for contracts and implement algorithms that perform mathematical operations on contracts with the goal of automated contract synthesis, contract refinement and error recovery in mind. It is recommended that students willing to contribute to this version of the project have a basic knowledge of formal methods (see [3] for a quick introduction to the specification language TLA+) and automata theory.

2. Find a design scenario of interest to which our contract framework applies and demonstrate how they can be implemented. Some examples are autonomous valet parking service with non-cooperative human drivers, supervisory controller to vehicle communication subsystems. For a more concrete example, see [2]. Students interested in this version of the project should have a good knowledge of control theory. Experience with implementing controllers and generating simulations is highly valued.

Both versions require programming experience. The student is expected to know Python or to have enough programming experience to learn it in a short time.
[[File:AVP_contracts.png|500px|left]]

==References==

[1] Albert Benveniste, Benoit Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, et al.. Contracts for System Design. [Research Report] RR-8147, INRIA. 2012, pp.65. 〈hal-00757488〉

[2] P. Nuzzo, H. Xu, N. Ozay, J. B. Finn, A. L. Sangiovanni-Vincentelli, R. M. Murray, A. Donze, S. A. Seshia. A Contract-Based Methodology for Aircraft Electric Power System Design. IEEE Access, 2014. DOI 10.1109/ACCESS.2013.2295764

[3] https://www.learntla.com/introduction/

SURF 2018: Contract-based Design of Control Systems

2017-12-08T20:27:47Z

Tmphan:

'''[[SURF 2018|2018 SURF]]: project description'''
* Mentor: Richard M. Murray
* Co-mentor: Tung Phan

==Description==

As systems grow in scale and complexity, a modular approach to design becomes mandatory. With this comes the question of generating specifications for implementing submodules such that when these are reassembled at the end of the design process, a complete system that designers originally had in mind will emerge. Despite the existence of various theories and tools that support "local" design of submodules from many subfields of computer science and engineering, studies into interactions between these are still lacking. A contract-based methodology for system design like the one proposed in [1] is an attractive step in the direction of developing a mathematical design and specification framework.

In this project, we will investigate methods for integrating design implementations from different domains into a unified platform in a correct-by-construction manner. In particular, we allow the student to either choose to

[[File:AVP.png|500px|right]]

1. Study how to write formal specifications for contracts and implement algorithms that perform mathematical operations on contracts with the goal of automated contract synthesis, contract refinement and error recovery in mind. It is recommended that students willing to contribute to this version of the project have a basic knowledge of formal methods (see [3] for a quick introduction to the specification language TLA+) and automata theory.

2. Find a design scenario of interest to which our contract framework applies and demonstrate how they can be implemented. Some examples are autonomous valet parking service with non-cooperative human drivers, supervisory controller to vehicle communication subsystems. For a more concrete example, see [2]. Students interested in this version of the project should have a good knowledge of control theory. Experience with implementing controllers and generating simulations is highly valued.

Both versions require programming experience. The student is expected to know Python or to have enough programming experience to learn it in a short time.

[[File:AVP_contracts.png|400px|left]]

==References==

[1] Albert Benveniste, Benoit Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, et al.. Contracts for System Design. [Research Report] RR-8147, INRIA. 2012, pp.65. 〈hal-00757488〉

[2] P. Nuzzo, H. Xu, N. Ozay, J. B. Finn, A. L. Sangiovanni-Vincentelli, R. M. Murray, A. Donze, S. A. Seshia. A Contract-Based Methodology for Aircraft Electric Power System Design. IEEE Access, 2014. DOI 10.1109/ACCESS.2013.2295764

[3] https://www.learntla.com/introduction/

File:AVP contracts.png

2017-12-08T20:21:58Z

Tmphan: Autonomous Valet Parking Garage Contract-based Design

Autonomous Valet Parking Garage Contract-based Design

File:AVP.png

2017-12-08T20:21:24Z

Tmphan: Autonomous Valet Parking Garage

Autonomous Valet Parking Garage

SURF 2018: Contract-based Design of Control Systems

2017-12-08T20:11:10Z

Tmphan: Created page with "'''2018 SURF: project description''' * Mentor: Richard M. Murray * Co-mentor: Tung Phan As systems grow in scale and complexity, a modular approach to design be..."

'''[[SURF 2018|2018 SURF]]: project description'''
* Mentor: Richard M. Murray
* Co-mentor: Tung Phan

As systems grow in scale and complexity, a modular approach to design becomes mandatory. With this comes the question of generating specifications for implementing submodules such that when these are reassembled at the end of the design process, a complete system that designers originally had in mind will emerge. Despite the existence of various theories and tools that support "local" design of submodules from many subfields of computer science and engineering, studies into interactions between these are still lacking. A contract-based methodology for system design like the one proposed in [1] is an attractive step in the direction of developing a mathematical design and specification framework.

In this project, we will investigate methods for integrating design implementations from different domains into a unified platform in a correct-by-construction manner. In particular, we allow the student to either choose to

1. Study how to write formal specifications for contracts and implement algorithms that perform mathematical operations on contracts with the goal of automated contract synthesis, contract refinement and error recovery in mind. It is recommended that students willing to contribute to this version of the project have a basic knowledge of formal methods (see [3] for a quick introduction to the specification language TLA+) and automata theory.

2. Find a design scenario of interest to which our contract framework applies and demonstrate how they can be implemented. Some examples are autonomous valet parking service with non-cooperative human drivers, supervisory controller to vehicle communication subsystems. For a more concrete example, see [2]. Students interested in this version of the project should have a good knowledge of control theory. Experience with implementing controllers and generating simulations is highly valued.

Both versions require programming experience. The student is expected to know Python or to have enough programming experience to learn it in a short time.

References

[1] Albert Benveniste, Benoit Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, et al.. Contracts for System Design. [Research Report] RR-8147, INRIA. 2012, pp.65. 〈hal-00757488〉

[2] P. Nuzzo, H. Xu, N. Ozay, J. B. Finn, A. L. Sangiovanni-Vincentelli, R. M. Murray, A. Donze, S. A. Seshia. A Contract-Based Methodology for Aircraft Electric Power System Design. IEEE Access, 2014. DOI 10.1109/ACCESS.2013.2295764

[3] https://www.learntla.com/introduction/

SURF 2018

2017-12-08T20:08:26Z

Tmphan:

{{righttoc}}
This page is intended for students interested in working on SURF projects in the Summer of 2018. It contains information about how to apply for a SURF project in my group along with a list of project areas.

'''Note:''' Projects will be posted here starting after finals week. Please check back after that time for more information.

=== Applying for a SURF project ===

Because I get many students interested in doing SURFs in my group and because we have several projects available, we use the first few weeks in January to sort out who we will work with in writing proposals. We only submit one proposal per project area and so we often can't accommodate everyone who wants to work in my group over the summer.

# A list of SURF project descriptions is given in the table below. Due to the number of SURF projects that we support, we are only able to support students who select from among these projects. Please make sure to read the project descriptions, required skills (if any) and skim a few of the listed references before contacting me about doing a SURF project.
# Students interested in writing proposals for SURF projects should contact me via e-mail by 10 Jan (Wed) and provide the following information:
#* A list of up to three SURF projects from the list below that you are interested in working on
#* A one page resume listing relevant experience and coursework
#* If you are not a Caltech student, I will also need the following additional information:
#** An unofficial copy of your academic transcript
#** Names of two faculty members at your current institution that I can contact for a reference
# Starting on 11 January, I will go through all applications and work with my group to identify who is a possible fit for each project. We will then contact you and ask for you to meet (or talk with) possible co-mentors so that we can eventually work out who we will work with in writing up a proposal.
# We hope to make final decisions on projects by about 20 Jan, at which point we will start working with students on writing up proposals.
# All applications should go through the normal SURF application process, described at www.surf.caltech.edu. SURF applications are due on ~22 Feb 2015 (Amgen applications are due a week earlier)..
# If you are selected for a SURF, please be aware of the following information
#* All SURF projects in my group will start on 19 Jun (Tue). If you can't start on that date, please make sure that you indicate this when you contact me
#* All SURF projects are for a minimum of 10 weeks, although I usually recommend that you try to stay for 12 weeks if possible. It's hard to complete a project in just 10 weeks and spending a few extra weeks can greatly improve the project.
#* All SURF students in my group will be expected to devote full-time effort to their SURF project, so you cannot have a second job in addition to your SURF.

=== List of available projects ===

Projects will be posted as they come available. I recommend waiting until near the deadline submission before submitting your project preferences.

{| border=1 width=100%
|-
| '''Title''' || '''Grant/Project''' || '''Co-Mentors''' || '''Comments'''
|-
| {{SURF entry|2018|Experimental verification of a semi-autonomous vehicle design based on human intention}}
| [[NSF VeHICaL]]
| Jin Ge
|
|-
| {{SURF entry|2018|Contract-based Design of Control Systems}}
| [[DENSO CPM]]
| Tung Phan
|

|}

Group Schedule, Summer 2017

2017-06-23T23:37:02Z

Tmphan:

This page contains information about various upcoming events that are of interest to the group. __NOTOC__
{| width=60%
|- valign=top
| width=50% |
* [[Schedule|Richard's calendar (travel)]]
| width=50% |
* [[Group Schedule, Spring 2017]]
|}

The schedule for group and subgroup meetings is given below. Contact Richard if you need to change the schedule. Unless otherwise noted, here are the locations of the meetings:

:{| width=100%
|- valign=top
| width=30% |
* Biocircuits subgroup - 111 Keck
| width=30% |
* NCS subgroup - 110 Steele
| width=30% |
* Group meetings - 213 ANB
|}

{| width=100% border=1
|- valign=top

| width=25% |
=== Week 1: 19 Jun - 23 Jun ===
'''NCS: Mon, 10a-12p'''
* Introductions
* Sofie Haesaert
<hr>
* No biocircuits meeting

| width=25% |
=== Week 2: 26 Jun - 30 Jun ===
'''Biocircuits: Mon, 10a-12p'''
* Ania Baetica
* George Artavanis
<hr>
* BioCon project meeting: Mon, 12p-2p - 111 Keck
* SURF kickoff meeting: Mon, 2p-3:30p - 111 Keck
* No NCS meeting

| width=25% |
=== Week 3: 3 Jul - 7 Jul ===
'''Biocircuits: Wed, 10a-12p'''
* Vipul Singhal
* Yong Wu
'''NCS: Wed, 1p-3p''' - 114 Steele
* Tony Fragoso
* Jake Reher (Ames)

|- valign=top
| width=25% |
=== Week 4: 10 Jul - 14 Jul ===
'''Biocircuits: Mon, 10a-12p'''
* James Parkin
* Mark Prator
* Swati Agrawal
'''NCS: Tue, 10a-12p'''
* Sumanth Dathathri
* Yashwanth Nakka (Chung)

| width=25% |

=== Week 5: 17 Jul - 21 Jul ===
* No group meetings, Richard out of town
'''Biocircuits: Mon, 11a-12p'''
* Lab cleanup

| width=25% |
=== Week 6: 24 Jul - 28 Jul ===
'''Biocircuits: Tue, 10a-12p'''
* Anand Swaminathan
* Shaobin Guo
'''NCS: Tue, 1p-3p'''
* Richard Cheng
* Ellen Feldman (Burdick)

|- valign=top
| width=25% |

=== Week 7: 31 Jul - 4 Aug ===
'''Biocircuits: Tue, 10a-12p'''
* Leo Green
* Sam Clamons
'''NCS: Wed, 10a-12p'''
* Ioannis Filippidis
* Wen-Loong Ma (Ames)

| width=25% |

=== Week 8: 7 Aug - 11 Aug ===
'''Biocircuits: Tue, 10a-12p'''
* SURF students
'''NCS: Wed, 10a-12p'''
* SURF students
<hr>
* BioCon project meeting: Mon, 10a-12p

| width=25% |
=== Week 9: 14 Aug - 18 Aug ===
'''Biocircuits: Tue, 10a-12p'''
* Andrey Shur
* Cindy Ren
* Note: this meeting will probably shift to Thu, 10a-12p - 114 Steele
'''NCS: Wed, 10a-12p'''
* Jin Ge (tentative)
* Matt Burkhardt (Burdick)
* Note: this meeting will probably shift to Thu, 1-3p - 114 Steele

|- valign=top
| width=25% |

=== Week 10: 21 Aug - 25 Aug ===
'''Biocircuits: Tue, 10a-12p'''
* Reed McCardell
* William Poole
'''NCS: Wed, 10a-12p'''
* Karena Cai
* Thomas Gurriet (Ames)

| width=25% |
=== Week 11: 28 Aug - 1 Sep ===
'''Biocircuits: Tue, 10a-12p'''
* Andy Halleran
* Shan Huang
'''NCS: Wed, 10a-12p'''
* Tung Phan
* Francesca Baldini (Chung)
* Note: this meeting will likely shift to Thu (31 Aug) - 114 Steele

| width=25% |

=== Week 12: 4 Sep - 8 Sep ===
* No group meetings, Richard out of town

|- valign=top
| width=25% |
=== Week 13: 11 Sep - 15 Sep ===
* No group meetings, Richard out of town
'''Biocircuits: Mon, 11a-12p'''
* Lab cleanup

| width=25% |
=== Week 14: 18 Sep - 22 Sep ===
'''Biocircuits: Mon, 12p-2p'''
* Michaelle Mayalu
* Rory Williams
<hr>
* BioCon project meeting: Mon, 10a-12p
* No NCS group meeting

| width=25% |
=== Week 15: 25 Sep - 29 Sep ===
* First week of classes; see [[Group Schedule, Fall 2017|fall term schedule]]
|}

May 2017 meeting schedule

2017-05-08T14:43:43Z

Tmphan:

Richard will be in town several different times in May. Please sign up for a time to meet below. Please note that these are likely the last "sabbatical" meetings until Richard returns to Pasadena in early July. __NOTOC__

{| border=1 width=100%
|- valign=top
| width=33% |
| width=33% |
==== 15 May (Mon) ====
* 9:30 am: Open
* 10:15 am: Open
* 11:00 am: Faculty meeting
* 11:30 am: Open
* 12:15 pm: Lunch
* 1:30 pm: Open
* 2:15 pm: Open
* 3:00 pm: Open
* 3:45 pm: Break
* 4:00 pm: Namita
* 4:45 pm: Open
* 5:30 pm: Open
* 6:15 pm: Done for the day

| width=33% |

==== 16 May (Tue)====
* 9:30 am: Open
* 10:15 am: Tung
* 11:00 am: Faculty meeting
* 12:00 pm: Lunch
* 1:30 pm: Depart
* 12:00 pm: Lunch
* 1:30 pm: Depart

|- valign=top
| width=33% |

====21 May (Sun) ====
* 1:45 pm: Open
* 2:30 pm: Open
* 3:15 pm: Open
* 4:00 pm: Break
* 4:15 pm: Open
* 5:00 pm: Open
* 5:45 pm: Open
* 6:30 pm: Done for the day

| width=33% |

==== 22 May (Mon) ====
* 10:15 am: Open
* 11:00 am: Open
* 11:45 am: Lunch
* 12:00 pm: DARPA BioCon meeting
* 2:00 pm: Open
* 2:45 pm: Off campus
* 4:15 pm: Open
* 5:00 pm: Non-Caltech meetings
* 6:30 pm: Done for the day

| width=33% |
==== 23 May (Tue) ====
* 9:30 am: Faculty discussion
* 10:30 am: Hold (Susan)
* 11:30 am: Lunch
* 12:00 pm: Telecon
* 1:00 pm: Anu thesis defense
* 3:00 pm: Terri (?)
* 3:30 pm: Depart

|- valign=top
| width=33% |

====28 May (Sun) ====
* 1:45 pm: Open
* 2:30 pm: Open
* 3:15 pm: Open
* 4:00 pm: Done for the day
| width=33% |
====29 May (Mon) ====
* 1:45 pm: Open (if needed)
* 2:30 pm: Open (if needed)
* 3:15 pm: Open (if needed)
* 4:00 pm: Done for the day
| width=33% |

==== 30 May (Tue) ====
* 9:30 am: Open
* 10:15 am: Open
* 11:00 am: Stepan seminar
* 12:00 pm: Lunch
* 1:30 pm: Namita
* 2:15 pm: Open
* 3:00 pm: Depart
|}

Apr 2017 meeting schedule

2017-04-12T15:12:39Z

Tmphan: /* 20 Apr (Thu) */

Richard will be in town 19-21 Apr. Please sign up for a time to meet below. __NOTOC__

{| border=1
|- valign=top
| width=25% |
==== 19 Apr (Wed) ====
* 9:30 am: Hold (Sofie or Leo)
* 10:30 am: Admin meeting (SP, MC)
* 11:15 am: Open
* 12:00 pm: DARPA BioCon meeting
* 2:00 pm: Candidacy exam
* 3:00 pm: CDS tea
* 3:45 pm: Open
* 4:30 pm: Admin meeting (LL)
* 5:00 pm: Open (tentative)
* 5:45 pm: Associates event

| width=25% |

==== 20 Apr (Thu) ====
* 9:30 am: Hold (Sofie or Leo)
* 10:30 am: Mark
* 11:15 am: Tony Fragoso
* 12:00 pm: Lunch
* 1:30 pm: EBRC telecon
* 2:30 pm: Open
* 3:15 pm: Open
* 4:00 pm: Vipul
* 4:45 pm: Break
* 5:00 pm: Tung
* 5:45 pm: Open
* 6:00 pm: Open (if needed)
* 6:45 pm: Open (if needed)
* 7:30 pm: Done for the day

| width=25% |

==== 21 Apr (Fri) ====
* 9:15 am: Open
* 10:00 am: JPL CIF meeting
* 11:15 am: Open
* 12:00 pm: Lunch
* 12:45 pm: Open
* 1:30 pm: Open
* 2:15 pm: Open
* 3:00 pm: Break
* 3:15 pm: Open
* 4:00 pm: Open
* 4:45 pm: Open
* 5:30 pm: Done for the day

| width=25% |

==== 23 Apr (Sun) ====
* 1:45 pm: Open
* 2:30 pm: Open
* 3:15 pm: Open
* 4:00 pm: Break
* 4:15 pm: Open
* 5:00 pm: Open
* 5:45 pm: Shan
* 6:30 pm: Done for the day
|}

Mar 2017 meeting schedule

2017-02-26T21:35:30Z

Tmphan: /* 7 Mar (Tue) */

Richard will be in town 3-7 Mar. Please sign up for a time to meet below. __NOTOC__

{| border=1
|- valign=top
| width=25% |
==== 3 Mar (Fri) ====
* 10:00 am: DENSO CPM telecon
* 11:00 am: Open
* 11:45 am: Shaobin
* 12:30 pm: Lunch
* 1:00 pm: Hold: DARPA telecon
* 2:00 pm: Open
* 2:45 pm: Open
* 3:30 pm: SBIR telecon (w/ Mark P)
* 4:00 pm: Faculty meeting
* 5:45 pm: Open
* 6:30 pm: Done for the day

| width=25% |

==== 5 Mar (Sun) ====
* 1:45 pm: Open
* 2:30 pm: Open
* 3:15 pm: Open
* 4:00 pm: Break
* 4:15 pm: Open
* 5:00 pm: Open
* 5:45 pm: Open
* 6:30 pm: Done for the day

| width=25% |

==== 6 Mar (Mon) ====
* 9:30 am: AFOSR BRI telecon
* 10:30 am: Yong
* 11:15 am: Fragoso
* 12:00 pm: Lunch
* 12:30 pm: Hold: DARPA telecon
* 1:30 pm: Open
* 2:15 pm: Open
* 3:00 pm: Open
* 3:45 pm: Break
* 4:00 pm: Open
* 4:45 pm: Open
* 5:30 pm: Open
* 6:15 pm: Done for the day

| width=25% |

==== 7 Mar (Tue) ====
* 9:30 am: Busy
* 10:15 am: Tung
* 11:00 am: Hold: DARPA telecon
* 12:00 pm: Lunch
* 12:45 pm: Hold
* 1:15 pm: Andrew M
* 2:00 pm: Andy Halleran
* 2:45 pm: Depart for airport
|}

Jan 2017 meeting schedule

2017-01-13T16:44:51Z

Tmphan: /* 24 Jan (Tue) */

Richard will be in town 20-24 Jan. Please sign up for a time to meet below. __NOTOC__

{| border=1
|- valign=top
| width=25% |
==== 20 Jan (Fri) ====
* Richard arrives on campus ~9:45 am
* 10:15 am: Mark
* 11:00 am: Yong
* 11:45 am: Open
* 12:30 pm: Lunch
* 1:30 pm: Yong and Frances A
* 2:30 pm: Open
* 3:15 pm: Open
* 4:00 pm: Open
* 4:45 pm: Break
* 5:00 pm: Open
* 5:45 pm: Open
* 6:30 pm: Done for the day

| width=25% |

==== 22 Jan (Sun) ====
* 1:45 pm: Open
* 2:30 pm: Open
* 3:15 pm: Open
* 4:00 pm: Break
* 4:15 pm: Open
* 5:00 pm: Open
* 5:45 pm: Open
* 6:30 pm: Done for the day

| width=25% |

==== 23 Jan (Mon) ====
* 8:00 am: Michaelle
* 9:00 am: Hold: Jaymie
* 10:00 am: BioCon meeting
* 12:00 pm: Seminar ([[Michaëlle Mayalu, Jan 2017|Michaelle]])
* 1:00 pm: Hold until needed
* 1:45 pm: Open
* 2:30 pm: CDS faculty meeting
* 4:15 pm: Tony Fragoso
* 5:00 pm: Open
* 5:45 pm: Open
* 6:30 pm: Dinner with visitors

| width=25% |

==== 24 Jan (Tue) ====
* 9:45 am: Henrike
* 10:30 am: Open
* 11:15 am: Tung
* 12:00 pm: Seminar ([[Henrike Niederholtmeyer, Jan 2017|Henrike]])
* 1:15 pm: [[Michaëlle Mayalu, Jan 2017|Michaelle]]
* 2:00 pm: Open
* 2:45 pm: [[Henrike Niederholtmeyer, Jan 2017|Henrike]]
* 3:30 pm: Depart for airport
|}

Nov 2016 meeting schedule

2016-11-03T18:55:28Z

Tmphan: /* 14 Nov (Mon) */

Richard will be in town 13-16 Nov. Please sign up for a time to meet below.
__NOTOC__

{| border=1
|- valign=top
| width=25% |

==== 13 Nov (Sun) ====
 
 
<hr>
* 2 pm: Hold until needed
* 2:45 pm: Hold until needed
* 3:30 pm: Hold until needed
* 4:15 pm: Break
* 5:00 pm: Hold until needed
* 5:45 pm: Hold until needed
* 6:30 pm: Done for the day

| width=25% |

==== 14 Nov (Mon) ====
* 10:30 am: Open
* 11:15 am: Tung
<hr>
* 1:30 pm: Open
* 2:15 pm: Open
* 3:00 pm: Shaobin
* 3:45 pm: Break
* 4:00 pm: Open
* 4:45 pm: Open
* 5:30 pm: Open
* 6:15 pm: Done for the day
| width=25% |

====15 Nov (Tue) ====
* 10:30 am: Open
* 11:15 am: Open
<hr>
* 1:30 pm: Open
* 2:15 pm: Open
* 3:00 pm: Open
* 3:45 pm: Break
* 4:00 pm: Open
* 4:45 pm: Open
* 5:30 pm: Open
* 6:15 pm: Done for the day
| width=25% |

==== 16 Nov (Wed) ====
* 10:30 am: Open
* 11:15 am: Open
<hr>
* 1:30 pm: Open
* 2:15 pm: Open
* 3:00 pm: CDS tea
* Depart for airport at ~4 pm
|}

Sep/Oct 2016 meeting schedule

2016-09-17T17:19:43Z

Tmphan: /* 3 Oct (Mon) */

Richard will be in town 7-10 August 2016. Please sign up for a time to meet below.
__NOTOC__

{| border=1
|- valign=top
| width=25% |
==== 29 Sep (Thu) ====
* Flying in from SF in the morning
* 1:00 pm: Open
* 1:45 pm: Open
* 2:30 pm: Open
* 3:15 pm: Break
* 3:30 pm: Open
* 4:15 pm: Open
* 5:00 pm: Open
* 5:45 pm: Break
* 6:00 pm: Open
* 6:45 pm: Open
* 7:30 pm: Done for the day
| width=25% |

==== 30 Sep (Fri) ====
* Morning: busy with other meetings/phone calls
* 1:30-3:30 pm: Integrase project meeting (Victoria, Andrey, George, Sam, Ania, Cindy, Jining)
* 3:30 pm: Miki or Jaymie
* 4:30 pm: break
* 4:45 pm: Open
* 5:30 pm: Open
* 6:15 pm: Done for the day
| width=25% |

==== 2 Oct (Sun) ====
* 1:45 pm: Open
* 2:30 pm: Open
* 3:15 pm: Open
* 4:00 pm: Break
* 4:15 pm: Open
* 5:00 pm: Open
* 5:45 pm: Open
* 6:30 pm: Done for the day

| width=25% |

==== 3 Oct (Mon) ====
* 10 am - 12 pm: DARPA BioCon meeting
* 12:00 pm: Candidacy exam
* 1:45 pm: Jaymie or Miki
* 2:45 pm: Tung
* 3:30 pm: Open
* 4:15 pm: Open
* 5:00 pm: Break
* 5:15 pm: Open
* 6:00 pm: Open
* 6:45 pm: Open
* 7:30 pm: Done for the day
|}

Temporal Logic Specifications for Control System Design in Automotive Systems

2016-08-12T21:34:58Z

Tmphan:

{{righttoc}}
This project is a collaboration with DENSO as part of the Control Performance Modeling (CPM) project. We are exploring methods for handling “mixed specifications” that are spread between the multiple layers of control in a complex system. We are making use of tools from control theory and formal methods to provide a rigorous framework for specification, verification and synthesis of complex networked control systems, with application to automotive systems.

{| cellpadding=0 cellspacing=0 width=80%
|- valign=top
|
Current participants:
{{project current participants}}
Additional participants:
{{project additional participants}}
|
Collaborators:
* Qiming Zhao (DENSO)
Past participants:
{{project past participants}}
|}

=== Objectives ===
[[Image:denso16-cpm.png|right|400px]]
# Identify methods for establishing contracts (design specifications) between different layers of the design that insure that the overall properties of the system are met with the individual specifications at each layer of abstraction are satisfied. This type of specification will establish a pair of “vertical contract” (one to the next layer down in the hierarchy and the other to the next layer up).
# Given a set of specifications at the various layers, identify and/or develop the design tools required at least layer of abstraction to satisfy the contracts. We anticipate that many of these tools, especially at the inner and outer loop levels would be existing design methods (frequency domain design, optimization-based design, etc) with appropriate specifications. New tools may be needed to link the supervisory layer with the lower layers (basically this is the discrete to continuous challenge of hybrid systems.
# Apply these methods (specification and design) to a proof-of-concept example of interest to DENSO.

=== References ===
{{project paper list}}

[[Category:Active projects]]
[[Category:NCS projects]]
{{Project
|Title=Temporal Logic Specifications for Control System Design in Automotive Systems
|Agency=DENSO
|Start date=1 Jul 2016
|End date=30 Mar 2017
|Support summary=1 graduate student + travel
|Reporting requirements=Quarterly reports
|Project ID=DENSO CPM
}}

Aug 2016 meeting schedule

2016-07-31T00:17:40Z

Tmphan: /* 9 Aug (Tue) */

Richard will be in town 7-10 August 2016. Please sign up for a time to meet below.
__NOTOC__

{| border=1
|- valign=top
| width=25% |
==== 7 Aug (Sun) ====
* 2:15 pm: Open
* 3:00 pm: Open
* 3:45 pm: Open
* 4:00 pm: Break
* 4:45 pm: Open
* 5:30 pm: Open
* 6:30 pm: Open
| width=25% |
==== 8 Aug (Mon) ====
* 9-11 am: Integrase project meeting (Victoria, Andrey, Sam, Ania)
<hr>
* 12:45 pm: Anandh
* 1:30 pm: Open
* 2:15 pm: Open
* 3:00 pm: Open
* 3:45 pm: Break
* 4:00 pm: Open
* 4:45 pm: Open
| width=25% |

==== 9 Aug (Tue) ====
* 8:30 am: Open
* 9:15 am: Open
* 10:00 am: Jaymie
* 11 am - 2 pm: DARPA Biological Control project meeting (Anandh, Ania, Cindy, James, Reed, Andrey, Sam)
* 1:00 pm: Tung
* 1:45 pm: Open
* 2:30 pm: Open
* 3:15 pm: Break
* 3:30 pm: Vipul
* 4:15 pm: Open
* 5:00 pm: Open
* 5:45 pm: Break
| width=25% |

==== 10 Aug (Wed) ====
* 9-11 am: TX-TL project meeting (Clare, Mark, Shaobin, Yong, Vipul, Sam, Miki)
* 11:00 am: Open
* 11:45 am: Unavailable
* 12:45 pm: Miki
* 1:45 pm: Open
* 2:30 pm: Leave for airport
|}