nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Forward Bisimulations for Nondeterministic Symbolic Finite Automata

verfasst von : Loris D’Antoni, Margus Veanes

Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Symbolic automata allow transitions to carry predicates over rich alphabet theories, such as linear arithmetic, and therefore extend classic automata to operate over infinite alphabets, such as the set of rational numbers. Existing automata algorithms rely on the alphabet being finite, and generalizing them to the symbolic setting is not a trivial task. In our earlier work, we proposed new techniques for minimizing deterministic symbolic automata and, in this paper, we generalize these techniques and study the foundational problem of computing forward bisimulations of nondeterministic symbolic finite automata. We propose three algorithms. Our first algorithm generalizes Moore’s algorithm for minimizing deterministic automata. Our second algorithm generalizes Hopcroft’s algorithm for minimizing deterministic automata. Since the first two algorithms have quadratic complexity in the number of states and transitions in the automaton, we propose a third algorithm that only requires a number of iterations that is linearithmic in the number of states and transitions at the cost of an exponential worst-case complexity in the number of distinct predicates appearing in the automaton. We implement our algorithms and evaluate them on 3,625 nondeterministic symbolic automata from real-world applications.

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 Fair Termination for Parameterized Probabilistic Concurrent Systems

Nächstes Kapitel Up-To Techniques for Weighted Systems

Let the variable order of the BDD be the reverse bit order of the binary representation of a number, i.e., the most significant bit has the lowest ordinal, etc.

One can view one iteration of refinement from \({\mathcal {P}}_i\) to \({\mathcal {P}}_{i+1}\) as computing \(\not \sim _{i+1}\) from \(\not \sim _i\), which is often how Moore’s algorithm is presented for DFAs.

\(\varphi \Leftrightarrow \psi \) is defined as \(((\varphi \vee \lnot \psi )\wedge (\lnot \varphi \vee \psi ))\) and \(\varphi \nLeftrightarrow \psi \) stands for \(\lnot (\varphi \Leftrightarrow \psi )\).

This bound is obtained using the same amortized complexity argument used for Moore’s minimization algorithm [25].

AutomataDotNet (2015). https://github.com/AutomataDotNet/

Abdulla, P.A., Deneux, J., Kaati, L., Nilsson, M.: Minimization of non-deterministic automata with large alphabets. In: Farré, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol. 3845, pp. 31–42. Springer, Heidelberg (2006). doi:10.1007/11605157_3 CrossRef

Alur, R., D’Antoni, L., Raghothaman, M.: Drex: a declarative language for efficiently evaluating regular string transformations. SIGPLAN Not. 50(1), 125–137 (2015)CrossRefMATH

Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. Form. Methods Syst. Des. 10(2/3), 171–206 (1997)CrossRef

Berstel, J., Boasson, L., Carton, O.: Hopcroft’s automaton minimization algorithm and Sturmian words. In: DMTCS 2008, pp. 355–366 (2008)

Berstel, J., Carton, O.: On the complexity of Hopcroft’s state minimization algorithm. In: Domaratzki, M., Okhotin, A., Salomaa, K., Yu, S. (eds.) CIAA 2004. LNCS, vol. 3317, pp. 35–44. Springer, Heidelberg (2005). doi:10.1007/978-3-540-30500-2_4 CrossRef

Blum, N.: An \(0(n\log n)\) implementation of the standard method for minimizing \(n\)-state finite automata. Inf. Process. Lett. 57, 65–69 (1996)CrossRefMATH

Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372–386. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27813-9_29 CrossRef

Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)CrossRefMATH

10.

Brzozowski, J., Tamm, H.: Theory of átomata. Theoret. Comput. Sci. 539, 13–27 (2014)MathSciNetCrossRefMATH

11.

D’Antoni, L., Veanes, M.: Equivalence of extended symbolic finite transducers. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 624–639. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_41 CrossRef

12.

D’Antoni, L., Veanes, M.: Static analysis of string encoders and decoders. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 209–228. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35873-9_14 CrossRef

13.

D’Antoni, L., Veanes, M.: Minimization of symbolic automata. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL 2014), pp. 541–553. ACM (2014)

14.

D’Antoni, L., Veanes, M.: Minimization of symbolic tree automata. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. ACM (2016)

15.

D’Antoni, L., Veanes, M.: Monadic second-order logic on finite sequences. In: Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL 2017). ACM (2017)

16.

D’Antoni, L., Veanes, M., Livshits, B., Molnar, D.: Fast: a transducer-based language for tree manipulation. ACM Trans. Program. Lang. Syst. 38(1), 1–32 (2015)CrossRef

17.

Geldenhuys, J., Merwe, B., Zijl, L.: Reducing nondeterministic finite automata with SAT solvers. In: Yli-Jyrä, A., Kornai, A., Sakarovitch, J., Watson, B. (eds.) FSMNLP 2009. LNCS (LNAI), vol. 6062, pp. 81–92. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14684-8_9 CrossRef

18.

Gramlich, G., Schnitger, G.: Minimizing NFA’s and regular expressions. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, pp. 399–411. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31856-9_33 CrossRef

19.

Hopcroft, J.: An \(n\)log\(n\) algorithm for minimizing states in a finite automaton. In: Kohavi, Z. (ed.) Proceedings of International Symposium Technion, Theory of machines and computations, 1971, Haifa, pp. 189–196. Academic Press, New York (1971)

20.

Hopcroft, J.E., Ullman, J.D.: Formal Languages and Their Relation to Automata. Addison-Wesley Longman Publishing Co., Inc., Boston (1969)MATH

21.

Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison Wesley, Boston (1979)MATH

22.

Kameda, T., Weiner, P.: On the state minimization of nondeterministic finite automata. IEEE Trans. Comput. C-19(7), 617–627 (1970)

23.

Mayr, R., Clemente, L.: Advanced automata minimization. In: POPL 2013, pp. 63–74 (2013)

24.

Meyer, A.R., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential space. In: Proceedings of the 13th Annual Symposium on Switching and Automata Theory (SWAT 1972), pp. 125–129. IEEE (1972)

25.

Moore, E.F.: Gedanken-experiments on sequential machines. Autom. Stud. Ann. Math. Stud. 34, 129–153 (1956)MathSciNet

26.

Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)MathSciNetCrossRefMATH

27.

Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 417–431. Springer, Heidelberg (2011). doi:10.1007/978-3-642-21437-0_31 CrossRef

28.

Tamm, H.: New interpretation and generalization of the Kameda-Weiner method. In: Chatzigiannakis, I., Mitzenmacher, M., Rabani, Y., Sangiorgi, D. (eds.) ICALP 2016. LIPIcs, vol. 55, pp. 116:1–116:12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Wadern (2016)

29.

van Noord, G., Gerdemann, D.: Finite state transducers with predicates and identities. Grammars 4(3), 263–286 (2001)MathSciNetCrossRefMATH

30.

Veanes, M., Bjørner, N.: Symbolic automata: the toolkit. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 472–477. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28756-5_33 CrossRef

31.

Watson, B.W.: Implementing and using finite automata toolkits. In: Extended Finite State Models of Language, pp. 19–36. Cambridge University Press, New York (1999)

Titel: Forward Bisimulations for Nondeterministic Symbolic Finite Automata
verfasst von: Loris D’Antoni
Margus Veanes
Verlag: Springer Berlin Heidelberg
Buch: Tools and Algorithms for the Construction and Analysis of Systems
Print ISBN: 978-3-662-54576-8

Electronic ISBN: 978-3-662-54577-5

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-662-54577-5_30

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"