EECI 2020: Computer Session: MVP

EECI 2020: Minimum Violation Planning

2020-02-28T18:50:47Z

Nok: Created page with "{{righttoc}} == Lecture Materials == * Lecture slides == Further Reading == * [https://link.springer.com/content/pdf/10.1007%2F3-540-46002-0_30.pdf Temporal debugging fo..."

{{righttoc}}

== Lecture Materials ==
* Lecture slides

== Further Reading ==
* [https://link.springer.com/content/pdf/10.1007%2F3-540-46002-0_30.pdf Temporal debugging for concurrent systems] E.L. Gunter and D. Peled, TACAS 2002. Detail on finite LTL and translation to finite automaton

EECI 2020: Discrete Abstractions

2020-02-27T23:36:36Z

Nok:

{{righttoc}}

This lecture focuses on the abstraction of hybrid systems. We first discuss finite-state under- and over-approximations of hybrid dynamics and how these finite-state models coupled with the model checking tools can be used to verify temporal logic properties against hybrid dynamics. Then, we present a procedure for constructing finite-state, under-approximations which will later be used in the course in the synthesis of hierarchical control protocols.

== Lecture Materials ==
* [https://www.dropbox.com/s/yqjbcink8qzmhsp/L6_Abstractions-2020.pdf?dl=0 Lecture slides]

== Further Reading ==
* [http://robotics.eecs.berkeley.edu/~sastry/ee291e/lygeros.pdf Lecture Notes on Hybrid Systems] (by John Lygeros): A rough introduction to hybrid systems. Chapters 5 and 6 are on various analysis techniques relevant for this short course. 
* [http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf Receding horizon temporal logic planning],T. Wongpiromsarn, U. Topcu, and R. Murray, submitted to IEEE Transactions on Automatic Control, 2010. Details on the receding horizon temporal logic planning. 
* [http://www.cds.caltech.edu/~murray/wiki/index.php/EECI08:_Optimization-Based_Control Optimization based control]. A page prepared for EECI 2008 with information and material on basic receding horizon control.
* [http://control.ee.ethz.ch/~mpt/ Multiparametric Toolbox] The Multi-Parametric Toolbox (MPT) is a free Matlab toolbox for design, analysis and deployment of optimal controllers for constrained linear, nonlinear and hybrid systems. [http://www.cds.caltech.edu/tulip The receding horizon temporal logic planning toolbox] uses the polytope manipulation (intersection, union, set difference, projection, etc.) functionalities of MPT. 
* [http://www.cds.caltech.edu/~utopcu/images//9/98/WTM-aaai10.pdf Automatic synthesis of robust embedded control software], T. Wongpiromsarn, U. Topcu, and R. Murray, AAAI 2010 Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems, 2010. Details on the abstraction procedure covered in this lecture. 
* [http://www.mpc.berkeley.edu/mpc-course-material/BBMbook_Cambridge.pdf?attredirects=0&d=1 Predictive Control]: A book draft by Bemporap, Borrelli, and Morari. Details on some of the ideas in the implementation of the abstraction procedure presented in the slides can be found in this book. 
* [http://www.mpc.berkeley.edu/mpc-course-material/BBMbook_Cambridge.pdf?attredirects=0&d=1 Predictive Control]: A book draft by Bemporap, Borrelli, and Morari. Details on some of the ideas in the implementation of the abstraction procedure presented in the slides can be found in this book. 
* [http://www.cds.caltech.edu/~utopcu/eeci13/ltom-12-cdc.pdf Reactive controllers for differentially flat systems with temporal logic constraints], J. Liu, N. Ozay, U. Topcu, and R. Murray, Control and Decision Conference, 2012.

EECI 2020: Discrete Abstractions

2020-02-27T23:35:42Z

Nok: Created page with "This lecture focuses on the abstraction of hybrid systems. We first discuss finite-state under- and over-approximations of hybrid dynamics and how these finite-state models co..."

This lecture focuses on the abstraction of hybrid systems. We first discuss finite-state under- and over-approximations of hybrid dynamics and how these finite-state models coupled with the model checking tools can be used to verify temporal logic properties against hybrid dynamics. Then, we present a procedure for constructing finite-state, under-approximations which will later be used in the course in the synthesis of hierarchical control protocols.

== Lecture Materials ==
* [https://www.dropbox.com/s/yqjbcink8qzmhsp/L6_Abstractions-2020.pdf?dl=0 Lecture slides]

== Further Reading ==
* [http://robotics.eecs.berkeley.edu/~sastry/ee291e/lygeros.pdf Lecture Notes on Hybrid Systems] (by John Lygeros): A rough introduction to hybrid systems. Chapters 5 and 6 are on various analysis techniques relevant for this short course. 
* [http://www.cds.caltech.edu/~utopcu/images//4/4d/WTM-itac10R.pdf Receding horizon temporal logic planning],T. Wongpiromsarn, U. Topcu, and R. Murray, submitted to IEEE Transactions on Automatic Control, 2010. Details on the receding horizon temporal logic planning. 
* [http://www.cds.caltech.edu/~murray/wiki/index.php/EECI08:_Optimization-Based_Control Optimization based control]. A page prepared for EECI 2008 with information and material on basic receding horizon control.
* [http://control.ee.ethz.ch/~mpt/ Multiparametric Toolbox] The Multi-Parametric Toolbox (MPT) is a free Matlab toolbox for design, analysis and deployment of optimal controllers for constrained linear, nonlinear and hybrid systems. [http://www.cds.caltech.edu/tulip The receding horizon temporal logic planning toolbox] uses the polytope manipulation (intersection, union, set difference, projection, etc.) functionalities of MPT. 
* [http://www.cds.caltech.edu/~utopcu/images//9/98/WTM-aaai10.pdf Automatic synthesis of robust embedded control software], T. Wongpiromsarn, U. Topcu, and R. Murray, AAAI 2010 Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems, 2010. Details on the abstraction procedure covered in this lecture. 
* [http://www.mpc.berkeley.edu/mpc-course-material/BBMbook_Cambridge.pdf?attredirects=0&d=1 Predictive Control]: A book draft by Bemporap, Borrelli, and Morari. Details on some of the ideas in the implementation of the abstraction procedure presented in the slides can be found in this book. 
* [http://www.mpc.berkeley.edu/mpc-course-material/BBMbook_Cambridge.pdf?attredirects=0&d=1 Predictive Control]: A book draft by Bemporap, Borrelli, and Morari. Details on some of the ideas in the implementation of the abstraction procedure presented in the slides can be found in this book. 
* [http://www.cds.caltech.edu/~utopcu/eeci13/ltom-12-cdc.pdf Reactive controllers for differentially flat systems with temporal logic constraints], J. Liu, N. Ozay, U. Topcu, and R. Murray, Control and Decision Conference, 2012.

EECI 2020: Computer Session: Stormpy

2020-02-27T19:50:03Z

Nok:

{{righttoc}}

Hands-on probabilistic model checking exercises using stormpy.
* quantitative analysis of PCTL specifications against Markov chain model
* control strategy synthesis.

== Lecture Materials ==
* [https://www.dropbox.com/s/f7emn3p77w57nx9/C1_probabilistic.pdf?dl=0 Lecture slides]
* * Example files: [https://www.dropbox.com/s/hvk96u652m1m40d/light.pm?dl=0 light.pm], [https://www.dropbox.com/s/8bdi777j6aw8wc8/ma.nm?dl=0 ma.nm], [https://www.dropbox.com/s/1pp4klntys3zyac/mh.pm?dl=0 mh.pm], [https://www.dropbox.com/s/87ec672ifdi5yh5/policy.json?dl=0 policy.json], [https://www.dropbox.com/s/oagkzn0hnfeor2a/analysis_light.py?dl=0 analysis_light.py], [https://www.dropbox.com/s/81weaf5qyqahepa/analysis_compose.py?dl=0 analysis_compose.py], [https://www.dropbox.com/s/c561i4zcdw44p4t/analysis_policy.py?dl=0 analysis_policy.py], [https://www.dropbox.com/s/ctf79j7r34mgud7/synthesis.py?dl=0 synthesis.py]

== Further Reading ==
* [http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 Principles of Model Checking], C. Baier and J.-P. Katoen, The MIT Press, 2008. A detailed reference on model checking. Slides for this lecture follow Chapter 10 of this reference. 
* [https://moves-rwth.github.io/stormpy stormpy]. A comprehensive reference on stormpy 
* [https://www.prismmodelchecker.org/manual/Main/Welcome prism]. For the PRISM Language and properties 

== Additional Information ==

EECI 2020: Probabilistic Systems

2020-02-27T19:44:09Z

EECI-IGSC 2020

2020-02-27T18:55:47Z

Nok:

EECI-IGSC 2020

2020-02-27T18:54:44Z

Nok:

Model-Based Design and Qualification of Complex Systems

2010-06-22T22:47:24Z

Nok: /* Publications */

This is a joint project with [http://crossgroup.caltech.edu/index.html Michael Cross] and [http://www.cmp.caltech.edu/refael/ Gil Refael], funded by Boeing.

{| width=100%
|- valign=top
| Current participants:
* {{Andrea Censi}}
* Dennice Gayme (PhD student, CDS)
* {{Shou Han}}
* Oleg Kogan (PhD student, Physics)
* Tony Lee (PhD student, Physics)
* {{Dominic Rizzo}}
* Heywood Tam (PhD student, Physics)
* {{Pete Trautman}}
* {{Ufuk Topcu}}
* {{Nok Wongpiromsarn}}
| Past participants:
* David Alderson (CDS postdoc, NPS)
* {{Julia Braman}}
* Lijun Chen (CDS PhD, postdoc)
* Lars Cremean (ME PhD, Aerovironment)
* Stefano di Cairano (Visiting student, U. Siena)
* [http://www.cds.caltech.edu/~doyle John Doyle]
* Michael Epstein (PhD student, ME)
* Tamas Keviczky (postdoc, CDS)
* Dimitry Kogan (CDS MS)
* Lun Li (PhD student, EE)
* Alfred Martinez (PhD student, CDS)
* Stephen Prajna (CDS PhD)
* Demetri Spanos (PhD student, CDS)
* {{Johan Ugander}}
* Fei Wang (EE PhD; on leave)
|
__TOC__
|}

== Objectives ==

The broad goal of this project is to develop new theory, algorithms
and demonstrations of model-based design strategies for complex
systems. This activity is broken up into three broad themes:
* ''Systems Modeling Theory and Practice:'' Development of modeling and analysis tools, with emphasis on hierarchies of simulations that can be used for verification and testing at different levels of fidelity. A key issue is the development of multiple simulations that can be combined to form high fidelity models while at the same time being used in simpler combinations for rapid testing of higher level functions (where highly detailed models are too large or too slow to allow exploration of the relevant design space). 

* ''Engineering Implementation:'' Apply analysis and methods in robust-yet-fragile behavior and multi-scale modeling to specific engineering systems of systems that will provide an evaluation of the efficacy of both the framework and the tools toward applications. Two specific testbeds are being used for this purpose: the Caltech multi-vehicle wireless testbed (MVWT) and the Caltech autonomous vehicle testbed ("Alice").

* ''Multiscale Analysis of Complex Systems:'' Study novel approaches to multiscale analysis based on methodologies and techniques developed for physical dynamical systems. To develop the required methodologies and techniques we are focusing on an archetype complex system which may contain a multitude of scales, namely collections of disparate coupled nonlinear oscillators where each oscillator may have its own natural frequency. 

== Publications ==
'''2009-10'''
* Shuo Han, Andrea Censi, Andrew D. Straw, and Richard M. Murray, "A bio-plausible design for visual pose stabilization", International Conference on Intelligent Robots and Systems (IROS), 2010 (to appear).
* Peter Trautman and Andreas Krause, "Unfreezing the Robot: Navigation in Dense, Interacting Crowds". International Conference on Intelligent Robots and Systems, 2010 (submitted).
* Ufuk Topcu, T. Sullivan, M. McKerns, and H. Owhadi, "Uncertainty quantification via codimension-one partitioning". ''International Journal on Numerical Methods in Engineering'', 2010 (submitted)
* Ufuk Topcu, L. Lucas, H. Owhadi, and M. Ortiz, "Rigorous uncertainty quantification without integral testing". ''Reliability Engineering and System Safety'', 2010 (submitted).
* Nok Wongpiromsarn, Sayan Mitra, Richard M. Murray, and Andrew Lamperski. "Verification of Periodically Controlled Hybrid Systems: Application to An Autonomous Vehicle". ''ACM Transactions in Embedded Computing Systems (ACM TECS), Special Issue on the Verification of Cyber-Physical Software Systems'' (accepted).
* Nok Wongpiromsarn, Ufuk Topcu, and Richard M. Murray. "Receding Horizon Temporal Logic Planning". ''IEEE Transactions on Automatic Control'' (submitted).
* Nok Wongpiromsarn, Ufuk Topcu and Richard M. Murray, "Automatic synthesis of robust embedded control software". Proceedings of the AAAI 2010 Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems.
* Nok Wongpiromsarn, Ufuk Topcu and Richard M. Murray, "Receding horizon control for temporal logic specifications". Proceedings of the International Conference on Hybrid Systems: Computation and Control (HSCC), 2010.
* Nok Wongpiromsarn, Ufuk Topcu and Richard M. Murray, "Receding horizon temporal logic planning for dynamical systems". Conference on Decision and Control (CDC), 2009.
* Ufuk Topcu, Andrew Packard and Richard M. Murray, "Compositional stability analysis based on dual decomposition". Conference Decision and Control (CDC), 2009.

'''2008-09'''
* Julia M B Braman, Richard M Murray, "Automatic Conversion Software for the Safety Verification of Goal-Based Control Programs." International Conference on Software Engineering, 2009 (submitted).

* Julia M B Braman, Richard M Murray, "Control Program Verification for a Sample Titan Aerobot Mission." AIAA Infotech@Aerospace Conference, 2009 (submitted).

* Julia M B Braman, Richard M Murray, "Probabilistic Safety Analysis of Sensor-Driven Hybrid Automata." International Conference on Hybrid Systems: Computation and Control, 2009 (submitted).

* Tichakorn Wongpiromsarn, Sayan Mitra, Richard M. Murray, Andrew Lamperski, Verification of Periodically Controlled Hybrid Systems: Application to An Autonomous Vehicle. ACM Transactions in Embedded Computing Systems (ACM TECS), Special Issue on the Verification of Cyber-Physical Software Systems (submitted).

* Tichakorn Wongpiromsarn, Ufuk Topcu, Richard M. Murray, Receding Horizon Temporal Logic Planning for Dynamical Systems. Conference on Decision and Control (CDC), 2009 (submitted).

* Tichakorn Wongpiromsarn, Sayan Mitra, Richard M. Murray, Andrew Lamperski, [http://www.cds.caltech.edu/~murray/papers/2008r_wmml09-hscc.html Periodically Controlled Hybrid Systems: Verifying A Controller for An Autonomous Vehicle]. International Conference on Hybrid Systems: Computation and Control, 2009.

* Tichakorn Wongpiromsarn, Sayan Mitra, Richard M. Murray, Andrew Lamperski, [http://resolver.caltech.edu/CaltechCDSTR:2008.003 Periodically Controlled Hybrid Systems: Verifying A Controller for An Autonomous Vehicle]. CDS Technical Report, California Institute of Technology, 2008.

'''2007-08'''
* Julia M B Braman, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2008f_bm08-cdc.html Failure Probability of Verifiable Goal-based Control Programs due to State Estimation Uncertainty]. Conference on Decision and Control, 2008 (submitted).

* Julia M B Braman, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2007u_bm07-cds.html Conversion and Verification Procedure for Goal-Based Control Programs]. CDS Technical Report, California Institute of Technology, 2007.

* Julia M B Braman, Richard M Murray, David A Wagner, [http://www.cds.caltech.edu/~murray/papers/2007t_bmw07-iros.html Safety Verification of a Fault Tolerant Reconfigurable Autonomous Goal-Based Robotic Control System]. IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2007

* Julia M B Braman, Richard M Murray, Michel D Ingham, [http://www.cds.caltech.edu/~murray/papers/2007s_bmi07-infotech.html Verification Procedure for Generalized Goal-based Control Programs]. AIAA Infotech@Aerospace Conference and Exhibit, 2007.

* Julia M B Braman, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2007n_bm08-acc.html Safety Verification of Fault Tolerant Goal-based Control Programs with Estimation Uncertainty]. American Control Conference, 2008 (to appear).

* Julia M B Braman, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2007i_bm08-iros.html Automatic Conversion Software for the Safety Verification of Goal-based Control Programs]. Proceedings of the International Conference on Intelligent Robots and Systems, 2008 (submitted).

* Joel W Burdick, Noel duToit, Andrew Howard, Christian Looman, Jeremy Ma, Richard M Murray and Tichakorn Wongpiromsarn, [http://gc.caltech.edu/media/papers/dgc07-final.pdf Sensing, Navigation and Reasoning Technologies for the DARPA Urban Challenge], DARPA Urban Challenge Final Report, 2007.

* L. Chen, S. H. Low and J. C. Doyle, "Contention Control: A Game-theoretic Approach". Proceedings of IEEE CDC, December 2007.

* L. Chen, T. Cui, S. H. Low and J. C. Doyle, "A Game-Theoretic Model for Medium Access Control". Proceedings of International Wireless Internet Conference, October 2007.

* T. Cui, L. Chen, T. Ho, S. Low and L. Andrew, "Opportunistic Source Coding for Data Gathering in Wireless Sensor Networks,". Proceedings of IEEE Conference on Mobile Ad-hoc and Sensor Systems, October 2007.

* T. Cui, L. Chen and T. Ho, "Distributed Optimization in Wireless Networks Using Broadcast Advantage". Proceedings of IEEE CDC, December 2007.

* T. Cui, L. Chen and T. Ho, "Optimization Based Rate Control for Multicast with Network Coding: A Multipath Formulation". Proceedings of IEEE CDC, December 2007.

* T. Cui, T. Ho and L. Chen, "Distributed Minimum Cost Multicasting with Lossless Source Coding and Network Coding". Proceedings of IEEE CDC, December 2007.

* T. Cui, L. Chen and T. Ho, "Energy Efficient Opportunistic Network Coding for Wireless Networks". Proceedings of IEEE Infocom, April 2008.

* Noel E DuToit, Tichakorn Wongpiromsarn, Joel W Burdick, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2008c_dwbm08-ivcs.html Situational Reasoning for Road Driving in an Urban Environment]. International Workshop on Intelligent Vehicle Control Systems (IVCS), 2008 (to appear).

* Michael Epstein, Ling Shi, Abhishek Tiwari, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2008i_estm08-automatica.html Probabilistic Performance of State Estimation Across a Lossy Network]. Automatica, 2008 (to appear).

* Michael Epstein, Ling Shi, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2007w_esm07-cdc.html Estimation schemes for networked control systems using UDP-like communication]. Conference on Decision and Control (CDC), 3945 - 3951, 2007.

* Michael Epstein, Kevin Lynch, Karl Henrik Johansson, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2007p_eljm08-ifac.html Using Hierarchical Decomposition to Speed Up Average Consensus]. International Federation of Automatic Control (IFAC) World Congress, 2008 (to appear).

* Oleg Kogan, J. L. Rogers, Gil Refael, and M. C. Cross, "Renormalization group method for predicting frequency clusters in a chain of nearest-neighbor Kuramoto oscillators", 2008 (in preparation).

* Tichakorn Wongpiromsarn, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2008h_wm08-cdc.html Formal Verification of an Autonomous Vehicle System]. Conference on Decision and Control, 2008 (submitted).

* Tichakorn Wongpiromsarn, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2008d_wm08-ivcs.html Distributed Mission and Contingency Management for the DARPA Urban Challenge]. International Workshop on Intelligent Vehicle Control Systems (IVCS), 2008 (to appear).

'''2006-07'''
* D. Alderson and L. Li. [http://www.cds.caltech.edu/~lun/publications/PRE06.pdf On the Diversity of Graph with Highly Variable Connectivity]. ''Physical Review E'', 2007.

* F. Borrelli and T. Keviczky. Distributed LQR design for identical dynamically decoupled systems. ''IEEE Trans. Automatic Control'', 2007, submitted.


* L. Chen, T. Ho, S. H. Low, M. Chiang and J. C. Doyle, Optimization Based Rate Control for Multicast with Network Coding, Proceedings of IEEE Infocom, 2007.

* L. B. Cremean, T. B. Foote, J. H. Gillula, G. H. Hines, D. Kogan, K. L. Kriechbaum, J. C. Lamb, J. Leibs, L. Lindzey, C. E. Rasmussen, A. D. Stewart, J. W. Burdick, and R. M. Murray. {{htdb|2005t_cre+06-jfr|Alice: An information-rich autonomous vehicle for high-speed desert navigation}}. ''Journal of Field Robotics'', 2007.

* T. Cui, T. Ho and L. Chen, On Distributed Distortion Optimization for Correlated Sources with Network Coding, Proceedings of IEEE ISIT, 2007.

* T. Cui, L. Chen and T. Ho, Opportunistic Source Coding for Data Gathering in Wireless Sensor Networks, technical report, 2007.

* J.-C. Delvenne, H. Sandberg, and J. C. Doyle. Thermodynamics of Linear Systems. In ''Proceedings of the European Control Conference'', 2007.

* D. Gayme, "Streamwise Constant Model of Turbulence Statistics in Plane Couette Flow". CDS Candidacy Report, May 2008.

* D. Gayme, B. McKeon, A. Papachristodoulou, B. Bamieh and J.C. Doyle, "Streamwise Constant Model of Turbulence Statistics in Plane Couette Flow", Under preparation for journal submission, 2008.

* H. Sandberg, J.-C. Delvenne, and J. C. Doyle. The Statistical Mechanics of Fluctuation-Dissipation and Measurement Back Action. In ''Proceedings of the American Control Conference'', 2007.

* H. Sandberg, J.-C. Delvenne, and J. C. Doyle. Linear-Quadratic-Gaussian Heat Engines. Submitted, 2007.

* H. Sandberg and R. M. Murray. Frequency-Weighted Model Reduction with Applications to Structured Models. In ''Proceedings of the American Control Conference'', 2007.

* J. Wang, L. Li, S. H. Low, and J. C. Doyle. Cross-layer optimization in tcp/ip networks. ''IEEE/ACM Transactions on Networking'', 13(3), 2006.

'''2005-06'''
* D. Alderson, L. Li, W. Willinger, and J. C. Doyle. Understanding Internet topology: Principles, models, and validation. ''IEEE/ACM Transactions on Networking'', 13(6), 2005.

* D. Alderson and W. Willinger. A contrasting look at self-organization in the Internet and next-generation communication networks. ''IEEE Communications Magazine'', July 2005.

* L. Chen, S. H. Low, M. Chiang, and J. C. Doyle. Cross-layer congestion control, routing and scheduling design in ad hoc wireless networks. In ''Proceedings of IEEE Infocom'', 2006.

* L. Chen, S. H. Low, and J. C. Doyle. Joint congestion control and media access control design for wireless ad hoc networks. In ''Proceedings of IEEE Infocom'', 2005.

* L. Chen, S. H. Low and J. C. Doyle, Random Access Game and Medium Access Control Design, submitted, technical report, 2006.

* J. C. Doyle, D. Alderson, L. Li, S. Low, M. Roughan, S. Shalunov, R. Tanaka, and W. Willinger. The ``robust yet fragile'' nature of the Internet. ''Proceedings of the National Academy of Sciences'', 102(41):14497--14502, 2005.

* D. Gayme, J. C Doyle, S. Prajna, A. Papachristodoulou, and Maryam Fazel. Optimization based methods for determining basins of attraction in the logistic map and set membership in the mandelbrot set. Preprint, 2006.

* D. Gayme, M. Fazel, and J. C. Doyle. Sos proofs of invariant regions in the logistic map. In ''Proc. IEEE Control and Decision Conference'', 2006. Submitted.

* S. Glavaski, A. Papachristodoulou, and K. Ariyur. Safety verification of controlled advanced life support system using barrier certificates. In ''Hybrid Systems: Computation and Control'', 2005.

* D. Kogan. Realtime path planning through optimization methods. Master's thesis, California Institute of Technology, 2005.

* L. Li, D. Alderson, J. C. Doyle and W. Willinger. [http://www.cds.caltech.edu/~lun/publications/IM06.pdf Towards a Theory of Scale-Free Graphs: Definition, Properties, and Implications]. ''Internet Mathematics'' 2(4), p 431-523, Mar. 2006.

* L. Li, D. Alderson, W. Willinger and J. C. Doyle. [http://www.cds.caltech.edu/~lun/publications/sigcomm04.pdf A First-Principles Approach to Understanding the Internet's Router-level Topology]. Proceedings of ACM Sigcomm, 2004,

* S. H. Low, J. C. Doyle, L. Li, A. Tang, J. Wang, Optimization Model of Internet Protocols, Proceedings of ACM Sigmetrics, June 2005.

* S. Prajna and A. Jadbabaie. Safety verification of hybrid systems using barrier certificates. In ''Hybrid Systems: Computation and Control'', 2004.

* S. Prajna and A. Jadbabaie. Methods for safety verification of time-delay systems. In ''Proceedings of the IEEE Conference on Decision and Control'', 2005.

* S. Prajna, A. Jadbabaie, and G. J. Pappas. Stochastic safety verification using barrier certificates. In ''Proceedings of the IEEE Conference on Decision and Control'', 2004.

* S. Prajna, A. Papachristodoulou, P. J. Seiler, and P. A. Parrilo. SOSTOOLS -- Sum of Squares Optimization Toolbox, User's Guide. Available at http://www.cds.caltech.edu/sostools and http://www.mit.edu/~parrilo/sostools, 2002, 2004.

* S. Prajna and A. Rantzer. On the necessity of barrier certificates. In ''Proceedings of the IFAC World Congress'', 2005.

* S. Prajna and A. Rantzer. Primal-dual tests for safety and reachability. In ''Hybrid Systems: Computation and Control''. Springer-Verlag, 2005.

== Reports ==
* [[Media:boeing_report-may08.pdf|Annual report, May 2007 to April 2008]]
* [[Media:boeing_report-mar06.pdf|Annual report, January 2005 to March 2006]]
* [[Media:boeing_report-apr06.pdf|Annual report, March 2006 to April 2007]]

== Software ==
* SOSTOOLS

== Related Activities ==
* [[Connections II]] - Workshop on Foundations of Network Science (Caltech, August 2006)
* [http://www.cds.caltech.edu/~murray/VaVmuri V&V MURI] - Specification, Design and Verification of Distributed Embedded Systems (AFOSR MURI)
* [[Workshop: Specification and Verification of Embedded Systems]] - (Caltech, October 2008)
* [[Caltech Workshop on Verification and Validation]] - September 23-24, 2009

Model-Based Design and Qualification of Complex Systems

2010-06-22T22:46:21Z

Nok: /* Publications */

This is a joint project with [http://crossgroup.caltech.edu/index.html Michael Cross] and [http://www.cmp.caltech.edu/refael/ Gil Refael], funded by Boeing.

{| width=100%
|- valign=top
| Current participants:
* {{Andrea Censi}}
* Dennice Gayme (PhD student, CDS)
* {{Shou Han}}
* Oleg Kogan (PhD student, Physics)
* Tony Lee (PhD student, Physics)
* {{Dominic Rizzo}}
* Heywood Tam (PhD student, Physics)
* {{Pete Trautman}}
* {{Ufuk Topcu}}
* {{Nok Wongpiromsarn}}
| Past participants:
* David Alderson (CDS postdoc, NPS)
* {{Julia Braman}}
* Lijun Chen (CDS PhD, postdoc)
* Lars Cremean (ME PhD, Aerovironment)
* Stefano di Cairano (Visiting student, U. Siena)
* [http://www.cds.caltech.edu/~doyle John Doyle]
* Michael Epstein (PhD student, ME)
* Tamas Keviczky (postdoc, CDS)
* Dimitry Kogan (CDS MS)
* Lun Li (PhD student, EE)
* Alfred Martinez (PhD student, CDS)
* Stephen Prajna (CDS PhD)
* Demetri Spanos (PhD student, CDS)
* {{Johan Ugander}}
* Fei Wang (EE PhD; on leave)
|
__TOC__
|}

== Objectives ==

The broad goal of this project is to develop new theory, algorithms
and demonstrations of model-based design strategies for complex
systems. This activity is broken up into three broad themes:
* ''Systems Modeling Theory and Practice:'' Development of modeling and analysis tools, with emphasis on hierarchies of simulations that can be used for verification and testing at different levels of fidelity. A key issue is the development of multiple simulations that can be combined to form high fidelity models while at the same time being used in simpler combinations for rapid testing of higher level functions (where highly detailed models are too large or too slow to allow exploration of the relevant design space). 

* ''Engineering Implementation:'' Apply analysis and methods in robust-yet-fragile behavior and multi-scale modeling to specific engineering systems of systems that will provide an evaluation of the efficacy of both the framework and the tools toward applications. Two specific testbeds are being used for this purpose: the Caltech multi-vehicle wireless testbed (MVWT) and the Caltech autonomous vehicle testbed ("Alice").

* ''Multiscale Analysis of Complex Systems:'' Study novel approaches to multiscale analysis based on methodologies and techniques developed for physical dynamical systems. To develop the required methodologies and techniques we are focusing on an archetype complex system which may contain a multitude of scales, namely collections of disparate coupled nonlinear oscillators where each oscillator may have its own natural frequency. 

== Publications ==
'''2009-10'''
* Shuo Han, Andrea Censi, Andrew D. Straw, and Richard M. Murray, "A bio-plausible design for visual pose stabilization", International Conference on Intelligent Robots and Systems (IROS), 2010 (to appear).
* Peter Trautman and Andreas Krause, "Unfreezing the Robot: Navigation in Dense, Interacting Crowds". International Conference on Intelligent Robots and Systems, 2010 (submitted).
* Ufuk Topcu, T. Sullivan, M. McKerns, and H. Owhadi, "Uncertainty quantification via codimension-one partitioning". ''International Journal on Numerical Methods in Engineering'', 2010 (submitted)
* Ufuk Topcu, L. Lucas, H. Owhadi, and M. Ortiz, "Rigorous uncertainty quantification without integral testing". ''Reliability Engineering and System Safety'', 2010 (submitted).
* Nok Wongpiromsarn, Sayan Mitra, Richard M. Murray, and Andrew Lamperski. Verification of Periodically Controlled Hybrid Systems: Application to An Autonomous Vehicle. ACM Transactions in Embedded Computing Systems (ACM TECS), Special Issue on the Verification of Cyber-Physical Software Systems (accepted).
* Nok Wongpiromsarn, Ufuk Topcu, and Richard M. Murray. "Receding Horizon Temporal Logic Planning". IEEE Transactions on Automatic Control (submitted).
* Nok Wongpiromsarn, Ufuk Topcu and Richard M. Murray, "Automatic synthesis of robust embedded control software". Proceedings of the AAAI 2010 Spring Symposium on Embedded Reasoning: Intelligence in Embedded Systems.
* Nok Wongpiromsarn, Ufuk Topcu and Richard M. Murray, "Receding horizon control for temporal logic specifications". Proceedings of the International Conference on Hybrid Systems: Computation and Control (HSCC), 2010.
* Nok Wongpiromsarn, Ufuk Topcu and Richard M. Murray, "Receding horizon temporal logic planning for dynamical systems". Conference on Decision and Control (CDC), 2009.
* Ufuk Topcu, Andrew Packard and Richard M. Murray, "Compositional stability analysis based on dual decomposition". Conference Decision and Control (CDC), 2009.

'''2008-09'''
* Julia M B Braman, Richard M Murray, "Automatic Conversion Software for the Safety Verification of Goal-Based Control Programs." International Conference on Software Engineering, 2009 (submitted).

* Julia M B Braman, Richard M Murray, "Control Program Verification for a Sample Titan Aerobot Mission." AIAA Infotech@Aerospace Conference, 2009 (submitted).

* Julia M B Braman, Richard M Murray, "Probabilistic Safety Analysis of Sensor-Driven Hybrid Automata." International Conference on Hybrid Systems: Computation and Control, 2009 (submitted).

* Tichakorn Wongpiromsarn, Sayan Mitra, Richard M. Murray, Andrew Lamperski, Verification of Periodically Controlled Hybrid Systems: Application to An Autonomous Vehicle. ACM Transactions in Embedded Computing Systems (ACM TECS), Special Issue on the Verification of Cyber-Physical Software Systems (submitted).

* Tichakorn Wongpiromsarn, Ufuk Topcu, Richard M. Murray, Receding Horizon Temporal Logic Planning for Dynamical Systems. Conference on Decision and Control (CDC), 2009 (submitted).

* Tichakorn Wongpiromsarn, Sayan Mitra, Richard M. Murray, Andrew Lamperski, [http://www.cds.caltech.edu/~murray/papers/2008r_wmml09-hscc.html Periodically Controlled Hybrid Systems: Verifying A Controller for An Autonomous Vehicle]. International Conference on Hybrid Systems: Computation and Control, 2009.

* Tichakorn Wongpiromsarn, Sayan Mitra, Richard M. Murray, Andrew Lamperski, [http://resolver.caltech.edu/CaltechCDSTR:2008.003 Periodically Controlled Hybrid Systems: Verifying A Controller for An Autonomous Vehicle]. CDS Technical Report, California Institute of Technology, 2008.

'''2007-08'''
* Julia M B Braman, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2008f_bm08-cdc.html Failure Probability of Verifiable Goal-based Control Programs due to State Estimation Uncertainty]. Conference on Decision and Control, 2008 (submitted).

* Julia M B Braman, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2007u_bm07-cds.html Conversion and Verification Procedure for Goal-Based Control Programs]. CDS Technical Report, California Institute of Technology, 2007.

* Julia M B Braman, Richard M Murray, David A Wagner, [http://www.cds.caltech.edu/~murray/papers/2007t_bmw07-iros.html Safety Verification of a Fault Tolerant Reconfigurable Autonomous Goal-Based Robotic Control System]. IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2007

* Julia M B Braman, Richard M Murray, Michel D Ingham, [http://www.cds.caltech.edu/~murray/papers/2007s_bmi07-infotech.html Verification Procedure for Generalized Goal-based Control Programs]. AIAA Infotech@Aerospace Conference and Exhibit, 2007.

* Julia M B Braman, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2007n_bm08-acc.html Safety Verification of Fault Tolerant Goal-based Control Programs with Estimation Uncertainty]. American Control Conference, 2008 (to appear).

* Julia M B Braman, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2007i_bm08-iros.html Automatic Conversion Software for the Safety Verification of Goal-based Control Programs]. Proceedings of the International Conference on Intelligent Robots and Systems, 2008 (submitted).

* Joel W Burdick, Noel duToit, Andrew Howard, Christian Looman, Jeremy Ma, Richard M Murray and Tichakorn Wongpiromsarn, [http://gc.caltech.edu/media/papers/dgc07-final.pdf Sensing, Navigation and Reasoning Technologies for the DARPA Urban Challenge], DARPA Urban Challenge Final Report, 2007.

* L. Chen, S. H. Low and J. C. Doyle, "Contention Control: A Game-theoretic Approach". Proceedings of IEEE CDC, December 2007.

* L. Chen, T. Cui, S. H. Low and J. C. Doyle, "A Game-Theoretic Model for Medium Access Control". Proceedings of International Wireless Internet Conference, October 2007.

* T. Cui, L. Chen, T. Ho, S. Low and L. Andrew, "Opportunistic Source Coding for Data Gathering in Wireless Sensor Networks,". Proceedings of IEEE Conference on Mobile Ad-hoc and Sensor Systems, October 2007.

* T. Cui, L. Chen and T. Ho, "Distributed Optimization in Wireless Networks Using Broadcast Advantage". Proceedings of IEEE CDC, December 2007.

* T. Cui, L. Chen and T. Ho, "Optimization Based Rate Control for Multicast with Network Coding: A Multipath Formulation". Proceedings of IEEE CDC, December 2007.

* T. Cui, T. Ho and L. Chen, "Distributed Minimum Cost Multicasting with Lossless Source Coding and Network Coding". Proceedings of IEEE CDC, December 2007.

* T. Cui, L. Chen and T. Ho, "Energy Efficient Opportunistic Network Coding for Wireless Networks". Proceedings of IEEE Infocom, April 2008.

* Noel E DuToit, Tichakorn Wongpiromsarn, Joel W Burdick, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2008c_dwbm08-ivcs.html Situational Reasoning for Road Driving in an Urban Environment]. International Workshop on Intelligent Vehicle Control Systems (IVCS), 2008 (to appear).

* Michael Epstein, Ling Shi, Abhishek Tiwari, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2008i_estm08-automatica.html Probabilistic Performance of State Estimation Across a Lossy Network]. Automatica, 2008 (to appear).

* Michael Epstein, Ling Shi, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2007w_esm07-cdc.html Estimation schemes for networked control systems using UDP-like communication]. Conference on Decision and Control (CDC), 3945 - 3951, 2007.

* Michael Epstein, Kevin Lynch, Karl Henrik Johansson, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2007p_eljm08-ifac.html Using Hierarchical Decomposition to Speed Up Average Consensus]. International Federation of Automatic Control (IFAC) World Congress, 2008 (to appear).

* Oleg Kogan, J. L. Rogers, Gil Refael, and M. C. Cross, "Renormalization group method for predicting frequency clusters in a chain of nearest-neighbor Kuramoto oscillators", 2008 (in preparation).

* Tichakorn Wongpiromsarn, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2008h_wm08-cdc.html Formal Verification of an Autonomous Vehicle System]. Conference on Decision and Control, 2008 (submitted).

* Tichakorn Wongpiromsarn, Richard M Murray, [http://www.cds.caltech.edu/~murray/papers/2008d_wm08-ivcs.html Distributed Mission and Contingency Management for the DARPA Urban Challenge]. International Workshop on Intelligent Vehicle Control Systems (IVCS), 2008 (to appear).

'''2006-07'''
* D. Alderson and L. Li. [http://www.cds.caltech.edu/~lun/publications/PRE06.pdf On the Diversity of Graph with Highly Variable Connectivity]. ''Physical Review E'', 2007.

* F. Borrelli and T. Keviczky. Distributed LQR design for identical dynamically decoupled systems. ''IEEE Trans. Automatic Control'', 2007, submitted.


* L. Chen, T. Ho, S. H. Low, M. Chiang and J. C. Doyle, Optimization Based Rate Control for Multicast with Network Coding, Proceedings of IEEE Infocom, 2007.

* L. B. Cremean, T. B. Foote, J. H. Gillula, G. H. Hines, D. Kogan, K. L. Kriechbaum, J. C. Lamb, J. Leibs, L. Lindzey, C. E. Rasmussen, A. D. Stewart, J. W. Burdick, and R. M. Murray. {{htdb|2005t_cre+06-jfr|Alice: An information-rich autonomous vehicle for high-speed desert navigation}}. ''Journal of Field Robotics'', 2007.

* T. Cui, T. Ho and L. Chen, On Distributed Distortion Optimization for Correlated Sources with Network Coding, Proceedings of IEEE ISIT, 2007.

* T. Cui, L. Chen and T. Ho, Opportunistic Source Coding for Data Gathering in Wireless Sensor Networks, technical report, 2007.

* J.-C. Delvenne, H. Sandberg, and J. C. Doyle. Thermodynamics of Linear Systems. In ''Proceedings of the European Control Conference'', 2007.

* D. Gayme, "Streamwise Constant Model of Turbulence Statistics in Plane Couette Flow". CDS Candidacy Report, May 2008.

* D. Gayme, B. McKeon, A. Papachristodoulou, B. Bamieh and J.C. Doyle, "Streamwise Constant Model of Turbulence Statistics in Plane Couette Flow", Under preparation for journal submission, 2008.

* H. Sandberg, J.-C. Delvenne, and J. C. Doyle. The Statistical Mechanics of Fluctuation-Dissipation and Measurement Back Action. In ''Proceedings of the American Control Conference'', 2007.

* H. Sandberg, J.-C. Delvenne, and J. C. Doyle. Linear-Quadratic-Gaussian Heat Engines. Submitted, 2007.

* H. Sandberg and R. M. Murray. Frequency-Weighted Model Reduction with Applications to Structured Models. In ''Proceedings of the American Control Conference'', 2007.

* J. Wang, L. Li, S. H. Low, and J. C. Doyle. Cross-layer optimization in tcp/ip networks. ''IEEE/ACM Transactions on Networking'', 13(3), 2006.

'''2005-06'''
* D. Alderson, L. Li, W. Willinger, and J. C. Doyle. Understanding Internet topology: Principles, models, and validation. ''IEEE/ACM Transactions on Networking'', 13(6), 2005.

* D. Alderson and W. Willinger. A contrasting look at self-organization in the Internet and next-generation communication networks. ''IEEE Communications Magazine'', July 2005.

* L. Chen, S. H. Low, M. Chiang, and J. C. Doyle. Cross-layer congestion control, routing and scheduling design in ad hoc wireless networks. In ''Proceedings of IEEE Infocom'', 2006.

* L. Chen, S. H. Low, and J. C. Doyle. Joint congestion control and media access control design for wireless ad hoc networks. In ''Proceedings of IEEE Infocom'', 2005.

* L. Chen, S. H. Low and J. C. Doyle, Random Access Game and Medium Access Control Design, submitted, technical report, 2006.

* J. C. Doyle, D. Alderson, L. Li, S. Low, M. Roughan, S. Shalunov, R. Tanaka, and W. Willinger. The ``robust yet fragile'' nature of the Internet. ''Proceedings of the National Academy of Sciences'', 102(41):14497--14502, 2005.

* D. Gayme, J. C Doyle, S. Prajna, A. Papachristodoulou, and Maryam Fazel. Optimization based methods for determining basins of attraction in the logistic map and set membership in the mandelbrot set. Preprint, 2006.

* D. Gayme, M. Fazel, and J. C. Doyle. Sos proofs of invariant regions in the logistic map. In ''Proc. IEEE Control and Decision Conference'', 2006. Submitted.

* S. Glavaski, A. Papachristodoulou, and K. Ariyur. Safety verification of controlled advanced life support system using barrier certificates. In ''Hybrid Systems: Computation and Control'', 2005.

* D. Kogan. Realtime path planning through optimization methods. Master's thesis, California Institute of Technology, 2005.

* L. Li, D. Alderson, J. C. Doyle and W. Willinger. [http://www.cds.caltech.edu/~lun/publications/IM06.pdf Towards a Theory of Scale-Free Graphs: Definition, Properties, and Implications]. ''Internet Mathematics'' 2(4), p 431-523, Mar. 2006.

* L. Li, D. Alderson, W. Willinger and J. C. Doyle. [http://www.cds.caltech.edu/~lun/publications/sigcomm04.pdf A First-Principles Approach to Understanding the Internet's Router-level Topology]. Proceedings of ACM Sigcomm, 2004,

* S. H. Low, J. C. Doyle, L. Li, A. Tang, J. Wang, Optimization Model of Internet Protocols, Proceedings of ACM Sigmetrics, June 2005.

* S. Prajna and A. Jadbabaie. Safety verification of hybrid systems using barrier certificates. In ''Hybrid Systems: Computation and Control'', 2004.

* S. Prajna and A. Jadbabaie. Methods for safety verification of time-delay systems. In ''Proceedings of the IEEE Conference on Decision and Control'', 2005.

* S. Prajna, A. Jadbabaie, and G. J. Pappas. Stochastic safety verification using barrier certificates. In ''Proceedings of the IEEE Conference on Decision and Control'', 2004.

* S. Prajna, A. Papachristodoulou, P. J. Seiler, and P. A. Parrilo. SOSTOOLS -- Sum of Squares Optimization Toolbox, User's Guide. Available at http://www.cds.caltech.edu/sostools and http://www.mit.edu/~parrilo/sostools, 2002, 2004.

* S. Prajna and A. Rantzer. On the necessity of barrier certificates. In ''Proceedings of the IFAC World Congress'', 2005.

* S. Prajna and A. Rantzer. Primal-dual tests for safety and reachability. In ''Hybrid Systems: Computation and Control''. Springer-Verlag, 2005.

== Reports ==
* [[Media:boeing_report-may08.pdf|Annual report, May 2007 to April 2008]]
* [[Media:boeing_report-mar06.pdf|Annual report, January 2005 to March 2006]]
* [[Media:boeing_report-apr06.pdf|Annual report, March 2006 to April 2007]]

== Software ==
* SOSTOOLS

== Related Activities ==
* [[Connections II]] - Workshop on Foundations of Network Science (Caltech, August 2006)
* [http://www.cds.caltech.edu/~murray/VaVmuri V&V MURI] - Specification, Design and Verification of Distributed Embedded Systems (AFOSR MURI)
* [[Workshop: Specification and Verification of Embedded Systems]] - (Caltech, October 2008)
* [[Caltech Workshop on Verification and Validation]] - September 23-24, 2009