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
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 3/2016

03.12.2016

From LTL to deterministic automata

A safraless compositional approach

verfasst von: Javier Esparza, Jan Křetínský, Salomon Sickert

Erschienen in: Formal Methods in System Design | Ausgabe 3/2016

Einloggen

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

search-config
loading …

Abstract

We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula \(\varphi \). The automaton is the product of a co-Büchi automaton for \(\varphi \) and an array of Rabin automata, one for each \({\mathbf {G}}\)-subformula of \(\varphi \). The Rabin automaton for \({\mathbf {G}}\psi \) is in charge of recognizing whether \({\mathbf {F}}{\mathbf {G}}\psi \) holds. This information is passed to the co-Büchi automaton that decides on acceptance. As opposed to standard procedures based on Safra’s determinization, the states of all our automata have a clear logical structure, which allows for various optimizations. Experimental results show improvement in the sizes of the resulting automata compared to existing methods.
Vorheriger Artikel Infinite-state invariant checking with IC3 and predicate abstraction
Nächster Artikel A layered algorithm for quantifier elimination from linear modular constraints

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
Fußnoten
1
We could also speak of a product of automata, but the operational view behind the term parallel composition helps to convey the intuition.
 
2
Named in honour of Mojmír Křetínský, father of one of the authors.
 
3
For technical reasons, we also decree that the initial state cannot be a sink.
 
4
Observe that in the special case \(q_0\in F\) (all states are accepting), the first move of each token is considered succeeding.
 
5
If \(q_0\) is accepting then, by the definition of Mojmir automaton, all states reachable from \(q_0\) are accepting. This condition covers the corner case in which no transition into an accepting state is possible, because all states are accepting state.
 
6
In this case there is a merge between the token at q and the token newly created on state \(q_0\).
 
8
LTL\(_{\setminus {\mathbf {G}}{\mathbf {U}}}\) was introduced in [19] and disallows occurrences of \({\mathbf {U}}\) in the scope of \({\mathbf {G}}\).
 
Literatur
1.
Vardi MY (1999) Probabilistic linear-time model checking: an overview of the automata-theoretic approach. In: Formal methods for real-time and probabilistic systems, 5th international AMAST workshop, pp 265–276
2.
Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, pp 332–344
3.
4.
Couvreur J-M (1999) On-the-fly verification of linear temporal logic. In: World congress on formal, methods, pp 253–271
5.
6.
Gerth R, Peled D, Vardi MY, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In Proceedings of the fifteenth IFIP WG6.1 international symposium on protocol specification, testing and verification protocol specification, testing and verification XV, pp 3–18
7.
Babiak T, Křetínský M, Rehák V, Strejček J (2012) LTL to Büchi automata translation: fast and more deterministic. In: TACAS, pp 95–109
8.
Duret-Lutz A (2013) Manipulating LTL formulas using spot 1.0. In: ATVA, pp 442–445
9.
Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge, MAMATH
10.
Chatterjee K, Gaiser A, Křetínský J (2013) Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In: CAV, pp 559–575
11.
Safra S (1988) On the complexity of \(\omega \)-automata. In: FOCS. IEEE Computer Society, Los Alamitos, pp 319–327
12.
Piterman N (2006) From nondeterministic Büchi and Streett automata to deterministic parity automata. In: LICS, pp 255–264
13.
Schewe S (2009) Tighter bounds for the determinisation of Büchi automata. In: FOSSACS, pp 167–181
14.
Kwiatkowska MZ, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: CAV, pp 585–591
15.
Klein J (2005) Linear time logic and deterministic omega-automata. Master’s thesis, Rheinische Friedrich-Wilhelms Universität Bonn. The tool ltl2dstar—LTL to deterministic Streett and Rabin automata. http://​www.​ltl2dstar.​de/​
16.
Kupferman O (2012) Recent challenges and ideas in temporal synthesis. In: SOFSEM. LNCS, vol 7147. Springer, New York, pp 88–98
17.
Křetínský J, Esparza J (2012) Deterministic automata for the (F,G)-fragment of LTL. In: CAV, pp 7–22
18.
Gaiser A, Křetínský J, Esparza J (2012) Rabinizer: small deterministic automata for LTL(F,G). In: ATVA, pp 72–76
19.
Křetínský J, Ledesma-Garza R (2013) Rabinizer 2: small deterministic automata for LTL\(\setminus \)GU. In: ATVA, pp 446–450
20.
Esparza J, Křetínský J (2014) From LTL to deterministic automata: a safraless compositional approach. In: CAV, pp 192–208
21.
Daniele M, Giunchiglia F, Vardi MY (1999) Improved automata generation for linear temporal logic. In: CAV, pp 249–260
22.
Etessami K, Holzmann GJ (2000) Optimizing Büchi automata. In: CONCUR, pp 153–167
23.
Fritz C (2003) Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata. In: CIAA, pp 35–48
24.
Giannakopoulou D, Lerda F (2002) From states to transitions: improving translation of LTL formulae to Büchi automata. In: FORTE, pp 308–326
25.
Somenzi F, Bloem R (2000) Efficient Büchi automata from LTL formulae. In: CAV. LNCS, vol 1855. Springer, Heidelberg, pp 248–263
26.
Klein J, Baier C (2007) On-the-fly stuttering in the construction of deterministic \(\omega \)-automata. In: CIAA. LNCS, vol 4783. Springer, New York, pp 51–61
27.
Blahoudek F, Křetínský M, Strejček J (2013) Comparison of LTL to deterministic Rabin automata translators. In: LPAR, pp 164–172
28.
Pnueli A, Zaks A (2008) On the merits of temporal testers. In: 25 years of model checking—history, achievements, perspectives, pp 172–195
29.
Pnueli A, Rosner R (1988) A framework for the synthesis of reactive modules. In Concurrency. LNCS, vol 335. Springer, Heidelberg, pp 4–17
30.
Di Giampaolo B, Geeraerts G, Raskin J-F, Sznajder N (2010) Safraless procedures for timed specifications. In: FORMATS, pp 2–22
31.
Kupferman O, Piterman N, Vardi MY (2006) Safraless compositional synthesis. In: CAV. LNCS, vol 4144. Springer, New York, pp 31–44
32.
Kupferman O, Vardi MY (2005) Safraless decision procedures. In: FOCS. IEEE Computer Society, Los Alamitos, pp 531–542
33.
Alur R, La Torre S (2004) Deterministic generators and games for LTL fragments. ACM Trans Comput Log 5(1):1–25MathSciNetCrossRef
34.
Komárková Z, Křetínský J (2014) Rabinizer 3: safraless translation of LTL to small deterministic automata. In: ATVA, pp 235–241
35.
Babiak T, Blahoudek F, Duret-Lutz A, Klein J, Křetínský J, Müller D, Parker D, Strejček J (2015) The Hanoi omega-automata format. In: CAV, pp 479–486
36.
Babiak T, Blahoudek F, Křetínský M, Strejček J (2013) Effective translation of LTL to deterministic Rabin automata: beyond the (F, G)-fragment. In: ATVA, pp 24–39
37.
Babiak T, Badie T, Duret-Lutz A, Křetínský M, Strejček J (2013) Compositional approach to suspension and other improvements to LTL translation. In: SPIN, pp 81–98
38.
Pelánek R (2007) Beem: benchmarks for explicit model checkers. In: Proc of SPIN Workshop. LNCS, vol 4595. Springer, Heidelberg, pp 263–267
39.
Klein J, Baier C (2006) Experiments with deterministic \(\omega \)-automata for formulas of linear temporal logic. Theor Comput Sci 363(2):182–195MathSciNetCrossRefMATH
40.
Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: ICSE, pp 411–420
41.
Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL: a proof assistant for higher-order logic., Lecture notes in computer scienceSpringer, HeidelbergCrossRefMATH
42.
Esparza J, Lammich P, Neumann R, Nipkow T, Schimpf A, Smaus J-G (2013) A fully verified executable LTL model checker. In: CAV, pp 463–478
43.
44.
Wenzel M (2007) Isabelle/isar-a generic framework for human-readable proof documents. In: From insight to proof-festschrift in honour of Andrzej Trybulec, vol 10(23), pp 277–298
45.
Wenzel M (2014) The Isabelle/Isar reference manual
Metadaten
Titel
From LTL to deterministic automata
A safraless compositional approach
verfasst von
Javier Esparza
Jan Křetínský
Salomon Sickert
Publikationsdatum
03.12.2016
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 3/2016
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-016-0259-2

Premium Partner

    Bildnachweise