Decisiveness of stochastic systems and its application to hybrid models

Bouyer, Patricia; Brihaye, Thomas; Randour, Mickaël; Rivière, Cédric; Vandenhove, Pierre

doi:10.1016/j.ic.2021.104861

Download

Article (Scientific journals)

Decisiveness of stochastic systems and its application to hybrid models

Bouyer, Patricia; Brihaye, Thomas; Randour, Mickaël et al.

2022 • In Information and Computation, 289 (B), p. 104861

Peer Reviewed verified by ORBi

Permalink
https://hdl.handle.net/20.500.12907/43068

DOI
10.1016/j.ic.2021.104861

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

2009.13152.pdf

Author preprint (999.97 kB)

Download

All documents in ORBi UMONS are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Research center :

CREMMI - Modélisation mathématique et informatique

Disciplines :

Mathematics
Computer science

Author, co-author :

Bouyer, Patricia ; Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Gif-sur-Yvette, France

Brihaye, Thomas ; Université de Mons - UMONS > Faculté des Sciences > Service de Mathématiques effectives

Randour, Mickaël ; Université de Mons - UMONS > Faculté des Sciences > Service de Mathématiques effectives

Rivière, Cédric ; Université de Mons - UMONS > 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, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Gif-sur-Yvette, France

Language :

English

Title :

Decisiveness of stochastic systems and its application to hybrid models

Publication date :

November 2022

Journal title :

Information and Computation

ISSN :

0890-5401

eISSN :

1090-2651

Publisher :

Elsevier Inc.

Special issue title :

Special Issue on 11th Int. Symp. on Games, Automata, Logics and Formal Verification

Volume :

289

Issue :

Pages :

104861

Peer reviewed :

Peer Reviewed verified by ORBi

Additional URL :

https://api.elsevier.com/content/article/PII:S0890540121001930?httpAccept=text/xml

Research unit :

S820 - Mathématiques effectives

Research institute :

R150 - Institut de Recherche sur les Systèmes Complexes

Name of the research project :

3284 - CQ-Randour - ManySynth - Fédération Wallonie Bruxelles
3944 - MIS-Randour - ManySynth - Fédération Wallonie Bruxelles
4743 - ASP-Vandenhove - FrontieRS - Fédération Wallonie Bruxelles
5564 - ASPREN-Randour - FrontieRS - Fédération Wallonie Bruxelles

Funders :

F.R.S.-FNRS - Fonds de la Recherche Scientifique

Funding text :

Research partly supported by F.R.S.-FNRS under Grant n∘ F.4520.18 (ManySynth) and Grant n∘ T.0027.21 , by ENS Paris-Saclay visiting professorship (M. Randour, 2019), and by ANR MAVeriQ ( ANR-20-CE25-0012 ).

Available on ORBi UMONS :

since 27 June 2022

Statistics

Number of views

66 (8 by UMONS)

Number of downloads

81 (5 by UMONS)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

Bibliography

Abdulla, P.A., Ben Henda, N., Mayr, R., Decisive Markov chains. Log. Methods Comput. Sci., 3(4), 2007, 10.2168/LMCS-3(4:7)2007.
Bertrand, N., Bouyer, P., Brihaye, T., Carlier, P., When are stochastic transition systems tameable?. J. Log. Algebraic Methods Program. 99 (2018), 41–96, 10.1016/j.jlamp.2018.03.004.
Brihaye, T., Michaux, C., Rivière, C., Troestler, C., On o-minimal hybrid systems. Alur and Pappas [47], 2004, 219–233 https://doi.org/10.1007/978-3-540-24743-2_15.
Gentilini, R., Reachability problems on extended o-minimal hybrid automata. Pettersson, P., Yi, W., (eds.) Formal Modeling and Analysis of Timed Systems, Proceedings, Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005 Lecture Notes in Computer Science, vol. 3829, 2005, Springer, 162–176 https://doi.org/10.1007/11603009_14.
Lafferriere, G., Pappas, G.J., Sastry, S., O-minimal hybrid systems. Math. Control Signals Syst. 13:1 (2000), 1–21, 10.1007/PL00009858.
Baier, C., Katoen, J., Principles of Model Checking. 2008, MIT Press.
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P., What's decidable about hybrid automata?. J. Comput. Syst. Sci. 57:1 (1998), 94–124, 10.1006/jcss.1998.1581.
Henzinger, T.A., Raskin, J., Robust undecidability of timed and hybrid systems. Lynch and Krogh [48], 2000, 145–159 https://doi.org/10.1007/3-540-46430-1_15.
Alur, R., Dill, D.L., A theory of timed automata. Theor. Comput. Sci. 126:2 (1994), 183–235, 10.1016/0304-3975(94)90010-8.
Berarducci, A., Otero, M., An additive measure in o-minimal expansions of fields. Q. J. Math. 55:4 (2004), 411–419, 10.1093/qmath/hah010.
Tarski, A., A Decision Method for Elementary Algebra and Geometry. 1951, University of California Press, Berkeley, California.
Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Größer, M., Almost-sure model checking of infinite paths in one-clock timed automata. Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24–27 June 2008, 2008, IEEE Computer Society, Pittsburgh, PA, USA, 217–226 https://doi.org/10.1109/LICS.2008.25.
Bertrand, N., Bouyer, P., Brihaye, T., Markey, N., Quantitative model-checking of one-clock timed automata under probabilistic semantics. Fifth International Conference on the Quantitative Evaluation of Systems, QEST 2008, 14–17 September 2008, Saint-Malo, France, 2008, IEEE Computer Society, 55–64 https://doi.org/10.1109/QEST.2008.19.
Bertrand, N., Bouyer, P., Brihaye, T., Menet, Q., Baier, C., Größer, M., Jurdzinski, M., Stochastic timed automata. Log. Methods Comput. Sci., 10(4), 2014, 10.2168/LMCS-10(4:6)2014.
Carlier, P., Verification of stochastic timed automata. (Vérification des automates temporisés et stochastiques). Ph.D. thesis, 2017, University of Paris-Saclay, France https://tel.archives-ouvertes.fr/tel-01696130.
Hu, J., Lygeros, J., Sastry, S., Towards a theory of stochastic hybrid systems. Lynch and Krogh [48], 2000, 160–173 https://doi.org/10.1007/3-540-46430-1_16.
Cassandras, C.G., Lygeros, J., Stochastic Hybrid Systems. 2007, CRC Press https://doi.org/10.1201/9781420008548.
Lygeros, J., Prandini, M., Stochastic hybrid systems: a powerful framework for complex, large scale applications. Eur. J. Control 16:6 (2010), 583–594, 10.3166/ejc.16.583-594.
Bujorianu, L.M., Stochastic Reachability Analysis of Hybrid Systems. 2012, Springer Science & Business Media https://doi.org/10.1007/978-1-4471-2795-6.
Prandini, M., Hu, J., Application of reachability analysis for stochastic hybrid systems to aircraft conflict prediction. IEEE Trans. Autom. Control 54:4 (2009), 913–917, 10.1109/TAC.2008.2011011.
Prandini, M., Hu, J., Lygeros, J., Sastry, S., A probabilistic approach to aircraft conflict detection. IEEE Trans. Intell. Transp. Syst. 1:4 (2000), 199–220, 10.1109/6979.898224.
Hespanha, J.P., Stochastic hybrid systems: application to communication networks. Alur and Pappas [47], 2004, 387–401 https://doi.org/10.1007/978-3-540-24743-2_26.
Li, X., Omotere, O., Qian, L., Dougherty, E.R., Review of stochastic hybrid systems with applications in biological systems modeling and analysis. EURASIP J. Bioinform. Syst. Biol., 2017, 2017, 8, 10.1186/s13637-017-0061-5.
Singh, A., Hespanha, J.P., Stochastic hybrid systems for studying biochemical processes. Philos. Trans. R. Soc. A, Math. Phys. Eng. Sci. 368:1930 (2010), 4995–5011, 10.1098/rsta.2010.0211.
David, A., Du, D., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S., Statistical model checking for stochastic hybrid systems. Bartocci, E., Bortolussi, L., (eds.) Proceedings First International Workshop on Hybrid Systems and Biology, HSB 2012, Newcastle upon Tyne, UK, 3rd September 2012, vol. 92, 2012, 122–136 https://doi.org/10.4204/EPTCS.92.9.
Abate, A., Katoen, J., Lygeros, J., Prandini, M., Approximate model checking of stochastic hybrid systems. Eur. J. Control 16:6 (2010), 624–641, 10.3166/ejc.16.624-641.
Abate, A., Prandini, M., Lygeros, J., Sastry, S., Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44:11 (2008), 2724–2734, 10.1016/j.automatica.2008.03.027.
Bouyer, P., Brihaye, T., Randour, M., Rivière, C., Vandenhove, P., Decisiveness of stochastic systems and its application to hybrid models. Raskin, J., Bresolin, D., (eds.) Proceedings of the Eleventh International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, 21-22nd September 2020 EPTCS, vol. 326, 2020, 149–165 https://doi.org/10.4204/EPTCS.326.10.
Ash, R.B., Real Analysis and Probability. Probability and Mathematical Statistics, vol. 11, 1972, Academic Press, New York.
Pnueli, A., The temporal logic of programs., Providence Rhode Island, USA, 31 October - 1 November 1977 18th Annual Symposium on Foundations of Computer Science, 1977, IEEE Computer Society, 46–57 https://doi.org/10.1109/SFCS.1977.32.
Bogachev, V.I., Measure Theory, vol. 1. 2007, Springer Science & Business Media https://doi.org/10.1007/978-3-540-34514-5.
Gburek, D., Baier, C., Klüppelholz, S., Composition of stochastic transition systems based on spans and couplings. 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy LIPIcs, vol. 55, 2016, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 102:1–102:15 https://doi.org/10.4230/LIPIcs.ICALP.2016.102.
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S., The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138:1 (1995), 3–34, 10.1016/0304-3975(94)00202-T.
Henzinger, T.A., The theory of hybrid automata. Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, 1996, IEEE Computer Society, 278–292 https://doi.org/10.1109/LICS.1996.561342.
Bouyer, P., Dufourd, C., Fleury, E., Petit, A., Updatable timed automata. Theor. Comput. Sci. 321:2–3 (2004), 291–345, 10.1016/j.tcs.2004.04.003.
Hodges, W., A Shorter Model Theory. 1997, Cambridge University Press.
van den Dries, L., Remarks on Tarski's problem concerning (R, +, *, exp). Stud. Logic Found. Math. 112:C (1984), 97–121, 10.1016/S0049-237X(08)71811-1.
Pillay, A., Steinhorn, C., Definable sets in ordered structures. I. Trans. Am. Math. Soc. 295:2 (1986), 565–592, 10.2307/2000052.
Wilkie, A.J., Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function. J. Am. Math. Soc. 9:4 (1996), 1051–1094, 10.1090/S0894-0347-96-00216-0.
Macintyre, A., Wilkie, A.J., On the decidability of the real exponential field. Kreiseliana: About and Around Georg Kreisel, 1996, A.K. Peters, 441–467.
Knight, J.F., Pillay, A., Steinhorn, C., Definable sets in ordered structures. II. Trans. Am. Math. Soc. 295:2 (1986), 593–605, 10.1090/S0002-9947-1986-0833698-1.
Kaiser, T., First order tameness of measures. Ann. Pure Appl. Log. 163:12 (2012), 1903–1927, 10.1016/j.apal.2012.06.002.
Horváth, A., Paolieri, M., Ridi, L., Vicario, E., Transient analysis of non-Markovian models using stochastic state classes. Perform. Eval. 69:7–8 (2012), 315–335, 10.1016/j.peva.2011.11.002.
Paolieri, M., Horváth, A., Vicario, E., Probabilistic model checking of regenerative concurrent systems. IEEE Trans. Softw. Eng. 42:2 (2016), 153–169, 10.1109/TSE.2015.2468717.
Durrett, R., Probability: Theory and Examples. 5th edition Cambridge Series in Statistical and Probabilistic Mathematics, 2019, Cambridge University Press https://doi.org/10.1017/9781108591034.
Minsky, M.L., Computation: finite and infinite machines. Prentice-Hall Series in Automatic Computation, 1967, Prentice-Hall Inc.
Alur, R., Pappas, G.J., (eds.) Hybrid Systems: Computation and Control, Proceedings of the 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004 Lecture Notes in Computer Science, vol. 2993, 2004, Springer https://doi.org/10.1007/b96398.
Lynch, N.A., Krogh, B.H., (eds.) Hybrid Systems: Computation and Control, Proceedings of the Third International Workshop, HSCC 2000, Pittsburgh, PA, USA, March 23-25, 2000 Lecture Notes in Computer Science, vol. 1790, 2000, Springer https://doi.org/10.1007/3-540-46430-1.