Abstract
This work investigates the use of finite abstractions to study the finite-horizon probabilistic invariance problem over Stochastic Max-Plus-Linear (SMPL) systems. SMPL systems are probabilistic extensions of discrete-event MPL systems that are widely employed in the engineering practice for timing and synchronisation studies. We construct finite abstractions by re-formulating the SMPL system as a discrete-time Markov process, then tailoring formal abstraction techniques in the literature to generate a finite-state Markov Chain (MC), together with precise guarantees on the level of the introduced approximation. This finally allows to probabilistically model check the obtained MC against the finite-horizon probabilistic invariance specification. The approach is practically implemented via a dedicated software, and elucidated in this work over numerical examples.
The first two authors have equally contributed to this work. This work has been supported by the European Commission via STREP project MoVeS 257005, Marie Curie grant MANTRAS 249295, and IAPP project AMBI 324432.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baccelli, F., Cohen, G., Gaujal, B.: Recursive equations and basic properties of timed Petri nets. Discrete Event Dynamic Systems: Theory and Applications 1(4), 415–439 (1992)
Hillion, H., Proth, J.: Performance evaluation of job-shop systems using timed event graphs. IEEE Trans. Autom. Control 34(1), 3–9 (1989)
Heidergott, B., Olsder, G., van der Woude, J.: Max Plus at Work–Modeling and Analysis of Synchronized Systems: A Course on Max-Plus Algebra and Its Applications. Princeton University Press (2006)
Roset, B., Nijmeijer, H., van Eekelen, J., Lefeber, E., Rooda, J.: Event driven manufacturing systems as time domain control systems. In: Proc. 44th IEEE Conf. Decision and Control and European Control Conf. (CDC-ECC 2005), pp. 446–451 (December 2005)
van Eekelen, J., Lefeber, E., Rooda, J.: Coupling event domain and time domain models of manufacturing systems. In: Proc. 45th IEEE Conf. Decision and Control (CDC 2006), pp. 6068–6073 (December 2006)
Brackley, C.A., Broomhead, D.S., Romano, M.C., Thiel, M.: A max-plus model of ribosome dynamics during mRNA translation. Journal of Theoretical Biology 303, 128–140 (2012)
Heidergott, B.: Max-Plus Linear Stochastic Systems and Perturbation Analysis (The International Series on Discrete Event Dynamic Systems). Springer-Verlag New York, Inc., Secaucus (2006)
Olsder, G., Resing, J., De Vries, R., Keane, M., Hooghiemstra, G.: Discrete event systems with stochastic processing times. IEEE Trans. Autom. Control 35(3), 299–302 (1990)
Resing, J., de Vries, R., Hooghiemstra, G., Keane, M., Olsder, G.: Asymptotic behavior of random discrete event systems. Stochastic Processes and their Applications 36(2), 195–216 (1990)
van der Woude, J.W., Heidergott, B.: Asymptotic growth rate of stochastic max-plus systems that with a positive probability have a sunflower-like support. In: Proc. 8th Int. Workshop Discrete Event Systems, pp. 451–456 (July 2006)
Goverde, R., Heidergott, B., Merlet, G.: A coupling approach to estimating the Lyapunov exponent of stochastic max-plus linear systems. European Journal of Operational Research 210(2), 249–257 (2011)
Baccelli, F., Cohen, G., Olsder, G., Quadrat, J.P.: Synchronization and Linearity, An Algebra for Discrete Event Systems. John Wiley and Sons (1992)
Baccelli, F., Hong, D.: Analytic expansions of max-plus Lyapunov exponents. The Annals of Applied Probability 10(3), 779–827 (2000)
Gaubert, S., Hong, D.: Series expansions of Lyapunov exponents and forgetful monoids. Technical Report RR-3971, INRIA (July 2000)
Merlet, G.: Cycle time of stochastic max-plus linear systems. Electronic Journal of Probability 13(12), 322–340 (2008)
Farahani, S., van den Boom, T., van der Weide, H., De Schutter, B.: An approximation approach for model predictive control of stochastic max-plus linear systems. In: Proc. 10th Int. Workshop Discrete Event Systems, Berlin, DE, pp. 386–391 (August/September 2010)
Farahani, S., van den Boom, T., De Schutter, B.: Exact and approximate approaches to the identification of stochastic max-plus-linear systems. In: Discrete Event Dynamic Systems: Theory and Applications, pp. 1–25 (April 2013)
Adzkiya, D., De Schutter, B., Abate, A.: Finite abstractions of max-plus-linear systems. IEEE Trans. Autom. Control 58(12), 3039–3053 (2013)
Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton Series in Computer Science. Princeton University Press (1994)
Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuous-time Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 146–162. Springer, Heidelberg (1999)
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Verifying quantitative properties of continuous probabilistic timed automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 123–137. Springer, Heidelberg (2000)
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Kushner, H.J., Dupuis, P.: Numerical Methods for Stochastic Control Problems in Continuous Time. Springer, New York (2001)
Chaput, P., Danos, V., Panangaden, P., Plotkin, G.: Approximating Markov processes by averaging. Journal of the ACM 61(1), 5:1–5:45 (2014)
Koutsoukos, X., Riley, D.: Computational methods for reachability analysis of stochastic hybrid systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 377–391. Springer, Heidelberg (2006)
Prandini, M., Hu, J.: Stochastic reachability: Theory and numerical approximation. In: Cassandras, C., Lygeros, J. (eds.) Stochastic Hybrid Systems. Automation and Control Engineering Series, vol. 24, pp. 107–138. Taylor & Francis Group/CRC Press (2006)
Abate, A., Katoen, J.P., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. European Journal of Control 16(6), 624–641 (2010)
Esmaeil Zadeh Soudjani, S., Abate, A.: Adaptive gridding for abstraction and verification of stochastic hybrid systems. In: Proceedings of the 8th International Conference on Quantitative Evaluation of Systems, pp. 59–69 (September 2011)
Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724–2734 (2008)
Esmaeil Zadeh Soudjani, S., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM Journal on Applied Dynamical Systems 12(2), 921–956 (2013)
Abate, A.: Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey. Electronic Notes in Theoretical Computer Sciences, 3–25 (2014)
Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Information and Computation 179(2), 163–193 (2002)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Katoen, J.P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: Proc. 2nd Int. Conf. Quantitative Evaluation of Systems (QEST 2005), pp. 243–244. IEEE Computer Society, Los Alamos (2005)
Esmaeil Zadeh Soudjani, S., Gevaerts, C., Abate, A.: FAUST \(^{\textsf 2}\): Formal Abstractions of Uncountable-STate STochastic processes arXiv:1403.3286 (2014)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Adzkiya, D., Esmaeil Zadeh Soudjani, S., Abate, A. (2014). Finite Abstractions of Stochastic Max-Plus-Linear Systems. In: Norman, G., Sanders, W. (eds) Quantitative Evaluation of Systems. QEST 2014. Lecture Notes in Computer Science, vol 8657. Springer, Cham. https://doi.org/10.1007/978-3-319-10696-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-10696-0_7
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10695-3
Online ISBN: 978-3-319-10696-0
eBook Packages: Computer ScienceComputer Science (R0)