Quasi-Dependent Variables

HSCC 2014 Supporting Material

This page provides supporting material for the paper Quasi-Dependent Variables in Hybrid Automata [1], published in 17th International Conference on Hybrid Systems: Computation and Control (HSCC 2014).

Contents

1. Overview
2. Download
3. References

1. Overview

The concept of hybrid automata provides a powerful frame- work to model and analyze real-world problem domains. Due to the structural complexity of hybrid systems it is important to ensure the scalability of analysis algorithms. We approach this problem by providing an effective exten- sion of the recently introduced notion of quasi-equal [2] clocks to hybrid systems. For this purpose, we introduce the concept of quasi-dependent variables. Our contribution is two- fold: we demonstrate how such variables can be automati- cally detected, and we present a transformation leading to an abstraction with a smaller state space which, however, still retains the same properties as an original system. We demonstrate the practical applicability of our methods on a range of industrial benchmarks.

The crux behind our detection algorithm is the application of abstraction techniques while analyzing the relations between variables. Both continuous and discrete evolution can break the quasi-dependency between variables. However, interestingly, we only need to be precise while considering discrete jumps whereas in case of continuous evolution we can just check which quasi-dependencies still hold in the considered location. The intuition is that we can abstract away constraints other than the ones reflecting the quasi-dependencies because if a quasi-dependency holds before computing continuous successors (which is checked without precision loss in the preceding discrete step) then the continuous evolution obeys the quasi-dependency. The quasi-dependent variables can also be detected by a hybrid model checker, however, it would explore the state space of the system in a great detail, whereas our detection algorithm conducts a coarse analysis with the focus on the state space parts relevant for establishing quasi-dependencies. These ideas lead to an abstraction that is rather imprecise, yet results in a dramatic performance improvement of quasi-dependent variables detection. compared to the solution based on a standard hybrid model checker.

Our transformation replaces quasi-dependent variables by one representative variable and updates the system structure appropriately. Properties of the original system are preserved, that is, a forbidden configuration is reachable in the transformed system if and only if it is reachable in the original system.

If you use our benchmarks in your work, please cite as follows:

@inproceedings{quasidependentvarsHA,
  author={Bogomolov, Sergiy and Herrera, Christian and Mu{\~n}iz, Marco and 
          Westphal, Bernd and Podelski, Andreas},
  title={Quasi-Dependent Variables in Hybrid Automata},
  booktitle={HSCC},
  year={2014}
}

2. Download

Click here to download the archive which has the following contents:

1. Binaries of SpaceEx and sAsEt with the necessary libraries
2. Models of Class A and Class B benchmarks from detection part
3. Models of FSN instances from transformation part
4. Models of EPN instances from transformation part

3. References

1. Sergiy Bogomolov, Christian Herrera, Marco Muñiz, Bernd Westphal, Andreas Podelski: Quasi-Dependent Variables in Hybrid Automata, In: HSCC2014
2. Christian Herrera, Bernd Westphal, Sergio Feo-Arenis, Marco Muñiz, Andreas Podelski: Reducing quasi-equal clocks in networks of timed automata, In: FORMATS2012, pp. 144-170. No. 7595 in LNCS, Springer, Heidelberg