Article

Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata

Authors:

Pedro R. D'Argenio,

Arnd Hartmanns,

Sean SedwardsAuthors Info & Claims

IFM 2016: Proceedings of the 12th International Conference on Integrated Formal Methods - Volume 9681

Pages 99 - 114

https://doi.org/10.1007/978-3-319-33693-0_7

Published: 01 June 2016 Publication History

Abstract

The verification of probabilistic timed automata involves finding schedulers that optimise their nondeterministic choices with respect to the probability of a property. In practice, approaches based on model checking fail due to state-space explosion, while simulation-based techniques like statistical model checking are not applicable due to the nondeterminism. We present a new lightweight on-the-fly algorithm to find near-optimal schedulers for probabilistic timed automata. We make use of the classical region and zone abstractions from timed automata model checking, coupled with a recently developed smart sampling technique for statistical verification of Markov decision processes. Our algorithm provides estimates for both maximum and minimum probabilities. We compare our new approach with alternative techniques, first using tractable examples from the literature, then motivate its scalability using case studies that are intractable to numerical model checking and challenging for existing statistical techniques.

References

[1]

Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 1262, 183---235 1994

Digital Library

[2]

Bohnenkamp, H., D'Argenio, P., Hermanns, H., Katoen, J.P.: MoDeST: a compositional modeling formalism for real-time and stochastic systems. IEEE Trans. Softw. Eng. 3210, 812---830 2006

Digital Library

[3]

Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: a flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D'Argenio, P.R. eds. QEST 2013. LNCS, vol. 8054, pp. 160---164. Springer, Heidelberg 2013

Digital Library

[4]

Brázdil, T., Chatterjee, K., Chmelík, M., Forejt, V., Křetínský, J., Kwiatkowska, M., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. eds. ATVA 2014. LNCS, vol. 8837, pp. 98---114. Springer, Heidelberg 2014

[5]

D'Argenio, P., Legay, A., Sedwards, S., Traonouez, L.M.: Smart sampling for lightweight verification of Markov decision processes. STTT 174, 469---484 2015

Digital Library

[6]

David, A., Jensen, P.G., Larsen, K.G., Mikuă ionis, M., Taankvist, J.H.: Uppaal stratego. In: Baier, C., Tinelli, C. eds. TACAS 2015. LNCS, vol. 9035, pp. 206---211. Springer, Heidelberg 2015

Digital Library

[7]

David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT 174, 397---415 2015

Digital Library

[8]

Hahn, E.M., Hartmanns, A., Hermanns, H.: Reachability and reward checking for stochastic timed automata. ECEASST, 70 2014

[9]

Henriques, D., Martins, J.G., Zuliani, P., Platzer, A., Clarke, E.M.: Statistical model checking for Markov decision processes. In: 2012 Ninth International Conference on Quantitative Evaluation of Systems, pp. 84---93. IEEE 2012

Digital Library

[10]

Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. eds. VMCAI 2004. LNCS, vol. 2937, pp. 73---84. Springer, Heidelberg 2004

[11]

Jegourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking --- PLASMA. In: Flanagan, C., König, B. eds. TACAS 2012. LNCS, vol. 7214, pp. 498---503. Springer, Heidelberg 2012

Digital Library

[12]

Knuth, D.E.: The Art of Computer Programming: Sorting and Searching, 2nd edn. Addison-Wesley, Redwood 1998

Digital Library

[13]

Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proceedings of the 9th International Conference on Quantitative Evaluation of SysTems QEST 2012. pp. 203---204. IEEE CS Press, September 2012

Digital Library

[14]

Kwiatkowska, M.Z., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F.W. eds. FORMATS 2009. LNCS, vol. 5813, pp. 212---227. Springer, Heidelberg 2009

Digital Library

[15]

Kwiatkowska, M.Z., 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

Digital Library

[16]

Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. FMSD 291, 33---78 2006

Digital Library

[17]

Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 2821, 101---150 2002

Digital Library

[18]

Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 2057, 1027---1077 2007

Digital Library

[19]

Legay, A., Sedwards, S., Traonouez, L.: Estimating rewards & rare events in nondeterministic systems. ECEASST, 72 2015

[20]

Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. eds. CAV 2002. LNCS, vol. 2404, pp. 223---235. Springer, Heidelberg 2002

Digital Library

Cited By

Andriushchenko RBork ABudde CČeška MGrover KHahn EHartmanns AIsraelsen BJansen NJeppson JJunges SKöhl MKönighofer BKřetínský JMeggendorfer TParker DPranger SQuatmann TRuijters ETaylor LVolk MWeininger MZhang Z(2024)Tools at the Frontiers of Quantitative VerificationTOOLympics Challenge 202310.1007/978-3-031-67695-6_4(90-146)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-67695-6_4
Butkova YHartmanns AHermanns H(2021)A Modest Approach to Markov AutomataACM Transactions on Modeling and Computer Simulation10.1145/344935531:3(1-34)Online publication date: 24-Aug-2021
https://dl.acm.org/doi/10.1145/3449355
Hartmanns AKatoen JKohlen BSpel J(2021)Tweaking the Odds in Probabilistic Timed AutomataQuantitative Evaluation of Systems10.1007/978-3-030-85172-9_3(39-58)Online publication date: 23-Aug-2021
https://dl.acm.org/doi/10.1007/978-3-030-85172-9_3
Show More Cited By

Index Terms

Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking

Recommendations

Interrupt Timed Automata: verification and expressiveness

We introduce the class of Interrupt Timed Automata (ITA), a subclass of hybrid automata well suited to the description of timed multi-task systems with interruptions in a single processor environment.

While the reachability problem is undecidable for ...
Heuristics for probabilistic timed automata with abstraction refinement
MMB'12/DFT'12: Proceedings of the 16th international GI/ITG conference on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance

Probabilistic Timed Automata provide a theory to model and verify real-time systems with non-deterministic and probabilistic behaviors. The main approach to model checking Probabilistic Timed Automata is based on encoding the time behavior either with ...
Pushdown timed automata: a binary reachability characterization and safety verification

We consider pushdown timed automata (PTAs) that are timed automata (with dense clocks) augmented with a pushdown stack. A configuration of a PTA includes a state, dense clock values and a stack word. By using the pattern technique, we give a decidable ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

IFM 2016: Proceedings of the 12th International Conference on Integrated Formal Methods - Volume 9681

June 2016

512 pages

ISBN:9783319336923

Editors:
Erika Ábrahám
RWTH Aachen University, Aachen, Germany
,
Marieke Huisman
University of Twente, Enschede, The Netherlands

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 June 2016

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Andriushchenko RBork ABudde CČeška MGrover KHahn EHartmanns AIsraelsen BJansen NJeppson JJunges SKöhl MKönighofer BKřetínský JMeggendorfer TParker DPranger SQuatmann TRuijters ETaylor LVolk MWeininger MZhang Z(2024)Tools at the Frontiers of Quantitative VerificationTOOLympics Challenge 202310.1007/978-3-031-67695-6_4(90-146)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-67695-6_4
Butkova YHartmanns AHermanns H(2021)A Modest Approach to Markov AutomataACM Transactions on Modeling and Computer Simulation10.1145/344935531:3(1-34)Online publication date: 24-Aug-2021
https://dl.acm.org/doi/10.1145/3449355
Hartmanns AKatoen JKohlen BSpel J(2021)Tweaking the Odds in Probabilistic Timed AutomataQuantitative Evaluation of Systems10.1007/978-3-030-85172-9_3(39-58)Online publication date: 23-Aug-2021
https://dl.acm.org/doi/10.1007/978-3-030-85172-9_3
Budde CHartmanns AKlauck MKřetínský JParker DQuatmann TTurrini AZhang Z(2020)On Correctness, Precision, and Performance in Quantitative VerificationLeveraging Applications of Formal Methods, Verification and Validation: Tools and Trends10.1007/978-3-030-83723-5_15(216-241)Online publication date: 20-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-83723-5_15
D’Argenio PHartmanns ASedwards S(2018)Lightweight Statistical Model Checking in Nondeterministic Continuous TimeLeveraging Applications of Formal Methods, Verification and Validation. Verification10.1007/978-3-030-03421-4_22(336-353)Online publication date: 5-Nov-2018
https://dl.acm.org/doi/10.1007/978-3-030-03421-4_22
Hartmanns ASedwards SD'Argenio P(2017)Efficient simulation-based verification of probabilistic timed automataProceedings of the 2017 Winter Simulation Conference10.5555/3242181.3242296(1-12)Online publication date: 3-Dec-2017
https://dl.acm.org/doi/10.5555/3242181.3242296

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents