Skip to main content
SpringerLink
Log in

Schedulers are no Prophets

  • Chapter
  • First Online:
Semantics, Logics, and Calculi

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9560))

Abstract

Several formalisms for concurrent computation have been proposed in recent years that incorporate means to express stochastic continuous-time dynamics and non-determinism. In this setting, some obscure phenomena are known to exist, related to the fact that schedulers may yield too pessimistic verification results, since current non-determinism can surprisingly be resolved based on prophesying the timing of future random events. This paper provides a thorough investigation of the problem, and it presents a solution: Based on a novel semantics of stochastic automata, we identify the class of schedulers strictly unable to prophesy, and show a path towards verification algorithms with respect to that class. The latter uses an encoding into the model of stochastic timed automata under arbitrary schedulers, for which model checking tool support has recently become available.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In this paper we restrict all F(c) to absolutely continuous measures as it simplifies the overall notation and the technical treatment. Recall that a measure is absolutely continuous if it assigns 0 to any set with Lebesgue measure 0.

  2. 2.

    Note that this is not Zeno behaviour: An edge will eventually be taken after a finite number of steps with probability 1.

References

  1. ns-2 wiki. http://nsnam.isi.edu/nsnam/

  2. ns-3. https://www.nsnam.org/

  3. Andel, T.R., Yasinsac, A.: On the credibility of Manet simulations. IEEE Computer 39(7), 48–54 (2006)

    Article  Google Scholar 

  4. Bogdoll, J., Ferrer Fioriti, L.M., Hartmanns, A., Hermanns, H.: Partial Order Methods for Statistical Model Checking and Simulation. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 59–74. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  5. Bogdoll, J., Hartmanns, A., Hermanns, H.: Simulation and statistical model checking for Modestly nondeterministic models. In: Schmitt, J.B. (ed.) MMB/DFT. LNCS, vol. 7201, pp. 249–252. Springer, Heidelberg (2012)

    Google Scholar 

  6. Bohnenkamp, H.C., D’Argenio, P.R., Hermanns, H., Katoen, J.-P.: MoDeST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng. 32(10), 812–830 (2006)

    Article  Google Scholar 

  7. Bravetti, M., D’Argenio, P.R.: Tutte le algebre insieme: concepts, discussions and relations of stochastic process algebras with general distributions. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 44–88. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Bravetti, M., Gorrieri, R.: The theory of interactive generalized semi-Markov processes. Theor. Comput. Sci. 282(1), 5–32 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  9. Cavin, D., Sasson, Y., Schiper, A.: On the accuracy of MANET simulators. In: POMC, pp. 38–43. ACM (2002)

    Google Scholar 

  10. D’Argenio, P.R., Katoen, J.-P.: A theory of stochastic systems, part I: stochastic automata. Inf. Comput. 203(1), 1–38 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  11. D’Argenio, P.R., Katoen, J.-P.: A theory of stochastic systems, part II: process algebra. Inf. Comput. 203(1), 39–74 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  12. Giro, S., D’Argenio, P.R.: Quantitative model checking revisited: neither decidable nor approximable. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 179–194. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  13. Haas, P.J., Shedler, G.S.: Regenerative generalized semi-Markov processes. Commun. Stat. Stoch. Models 3(3), 409–438 (1987)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  15. Harrison, P.G., Strulo, B.: SPADES - a process algebra for discrete event simulation. J. Log. Comput. 10(1), 3–42 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  16. Hartmanns, A., Hermanns, H.: The Modest Toolset: an integrated environment for quantitative modelling and verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 593–598. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  17. Hartmanns, A., Timmer, M.: Sound statistical model checking for MDP using partial order and confluence reduction. STTT 17(4), 429–456 (2015)

    Article  Google Scholar 

  18. Hermanns, H., Krčál, J., Křetínský, J.: Probabilistic bisimulation: naturally on distributions. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 249–265. Springer, Heidelberg (2014)

    Google Scholar 

  19. Kurkowski, S., Camp, T., Colagrosso, M.: MANET simulation studies: the incredibles. Mob. Comput. Commun. Rev. 9(4), 50–61 (2005)

    Article  Google Scholar 

  20. Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods Syst. Design 29(1), 33–78 (2006)

    Article  MATH  Google Scholar 

  21. Matthes, K.: Zur Theorie der Bedienungsprozesse. In: Transactions of the 3rd Prague Conference on Information Theory, Statistics Decision Functions and Random Processes, pp. 513–528 (1962)

    Google Scholar 

  22. Nielson, F., Nielson, H.R., Zeng, K.: Stochastic model checking of the stochastic quality calculus. In: De Nicola, R., Hennicker, R. (eds.) Wirsing Festschrift. LNCS, vol. 8950, pp. 522–537. Springer, Heidelberg (2015)

    Google Scholar 

  23. Pongor, G.: OMNeT: objective modular network testbed. In: MASCOTS, pp. 323–326. The Society for Computer Simulation (1993)

    Google Scholar 

  24. Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming, 1st edn. John Wiley & Sons Inc, New York (1994)

    Book  MATH  Google Scholar 

  25. Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D thesis, Laboratory for Computer Science, Massachusetts Institute of Technology (1995)

    Google Scholar 

  26. Stojmenovic, I.: Simulations in wireless sensor and ad hoc networks: matching and advancing models, metrics, and solutions. IEEE Commun. Mag. 46(12), 102–107 (2008)

    Article  Google Scholar 

  27. Strulo, B.: Process algebra for discrete event simulation. Ph.D thesis, Imperial College of Science, Technology and Medicine. University of London, October 1993

    Google Scholar 

  28. Timmer, M., van de Pol, J., Stoelinga, M.I.A.: Confluence reduction for Markov automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 243–257. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  29. Wolovick, N.: Continuous probability and nondeterminism in labeled transaction systems. PhD thesis, Universidad Nacional de Córdoba, Córdoba (2012)

    Google Scholar 

  30. Zeng, X., Bagrodia, R., Gerla, M.: GloMoSim: a library for parallel simulation of large-scale wireless networks. In: PADS, pp. 154–161. IEEE Computer Society (1998)

    Google Scholar 

Download references

Acknowledgements

This work is partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by the Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the CDZ project 1023 (CAP), and by the CAS/SAFEA International Partnership Program for Creative Research Teams.

Author information

Authors and Affiliations

  1. Computer Science, Saarland University, Saarbrücken, Germany

    Arnd Hartmanns, Holger Hermanns & Jan Krčál

Authors
  1. Arnd Hartmanns
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Holger Hermanns
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jan Krčál
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jan Krčál .

Editor information

Editors and Affiliations

  1. Technical University of Denmark, Kongens Lyngby, Denmark

    Christian W. Probst

  2. Imperial College London, London, United Kingdom

    Chris Hankin

  3. Aalborg University, Aalborg, Denmark

    René Rydhof Hansen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Hartmanns, A., Hermanns, H., Krčál, J. (2016). Schedulers are no Prophets. In: Probst, C., Hankin, C., Hansen, R. (eds) Semantics, Logics, and Calculi. Lecture Notes in Computer Science(), vol 9560. Springer, Cham. https://doi.org/10.1007/978-3-319-27810-0_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-27810-0_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-27809-4

  • Online ISBN: 978-3-319-27810-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation