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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2016 | OriginalPaper | Buchkapitel

SMT-Based Parameter Synthesis for Parametric Timed Automata

verfasst von : Michał Knapik, Wojciech Penczek

Erschienen in: Challenging Problems and Solutions in Intelligent Systems

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We present a simple method for representing finite executions of Parametric Timed Automata using Satisfiability Modulo Theories (SMT). The transition relation of an automaton is translated to a formula of SMT, which is used to represent all the prefixes of a given length of all the executions. This enables to underapproximate the set of parameter valuations for the undecidable problem of parametric reachability. We introduce a freely available, open-source tool PTA2SMT and show its application to the synthesis of parameter valuations under which a timed mutual exclusion protocol fails.

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
Nächstes Kapitel On the Identification of -Asynchronous Cellular Automata in the Case of Partial Observations with Spatially Separated Gaps
Fußnoten
1
We can always relabel the labels.
 
Literatur
1.
Alur, R., Henzinger, T., Vardi, M.: Parametric real-time reasoning. In: Proceedings of the 25th Annual Symposium on Theory of Computing, pp. 592–601. ACM (1993)
2.
André, É., Chatain, T., Fribourg, L., Encrenaz, E.: An inverse method for parametric timed automata. Int. J. Found. Comput. Sci. 20(5), 819–836 (2009)MathSciNetCrossRefMATH
3.
Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. Technical report. Department of Computer Science, The University of Iowa, available at www.​SMT-LIB.​org (2010)
4.
Barrett, C., Tinelli, C.: CVC3. In: Proceedings of the 19th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 4590, pp. 298–302. Springer, Berlin (2007)
5.
6.
de Moura, L.M., Bjørner, N.: Satisfiability modulo theories: an appetizer. Formal Methods: Foundations and Applications. In: 12th Brazilian Symposium on Formal Methods, (SBMF), Revised Selected Papers. Lecture Notes in Computer Science, vol. 5902, pp. 23–36. Springer (2009)
7.
Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52–53, 183–220 (2002)MathSciNetCrossRefMATH
8.
Jovanovic, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 7795, pp. 401–415. Springer (2013)
9.
10.
Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. Trans. Petri Nets Models Concurr. 5, 141–159 (2012)CrossRefMATH
11.
Knapik, M., Penczek, W.: SMT-based parameter synthesis for L/U automata. In: Proceedings of the International Workshop on Petri Nets and Software Engineering, vol. 851, pp. 77–92. CEUR, Hamburg, 25–26 June 2012
12.
13.
Knapik, M., Penczek, W., Szreter, M., Pólrola, A.: Bounded parametric verification for distributed time petri nets with discrete-time semantics. Fundam. Inform. 101(1–2), 9–27 (2010)MathSciNetMATH
14.
Knapik, M., Szreter, M., Penczek, W.: Bounded parametric model checking for elementary net systems. Trans. Petri Nets Models Concurr. 4, 42–71 (2010)MATH
15.
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997)CrossRefMATH
16.
Penczek, W., Pólrola, A., Zbrzezny, A.: SAT-based (parametric) reachability for a class of distributed time petri nets. Trans. Petri Nets Models Concurr. 4, 72–97 (2010)MATH
17.
Penczek, W., Szreter, M.: SAT-based unbounded model checking of timed automata. Fundam. Inform. 85(1–4), 425–440 (2008)MathSciNetMATH
18.
Spelberg, R.F.L., Toetenel, W.J.: Splitting trees and partition refinement in real-time model checking. In: 35th Hawaii International Conference on System Sciences (HICSS-35 2002), CD-ROM/Abstracts Proceedings, Big Island, HI, USA. p. 278, IEEE Computer Society, 7–10 January 2002. http://​dx.​doi.​org/​10.​1109/​HICSS.​2002.​994478
19.
Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Form. Methods Syst. Design 18(1), 25–68 (2001)CrossRefMATH
20.
Wang, F.: Parametric analysis of computer systems. Form. Methods Syst. Design 17(1), 39–60 (2000)CrossRef
21.
Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundam. Inform. 67(1–3), 303–322 (2005)MathSciNetMATH
Metadaten
Titel
SMT-Based Parameter Synthesis for Parametric Timed Automata
verfasst von
Michał Knapik
Wojciech Penczek
Copyright-Jahr
2016
Buch
Challenging Problems and Solutions in Intelligent Systems

Print ISBN: 978-3-319-30164-8

Electronic ISBN: 978-3-319-30165-5

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-30165-5_1