TY - GEN

T1 - Anonymized reachability of hybrid automata networks

AU - Johnson, Taylor T.

AU - Mitra, Sayan

N1 - Copyright:
Copyright 2016 Elsevier B.V., All rights reserved.

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

KW - hybrid automata network

KW - reachability

KW - symmetry

KW - verification

UR - http://www.scopus.com/inward/record.url?scp=84958524736&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84958524736&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-10512-3_10

DO - 10.1007/978-3-319-10512-3_10

M3 - Conference contribution

AN - SCOPUS:84958524736

SN - 9783319105116

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 130

EP - 145

BT - Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings

PB - Springer

T2 - 12th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2014

Y2 - 8 September 2014 through 10 September 2014

ER -