Brihaye, Thomas ; Université de Mons > Faculté des Sciences > Service de Mathématiques effectives
Randour, Mickaël ; Université de Mons > Faculté des Sciences > Service de Mathématiques effectives
Rivière, Cédric ; Université de Mons > Faculté des Sciences > Service de Mathématiques appliquées
Vandenhove, Pierre ; Université de Mons - UMONS > Faculté des Sciences > Service de Mathématiques effectives ; Université Paris-Saclay > Laboratoire Méthodes Formelles (LMF)
Language :
English
Title :
Decisiveness of Stochastic Systems and its Application to Hybrid Models
Publication date :
21 September 2020
Event name :
International Symposium on Games, Automata, Logics and Formal Verification
Event place :
Brussels, Belgium
Event date :
2020
Audience :
International
Journal title :
Electronic Proceedings in Theoretical Computer Science
eISSN :
2075-2180
Publisher :
[Open Publishing Association], Sydney, Australia
Volume :
326
Pages :
149-165
Peer reviewed :
Peer Reviewed verified by ORBi
Research unit :
S820 - Mathématiques effectives
Research institute :
R150 - Institut de Recherche sur les Systèmes Complexes
Alessandro Abate, Joost-Pieter Katoen, John Lygeros & Maria Prandini (2010): Approximate Model Checking of Stochastic Hybrid Systems. Eur. J. Control 16(6), pp. 624-641, doi:10.3166/ejc.16.624-641.
Alessandro Abate, Maria Prandini, John Lygeros & Shankar Sastry (2008): Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), pp. 2724-2734, doi:10.1016/j.automatica.2008.03.027.
Parosh A. Abdulla, Noomene Ben Henda & Richard Mayr (2007): Decisive Markov Chains. Log. Methods Comput. Sci. 3(4), doi:10.2168/LMCS-3(4:7)2007.
Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis & Sergio Yovine (1995): The Algorithmic Analysis of Hybrid Systems. Theor. Comput. Sci. 138(1), pp. 3-34, doi:10.1016/0304-3975(94)00202-T.
Rajeev Alur & David L. Dill (1994): A Theory of Timed Automata. Theor. Comput. Sci. 126(2), pp. 183-235, doi:10.1016/0304-3975(94)90010-8.
Rajeev Alur & George J. Pappas, editors (2004): Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004, Proceedings. Lecture Notes in Computer Science 2993, Springer, doi:10.1007/b96398.
Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye & Marcus Größer (2008): Almost- Sure Model Checking of Infinite Paths in One-Clock Timed Automata. In: Proceedings of the Twenty- Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, IEEE Computer Society, pp. 217-226, doi:10.1109/LICS.2008.25. Available at https://ieeexplore.ieee.org/xpl/conhome/4557886/proceeding.
Christel Baier & Joost-Pieter Katoen (2008): Principles of model checking. MIT Press.
Alessandro Berarducci & Margarita Otero (2004): An additive measure in o-minimal expansions of fields. Q. J. Math. 55(4), pp. 411-419, doi:10.1093/qmath/hah010.
Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye & Pierre Carlier (2018): When are stochastic transition systems tameable? J. Log. Algebr. Meth. Program. 99, pp. 41-96, doi:10.1016/j.jlamp.2018.03.004.
Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye & Nicolas Markey (2008): Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics. In: Fifth International Conference on the Quantitative Evaluation of Systems (QEST 2008), 14-17 September 2008, Saint-Malo, France, IEEE Computer Society, pp. 55-64, doi:10.1109/QEST.2008.19. Available at https://ieeexplore.ieee.org/xpl/conhome/4634932/proceeding.
Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Quentin Menet, Christel Baier, Marcus Größer & Marcin Jurdzinski (2014): Stochastic Timed Automata. Log. Methods Comput. Sci. 10(4), doi:10.2168/LMCS-10(4:6)2014.
Vladimir I. Bogachev (2007): Measure theory. 1, Springer Science & Business Media, doi:10.1007/978-3-540-34514-5.
Patricia Bouyer, Thomas Brihaye, Mickael Randour, Cédric Rivière & Pierre Vandenhove (2020): Decisiveness of Stochastic Systems and its Application to Hybrid Models (Full Version). CoRR.
Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury & Antoine Petit (2004): Updatable timed automata. Theor. Comput. Sci. 321(2-3), pp. 291-345, doi:10.1016/j.tcs.2004.04.003.
Thomas Brihaye, Christian Michaux, Cédric Rivière & Christophe Troestler (2004): On O-Minimal Hybrid Systems. In Alur & Pappas [6], pp. 219-233, doi:10.1007/978-3-540-24743-2_15.
Luminita Manuela Bujorianu (2012): Stochastic reachability analysis of hybrid systems. Springer Science & Business Media, doi:10.1007/978-1-4471-2795-6.
Pierre Carlier (2017): Verification of Stochastic Timed Automata. (Vérification des automates temporisés et stochastiques). Ph.D. thesis, University of Paris-Saclay, France. Available at https://tel.archives-ouvertes.fr/tel-01696130.
Christos G. Cassandras & John Lygeros (2007): Stochastic Hybrid Systems. CRC Press, doi:10.1201/9781420008548.
Alexandre David, Dehui Du, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen & Sean Sedwards (2012): Statistical Model Checking for Stochastic Hybrid Systems. In Ezio Bartocci & Luca Bortolussi, editors: Proceedings First International Workshop on Hybrid Systems and Biology, HSB 2012, Newcastle Upon Tyne, UK, 3rd September 2012, EPTCS 92, pp. 122-136, doi:10.4204/EPTCS.92.9.
Daniel Gburek, Christel Baier & Sascha Klüppelholz (2016): Composition of Stochastic Transition Systems Based on Spans and Couplings. In: 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, LIPIcs 55, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 102:1-102:15, doi:10.4230/LIPIcs.ICALP.2016.102.
Raffaella Gentilini (2005): Reachability Problems on Extended O-Minimal Hybrid Automata. In Paul Pettersson & Wang Yi, editors: Formal Modeling and Analysis of Timed Systems, Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings, Lecture Notes in Computer Science 3829, Springer, pp. 162-176, doi:10.1007/11603009_14.
Thomas A. Henzinger (1996): The Theory of Hybrid Automata. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, IEEE Computer Society, pp. 278-292, doi:10.1109/LICS.1996.561342. Available at https://ieeexplore.ieee.org/xpl/conhome/4265/proceeding.
Thomas A. Henzinger, Peter W. Kopke, Anuj Puri & Pravin Varaiya (1998): What's Decidable about Hybrid Automata? J. Comput. Syst. Sci. 57(1), pp. 94-124, doi:10.1006/jcss.1998.1581.
Thomas A. Henzinger & Jean-François Raskin (2000): Robust Undecidability of Timed and Hybrid Systems. In Lynch & Krogh [35], pp. 145-159, doi:10.1007/3-540-46430-1_15.
João P. Hespanha (2004): Stochastic Hybrid Systems: Application to Communication Networks. In Alur & Pappas [6], pp. 387-401, doi:10.1007/978-3-540-24743-2_26.
Wilfrid Hodges (1997): A Shorter Model Theory. Cambridge University Press.
András Horváth, Marco Paolieri, Lorenzo Ridi & Enrico Vicario (2012): Transient analysis of non-Markovian models using stochastic state classes. Perform. Eval. 69(7-8), pp. 315-335, doi:10.1016/j.peva.2011.11.002.
Jianghai Hu, John Lygeros & Shankar Sastry (2000): Towards a Theory of Stochastic Hybrid Systems. In Lynch & Krogh [35], pp. 160-173, doi:10.1007/3-540-46430-1_16.
Tobias Kaiser (2012): First order tameness of measures. Ann. Pure Appl. Logic 163(12), pp. 1903-1927, doi:10.1016/j.apal.2012.06.002.
Julia F. Knight, Anand Pillay & Charles Steinhorn (1986): Definable sets in ordered structures. II. Transactions of the American Mathematical Society 295(2), pp. 593-605, doi:10.1090/S0002-9947-1986-0833698-1.
Gerardo Lafferriere, George J. Pappas & Shankar Sastry (2000): O-Minimal Hybrid Systems. Math. Control Signals Syst. 13(1), pp. 1-21, doi:10.1007/PL00009858.
Xiangfang Li, Oluwaseyi Omotere, Lijun Qian & Edward R. Dougherty (2017): Review of stochastic hybrid systems with applications in biological systems modeling and analysis. EURASIP J. Bioinformatics and Systems Biology 2017, p. 8, doi:10.1186/s13637-017-0061-5.
John Lygeros & Maria Prandini (2010): Stochastic Hybrid Systems: A Powerful Framework for Complex, Large Scale Applications. Eur. J. Control 16(6), pp. 583-594, doi:10.3166/ejc.16.583-594.
Nancy A. Lynch & Bruce H. Krogh, editors (2000): Hybrid Systems: Computation and Control, Third International Workshop, HSCC 2000, Pittsburgh, PA, USA, March 23-25, 2000, Proceedings. Lecture Notes in Computer Science 1790, Springer, doi:10.1007/3-540-46430-1.
Angus Macintyre & Alex J. Wilkie (1996): On the decidability of the real exponential field. In: Kreiseliana: About and around Georg Kreisel, A. K. Peters, pp. 441-467.
Marco Paolieri, András Horváth & Enrico Vicario (2016): Probabilistic Model Checking of Regenerative Concurrent Systems. IEEE Trans. Software Eng. 42(2), pp. 153-169, doi:10.1109/TSE.2015.2468717.
Anand Pillay & Charles Steinhorn (1986): Definable sets in ordered structures. I. Transactions of the American Mathematical Society 295(2), pp. 565-592, doi:10.2307/2000052.
Amir Pnueli (1977): The Temporal Logic of Programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, IEEE Computer Society, pp. 46-57, doi:10.1109/SFCS.1977.32. Available at https://ieeexplore.ieee.org/xpl/conhome/4567914/proceeding.
Maria Prandini & Jianghai Hu (2009): Application of Reachability Analysis for Stochastic Hybrid Systems to Aircraft Conflict Prediction. IEEE Trans. Automat. Contr. 54(4), pp. 913-917, doi:10.1109/TAC.2008.2011011.
Maria Prandini, JianghaiHu, John Lygeros& Shankar Sastry (2000): A probabilistic approach to aircraft conflict detection. IEEE Trans. Intelligent Transportation Systems 1(4), pp. 199-220, doi:10.1109/6979.898224.
Abhyudai Singh & Joao P. Hespanha (2010): Stochastic hybrid systems for studying biochemical processes. Philosophical Transactions of the Royal Society A:Mathematical, Physical and Engineering Sciences 368(1930), pp. 4995-5011, doi:10.1098/rsta.2010.0211.
Alfred Tarski (1951): A decision method for elementary algebra and geometry. University of California Press, Berkeley, California.
Lou van den Dries (1984): Remarks on Tarski's problem concerning (R, +, ∗, exp). Studies in Logic and the Foundations of Mathematics 112(C), pp. 97-121, doi:10.1016/S0049-237X(08)71811-1.
Alex J. Wilkie (1996): Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function. Journal of the American Mathematical Society 9(4), pp. 1051-1094, doi:10.1090/S0894-0347-96-00216-0.
