Skip to main content
SpringerLink
Log in

Model Checking the STL Time-Bounded Until on Hybrid Petri Nets Using Nef Polyhedra

  • Conference paper
  • First Online:
Computer Performance Engineering (EPEW 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10497))

Included in the following conference series:

Abstract

Hybrid Petri nets have been extended with so-called general transitions, which add one random variable and one dimension to the underlying state space for each firing of a general transition. We propose an algorithm for model checking the time-bounded until operator in hybrid Petri nets with two general transition firings, based on boolean-set operations on Nef polyhedra. A case study on (dis)-charging an electrical vehicle shows the feasibility of the approach. Results are validated against a simulation tool and computation times are compared.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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.

    The change of fluid per time.

  2. 2.

    The model used for computation consists of 19 places and 26 transitions.

  3. 3.

    Corresponding to 1440 min or 24 h.

References

  1. Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  2. Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Uni. Hamburg (1962)

    Google Scholar 

  3. David, R., Alla, H.: On hybrid petri nets. Discrete Event Dyn. Syst. 11(1), 9–40 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  4. Henzinger, T.A.: The theory of hybrid automata. In: 11th Annual IEEE Symposium on Logic in Computer Science, p. 278, IEEE Computer Society (1996)

    Google Scholar 

  5. Gribaudo, M., Remke, A.: Hybrid petri nets with general one-shot transitions. Perform. Eval. 105, 22–50 (2016)

    Article  Google Scholar 

  6. Ghasemieh, H., Remke, A., Haverkort, B., Gribaudo, M.: Region-based analysis of hybrid petri nets with a single general one-shot transition. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 139–154. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33365-1_11

    Chapter  Google Scholar 

  7. Ghasemieh, H., Remke, A., Haverkort, B.: Hybrid petri nets with multiple stochastic transition firings. In: 8th EAI International Conference on Performance Evaluation Methodologies and Tools (ICST), pp. 217–224 (2014)

    Google Scholar 

  8. Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)

    Article  MathSciNet  Google Scholar 

  9. Nef, W.: Beiträge zur Theorie der Polyeder: mit Anwendungen in der Computergraphik. Beiträge zur Mathematik, Informatik und Nachrichtentechnik (1978)

    Google Scholar 

  10. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  11. Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101–150 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  12. Asarin, E., Maler, O., Pnueli, A.: Reachability analysis of dynamical systems having piecewise-constant derivatives. Theor. Comput. Sci. 138(1), 35–65 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  13. Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43, 116–146 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  14. Nickovic, D., Maler, O.: AMT: a property-based monitoring tool for analog systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 304–319. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75454-1_22

    Chapter  Google Scholar 

  15. Ghasemieh, H., Remke, A., Haverkort, B.R.: Survivability evaluation of fluid critical infrastructures using hybrid petri nets. In: IEEE 19th Pacific Rim International Symposium on Dependable Computing, pp. 152–161. IEEE (2013)

    Google Scholar 

  16. Pilch, C., Remke, A.: Statistical model checking for hybrid petri nets with multiple general transitions. In: 47th IEEE/IFIP International Conference on Dependable Systems and Networks. IEEE (2016). http://go.wwu.de/pbptn

  17. Abate, A., D’Innocenzo, A., Benedetto, M.D.D.: Approximate abstractions of stochastic hybrid systems. IEEE Trans. Autom. Control 56(11), 2688–2694 (2011)

    Article  MathSciNet  Google Scholar 

  18. Fränzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems (2011)

    Google Scholar 

  19. Hüls, J., Remke, A.: Coordinated charging strategies for plug-in electric vehicles to ensure a robust charging process. In: 10th EAI International Conference on Performance Evaluation Methodologies and Tools, ICST (2016)

    Google Scholar 

  20. The CGAL Project: CGAL User and Reference Manual. CGAL Editorial Board, 4.10 ed. (2017)

    Google Scholar 

  21. Schupp, S., Ábrahám, E., Makhlouf, I.B., Kowalewski, S.: HyPro: a C++ library of state set representations for hybrid systems reachability analysis. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 288–294. Springer, Cham (2017). doi:10.1007/978-3-319-57288-8_20

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Mathematics and Computer Science, Westfälische Wilhelms-Universität Münster, Münster, Germany

    Adrian Godde & Anne Remke

Authors
  1. Adrian Godde
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Anne Remke
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Anne Remke .

Editor information

Editors and Affiliations

  1. Bristol, Germany

    Philipp Reinecke

  2. University of L’Aquila, L’Aquila, Italy

    Antinisca Di Marco

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Godde, A., Remke, A. (2017). Model Checking the STL Time-Bounded Until on Hybrid Petri Nets Using Nef Polyhedra. In: Reinecke, P., Di Marco, A. (eds) Computer Performance Engineering. EPEW 2017. Lecture Notes in Computer Science(), vol 10497. Springer, Cham. https://doi.org/10.1007/978-3-319-66583-2_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66583-2_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66582-5

  • Online ISBN: 978-3-319-66583-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation