Benchmarks for Hybrid Systems

Ansgar Fehnker1 and Franjo Ivančić2

1Carnegie Mellon University, 5000 Forbes Ave, Pittsburgh, PA 15213 (USA)
Email: ansgar@cmu.edu
2 NEC Laboratories America Inc., 4 Independence Way, Princeton, NJ 08540 (USA)
Email: ivancic@nec-labs.com

Introduction

The following contains information regarding the benchmarks that we proposed at the Workshop Hybrid Systems : Computation and Control at University of Pennsylvania, 2004. Comments, questions and suggestions are welcome. My current email address is ansgar.fehnker@nicta.com.au

Documentation

Benchmarks

The instances come in triples of similar size. While the first instance of a triple is supposed to be easier than the last instance, it is usually hard to judge if the first instance of the next triple is easier or more difficult to solve that the last. Even if the last instance of a triple turns out to be too dificult, the next instance may be somewhat easier to solve.
  1. Navigation Benchmark
  2. Leaking Procedure Benchmark
  3. Room Heating Benchmark
  4. Remark: The lower bound on the temperature is defined for each room. See vector lower in the problem definition.

Links

  • Hybrid Systems Verification Wiki, a repository for software tools for modeling, verifying, and designing hybrid systems, maintained by George Pappas.
  • Benchmarks by Stefan Ratschan, used for HSOLVER. Includes an instance of the heating benchmark.
  • Phaver, a tool for verifying safety properies of hybrid systems, by Goran Frehse. Includes a number of other examples.

References

  • R. Alur, T. Dang, and F. Ivančić. Predicate abstraction for reachability analysis of hybrid systems. Trans. on Embedded Computing Sys. 2006.
  • M. Anand, J. Kim, S. Fischmeister, and I. Lee. Generating Sound and Resource-Aware Code from Hybrid System Models. Workshop on Advanced Automotive Software and Systems Development, San Diego (ASWSD'06), 2006.
  • L. Doyen, T. Henzinger, and J. Raskin. Automatic Rectangular Refinement of Affine Hybrid Systems. Proceedings of the Third International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), LNCS3829, 2005.
  • X. Koutsoukos and D. Riley. Computational Methods for Reachability Analysis of Stochastic Hybrid Systems. Hybrid Systems: Computation and Control (HSCC 2006), LNCS 3927, 2006.
  • S. Ratschan and Z. She. Safety Verification of Hybrid Systems by Constraint Propagation Based Abstraction Refinement. ACM Transactions on Embedded Computing Systems, 2006.
  • S. Sankaranarayanan, H. Sipma, Z. Manna. Fixed Point Iteration for Computing the Time Elapse Operator. Hybrid Systems: Computation and Control (HSCC 2006), LNCS 3927, 2006.