Skip to main content

ParetoLib: A Python Library for Parameter Synthesis

  • Conference paper
  • First Online:
Book cover Formal Modeling and Analysis of Timed Systems (FORMATS 2019)

Abstract

This paper presents ParetoLib, a Python library that implements a new method for inferring the Pareto front in multi-criteria optimization problems. The tool can be applied in the parameter synthesis of temporal logic predicates where the influence of parameters is monotone. ParetoLib currently provides support for the parameter synthesis of standard (STL) and extended (STLe) Signal Temporal Logic specifications. The tool is easily upgradeable for synthesizing parameters in other temporal logics in the near future. An example illustrates the usage and performance of our tool. ParetoLib is free and publicly available on Internet.

Oded Maler passed away at the beginning of September 2018. This work was initiated by him [8] continued with and finished by the rest of us.

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

Access this chapter

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

References

  1. Bakhirkin, A.: StlEval, STL Evaluator (2019). https://gitlab.com/abakhirkin/StlEval

  2. Bakhirkin, A., Basset, N.: Specification and efficient monitoring beyond STL. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 79–97. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_5

    Chapter  Google Scholar 

  3. Bakhirkin, A., Basset, N., Maler, O., Requeno, J.I.: Learning Pareto Front and Application to Parameter Synthesis of STL (2019). https://hal.archives-ouvertes.fr/hal-02125140, technical report

  4. Basset, N., Maler, O., Jarabo, J.I.R.: ParetoLib library (2018). https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/tempo/multidimensional_search

  5. Donzé, A., Ferrère, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264–279. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_19

    Chapter  Google Scholar 

  6. Donzé, A., Maler, O.: Robust Satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15297-9_9

    Chapter  MATH  Google Scholar 

  7. Jaszkiewicz, A., Lust, T.: ND-Tree-based update: a fast algorithm for the dynamic non-dominance problem. IEEE Trans. Evol. Comput. 22(5), 778–791 (2018). https://doi.org/10.1109/TEVC.2018.2799684

    Article  Google Scholar 

  8. Maler, O.: Learning Monotone Partitions of Partially-Ordered Domains (Work in Progress), July 2017. https://hal.archives-ouvertes.fr/hal-01556243, working paper or preprint

  9. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_12

    Chapter  MATH  Google Scholar 

  10. Ničković, D., Lebeltel, O., Maler, O., Ferrère, T., Ulus, D.: AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 303–319. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3_18

    Chapter  Google Scholar 

  11. Vazquez-Chanlatte, M.: Multidimensional thresholds (2018), https://github.com/mvcisback/multidim-threshold

  12. Vazquez-Chanlatte, M., Deshmukh, J.V., Jin, X., Seshia, S.A.: Logical clustering and learning for time-series data. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 305–325. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_15

    Chapter  Google Scholar 

  13. Vazquez-Chanlatte, M., Ghosh, S., Deshmukh, J.V., Sangiovanni-Vincentelli, A., Seshia, S.A.: Time-Series learning using monotonic logical properties. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 389–405. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03769-7_22

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to José-Ignacio Requeno Jarabo .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bakhirkin, A., Basset, N., Maler, O., Jarabo, JI.R. (2019). ParetoLib: A Python Library for Parameter Synthesis. In: André, É., Stoelinga, M. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2019. Lecture Notes in Computer Science(), vol 11750. Springer, Cham. https://doi.org/10.1007/978-3-030-29662-9_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29662-9_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29661-2

  • Online ISBN: 978-3-030-29662-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics