Murray Wiki - User contributions [en]

Group Schedule, Fall 2015

2015-11-11T02:10:42Z

Farahani: /* Week 8: 16 Nov - 20 Nov */

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, Summer 2015]]
|}

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% |
* Group meetings - 213 ANB
| width=30% |
* Biocircuits subgroup - 111 Keck
| width=30% |
* NCS subgroup - 243 ANB
|}

{| width=100% border=1

|- valign=top
| width=25% |
=== Week 1: 28 Sep - 2 Oct ===
'''NCS: Thu, 3p-4:30p'''
* Ioannis Filippidis (main)
* Open (short)

| width=25% |

=== Week 2: 5 Oct - 9 Oct ===
'''Biocircuits: Tue, 10a-12p'''
* Clare Hayes (long)
* Yutaka Hori (short)
'''NCS: Wed, 10:30a-12p'''
* Cat McGhan (main)
* Open (short)

| width=25% |

=== Week 3: 12 Oct - 18 Oct ===
'''Biocircuits: Tue, 10a-12p'''
* Abel Chiao (long)
* Vipul Singhal (short)
'''NCS: Tue, 2:00p-3:30p'''
* Sonja Glavaski (main)
* Open (short)

|- valign=top
| width=25% |

=== Week 4: 19 Oct - 23 Oct ===
'''Biocircuits: Tue, 10a-12p'''
* <s>Anandh Swaminathan (long)</s>
* Victoria Hsiao (short)
'''NCS: Wed, 10:30a-12p'''
* Tony Fragoso (main)
* Open (short)

| width=25% |

=== Week 5: 26 Oct - 30 Oct ===
'''Biocircuits: Tue, 10a-12p'''
* Anandh Swaminathan (long)
* <s>Ania Baetica (short)</s>
'''NCS: Wed, 10:30a-12p'''
* Sumanth Dathathri (main)
* Open (short)

| width=25% |

=== Week 6: 2 Nov - 6 Nov ===
'''Biocircuits: Tue, 10a-12p'''
* Anu Thubagere (long)
* Ania Baetica (short)
'''NCS: Wed, 10:30a-12p'''
* Daniel Naftalovich (main)
* Open (short)

|- valign=top
| width=25% |

=== Week 7: 9 Nov - 13 Nov ===
'''Biocircuits: Tue, 10a-12p'''
* Shaobin Guo (long)
* Enoch Yeung (short)
'''NCS: Tue, 3p-4p'''
* Ivan Papusha (main)

| width=25% |

=== Week 8: 16 Nov - 20 Nov ===

'''Biocircuits: Thu, 10a-12p'''
* James Parkin (long)
* Yong Wu (short)

'''NCS: Thu, 3:30p-5p'''
* Jiangang Li (main)
* Samira Farahani (short)

| width=25% |

=== Week 9: 23 Nov - 27 Nov ===
'''Biocircuits: Tue, 10a-12p'''
* Sean Sanchez (long)
* Tiffany Zhou (short)

|- valign=top
| width=25% |

=== Week 10: 30 Nov - 4 Dec ===
'''NCS: Mon, 10:30a-12p'''
* Samira Farahani (main)
* Open (short)
'''Biocircuits: Tue, 10a-12p'''
* Sam Clamons (long)
* Tina Xu (short)

| width=25% |

=== Week 11: 7 Dec - 11 Dec ===
'''Biocircuits: Tue, 10a-12p'''
* Prakriti Paul (rotation)
* Georgios Artavanis (rotation)
'''NCS: Wed, 10:30a-12p'''
* Benson Christalin (main)
* Open (short)

| width=25% |

=== Week 12: 14 Dec - 18 Dec ===
'''Biocircuits: Tue, 10a-12p'''
* Open (long)
* Open (short)
'''NCS: Wed, 10:30a-12p'''
* Open (main)
* Open (short)
<hr>
CDC (Osaka)
|}

Group Schedule, Fall 2015

2015-11-11T02:09:28Z

Farahani: /* Week 8: 16 Nov - 20 Nov */

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, Summer 2015]]
|}

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% |
* Group meetings - 213 ANB
| width=30% |
* Biocircuits subgroup - 111 Keck
| width=30% |
* NCS subgroup - 243 ANB
|}

{| width=100% border=1

|- valign=top
| width=25% |
=== Week 1: 28 Sep - 2 Oct ===
'''NCS: Thu, 3p-4:30p'''
* Ioannis Filippidis (main)
* Open (short)

| width=25% |

=== Week 2: 5 Oct - 9 Oct ===
'''Biocircuits: Tue, 10a-12p'''
* Clare Hayes (long)
* Yutaka Hori (short)
'''NCS: Wed, 10:30a-12p'''
* Cat McGhan (main)
* Open (short)

| width=25% |

=== Week 3: 12 Oct - 18 Oct ===
'''Biocircuits: Tue, 10a-12p'''
* Abel Chiao (long)
* Vipul Singhal (short)
'''NCS: Tue, 2:00p-3:30p'''
* Sonja Glavaski (main)
* Open (short)

|- valign=top
| width=25% |

=== Week 4: 19 Oct - 23 Oct ===
'''Biocircuits: Tue, 10a-12p'''
* <s>Anandh Swaminathan (long)</s>
* Victoria Hsiao (short)
'''NCS: Wed, 10:30a-12p'''
* Tony Fragoso (main)
* Open (short)

| width=25% |

=== Week 5: 26 Oct - 30 Oct ===
'''Biocircuits: Tue, 10a-12p'''
* Anandh Swaminathan (long)
* <s>Ania Baetica (short)</s>
'''NCS: Wed, 10:30a-12p'''
* Sumanth Dathathri (main)
* Open (short)

| width=25% |

=== Week 6: 2 Nov - 6 Nov ===
'''Biocircuits: Tue, 10a-12p'''
* Anu Thubagere (long)
* Ania Baetica (short)
'''NCS: Wed, 10:30a-12p'''
* Daniel Naftalovich (main)
* Open (short)

|- valign=top
| width=25% |

=== Week 7: 9 Nov - 13 Nov ===
'''Biocircuits: Tue, 10a-12p'''
* Shaobin Guo (long)
* Enoch Yeung (short)
'''NCS: Tue, 3p-4p'''
* Ivan Papusha (main)

| width=25% |

=== Week 8: 16 Nov - 20 Nov ===

'''Biocircuits: Thu, 10a-12p'''
* James Parkin (long)
* Yong Wu (short)

'''NCS: Thu, 3:30p-5p'''
* Jiangang Li (main)
* Samira (short)

| width=25% |

=== Week 9: 23 Nov - 27 Nov ===
'''Biocircuits: Tue, 10a-12p'''
* Sean Sanchez (long)
* Tiffany Zhou (short)

|- valign=top
| width=25% |

=== Week 10: 30 Nov - 4 Dec ===
'''NCS: Mon, 10:30a-12p'''
* Samira Farahani (main)
* Open (short)
'''Biocircuits: Tue, 10a-12p'''
* Sam Clamons (long)
* Tina Xu (short)

| width=25% |

=== Week 11: 7 Dec - 11 Dec ===
'''Biocircuits: Tue, 10a-12p'''
* Prakriti Paul (rotation)
* Georgios Artavanis (rotation)
'''NCS: Wed, 10:30a-12p'''
* Benson Christalin (main)
* Open (short)

| width=25% |

=== Week 12: 14 Dec - 18 Dec ===
'''Biocircuits: Tue, 10a-12p'''
* Open (long)
* Open (short)
'''NCS: Wed, 10:30a-12p'''
* Open (main)
* Open (short)
<hr>
CDC (Osaka)
|}

Group Schedule, Spring 2015

2015-03-18T18:16:09Z

Farahani: /* Week 10: 1 Jun - 5 Jun */

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, Winter 2015]]
|}

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=33% |
* Group meetings - 213 ANB
| width=33% |
* Biocircuits subgroup - 111 Keck
| width=33% |
* NCS subgroup - 243 ANB
|}

{| width=100% border=1

|- valign=top
| width=33% |
=== Week 1: 30 Mar - 3 Apr ===
'''NCS: 30 Mar (Mon), 4p-5:30p'''
* Anthony Fragoso (main)
* James Bern (short)
'''Biocircuits: 1 Apr (Wed), 10a-12p'''
* Lab safety (Clare, Richard)
* Yutaka Hori (short)

| width=33% |

=== Week 2: 6 Apr - 10 Apr ===
'''NCS: 6 Apr (Mon), 2:30p-4p'''
* Catharine McGhan (main)
* Open (short)
'''Biocircuits: 8 Apr (Wed), 10a-12p'''
* Emzo de los Santos (long)
* Ania Baetica (short)
| width=33% |

=== Week 3: 13 Apr - 17 Apr ===
* Richard out of town, Mon-Thu
* Biocircuits lab cleanup, Wed @ 10 am
|- valign=top
| width=33% |

=== Week 4: 20 Apr - 24 Apr ===
'''NCS: 20 Apr (Mon), 2:30p-4p
* Yilin Mo (main)
* Open (short)
'''Biocircuits: 22 Apr (Wed), 10a-12p
* Anandh Saminathan (long)
* Victoria Hsiao (short)
| width=33% |

=== Week 5: 27 Apr - 1 May ===
'''Biocircuits: 29 Apr (Wed), 10a-12p'''
* Anu Thubagere (long)
* Dan Siegal (short)
<hr>
* NASA Formal Methods Symposium, Mon-Wed

| width=33% |

=== Week 6: 4 May - 8 May ===
'''NCS: 4 May (Mon), 2:30p-4p
* Ivan Papusha (main)
* Open (short)
'''Biocircuits: 6 May (Wed), 10a-12p'''
* Clare Hayes (long)
* Vipul Singhal (short)
|- valign=top
| width=33% |

=== Week 7: 11 May - 15 May ===
'''NCS: 11 May (Mon), 2:30p-4p
* Vasu Raman (main)
* Open (short)
'''Biocircuits: 13 May (Wed), 10a-12p'''
* Shaobin Guo (long)
* Yong Wu (short)

| width=33% |

=== Week 8: 18 May - 22 May ===
'''Biocircuits: 20 May (Wed), 10a-12p'''
* Zach Sun (long)
* Enoch Yeung (short)
'''NCS: 20 May (Wed), 4-5:30p
* Samira Farahani (main)
* Open (short)

| width=33% |

=== Week 9: 25 May - 29 May ===
'''NCS: 25 May (Mon), 2:30p-4p
* Scott Livingston (main)
* Open (short)
'''Biocircuits: 27 May (Wed), 10a-12p'''
* Rotation student (long)
* Sean Sanchez (short)

|- valign=top
| width=33% |

=== Week 10: 1 Jun - 5 Jun ===
'''NCS: 1 Jun (Mon), 2:30p-4p
* Ioannis Filippidis (main)
* Open (short)
'''Biocircuits: 4 Jun (Thu), 10a-12p'''
* Rotation student (long)
* Tiffany Zhou (short)

| width=33% |

=== Week 11: 8 Jun - 12 Jun ===
'''NCS: 8 Jun (Mon), 2:30p-4p
* Benson Christalin (short)
* Daniel Naftalovich (short)
<hr>
* SEED: Wed-Sat in Boston
| width=33% |

|}

Group Schedule, Spring 2015

2015-03-18T18:15:50Z

Farahani: /* Week 8: 18 May - 22 May */

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, Winter 2015]]
|}

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=33% |
* Group meetings - 213 ANB
| width=33% |
* Biocircuits subgroup - 111 Keck
| width=33% |
* NCS subgroup - 243 ANB
|}

{| width=100% border=1

|- valign=top
| width=33% |
=== Week 1: 30 Mar - 3 Apr ===
'''NCS: 30 Mar (Mon), 4p-5:30p'''
* Anthony Fragoso (main)
* James Bern (short)
'''Biocircuits: 1 Apr (Wed), 10a-12p'''
* Lab safety (Clare, Richard)
* Yutaka Hori (short)

| width=33% |

=== Week 2: 6 Apr - 10 Apr ===
'''NCS: 6 Apr (Mon), 2:30p-4p'''
* Catharine McGhan (main)
* Open (short)
'''Biocircuits: 8 Apr (Wed), 10a-12p'''
* Emzo de los Santos (long)
* Ania Baetica (short)
| width=33% |

=== Week 3: 13 Apr - 17 Apr ===
* Richard out of town, Mon-Thu
* Biocircuits lab cleanup, Wed @ 10 am
|- valign=top
| width=33% |

=== Week 4: 20 Apr - 24 Apr ===
'''NCS: 20 Apr (Mon), 2:30p-4p
* Yilin Mo (main)
* Open (short)
'''Biocircuits: 22 Apr (Wed), 10a-12p
* Anandh Saminathan (long)
* Victoria Hsiao (short)
| width=33% |

=== Week 5: 27 Apr - 1 May ===
'''Biocircuits: 29 Apr (Wed), 10a-12p'''
* Anu Thubagere (long)
* Dan Siegal (short)
<hr>
* NASA Formal Methods Symposium, Mon-Wed

| width=33% |

=== Week 6: 4 May - 8 May ===
'''NCS: 4 May (Mon), 2:30p-4p
* Ivan Papusha (main)
* Open (short)
'''Biocircuits: 6 May (Wed), 10a-12p'''
* Clare Hayes (long)
* Vipul Singhal (short)
|- valign=top
| width=33% |

=== Week 7: 11 May - 15 May ===
'''NCS: 11 May (Mon), 2:30p-4p
* Vasu Raman (main)
* Open (short)
'''Biocircuits: 13 May (Wed), 10a-12p'''
* Shaobin Guo (long)
* Yong Wu (short)

| width=33% |

=== Week 8: 18 May - 22 May ===
'''Biocircuits: 20 May (Wed), 10a-12p'''
* Zach Sun (long)
* Enoch Yeung (short)
'''NCS: 20 May (Wed), 4-5:30p
* Samira Farahani (main)
* Open (short)

| width=33% |

=== Week 9: 25 May - 29 May ===
'''NCS: 25 May (Mon), 2:30p-4p
* Scott Livingston (main)
* Open (short)
'''Biocircuits: 27 May (Wed), 10a-12p'''
* Rotation student (long)
* Sean Sanchez (short)

|- valign=top
| width=33% |

=== Week 10: 1 Jun - 5 Jun ===
'''NCS: 1 Jun (Mon), 2:30p-4p
* Samira Farahani (main)
* Open (short)
'''Biocircuits: 4 Jun (Thu), 10a-12p'''
* Rotation student (long)
* Tiffany Zhou (short)

| width=33% |

=== Week 11: 8 Jun - 12 Jun ===
'''NCS: 8 Jun (Mon), 2:30p-4p
* Benson Christalin (short)
* Daniel Naftalovich (short)
<hr>
* SEED: Wed-Sat in Boston
| width=33% |

|}

Group Schedule, Winter 2015

2015-02-16T07:45:55Z

Farahani: /* Week 7: 16 Feb - 20 Feb */

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, Fall 2014]]
|}

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% |
* Group meetings - 213 ANB
| width=30% |
* Biocircuits subgroup - 111 Keck
| width=30% |
* NCS subgroup - 243 ANBzachza
|}

{| width=100% border=1

|- valign=top
| width=25% |
=== Week 1: 5 Jan - 9 Jan ===
'''Biocircuits: 6 Jan (Tue), 10a-12p'''
* Yutaka Hori (long)
* Lab updates (Richard)
'''NCS: 8 Jan (Thu), 9:30-11a 111 Keck'''
* Anthony Fragoso (main)
* Open (short)
<hr>
* MPP retreat, Fri-Sun (SF)
| width=25% |

=== Week 2: 12 Jan - 16 Jan ===
'''Biocircuits: 12 Jan, 1p - 3p'''
* Ania Baetica (long)
* Emzo de los Santos (short)
<hr>
* AFOSR BRI call: Mon, 8:30a-10a
* iCyPhy BIT mini-workshop: Tue, 8a-5p
* RMM unavailable Wed-Fri

| width=25% |

=== Week 3: 19 Jan - 23 Jan ===
'''Biocircuits: 20 Jan (Tue), 10a-12p'''
* Anandh Swaminathan (short)
* Victoria Hsiao (long)
'''NCS: 22 Jan (Thu), 9:30a-11a 110 Steele'''
* Ivan Papusha (main)
* Open (short)

|- valign=top
| width=25% |

=== Week 4: 26 Jan - 30 Jan ===
'''Biocircuits: 27 Jan (Tue), 10a-12p'''
* Dan Siegal (long)
* Anu Thubagere (short)

'''NCS: 29 Jan (Thu), 9:30a-11a 110 Steele'''
* Yilin Mo (main)
* Open (short)
<hr>
* Brian Munsky visit on Mon
* Rahul Sarpeshkar visit on Mon
* Richard out of town on Wed?

| width=25% |

=== Week 5: 2 Feb - 6 Feb ===
'''NCS: 5 Feb (Thu), 3:30p-5p, 110 Steele'''
* Vasu Raman (main)
* Open (short)
<hr>
* AFOSR BRI telecon: Mon, 8:30a-10a
* iCyPhy planning meeting: Mon-Tue, in Berkeley
* Biocircuits lab cleanup: Tue, 10a-12p

| width=25% |

=== Week 6: 9 Feb - 13 Feb ===
'''Biocircuits: 10 Feb (Tue), 10a-12p'''
* Ye Yuan (long)
* <s>Vanessa Jonsson (short)</s>
'''NCS: 12 Feb (Thu), 9:30a-11a 110 Steele'''
* Cat McGhan (main)
* Cat McGhan (short)
'''Group Meeting: 9 Feb (Mon), 12p-1:15p 121 ANB'''
* Nikolay Atanasov - University of Pennsylvania
<hr>
* Richard out of town on Fri
|- valign=top
| width=25% |

=== Week 7: 16 Feb - 20 Feb ===
'''Biocircuits: 17 Feb (Tue), 10a-12p'''
* Vipul Singhal (long)
* Clare Hayes (short)
'''NCS: 19 Feb (Thu), 9:30a-11a 110 Steele'''
* Ioannis Filippidis (main)
* Samira Farahani (short)
'''Group Meeting: 20 Feb (Fri), 12p-1:15p 107 ANB'''
* Mark Muller - ETH

| width=25% |

=== Week 8: 23 Feb - 27 Feb ===
'''Biocircuits: 23 Feb (Mon), 1p-3p'''
* Yong Wu (long)
* Shaobin Guo (short)
'''NCS: 25 Feb (Wed), 4p-5:30p 114 Steele Library'''
* Scott Livingston
* Open (short)
<hr>
* MPP protocol synthesis workshop: Thu-Fri

| width=25% |

=== Week 9: 2 Mar - 6 Mar ===
'''Biocircuits: 2 Mar (Mon), 1p-3p 114 Steele Library'''
* Enoch Yeung (long)
* Zach Sun (short)
'''NCS: 5 Mar (Thu), 9:30a-11a 110 Steele'''
* Samira Farahani
* Open (short)
<hr>
* Richard out of town Tue-Wed (Seattle)

|- valign=top
| width=25% |

=== Week 10: 9 Mar - 13 Mar===
'''Biocircuits: 9 Mar (Mon), 9a-11a'''
* Henrike N (long)
* Sean Sanchez (short)
'''NCS: 12 Mar (Thu), 9:30a-11a 110 Steele'''
* Daniel Naftalovich (short)
* Benson Christalin (short)
<hr>
* Richard out of town, Tue-Wed (Boston)
* Group camping trip, 13-15 Mar

| width=25% |

=== Week 11: 16 Mar - 20 Mar ===
Finals week
<hr>
* Richard out of town, Mon-Fri
* Biocircuits lab cleanup: Tue, 10a-12p

| width=25% |

=== Week 12: 23 Mar - 27 Mar ===
Spring break
|}

SURF discussions, Jan 2015

2015-01-20T15:54:14Z

Farahani: /* 21 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__

{| width=100% border=1
|- valign=top
|
==== 21 Jan (Wed) ====
* 9:20: Samira and Nuno
* 9:50: Open
<hr>
* 14:30: Rafsan Chowdhury
<hr>
* 15:30: Open
|

==== 22 Jan (Thu) ====
* 9:00: Open
<hr>
* 17:30: Open
* 18:00: Open
|

==== 23 Jan (Fri) ====
* 10:00:Aileen Cheng
<hr>
* 14:00: Open
* 14:30: Open
<hr>
* 16:00: Open
|

==== 26 Jan (Mon) ====
* 8:00: Open
* 8:30: Open
<hr>
* 17:30: Samira, Vasu, Yuening (tentative)
* 18:00: 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 2015: Optimal Trajectory Generation under Environmental Uncertainties using Signal Temporal Logic Specifications

2014-12-29T17:47:44Z

Farahani:

'''[[SURF 2015|2015 SURF]] project description'''
* Mentor: Richard Murray
* Co-mentor: Samira Farahani

In safety-critical robotics applications in which autonomous air, ground, and space vehicles carry out complex tasks, it is important to concisely and unambiguously specify the desired system behavior to be able to automatically synthesize a controller that implements this behavior. Controller synthesis is complicated by the fact that autonomous systems often have high-dimensional, nonlinear dynamics and require efficient (not just feasible) controllers.

This project aims at designing a “correct by construction” controller for an autonomous vehicle that is capable of responding to a dynamic environment, visiting goals, periodically monitoring areas, staying safe, and remaining stable. To this end, we will take advantage of the new tools and techniques for formal specification, design, and verification of embedded control systems [3]. In these approaches, we either verify that a given design satisfies the specification or synthesize a controller that satisfies the specification, as summarized in the following figure.

The formal language that we use in this project is Signal Temporal Logic (STL), which allows the specification of properties of dense-time, real-valued signals. For an efficient implementation, we will directly encode an STL formula as mixed-integer linear constraints on the original dynamical system [2]. Of particular interest are mixed logical dynamical (MLD) systems and certain differentially flat systems, whose dynamics can be encoded with mixed-integer linear constraints. MLD systems include constrained linear systems, linear hybrid automata, and piecewise affine systems. Differentially flat systems include quadrotors and car-like robots.

After the successful design the controller, we are going to perform a detailed comparison of mixed-integer linear programming solvers and Boolean satisfiability solvers that have been extended to support linear operations, e.g., [1]. Moreover, depending on the progress lever, we can also implement the controller on of the available robots in the lab for experimental purposes.

[[File:Agent.png]]

''Required Skills:'' The software we will use for the implementation of formal methods is called TuLiP [4] and the programming language underlying TuLiP is Python. The student is expected to know Matlab and Python or to have enough programming experience to learn it in a short time. Some familiarity with or willingness to learn automata theory, formal languages, and model checking (see for instance to the extent of the first 5 lectures in [5]) is desired.

References:

[1] M. Fränzle and C. Herde. Efficient proof engines for bounded model checking of hybrid systems. Electronic Notes in Theoretical Computer Science, 133:119–137, 2005.
http://homepage.divms.uiowa.edu/~tinelli/classes/AR-group/readingsF04/FMICS04_Fraenzle_Herde.pdf

[2] V. Raman, A. Donzé, M. Maasoumy, R. M. Murray, A. Sangiovanni-Vincentelli, S. A. Seshia, Model Predictive Control with Signal Temporal Logic Specifications, CDC 2014.
http://users.cms.caltech.edu/~vasu/papers/vraman_cdc_14.pdf

[3] E. M. Wolff, U. Topcu, and R. M. Murray, Optimization-based trajectory generation with linear temporal logic specifications, International Conference on Robotics and Automation (ICRA), 2014.
http://www.cds.caltech.edu/~ewolff/wolff_icra14.pdf

[4] Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R.~M. Murray, TuLiP: a software toolbox for receding horizon temporal logic planning, International Conference on Hybrid Systems: Computation and Control, 2011 (software available at http://tulip-control.sourceforge.net).
http://www.aero.umd.edu/~mumu/files/wtoxm_HSCC2011.pdf

[5] EECI, "Specification, Design, and Verification of Distributed Embedded Systems" course website
http://www.cds.caltech.edu/~murray/wiki/index.php/HYCON-EECI,_Spring_2013

SURF 2015: Optimal Trajectory Generation under Environmental Uncertainties using Signal Temporal Logic Specifications

2014-12-29T02:17:18Z

Farahani:

'''[[SURF 2015|2015 SURF]] project description'''
* Mentor: Richard Murray
* Co-mentor: Samira Farahani

In safety-critical robotics applications in which autonomous air, ground, and space vehicles carry out complex tasks, it is important to concisely and unambiguously specify the desired system behavior to be able to automatically synthesize a controller that implements this behavior. Controller synthesis is complicated by the fact that autonomous systems often have high-dimensional, nonlinear dynamics and require efficient (not just feasible) controllers.

This project aims at designing a “correct by construction” controller for an autonomous vehicle that is capable of responding to a dynamic environment, visiting goals, periodically monitoring areas, staying safe, and remaining stable. To this end, we will take advantage of the new tools and techniques for formal specification, design, and verification of embedded control systems [3,4,5,7]. In these approaches, we either verify that a given design satisfies the specification or synthesize a controller that satisfies the specification, as summarized in the following figure.

The formal language that we use in this project is Signal Temporal Logic (STL), which allows the specification of properties of dense-time, real-valued signals. For an efficient implementation, we will directly encode an STL formula as mixed-integer linear constraints on the original dynamical system [6]. Of particular interest are mixed logical dynamical (MLD) systems and certain differentially flat systems [2], whose dynamics can be encoded with mixed-integer linear constraints. MLD systems include constrained linear systems, linear hybrid automata, and piecewise affine systems. Differentially flat systems include quadrotors and car-like robots.

After the successful design the controller, we are going to perform a detailed comparison of mixed-integer linear programming solvers and Boolean satisfiability solvers that have been extended to support linear operations, e.g., [1]. Moreover, depending on the progress lever, we can also implement the controller on of the available robots in the lab for experimental purposes.

[[File:Agent.png]]

''Required Skills:'' The software we will use for the implementation of formal methods is called TuLiP [5] and the programming language underlying TuLiP is Python. The student is expected to know Matlab and Python or to have enough programming experience to learn it in a short time. Some familiarity with or willingness to learn automata theory, formal languages, and model checking (see for instance to the extent of the first 5 lectures in [6]) is desired.

References:

[1] M. Fränzle and C. Herde. Efficient proof engines for bounded model checking of hybrid systems. Electronic Notes in Theoretical Computer Science, 133:119–137, 2005.
http://homepage.divms.uiowa.edu/~tinelli/classes/AR-group/readingsF04/FMICS04_Fraenzle_Herde.pdf

[2] S. M. LaValle. Planning Algorithms. Cambridge Univ. Press, 2006.
http://planning.cs.uiuc.edu/bookbig.pdf

[3] S. Livingston, R. M. Murray, and J. W. Burdick. Backtracking temporal logic synthesis for uncertain environments. In Proc. IEEE International Conference on Robotics and Automation, 2012.
http://scottman.net/pub/Livingston-Murray-Burdick-ICRA2012.pdf

[4] U. Topcu, N. Ozay, J. Liu, , and R. M. Murray. On synthesizing robust discrete controllers under modeling uncertainty. In Hybrid Systems: Computation and Control, 2012.
http://www.cds.caltech.edu/~murray/preprints/tolm12-hscc_s.pdf

[5] E. M. Wolff, U. Topcu, and R. M. Murray, Optimization-based trajectory generation with linear temporal logic specifications, International Conference on Robotics and Automation (ICRA), 2014.
http://www.cds.caltech.edu/~ewolff/wolff_icra14.pdf

[6] V. Raman, A. Donzé, M. Maasoumy, R. M. Murray, A. Sangiovanni-Vincentelli, S. A. Seshia, Model Predictive Control with Signal Temporal Logic Specifications, CDC 2014.
http://users.cms.caltech.edu/~vasu/papers/vraman_cdc_14.pdf

[7] T. Wongpiromsarn, U. Topcu, and R. M. Murray. Receding horizon temporal logic planning. IEEE Transactions on Automatic Control, 57(11):2817{2830, 2012. http://www.seas.upenn.edu/~utopcu/pubs/WTM-itac12.pdf

[8] Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R.~M. Murray, TuLiP: a software toolbox for receding horizon temporal logic planning, International Conference on Hybrid Systems: Computation and Control, 2011 (software available at http://tulip-control.sourceforge.net).
http://www.aero.umd.edu/~mumu/files/wtoxm_HSCC2011.pdf

[9] EECI, "Specification, Design, and Verification of Distributed Embedded Systems" course website
http://www.cds.caltech.edu/~murray/wiki/index.php/HYCON-EECI,_Spring_2013

SURF 2015: Optimal Trajectory Generation under Environmental Uncertainties using Signal Temporal Logic Specifications

2014-12-11T22:29:57Z

Farahani:

Mentor: Richard Murray

Co-mentor: Samira Farahani

The recent planetary decadal survey describes missions that impose tremendously challenging requirements on resilience. The Uninhabited Aerial Vehicles (UAVs) and spacecraft that support these missions will need to be capable of reasoning about their own state and the state of the environment in order to predict and avoid hazardous conditions, to recover from internal failures, and to ultimately meet critical science objectives in the presence of substantial uncertainties.

This project aims at designing a “correct by construction” controller for a UAV to satisfy its mission under the environmental uncertainties. To this end, we will take advantage of the new tools and techniques for formal specification, design, and verification of embedded control systems [1,2,3,4]. In these approaches, we either verify that a given design satisfies the specification or synthesize a controller that satisfies the specification, as summarized in the following figure.

Once the model is designed and tested using computer simulation, it is going to be implemented on one of the UAVs that are available in our lab. The idea is to use this UAV as a benchmark to experiment the effect of environmental changes on the controller and to investigate the responsiveness of the controller to these changes.

[[File:Agent.png]]

''Required Skills:'' The software we will use for the implementation of formal methods is called TuLiP [5] and the programming language underlying TuLiP is Python. The student is expected to know Python or to have enough programming experience to learn it in a short time. Some familiarity with or willingness to learn automata theory, formal languages, and model checking (see for instance to the extent of the first 5 lectures in [6]) is desired.

References:

[1] S. Livingston, R. M. Murray, and J. W. Burdick. Backtracking temporal logic synthesis for uncertain environments. In Proc. IEEE International Conference on Robotics and Automation, 2012.
http://scottman.net/pub/Livingston-Murray-Burdick-ICRA2012.pdf

[2] U. Topcu, N. Ozay, J. Liu, , and R. M. Murray. On synthesizing robust discrete controllers under modeling uncertainty. In Hybrid Systems: Computation and Control, 2012.
http://www.cds.caltech.edu/~murray/preprints/tolm12-hscc_s.pdf

[3] E. M. Wolff, U. Topcu, and R. M. Murray. Robust control of uncertain Markov decision processes with temporal logic speci_cations. In Proc. American Control Conference, 2012.
http://www.cds.caltech.edu/~ewolff/wolff_cdc12.pdf

4] T. Wongpiromsarn, U. Topcu, and R. M. Murray. Receding horizon temporal logic planning. IEEE Transactions on Automatic Control, 57(11):2817{2830, 2012. http://www.seas.upenn.edu/~utopcu/pubs/WTM-itac12.pdf

[5] Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R.~M. Murray, TuLiP: a software toolbox for receding horizon temporal logic planning, International Conference on Hybrid Systems: Computation and Control, 2011 (software available at http://tulip-control.sourceforge.net).
http://www.aero.umd.edu/~mumu/files/wtoxm_HSCC2011.pdf

[6] EECI, "Specification, Design, and Verification of Distributed Embedded Systems" course website
http://www.cds.caltech.edu/~murray/wiki/index.php/HYCON-EECI,_Spring_2013

SURF 2015: Optimal Trajectory Generation under Environmental Uncertainties using Signal Temporal Logic Specifications

2014-12-11T22:27:33Z

Farahani:

The recent planetary decadal survey describes missions that impose tremendously challenging requirements on resilience. The Uninhabited Aerial Vehicles (UAVs) and spacecraft that support these missions will need to be capable of reasoning about their own state and the state of the environment in order to predict and avoid hazardous conditions, to recover from internal failures, and to ultimately meet critical science objectives in the presence of substantial uncertainties.

This project aims at designing a “correct by construction” controller for a UAV to satisfy its mission under the environmental uncertainties. To this end, we will take advantage of the new tools and techniques for formal specification, design, and verification of embedded control systems [1,2,3,4]. In these approaches, we either verify that a given design satisfies the specification or synthesize a controller that satisfies the specification, as summarized in the following figure.

Once the model is designed and tested using computer simulation, it is going to be implemented on one of the UAVs that are available in our lab. The idea is to use this UAV as a benchmark to experiment the effect of environmental changes on the controller and to investigate the responsiveness of the controller to these changes.

[[File:Agent.png]]

''Required Skills:'' The software we will use for the implementation of formal methods is called TuLiP [5] and the programming language underlying TuLiP is Python. The student is expected to know Python or to have enough programming experience to learn it in a short time. Some familiarity with or willingness to learn automata theory, formal languages, and model checking (see for instance to the extent of the first 5 lectures in [6]) is desired.

References:
[1] S. Livingston, R. M. Murray, and J. W. Burdick. Backtracking temporal logic synthesis for uncertain environments. In Proc. IEEE International Conference on Robotics and Automation, 2012.
http://scottman.net/pub/Livingston-Murray-Burdick-ICRA2012.pdf

[2] U. Topcu, N. Ozay, J. Liu, , and R. M. Murray. On synthesizing robust discrete controllers under modeling uncertainty. In Hybrid Systems: Computation and Control, 2012.
http://www.cds.caltech.edu/~murray/preprints/tolm12-hscc_s.pdf

[3] E. M. Wolff, U. Topcu, and R. M. Murray. Robust control of uncertain Markov decision processes with temporal logic speci_cations. In Proc. American Control Conference, 2012.
http://www.cds.caltech.edu/~ewolff/wolff_cdc12.pdf

4] T. Wongpiromsarn, U. Topcu, and R. M. Murray. Receding horizon temporal logic planning. IEEE Transactions on Automatic Control, 57(11):2817{2830, 2012. http://www.seas.upenn.edu/~utopcu/pubs/WTM-itac12.pdf

[5] Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R.~M. Murray, TuLiP: a software toolbox for receding horizon temporal logic planning, International Conference on Hybrid Systems: Computation and Control, 2011 (software available at http://tulip-control.sourceforge.net).
http://www.aero.umd.edu/~mumu/files/wtoxm_HSCC2011.pdf

[6] EECI, "Specification, Design, and Verification of Distributed Embedded Systems" course website
http://www.cds.caltech.edu/~murray/wiki/index.php/HYCON-EECI,_Spring_2013

File:Agent.png

2014-12-11T22:22:19Z

Farahani:

Jin Ge, Dec 2014

2014-12-10T02:07:20Z

Farahani: /* Schedule */

Jin Ge is a graduate student working with Gabor Orosz who will be visiting on 11 Dec (Thu).

=== Schedule ===
* 9:45 am - meet Richard in 109 Steele Lab
* 10 - 12 pm - Networked Control Systems group meeting
* 12-1:30 - group meeting (seminar)
* 1:30 - 2:15: Yilin Mo (Ann 310)
* 2:15 - 3:00: Ioannis Filippidis (Ann 330)
* 3:00 - 3:45: Samira Farahani (Ann 203)
* 3:45 - 4:30: Open

=== Talk info ===
Title: Linear Quadratic Regulation (LQR) for Time-Varying Systems with Delay 
Thu, 12 pm -- 213 Annenberg

In this talk, linear quadratic regulation (LQR) for time-varying systems with delay is used to optimize the control gains for connected cruise control (CCC). We assume that the CCC vehicle receives kinematic information through wireless vehicle-to-vehicle (V2V) communication from several vehicles ahead. An optimized feedback law is obtained by minimizing a cost function defined by distance and velocity errors and the acceleration of the CCC vehicle on an infinite horizon. Communication delays, driver reaction times, and heterogeneity among vehicles are taken into account. We show that the feedback gains can be obtained recursively as signals from vehicles farther ahead become available, and that the optimal gains decay with the number of cars between the source of the signal and the CCC vehicle. To ensure smooth traffic flow the head-to-tail string stability is investigated and the robustness against connectivity loss and delay variations is tested. The analytical results are verified by numerical simulations of connected vehicle systems