Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Poling: SMT Aided Linearizability Proofs Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Time Robustness in MTL and Expressivity in Hybrid System Falsification

verfasst von : Takumi Akazaki, Ichiro Hasuo

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Building on the work by Fainekos and Pappas and the one by Donzé and Maler, we introduce \(\mathbf{AvSTL }\), an extension of metric interval temporal logic by averaged temporal operators. Its expressivity in capturing both space and time robustness helps solving falsification problems (searching for a critical path in hybrid system models); it does so by communicating a designer’s intention more faithfully to the stochastic optimization engine employed in a falsification solver. We also introduce a sliding window-like algorithm that keeps the cost of computing truth/robustness values tractable.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Automatic Verification of Stability and Safety for Delay Differential Equations
Nächstes Kapitel Adaptive Concretization for Parallel Program Synthesis
Fußnoten
1
This is the control case of our experiments. We do not use S-TaLiRo itself, because we would like to disregard the potential disadvantage caused by the communication between the \(\mathbf{AvSTL }\) evaluator (the additional component) and S-TaLiRo. We note that the \(\mathbf{AvSTL }\) evaluator is capable of evaluating \(\mathbf{STL }\) formulas, too.
 
2
There is no distinction between strict inequalities (\(<\)) and non-strict ones (\(\le \)). This is inevitable in the current robustness framework. This is also the case with \(\mathbf{STL }\) in [12, 13].
 
3
In the rest of Sect. 3.1, for simplicity of presentation, we assume that \([\varphi ]_{\sigma }\) is piecewise-constant. We note that the algorithm in [12] nevertheless extends to piecewise-linear \([\varphi ]_{\sigma }\).
 
Literatur
1.
2.
Abbas, H., Hoxha, B., Fainekos, G.E., Deshmukh, J.V., Kapinski, J., Ueda, K.: Conformance testing as falsification for cyber-physical systems. In: CoRR, abs/1401.5200 (2014)
3.
Abbas, H., Hoxha, B., Fainekos, G.E., Deshmukh, J.V., Kapinski, J., Ueda, K.: Wip abstract: conformance testing as falsification for cyber-physical systems. In: ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS, Berlin, Germany, April 14–17, 2014, pp. 211. IEEE Computer Society (2014)
4.
5.
Almagor, S., Boker, U., Kupferman, O.: Discounting in LTL. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 424–439. Springer, Heidelberg (2014) CrossRef
6.
7.
Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011) CrossRef
8.
Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33–47. Springer, Heidelberg (2008) CrossRef
9.
Brenguier, R., Cassez, F., Raskin, J.-F.: Energy and mean-payoff timed games. In: Fränzle, M., Lygeros, J. (eds.) Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, pp. 283–292. ACM, New York (2014)
10.
Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: 20th IEEE Symposium on Logic in Computer Science, LICS, 26–29 June 2005, Chicago, IL, USA, pp. 178–187. IEEE Computer Society (2005)
11.
Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010) CrossRef
12.
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) CrossRef
13.
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) CrossRef
14.
15.
Fainekos, G.E., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using S-TaLiRo. Am. Control Conf. (ACC) 2012, 3567–3572 (2012)MATH
16.
Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)MathSciNetCrossRefMATH
17.
Fränzle, M., Lygeros, J. (eds.) 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC 2014, Berlin, Germany, April 15–17, 2014. ACM (2014)
18.
Hoxha, B., Abbas, H., Fainekos, G.: Benchmarks for temporal logic requirements for automotive systems. In: Proceedings of Applied Verification for Continuous and Hybrid Systems (2014)
19.
Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain control verification benchmark. In: Fränzle, M., Lygeros, J. (eds.) Proceedings of the 17th international conference on Hybrid systems: computation and control, pp. 253–262. ACM, New York (2014)
20.
Jin, X., Donzé, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. In: Belta, C., Ivancic, F. (eds.) Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, HSCC 2013, pp. 43–52. ACM, New York (2013)
21.
Kong, Z., Jones, A., Ayala, A.M., Gol, E.A., Belta, C.: Temporal logic inference for classification and prediction from data. In: Fränzle, M., Lygeros, J. (eds.) Proceedings of the 17th international conference on Hybrid systems: computation and control, pp. 273–282. ACM, New York (2014)
22.
Lemire, D.: Streaming maximum-minimum filter using no more than three comparisons per element. Nord. J. Comput. 13(4), 328–339 (2006)MathSciNetMATH
23.
Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004) CrossRef
24.
Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2012, pp. 125–134. ACM, New York, NY, USA (2012)
25.
Yang, H., Hoxha, B., Fainekos, G.: Querying parametric temporal logic properties on embedded systems. In: Nielsen, B., Weise, C. (eds.) ICTSS 2012. LNCS, vol. 7641, pp. 136–151. Springer, Heidelberg (2012) CrossRef
26.
Zutshi, A., Deshmukh, J.V., Sankaranarayanan, S., Kapinski, J.: Multiple shooting, cegar-based falsification for hybrid systems. In: Proceedings of the 14th International Conference on Embedded Software, EMSOFT 2014, pp. 5:1–5:10, ACM, New York, NY, USA (2014)
Metadaten
Titel
Time Robustness in MTL and Expressivity in Hybrid System Falsification
verfasst von
Takumi Akazaki
Ichiro Hasuo
Copyright-Jahr
2015
Buch
Computer Aided Verification

Print ISBN: 978-3-319-21667-6

Electronic ISBN: 978-3-319-21668-3

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-21668-3_21

Premium Partner

    Bildnachweise