@InProceedings{JM:FORMATS2014,
  Title                    = {Anonymized Reachability of Hybrid Automata Networks},
  Author                   = {Taylor Johnson and Sayan Mitra},
  Booktitle                = {Proceedings of Formal Modelling and Analysis of Timed Systems (FORMATS 2014)},
  Year                     = {2014},
  Series                   = {LNCS},

  Abstract                 = {In this paper, we present a method for computing the reach set for networks composed of a finite number of hybrid automata. The method utilizes a symmetric representation of reach set modulo the automata indices, which makes it scalable. Rather than explicitly enumerating all the automata indices in formulas representing states, the representation tracks only: (a) the classes of automata, which are the states of automata represented with formulas over symbolic indices, and (b) the number of automata in each of the classes. We present an algorithm for over-approximating the reach set by computing state transitions in this representation. Unlike symmetry reduction for FSMs, the timed transition of a hybrid network causes all the automata�s continuous variables to evolve simultaneously. Our representation reduces both the discrete and continuous complexity. We evaluate a prototype implementation in an SMT-based tool. Our experimental results are promising, and in some instances, allow for scaling to networks composed of hundreds of automata.},
  Autor                    = {Taylor Johnson and Sayan Mitra},
  Codeurl                  = {https://publish.illinois.edu/passel-tool/},
  Keywords                 = {Verification},
  Owner                    = {mitras},
  Pdfurl                   = {research/2014/JM_FORMATS2014.pdf},
  Timestamp                = {2014.06.10},
  Url                      = {http://link.springer.com/chapter/10.1007%2F978-3-319-10512-3_10#page-1}
}