Program

CPSWeek tutorials and workshops to be held on April 8th, 2013. 

HSCC talks and presentations will be held on April 9th - 11th, 2013. 

A PDF version of the program is now available here: HSCC'13 program (PDF)

A compact version of the program (please fold it): Compact program (PDF)

Online proceedings: ACM Digital Library

Tuesday, April 9th, 2013

8:30-10:00

CPSWeek Keynote at Seaport auditorium

[8:30] CPSWeek Welcome Message

[8:45] Deborah Estrin: “Sensemaking for Mobile Health”

10:00-10:30

Coffee break

10:30-12:05

Control I (Session Chair: Paulo Tabuada)

[10:30] HSCC Chairs Welcome

[10:35] Jana Tumova, Gavin C. Hall, Sertac Karaman, Emilio Frazzoli and Daniela Rus: “Least-violating Control Strategy Synthesis with Safety Rules”

[11:00] Daniel Liberzon: “Limited-information control of hybrid systems via reachable set propagation”

[11:25] Heath Leblanc and Xenofon Koutsoukos: “Resilient Synchronization in Robust Networked Multi-Agent Systems”

[11:50] Tool Teaser: Sebti Mouelhi, Antoine Girard and Gregor Goessler: “CoSyMA: A Tool for Controller Synthesis using Multi-scale Abstractions”

[11:58] Tool Teaser: Robert Rogersten, Huan Xu, Necmiye Ozay, Ufuk Topcu and Richard M. Murray: “An Aircraft Electric Power Testbed for Validating Automatically Synthesized Reactive Control Protocols”

12:05-1:00

Lunch

1:00-2:00

HSCC Invited Talk (Session Chair: Calin Belta)

[1:00] Aaron D. Ames: "Human-Inspired Control of Bipedal Robots via Control Lyapunov Functions and Quadratic Programs"

2:00-3:05

Learning (Session Chair: Sriram Sankaranarayanan)

[2:00] Van Luong Le, Fabien Lauer, Laurent Bako and Gérard Bloch: “Learning Nonlinear Hybrid Systems: from Sparse Optimization to Support Vector Regression”

[2:25] Xiaoqing Jin, Alexandre Donzé, Jyotirmoy Deshmukh and Sanjit Seshia: “Mining Requirements from Closed-loop Control Models”

[2:50] Tool Teaser: Zhi Han and Pieter Mosterman: “Towards Sensitivity Analysis of Hybrid Systems Using Simulink”

[2:58] Tool Teaser: Ricardo Sanfelice, David Copp and Pablo Ñañez: “A Toolbox for Simulation of Hybrid Systems in Matlab/Simulink”

3:05-3:30

Coffee break

3:30-5:00

Stability (Session Chair: Xenofon Koutsoukos)

[3:30] Pavithra Prabhakar and Mahesh Viswanathan: “On the Decidability of Stability of Hybrid Systems”

[3:55] Michael Posa, Mark Tobenkin and Russ Tedrake: “Lyapunov Analysis of Rigid Body Systems with Impacts and Friction via Sums-of-Squares

[4:20] Stefano Di Cairano, Maurice Heemels, Mircea Lazar and Alberto Bemporad: “Hybrid Control Lyapunov Functions for Stabilization of Hybrid Systems”

[4:45] Tool Teaser: Eike Moehlmann and Oliver Theel: “Stabhyli -- A Tool for Automatic Stability Verification of Non-Linear Hybrid Systems”

[4:53] Tool Teaser: Timothy Bourke and Marc Pouzet: “Zélus: A Synchronous Language with ODEs”

5:00-8:00

CPSWeek Poster and Demo session with Reception

Includes all tool and case study papers accepted as HSCC, as well as HSCC accepted demo and poster abstract submissions (see below).



Wednesday, April 10th, 2013

8:45-10:00

CPSWeek Keynote at Seaport auditorium

[8:45] Vijay Kumar: “Aerial Robot Swarms”

10:00-10:30

Coffee beak

10:30-12:00

State estimation (Session chair: Stefano diCairano)

[10:30] Jerome Thai and Alexandre Bayen: State estimation for polyhedral hybrid systems and applications to the Godunov scheme”

[10:55] Dirk van Zwieten, Erjen Lefeber and W.P.M.H. Heemels: “Observer design for a class of piecewise affine hybrid systems”

[11:20] Krishnendu Chatterjee, Alexander Kößler and Ulrich Schmid: “Automated Analysis of Real-Time Scheduling using Graph Games”

[11:45] Case Study Paper: Ganesh Kumar, Aurelie Buffin, Theodore Pavlic, Stephen Pratt and Spring Berman: “A Stochastic Hybrid System Model of Collective Transport in the Desert Ant Aphaenogaster cockerelli”

12:00-1:00

Lunch

1:00-3:05

Reachability (Session Chair: Alessandro Abate)

[1:00] Matthias Althoff: “Reachability Analysis of Nonlinear Systems using Conservative Polynomialization and Non-Convex Sets”

[1:25] Insoon Yang, Sabine Becker-Weimann, Mina J. Bissell and Claire J. Tomlin: “One-Shot Computation of Reachable Sets for Differential Games”

[1:50] Massimo Benerecetti and Marco Faella: “Tracking Differentiable Trajectories across Polyhedra Boundaries”

[2:15] Goran Frehse, Colas Le Guernic and Rajat Kateja: “Flowpipe Approximation and Clustering in Space-Time”

[2:40] Quan Zu, Miaomiao Zhang, Jiaqi Zhu and Naijun Zhan: ”Bounded Model-checking of Discrete Duration Calculus”

3:05-3:30

Coffee break

3:30-5:00

Scheduling (Session chair: Goran Frehse)

[3:30] Arquimedes Canedo, Livio Dalloro and Hartmut Ludwig: “Pipelining for Cyclic Control Systems”

[3:55] Daniele Fontanelli, Luca Greco and Luigi Palopoli: “Optimal CPU Allocation to a Set of Control Tasks with Soft Real--Time Execution Constraints”

[4:20] Rajeev Alur, Vojtech Forejt, Salar Moarref and Ashutosh Trivedi: “Safe Schedulability of Bounded-Rate Multi-Mode Systems”

[4:45] Case Study Paper: Sarah Loos, David Renshaw and André Platzer: “Formal Verification of Distributed Aircraft Controllers”

6:00-

CPSWeek Banquet on the Battleship New Jersey

Best Paper Award and Best Student Paper Award will be announced during the Banquet. 



Thursday, April 11th, 2013

8:45-10:00

CPSWeek Keynote at Seaport auditorium

[8:45] Manfred Broy: “Challenges in Modeling Cyber-Physical Systems”

10:00-10:30

Coffee beak

10:30-12:00

Verification (Session chair: Rajeev Alur)

[10:30] Akshay Rajhans and Bruce Krogh: “Compositional Heterogeneous Abstraction”

[10:55] Yanni Kouskoulas, David Renshaw, André Platzer and Peter Kazanzides: “Certifying the Safe Design of a Virtual Fixture Control Algorithm for a Surgical Robot”

[11:20] Krishnendu Chatterjee and Vinayak Prabhu: “Quantitative Timed Simulation Functions and Refinement Metrics for Real-Time Systems”

[11:45] Case Study Paper: Taolue Chen, Marco Diciolla, Marta Kwiatkowska and Alexandru Mereacre: “A Simulink Hybrid Heart Model for Quantitative Verification of Cardiac Pacemakers”

12:00-1:00

Lunch

1:00-3:05

Stochastic Hybrid Systems (Session chair: Marta Kwiatkowska)

[1:00] Ilya Tkachev and Alessandro Abate: “Formula-free finite abstractions for linear temporal verification of Stochastic Hybrid Systems”

[1:25] Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen and Alessandro Abate: “Quantitative Automata-based Controller Synthesis for Non-Autonomous Stochastic Hybrid Systems”

[1:50] Maryam Kamgarpour, Sean Summers and John Lygeros: “Control Design for Property Specifications on Stochastic Hybrid Systems”

[2:15] Ernst Moritz Hahn and Holger Hermanns: “Rewarding Probabilistic Hybrid Automata”

[2:40] Hongfei Fu: “Approximating Acceptance Probabilities of CTMC-Paths on Multi-Clock Deterministic Timed Automata”

3:05-3:30

Coffee break

3:30-5:00

Control II (Session Chair: Agung Julius)

[3:30] Matthias Rungger, Manuel Mazo and Paulo Tabuada: “Specification guided controller synthesis for linear systems and safe linear-time temporal logic”

[3:55] Ebru Aydin Gol and Mircea Lazar: “Temporal Logic Model Predictive Control for Discrete-Time Systems

[4:20] Matthew R. Maly, Morteza Lahijanian, Lydia E. Kavraki, Hadas Kress-Gazit and Moshe Y. Vardi:  “Iterative Temporal Motion Planning for Hybrid Systems in Partially Unknown Environments”

[4:45] Case Study Paper: Koushil Sreenath, Connie Hill and Vijay Kumar: “A Partially Observable Hybrid System Model for Bipedal Locomotion for Adapting to Terrain Variations”


HSCC Contributions to the CPSWeek Poster and Demo Session 

(Tuesday, April 9th, 5PM-8PM)

Tool Paper Demos

Timothy Bourke and Marc Pouzet: “Zélus: A Synchronous Language with ODEs”

Zhi Han and Pieter Mosterman: “Towards Sensitivity Analysis of Hybrid Systems Using Simulink”

Eike Moehlmann and Oliver Theel: “Stabhyli -- A Tool for Automatic Stability Verification of Non-Linear Hybrid Systems”

Sebti Mouelhi, Antoine Girard and Gregor Goessler: “CoSyMA: A Tool for Controller Synthesis using Multi-scale Abstractions”

Robert Rogersten, Huan Xu, Necmiye Ozay, Ufuk Topcu and Richard M. Murray: “An Aircraft Electric Power Testbed for Validating Automatically Synthesized Reactive Control Protocols”

Ricardo Sanfelice, David Copp and Pablo Ñañez: “A Toolbox for Simulation of Hybrid Systems in Matlab/Simulink”

Case Study Posters

Taolue Chen, Marco Diciolla, Marta Kwiatkowska and Alexandru Mereacre: “A Simulink Hybrid Heart Model for Quantitative Verification of Cardiac Pacemakers”

Ganesh Kumar, Aurelie Buffin, Theodore Pavlic, Stephen Pratt and Spring Berman: “A Stochastic Hybrid System Model of Collective Transport in the Desert Ant Aphaenogaster cockerelli”

Sarah Loos, David Renshaw and André Platzer: “Formal Verification of Distributed Aircraft Controllers”

Koushil Sreenath, Connie Hill and Vijay Kumar: “A Partially Observable Hybrid System Model for Bipedal Locomotion for Adapting to Terrain Variations”

HSCC Accepted Demos

Stanley Bak and Marco Caccamo: “Computing Reachability for Nonlinear Systems with HyCreate”   

Goran Frehse: “A Comparison of the STC and LGG Reachability Algorithms in SpaceEx”

Sicun Gao, Soonho Kong, and Edmund M. Clarke: “dReach: A Reachability Analysis Tool for Nonlinear Hybrid Systems”

Arnd Hartmanns and Holger Hermanns: “Modeling and Analysis of Stochastic, Hybrid and Real-Time Systems with the Modest Toolset”

Taylor T. Johnson and Sayan Mitra: “The Passel Verification Tool for Hybrid Automata Networks” 

Stefan Mitsch and André Platzer: “Modeling and Verification of Hybrid Systems with Sphinx and KeYmaera”

Yash Vardhan Pant, Harsh Jain, Abhijeet Mulay, and Rahul Mangharam: “ProtoDrive: An Experimental Platform for Electric Vehicle Energy Scheduling and Control”

HSCC Accepted Posters

Nikolaos Athanasopoulos and Mircea Lazar: “On stability analysis of switched linear systems via stability theory in the space of compact sets” 

Martin Clochard, Swarat Chaudhuri, and Armando Solar-Lezama: “Stochastic Program Synthesis with Smoothed Numerical Search” 

Yi Deng, Akshay Rajhans, and A. Agung Julius: “STRONG: A Trajectory-based Verification Toolbox for Hybrid Systems”

Charles Freundlich, Philippos Mordohai, and Michael M. Zavlanos: “A Hybrid Control Approach to the Next-Best-View Problem using Stereo Vision”

Jie Fu, Herbert G. Tanner, and Jeffrey Heinz: “Adaptive Symbolic Design with Grammatical Inference”

Shahab Kaynama, Ian M. Mitchell, Meeko Oishi, and Guy A. Dumont: “Safety-Preserving Control of High-Dimensional Continuous-Time Uncertain Linear Systems” 

Fei Miao, Miroslav Pajic, and George J. Pappas: “A stochastic game formulation for system against replay attack” 

Andrew K. Winn and A. Agung Julius: “Optimization-based Improvements for Safety Controller Synthesis via Human Generated Trajectories” 


Presentation formats
Regular papers: 25 minutes presentation (please allow for 5 minutes of Q&A, that is 20 minutes talk, and 5 minutes for Q&A)
Case study papers: A poster will be presented during the CPSWeek demo-and-poster session, on Tuesday, April 9th, 5-8PM. In addition, a 15 minute presentation of the paper during a HSCC session on Wednesday or Thursday (please allow for 3 minutes of Q&A). 
Tool papers: A demo of the tool will be presented during the CPSWeek demo-and-poster session on Tuesday, April 9th, 5-8PM. In addition, a 7 minute tool teaser presentation during a HSCC session earlier on the same day to encourage listeners to attend your demo (please allow for 2 minutes of Q&A).
Unpublished posters: A poster will be presented during the CPSWeek demo-and-poster session, on Tuesday, April 9th, 5-8PM. 
Unpublished demos: A demo of the tool will be presented during the CPSWeek demo-and-poster session on Tuesday, April 9th, 5-8PM.