Bibliography

This page includes references to the scientific works that we have applied throughout this library. Although the list is not meant to be exhaustive, we think it should give a solid starting place for those who want to explore further.

If you use ReachabilityAnalysis.jl for your own work, please consider citing the appropriate original reference(s). We provide the BibTeX entries in each case.

If you find that a reference here is missing, if you spot a typo or want to update a reference, do not hesitate to contact us by email, or open an issue. Sorting is alphabetic.

[A20]

Althoff, Matthias. Reachability Analysis of Large Linear Systems With Uncertain Inputs in the Krylov Subspace. IEEE Transactions on Automatic Control 2 (2020).

BibTex entry

@article{Althoff20,
  author       = {Matthias Althoff},
  title        = {Reachability Analysis of Large Linear Systems With Uncertain Inputs
                  in the {K}rylov Subspace},
  journal      = {{IEEE} Trans. Autom. Control.},
  volume       = {65},
  number       = {2},
  pages        = {477--492},
  year         = {2020},
  url          = {https://doi.org/10.1109/TAC.2019.2906432},
  doi          = {10.1109/TAC.2019.2906432}
}

[AFG20]

Althoff, Matthias, Goran Frehse, and Antoine Girard. Set Propagation Techniques for Reachability Analysis.. Annual Review of Control, Robotics, and Autonomous Systems 4 (2020).

BibTex entry

@article{althoff2020set,
  title={Set Propagation Techniques for Reachability Analysis},
  author={Althoff, Matthias and Frehse, Goran and Girard, Antoine},
  journal={Annual Review of Control, Robotics, and Autonomous Systems},
  volume={4},
  year={2020},
  publisher={Annual Reviews}
}

[ALU95]

Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P. H., Nicollin, X., ... & Yovine, S. (1995). The algorithmic analysis of hybrid systems. Theoretical computer science, 138(1), 3-34.

BibTex entry

@article{alur1995algorithmic,
  title={The algorithmic analysis of hybrid systems},
  author={Alur, Rajeev and Courcoubetis, Costas and Halbwachs, Nicolas and Henzinger, Thomas A and Ho, Pei-Hsin and Nicollin, Xavier and Olivero, Alfredo and Sifakis, Joseph and Yovine, Sergio},
  journal={Theoretical computer science},
  volume={138},
  number={1},
  pages={3--34},
  year={1995},
  publisher={Citeseer}
}

[ALT10]

Althoff, Matthias. Reachability analysis and its application to the safety assessment of autonomous cars. Diss. Technische Universität München, 2010.

BibTex entry

@phdthesis{althoff2010reachability,
  title={Reachability analysis and its application to the safety assessment of autonomous cars},
  author={Althoff, Matthias},
  year={2010},
  school={Technische Universit{\"a}t M{\"u}nchen}
}

[ASB07]

M. Althoff, O. Stursberg, and M. Buss. Reachability analysis of linear systems with uncertain parameters and inputs. In Proc. of the 46th IEEE Conference on Decision and Control, pages 726–732, 2007.

BibTex entry

@inproceedings{althoff2007reachability,
  title={Reachability analysis of linear systems with uncertain parameters and inputs},
  author={Althoff, Matthias and Stursberg, Olaf and Buss, Martin},
  booktitle={2007 46th IEEE Conference on Decision and Control},
  pages={726--732},
  year={2007},
  organization={IEEE}
}

[BFFPSV18]

Bogomolov, S., Forets, M., Frehse, G., Viry, F., Podelski, A., & Schilling, C. (2018, April). Reach set approximation through decomposition with low-dimensional sets and high-dimensional matrices. In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week) (pp. 41-50).

BibTex entry

@inproceedings{bogomolov2018reach,
  title={Reach set approximation through decomposition with low-dimensional sets and high-dimensional matrices},
  author={Bogomolov, Sergiy and Forets, Marcelo and Frehse, Goran and Viry, Fr{\'e}d{\'e}ric and Podelski, Andreas and Schilling, Christian},
  booktitle={Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)},
  pages={41--50},
  year={2018}
}

[BFFPS19]

Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., & Schilling, C. (2020). Reachability analysis of linear hybrid systems via block decomposition. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 39(11), 4018-4029.

BibTex entry

@article{bogomolov2020reachability,
  title={Reachability analysis of linear hybrid systems via block decomposition},
  author={Bogomolov, Sergiy and Forets, Marcelo and Frehse, Goran and Potomkin, Kostiantyn and Schilling, Christian},
  journal={IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
  volume={39},
  number={11},
  pages={4018--4029},
  year={2020},
  publisher={IEEE}
}

[CHEN15]

Chen, Xin. Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models. Diss. Fachgruppe Informatik, RWTH Aachen University, 2015.

BibTex entry

@phdthesis{chen2015reachability,
  title={Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models},
  author={Chen, Xin},
  year={2015},
  school={Fachgruppe Informatik, RWTH Aachen University}
}

[COMB03]

Combastel, C. A state bounding observer based on zonotopes. 2003 European Control Conference (ECC). IEEE, 2003.

BibTex entry

@inproceedings{combastel2003state,
  title={A state bounding observer based on zonotopes},
  author={Combastel, C},
  booktitle={2003 European Control Conference (ECC)},
  pages={2589--2594},
  year={2003},
  organization={IEEE}
}

[CPPSV06]

Carloni, L. P., Passerone, R., Pinto, A., & Sangiovanni-Vincentelli, A. L. Languages and tools for hybrid systems design. Foundations and Trends® in Electronic Design Automation, 1(1–2), 1-193. 2006.

BibTex entry

@article{carloni2006languages,
  title={Languages and tools for hybrid systems design},
  author={Carloni, Luca P and Passerone, Roberto and Pinto, Alessandro and Sangiovanni-Vincentelli, Alberto L and others},
  journal={Foundations and Trends{\textregistered} in Electronic Design Automation},
  volume={1},
  number={1--2},
  pages={1--193},
  year={2006},
  publisher={Now Publishers, Inc.}
}

[FRE11]

Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., ... & Maler, O. (2011, July). SpaceEx: Scalable verification of hybrid systems. In International Conference on Computer Aided Verification (pp. 379-395). Springer, Berlin, Heidelberg. pdf, appendix, presentation

BibTex entry

@inproceedings{frehse2011spaceex,
  title={SpaceEx: Scalable verification of hybrid systems},
  author={Frehse, Goran and Le Guernic, Colas and Donz{\'e}, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded},
  booktitle={International Conference on Computer Aided Verification},
  pages={379--395},
  year={2011},
  organization={Springer}
}

[FRE16]

Frehse, G. (2016). Scalable verification of hybrid systems. Habilitation á diriger des recherches, Univ. Grenoble Alpes.

BibTex entry

@phdthesis{frehse2016scalable,
  title={Scalable verification of hybrid systems},
  author={Frehse, Goran},
  year={2016}
}

[FR12]

Frehse, Goran, and Rajarshi Ray. Flowpipe-Guard Intersection for Reachability Computations with Support Functions. ADHS. 2012.

BibTex entry

@inproceedings{frehse2012flowpipe,
  title={Flowpipe-Guard Intersection for Reachability Computations with Support Functions.},
  author={Frehse, Goran and Ray, Rajarshi},
  booktitle={ADHS},
  pages={94--101},
  year={2012}
}

[GIR04]

Girard, Antoine. Analyse algorithmique des systemes hybrides. Diss. Institut National Polytechnique de Grenoble-INPG, 2004.

BibTex entry

@phdthesis{girard2004analyse,
  title={Analyse algorithmique des systemes hybrides},
  author={Girard, Antoine},
  year={2004},
  school={Institut National Polytechnique de Grenoble-INPG}
}

[GIR05]

Girard, A. (2005, March). Reachability of uncertain linear systems using zonotopes. In International Workshop on Hybrid Systems: Computation and Control (pp. 291-305). Springer, Berlin, Heidelberg.

BibTex entry

@inproceedings{girard2005reachability,
  title={Reachability of uncertain linear systems using zonotopes},
  author={Girard, Antoine},
  booktitle={International Workshop on Hybrid Systems: Computation and Control},
  pages={291--305},
  year={2005},
  organization={Springer}
}

[GIR13]

Girard, Antoine. Computational approaches to analysis and control of hybrid systems. Diss. 2013.

BibTex entry

@phdthesis{girard2013computational,
  title={Computational approaches to analysis and control of hybrid systems},
  author={Girard, Antoine},
  year={2013}
}

[GLGM06]

Girard, A., Le Guernic, C., & Maler, O. (2006, March). Efficient computation of reachable sets of linear time-invariant systems with inputs. In International Workshop on Hybrid Systems: Computation and Control (pp. 257-271). Springer, Berlin, Heidelberg.

BibTex entry

@inproceedings{girard2006efficient,
  title={Efficient computation of reachable sets of linear time-invariant systems with inputs},
  author={Girard, Antoine and Le Guernic, Colas and Maler, Oded},
  booktitle={International Workshop on Hybrid Systems: Computation and Control},
  pages={257--271},
  year={2006},
  organization={Springer}
}

[HG19]

el Hakim, Viktorio S., and Marco JG Bekooij. Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics. Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems. 2019.

BibTex entry

@inproceedings{el2019reachability,
  title={Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics},
  author={el Hakim, Viktorio S and Bekooij, Marco JG},
  booktitle={Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems},
  pages={27--36},
  year={2019}
}

[JOL]

Joldes, M. M. (2011). Approximations polynomiales rigoureuses et applications. Doctoral dissertation, Lyon, École normale supérieure.

BibTex entry

@phdthesis{joldes2011approximations,
  title={Approximations polynomiales rigoureuses et applications},
  author={Joldes, Mioara Maria},
  year={2011},
  school={Lyon, {\'E}cole normale sup{\'e}rieure}
}

[KEK18]

Kekatos, Nikolaos. Vérification formelle des systèmes cyber-physiques dans le processus industriel de la conception basée sur modèle. Diss. Grenoble Alpes, 2018.

BibTex entry

@phdthesis{kekatos2018verification,
  title={V{\'e}rification formelle des syst{\`e}mes cyber-physiques dans le processus industriel de la conception bas{\'e}e sur mod{\`e}le},
  author={Kekatos, Nikolaos},
  year={2018},
  school={Grenoble Alpes}
}

[LGG09]

Le Guernic, Colas, and Antoine Girard. Reachability analysis of linear systems using support functions. Nonlinear Analysis: Hybrid Systems 4.2 (2010): 250-262. pdf

BibTex entry

@article{le2010reachability,
  title={Reachability analysis of linear systems using support functions},
  author={Le Guernic, Colas and Girard, Antoine},
  journal={Nonlinear Analysis: Hybrid Systems},
  volume={4},
  number={2},
  pages={250--262},
  year={2010},
  publisher={Elsevier}
}

[LGG09b]

Le Guernic, Colas, and Antoine Girard. Reachability analysis of hybrid systems using support functions. International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 2009.

BibTex entry

@inproceedings{le2009reachability,
  title={Reachability analysis of hybrid systems using support functions},
  author={Le Guernic, Colas and Girard, Antoine},
  booktitle={International Conference on Computer Aided Verification},
  pages={540--554},
  year={2009},
  organization={Springer}
}

[LG09]

Le Guernic, Colas. Calcul d’Atteignabilité des Systemes Hybrides a Partie Continue Linéaire. Diss. PhD thesis, Université Grenoble I, 2009.

BibTex entry

@phdthesis{le2009calcul,
  title={Calcul d’Atteignabilit{\'e} des Systemes Hybrides a Partie Continue Lin{\'e}aire},
  author={Le Guernic, Colas},
  year={2009},
  school={Citeseer}
}

[M65]

Moore, Ramon E. Automatic local coordinate transformations to reduce the growth of error bounds in interval computation of solutions of ordinary differential equations. Error in digital computation 2 (1965): 103-140.

BibTex entry

@article{moore1965automatic,
  title={Automatic local coordinate transformations to reduce the growth of error bounds in interval computation of solutions of ordinary differential equations},
  author={Moore, Ramon E},
  journal={Error in digital computation},
  volume={2},
  pages={103--140},
  year={1965}
}

[RAY12]

Ray, Rajarshi. Calcul d'Atteignabilité des systèmes hybrides avec des fonctions de support. Diss. 2012.

BibTex entry

@phdthesis{ray2012calcul,
  title={Calcul d'Atteignabilit{\'e} des syst{\`e}mes hybrides avec des fonctions de support},
  author={Ray, Rajarshi},
  year={2012}
}

[ROC18]

Rocca, Alexandre. Formal methods for modelling and validation of biological models. Diss. Grenoble Alpes, 2018.

BibTex entry

@phdthesis{rocca2018formal,
  title={Formal methods for modelling and validation of biological models},
  author={Rocca, Alexandre},
  year={2018},
  school={Grenoble Alpes}
}

[SCHI18]

Schilling, Christian-Matthias. Fundamental techniques for the scalable analysis of systems. Diss. University of Freiburg, Freiburg im Breisgau, Germany, 2018.

BibTex entry

@phdthesis{schilling2018fundamental,
  title={Fundamental techniques for the scalable analysis of systems.},
  author={Schilling, Christian-Matthias},
  year={2018},
  school={University of Freiburg, Freiburg im Breisgau, Germany}
}

[SCHU19]

Schupp, Stefan. State set representations and their usage in the reachability analysis of hybrid systems. No. RWTH-2019-08875. Fachgruppe Informatik, 2019.

BibTex entry

@techreport{schupp2019state,
  title={State set representations and their usage in the reachability analysis of hybrid systems},
  author={Schupp, Stefan},
  year={2019},
  institution={Fachgruppe Informatik}
}

[YS18]

Yang, Xuejiao, and Joseph K. Scott. A comparison of zonotope order reduction techniques. Automatica 95 (2018): 378-384.

BibTex entry

@article{yang2018comparison,
  title={A comparison of zonotope order reduction techniques},
  author={Yang, Xuejiao and Scott, Joseph K},
  journal={Automatica},
  volume={95},
  pages={378--384},
  year={2018},
  publisher={Elsevier}
}