Anonymized reachability of hybrid automata networks

Taylor T. Johnson, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationFormal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings
PublisherSpringer
Pages130-145
Number of pages16
ISBN (Print)9783319105116
DOIs
StatePublished - 2014
Event12th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2014 - Florence, Italy
Duration: Sep 8 2014Sep 10 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8711 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other12th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2014
Country/TerritoryItaly
CityFlorence
Period9/8/149/10/14

Keywords

  • hybrid automata network
  • reachability
  • symmetry
  • verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Anonymized reachability of hybrid automata networks'. Together they form a unique fingerprint.

Cite this