nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Practical “Paritizing” of Emerson-Lei Automata

verfasst von : Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet

Erschienen in: Automated Technology for Verification and Analysis

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an \(\omega \)-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a latest appearance record principle, and introduces a partial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step.

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 Faithful and Effective Reward Schemes for Model-Free Reinforcement Learning of Omega-Regular Objectives

Nächstes Kapitel Complexity of Verification and Synthesis of Threshold Automata

To reproduce these results, see https://www.lrde.epita.fr/~frenkin/atva20/.

Babiak, T., Badie, T., Duret-Lutz, A., Křetínský, M., Strejček, J.: Compositional approach to suspension and other improvements to LTL translation. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 81–98. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39176-7_6CrossRef

Babiak, T., et al.: The hanoi omega-automata format. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479–486. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_31CrossRef

Baier, C., Blahoudek, F., Duret-Lutz, A., Klein, J., Müller, D., Strejček, J.: Generic emptiness check for fun and profit. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 445–461. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31784-3_26CrossRefMATH

Bloem, R., Chatterjee, K., Jobstmann, B.: Graph Games and reactive synthesis. Handbook of Model Checking, pp. 921–962. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_27CrossRef

Carton, O., Maceiras, R.: Computing the Rabin index of a parity automaton. Informatique théorique et applications 33(6), 495–505 (1999)MathSciNetCrossRef

Duret-Lutz, A.: LTL translation improvements in Spot 1.0. Int. J. Critical Comput. Based Syst. 5(1/2), 31–54 (2014)

Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0 — A framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122–129. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_8CrossRef

Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8(3), 275–306 (1987)MathSciNetCrossRef

Esparza, J., Křetínský, J., Sickert, S.: One theorem to rule them all: a unified translation of LTL into \(\omega \)-automata. In: LICS 2018, pp. 384–393. ACM (2018)

10.

Farwer, B.: \(\omega \)-Automata, LNCS 2500, chap. 1, pp. 3–20. Springer, Heidelberg (2001)

11.

Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: CAV 2001, LNCS 2102, pp. 53–65. Springer, Cham (2001)

12.

Křetínský, J., Esparza, J.: Deterministic automata for the (F,G)-Fragment of LTL. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 7–22. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_7CrossRef

13.

Křetínský, J., Meggendorfer, T., Sickert, S.: Owl: a library for \(\omega \)-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 543–550. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_34CrossRef

14.

Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic \(\omega \)-automata vis-a-vis deterministic Büchi automata. In: ISAAC 1994, LNCS 834, pp. 378–386. Springer, Cham (1994)

15.

Křetínský, J., Meggendorfer, T., Waldmann, C., Weininger, M.: Index appearance record for transforming rabin automata into parity automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 443–460. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_26CrossRef

16.

Löding, C.: Methods for the transformation of \(\omega \)-automata: complexity and connection to second order logic. Diploma thesis, Institue of Computer Science and Applied Mathematics (1998)

17.

Löding, C.: Optimal bounds for transformations of automata. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds.) FSTTCS 1999. LNCS, vol. 1738, pp. 97–109. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-46691-6_8CrossRefMATH

18.

Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica, 57, 3—36 (2020). Originally published on 21 November 2019

19.

Major, J., Blahoudek, F., Strejcek, J., Sasaráková, M., Zboncáková, T.: ltl3tela: LTL to small deterministic or nondeterministic Emerson-Lei automata. In: ATVA 2019, LNCS 11781, pp. 357–365. Springer, Cham (2019)

20.

Michaud, T., Colange, M.: Reactive synthesis from LTL specification with Spot. In: SYNT 2018 (2018). http://www.lrde.epita.fr/dload/papers/michaud.18.synt.pdf

21.

Müller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: GandALF 2017, vol. 256 of EPTCS, pp. 180–194 (2017)

22.

Piterman, N.: From nondeterministic büchi and streett automata to deterministic parity automata. Logical Methods Comput. Sci. 3(3), 1057–1065 (2007)

23.

Redziejowski, R.: An improved construction of deterministic omega-automaton using derivatives. Fundamenta Informaticae 119(3–4), 393–406 (2012)MathSciNetCrossRef

24.

Safra, S., Vardi, M.Y.: On \(\omega \)-automata and temporal logic. In: STOC 1989, pp. 127–137. ACM (1989)

Titel: Practical “Paritizing” of Emerson-Lei Automata
verfasst von: Florian Renkin
Alexandre Duret-Lutz
Adrien Pommellet
Verlag: Springer International Publishing
Buch: Automated Technology for Verification and Analysis
Print ISBN: 978-3-030-59151-9

Electronic ISBN: 978-3-030-59152-6

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-59152-6_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner