Anonymized Reachability of Hybrid Automata Networks

Johnson, Taylor T.; Mitra, Sayan

doi:10.1007/978-3-319-10512-3_10

Abstract:

In this paper, we present a method for computing the set of reachable states for networks consisting of the parallel composition of a finite number of the same hybrid automaton template with rectangular dynamics. The method utilizes a symmetric representation of the set of reachable states (modulo the automata indices) that we call anonymized states, which makes it scalable. Rather than explicitly enumerating each automaton index in formulas representing sets of states, the anonymized representation encodes 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 overapproximating the reachable states by computing state transitions in this anonymized representation. Unlike symmetry reduction techniques used in finite state models, the timed transition of a network composed of hybrid automata causes the continuous variables of all the automata to evolve simultaneously. The anonymized representation is amenable to both reducing the discrete and continuous complexity. We evaluate a prototype implementation of the representation and reachability algorithm in our satisfiability modulo theories (SMT)-based tool, Passel. Our experimental results are promising, and generally allow for scaling to networks composed of tens of automata, and in some instances, hundreds (or more) of automata.

Reference:

Taylor T. Johnson, Sayan Mitra, "Anonymized Reachability of Hybrid Automata Networks", In Proceedings of the 12th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2014), Florence, Italy, pp. , 2014, sep.

Bibtex Entry:

@inproceedings{johnson2014formats,
        author          =       {Taylor T. Johnson and Sayan Mitra},
        title           =       {Anonymized Reachability of Hybrid Automata Networks},
        year            =       {2014},
        booktitle       =       {Proceedings of the 12th International Conference on Formal Modeling and Analysis of Timed Systems (<a href="http://formats2014.unifi.it/">FORMATS 2014</a>)},
    address     =   {Florence, Italy},
        month           =       sep,
        pages           =       {},
        doi     =   {10.1007/978-3-319-10512-3_10},
        gsid        =   {},
        abstract    =   {In this paper, we present a method for computing the set of reachable states for networks consisting of the parallel composition of a finite number of the same hybrid automaton template with rectangular dynamics.  The method utilizes a symmetric representation of the set of reachable states (modulo the automata indices) that we call anonymized states, which makes it scalable.  Rather than explicitly enumerating each automaton index in formulas representing sets of states, the anonymized representation encodes 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 overapproximating the reachable states by computing state transitions in this anonymized representation.  Unlike symmetry reduction techniques used in finite state models, the timed transition of a network composed of hybrid automata causes the continuous variables of all the automata to evolve simultaneously.  The anonymized representation is amenable to both reducing the discrete and continuous complexity.  We evaluate a prototype implementation of the representation and reachability algorithm in our satisfiability modulo theories (SMT)-based tool, Passel.  Our experimental results are promising, and generally allow for scaling to networks composed of tens of automata, and in some instances, hundreds (or more) of automata.},
        pdf = {http://www.taylortjohnson.com/research/johnson2014formats.pdf},
}