Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design
Published in: Formal Methods in System Design 3/2016

03-12-2016

From LTL to deterministic automata

A safraless compositional approach

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

Published in: Formal Methods in System Design | Issue 3/2016

Log in

Activate our intelligent search to find suitable subject content or patents.

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.
previous article Infinite-state invariant checking with IC3 and predicate abstraction
next article A layered algorithm for quantifier elimination from linear modular constraints

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Appendix
Available only for authorised users
Footnotes
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}}\).
 
Literature
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.
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
Metadata
Title
From LTL to deterministic automata
A safraless compositional approach
Authors
Javier Esparza
Jan Křetínský
Salomon Sickert
Publication date
03-12-2016
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 3/2016
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-016-0259-2

Premium Partner

    Image Credits