VVPS. Verification and Validation of Planning and Scheduling Systems
The VVPS workshop aims to enhance a stable forum on relevant topics connected to contaminations between V&V and P&S. The workshop will deepen the debate on relevant aspects of interactions between V&V methods and P&S-based systems. Important goals are to investigate new solutions and identify open issues.
Schedule
The workshop will be held on June 13, 2011 in hall 101–01–009/013 on the computer science campus.
09:00-10:00 |
Invited Talk Maria Fox Policy Learning for Autonomous Feature Tracking (pdf) |
10:00-10:30 |
Siddharth Srivastava, Neil Immerman, Shlomo Zilberstein and Tianjiao Zhang Directed Search for Generalized Plans Using Classical Planners (pdf) |
Coffee Break | |
11:00-11:30 |
Jason Crampton and Michael Huth Synthesizing and Verifying Plans for Constrained Workflows: Transferring Tools from Formal Methods (pdf) |
11:30-12:00 |
Andrea Orlandini, Alberto Finzi, Amedeo Cesta and Simone Fratini Generating Controllers for Flexible Plan Execution: a TGA Approach (pdf) |
12:00-12:30 |
Robert P. Goldman, Michael Pelican and David Musliner A Loop Acceleration Technique to Speed Up Verification of Automatically-Generated Plans (pdf) |
Lunch Break | |
14:00-14:30 |
Niloofar Razavi, Azadeh Farzan and Sheila McIlraith Predicting Atomicity Violations in Concurrent Programs via Planning (pdf) |
14:30-15:00 |
Rosella Gennari, Anna Roubickova and Marco Roveri A Critical Overview and Open Questions for Temporal Planning with Uncertainty (pdf) |
15:00-15:30 |
Ilias Garnier, Christophe Aussaguès, Vincent David and Guy Vidal-Naquet Formally Ensuring Time Constraints in a Development Process (pdf) |
Coffee Break | |
16:00-17:30 | Special Session "Darmstadt, we have a problem" — Open Discussion about a Planning Domain inspired by an ESA Robotic Mission |
Invited Talk: Maria Fox
Policy Learning for Autonomous Feature Tracking
Abstract:
When operating under uncertainty, a robust behaviour can often be learned by sam- pling a large number of cases, planning what to do precisely in those cases (which are deterministic) and then learning a general policy for what to do in future unseen cases. The learning can be done by classifying the actions that can be performed into the states that were met in the training cases. The resulting policy will be good if the sampling was representative.
This talk presents an example of this approach applied to the problem of tracking a moving patch of water in the ocean. The same approach has been successfully ap- plied to the problem of load management for multiple independent batteries. The talk will address the modelling problems that arise in the patch-tracking case, some of the subtleties that affect the quality of the learned policy, and the performance of the sys- tem executing the learned policy. The results we have obtained so far suggest that the planning followed by classification approach is highly scalable and is a practical and effective method for achieving intelligent behaviour under uncertainty.
Call for Papers
Topic and Objectives
Planning and scheduling (P&S) systems are finding increased application in safety- and mission-critical systems that require a high level of assurance. However, tools and methodologies for verification and validation (V&V) of P&S systems have received relatively little attention. Therefore, important goals of the workshop are (i) to encourage the ongoing interaction between P&S and V&V communities, (ii) to identify innovative tools and methodologies (iii) and to elicit open issues and real challenges.
The workshop also aims to enhance a stable, long-term establishment of a forum on relevant topics connected to the influence between V&V and P&S. The workshop series began in 2005 with the first edition of the workshop during ICAPS '05 and continued in 2009 with the second edition during ICAPS '09. These workshops presented a stimulating environment where researchers could discuss about the opportunities and challenges in integrating V&V and P&S.
Topics of interest include: V&V of domain models, using technologies such as static analysis, theorem proving, and model checking; consistency and completeness of domain models; domain model coverage metrics; regression, stress and boundary testing; runtime verification of plan executions; generation of robust plans; compositional verification of domain models; how to structure domain models which are more amenable to static analysis; inspection methods; the relationship between timed automata and domain models; investigations of the impact wrt. V&V of procedural versus declarative plan models; application of P&S techniques to V&V; Planning as model checking; etc.
Important Dates
- Paper submission: March 25, 2011
- Notifications of acceptance/rejection: April 15, 2011
- Workshop Date: June 13th, 2011
Submissions
There are two types of submissions: short position statements and regular papers. Position papers are a maximum of 2 (two) pages. Regular papers are a maximum of 10 (ten) pages. Papers should be submitted via the VVPS easychair website and should follow the format indicated. All papers should be typeset in the AAAI style, described at http://www.aaai.org/Publications/Author/author.php removing AAAI copyright. Accepted papers will be published on the workshop website and printed as a hard-copy.
A selection of the accepted papers will be published in a special issue of the International Journal on Software Tools for Technology Transfer.
Any additional question can be directed towards the general workshop contact email: vvps11@easychair.org
Organization Chairs
-
Saddek Bensalem
VERIMAG, France
saddek.bensalem@imag.fr -
Klaus Havelund
NASA JPL, USA
klaus.havelund@jpl.nasa.gov -
Andrea Orlandini
ITIA-CNR, Italy
andrea.orlandini@itia.cnr.it
Programme Committee
- Howard Barringer (University of Manchester, UK)
- Andreas Bauer (NICTA, Australia)
- Saddek Bensalem (Verimag/UJF, France) (Co-Chair)
- Amedeo Cesta (ISTC-CNR, Rome, Italy)
- Alessandro Cimatti (FBK, Trento, Italy)
- Alexandre David (Aalborg University, Denmark)
- Giuseppe Della-Penna (University of L'Aquila, L'Aquila, Italy)
- Lucas Dixon (University of Edinburgh, Edinburgh, UK)
- Bernd Finkbeiner (Saarland University, Germany)
- Alberto Finzi (University of Naples, Naples, Italy)
- Maria Fox (University of Strathclyde, UK)
- Dimitra Giannakopoulou (NASA Ames Research Center, USA)
- Enrico Giunchiglia (University of Genova, Italy)
- Alex Groce (Oregon State University, USA)
- Klaus Havelund (JPL, USA) (Co-Chair)
- Gerard Holzmann (JPL, USA)
- Felix Ingrand (LAAS-CNRS, France)
- Hadas Kress-Gazit (Cornell University, USA)
- Kim G. Larsen (Aalborg University, Denmark)
- Martin Leucker (Technische Universität München, Germany)
- Lee McCluskey (University of Huddersfield, UK)
- David Musliner (SIFT, USA)
- Andrea Orlandini (ITIA-CNR, Milan, Italy) (Co-Chair)
- Corina Pasareanu (NASA Ames Research Center, USA)
- Charles Pecheur (Université catholique de Louvain, Belgium)
- Paul Pettersson (Malardalen University, Sweden)
- Douglas Smith (Kestrel Institute, USA)