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
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 1/2015

01.02.2015

A game approach to determinize timed automata

verfasst von: Nathalie Bertrand, Amélie Stainer, Thierry Jéron, Moez Krichen

Erschienen in: Formal Methods in System Design | Ausgabe 1/2015

Einloggen

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

search-config
loading …

Abstract

Timed automata are frequently used to model real-time systems. Their determinization is a key issue for several validation problems. However, not all timed automata can be determinized, and determinizability itself is undecidable. In this paper, we propose a game-based algorithm which, given a timed automaton, tries to produce a language-equivalent deterministic timed automaton, otherwise a deterministic over-approximation. Our method generalizes two recent contributions: the determinization procedure of  Baier et al. (Proceedings of the 36th international colloquium on automata, languages and programming (ICALP’09), 2009) and the approximation algorithm of Krichen and Tripakis (Form Methods Syst Des 34(3):238–304, 2009). Moreover, we extend it to apply to timed automata with invariants and \(\varepsilon \)-transitions, and also consider other useful approximations: under-approximation, and combination of under- and over-approximations.
Vorheriger Artikel Generating models of infinite-state communication protocols using regular inference with abstraction
Nächster Artikel Vacuity in practice: temporal antecedent failure

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 "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

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
Anhänge
Nur mit Berechtigung zugänglich
Literatur
1.
2.
Finkel O (2006) Undecidable problems about timed automata. In: Proceedings of the 4th international conference on formal modeling and analysis of timed systems (FORMATS’06) (Lecture Notes in Computer Science), vol 4202. Springer, pp. 187–199
3.
4.
Asarin E, Maler O, Pnueli A, Sifakis J (1998) Controller synthesis for timed automata. In: Proceedings of the 5th IFAC symposium on system structure and control (SSSC’98). Elsevier Science, Amsterdam, pp. 469–474
5.
Alur R, Fix L, Henzinger TA (1994) A determinizable class of timed automata. In: Proceedings of the 6th international conference on computer aided verification (CAV’94) (Lecture Notes in Computer Science), vol 818. Springer, New York, pp 1–13
6.
Vijay SP, Pandya PK, Narayanan KS, Lakshmi M (2008) Timed automata with integer resets: language inclusion and expressiveness. In: Proceedings of the 6th international conference on formal modeling and analysis of timed systems (FORMATS’08) (Lecture Notes in Computer Science), vol 5215. Springer, pp. 78–92
7.
Baier C, Bertrand N, Bouyer P, Brihaye T (2009) When are timed automata determinizable? In: Proceedings of the 36th international colloquium on automata, languages and programming (ICALP’09) (Lecture Notes in Computer Science), vol 5556. Springer, Rhodes, pp. 43–54
8.
Krichen M, Tripakis S (2009) Conformance testing for real-time systems. Form Methods Syst Des 34(3):238–304CrossRefMATH
9.
Bouyer P, Chevalier F, D’Souza D (2005) Fault diagnosis using timed automata. In: Proceedings of the 8th international conference on foundations of software science and computational structures (FOSSACS’05) (Lecture Notes in Computer Science), vol 3441. Springer, San Diego, pp. 219–233
10.
Bertrand N, Jéron T, Stainer A, Krichen M (2012) Off-line test selection with test purposes for non-deterministic timed automata. Log Methods Comput Sci 8(4:8):1
11.
Bertrand N, Stainer A, Jéron T, Krichen M (2011) A game approach to determinize timed automata. In: Proceedings of the 14th international conference on foundations of software science and computation structures (FOSSACS’11) (Lecture Notes in Computer Science), vol 6604. Springer, pp. 245–259.
12.
Grädel E, Thomas W, Wilke T (2002) (eds) Automata, logics, and infinite games: a guide to current research (Lecture Notes in Computer Science), (vol 2500). Springer, Berlin
13.
Bouyer P, Dufourd C, Fleury E, Petit A (2004) Updatable timed automata. Theor Comput Sci 321(2–3):291–345
14.
15.
Bouyer P (2004) Forward analysis of updatable timed automata. Form Methods Syst Des 24(3):281–320CrossRefMATH
16.
Bertrand N, Jéron T, Stainer A, Krichen M (2011) Off-line test selection with test purposes for non-deterministic timed automata. In: Proceedings of the 17th international conference on tools and algorithms for the construction and analysis of systems (TACAS’11) (Lecture Notes in Computer Science), vol 6605. Springer, pp. 96–111
17.
Alur R, Henzinger TA, Kupferman O, Vardi MY (1998) Alternating refinement relations. In: Proceedings of the 9th international conference on concurrency theory (CONCUR’98) (Lecture Notes in Computer Science), vol 1466. Springer, New York, pp 163–178
18.
David A, Larsen KG, Legay A, Nyman U, Wasowski A (2010) Timed i/o automata: a complete specification theory for real-time systems. In: Proceedings of the 13th ACM international conference on hybrid systems: computation and control (HSCC’10). ACM, pp. 91–100
Metadaten
Titel
A game approach to determinize timed automata
verfasst von
Nathalie Bertrand
Amélie Stainer
Thierry Jéron
Moez Krichen
Publikationsdatum
01.02.2015
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 1/2015
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-014-0220-1

Premium Partner

    Bildnachweise