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
Published in:
Validation, Synthesis and Optimization for Cyber-Physical Systems Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Minimization of Visibly Pushdown Automata Using Partial Max-SAT

Authors : Matthias Heizmann, Christian Schilling, Daniel Tischner

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

Publisher: Springer Berlin Heidelberg

Log in

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

search-config
loading …

Abstract

We consider the problem of state-space reduction for nondeterministic weakly-hierarchical visibly pushdown automata (Vpa). Vpa recognize a robust and algorithmically tractable fragment of context-free languages that is natural for modeling programs.
We define an equivalence relation that is sufficient for language-preserving quotienting of Vpa. Our definition allows to merge states that have different behavior, as long as they show the same behavior for reachable equivalent stacks. We encode the existence of such a relation as a Boolean partial maximum satisfiability (PMax-Sat) problem and present an algorithm that quickly finds satisfying assignments. These assignments are sub-optimal solutions to the PMax-Sat problem but can still lead to a significant reduction of states.
We integrated our method in the automata-based software verifier Ultimate Automizer and show performance improvements on benchmarks from the software verification competition SV-COMP.

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

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
previous chapter Index Appearance Record for Transforming Rabin Automata into Parity Automata
next chapter CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
Literature
1.
Abdulla, P.A., Chen, Y., Holík, L., Vojnar, T.: Mediating for reduction (on minimizing alternating Büchi automata). In: FSTTCS, LIPIcs, vol. 4, pp. 1–12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2009)
2.
Abel, A., Reineke, J.: MeMin: SAT-based exact minimization of incompletely specified mealy machines. In: ICCAD, pp. 94–101. IEEE (2015)
3.
4.
Alur, R., Bouajjani, A., Esparza, J.: Model checking procedural programs. In: Handbook of Model Checking. Springer, Heidelberg (2017, to appear)
5.
Alur, R., Kumar, V., Madhusudan, P., Viswanathan, M.: Congruences for visibly pushdown languages. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1102–1114. Springer, Heidelberg (2005). doi:10.​1007/​11523468_​89 CrossRef
6.
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC, pp. 202–211. ACM (2004)
7.
Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3) (2009). Article No. 16
8.
Baarir, S., Duret-Lutz, A.: Mechanizing the minimization of deterministic generalized Büchi automata. In: Ábrahám, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 266–283. Springer, Heidelberg (2014). doi:10.​1007/​978-3-662-43613-4_​17 CrossRef
9.
Baarir, S., Duret-Lutz, A.: SAT-based minimization of deterministic \(\omega \)-automata. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 79–87. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-48899-7_​6 CrossRef
10.
Beyer, D.: Reliable and reproducible competition results with BenchExec and witnesses (report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887–904. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49674-9_​55 CrossRef
11.
12.
Cha, B., Iwama, K., Kambayashi, Y., Miyazaki, S.: Local search algorithms for partial MAXSAT. In: AAAI/IAAI, pp. 263–268. AAAI Press/The MIT Press (1997)
13.
14.
15.
D’Antoni, L., Veanes, M.: Minimization of symbolic automata. In: POPL, pp. 541–554. ACM (2014)
16.
Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for language inclusion using simulation preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 255–265. Springer, Heidelberg (1992). doi:10.​1007/​3-540-55179-4_​25 CrossRef
17.
18.
Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for Büchi automata. SIAM J. Comput. 34(5), 1159–1175 (2005)MathSciNetCrossRefMATH
19.
Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252–265. Springer, Heidelberg (2006). doi:10.​1007/​11814948_​25 CrossRef
20.
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
21.
Habermehl, P., Holík, L., Rogalewicz, A., Simácek, J., Vojnar, T.: Forest automata for verification of heap manipulation. Formal Methods Syst. Des. 41(1), 83–106 (2012)CrossRefMATH
22.
23.
Heizmann, M., Dietsch, D., Greitschus, M., Leike, J., Musa, B., Schätzle, C., Podelski, A.: Ultimate automizer with two-track proofs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 950–953. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49674-9_​68 CrossRef
24.
Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: POPL, pp. 471–482. ACM (2010)
25.
Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-39799-8_​2 CrossRef
26.
Heizmann, M., Schilling, C., Tischner, D.: Minimization of visibly pushdown automata using partial Max-SAT, vol. abs/1701.05160 (2017)
27.
Holzmann, G.J., Puri, A.: A minimized automaton representation of reachable states. STTT 2(3), 270–278 (1999)CrossRefMATH
28.
Hopcroft, J.E.: An n log n algorithm for minimizing states in a finite automaton. In: Theory of Machines and Computations, pp. 189–196. Academic Press (1971)
29.
30.
Kumar, V., Madhusudan, P., Viswanathan, M.: Minimization, learning, and conformance testing of boolean programs. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 203–217. Springer, Heidelberg (2006). doi:10.​1007/​11817949_​14 CrossRef
31.
Kumar, V., Madhusudan, P., Viswanathan, M.: Visibly pushdown automata for streaming XML. In: WWW, pp. 1053–1062. ACM (2007)
32.
Mayr, R., Clemente, L.: Advanced automata minimization. In: POPL, pp. 63–74. ACM (2013)
33.
Mozafari, B., Zeng, K., Zaniolo, C.: High-performance complex event processing over XML streams. In: SIGMOD Conference, pp. 253–264. ACM (2012)
34.
Pitcher, C.: Visibly pushdown expression effects for XML stream processing. Programming Language Technologies for XML 1060, 1–14 (2005)
35.
Srba, J.: Beyond language equivalence on visibly pushdown automata. Logical Methods Comput. Sci. 5(1) (2009)
36.
Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata constructions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 396–411. Springer, Heidelberg (2005). doi:10.​1007/​11591191_​28 CrossRef
37.
Thakur, A., Lim, J., Lal, A., Burton, A., Driscoll, E., Elder, M., Andersen, T., Reps, T.: Directed proof generation for machine code. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 288–305. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-14295-6_​27 CrossRef
38.
Thomo, A., Venkatesh, S., Ye, Y.Y.: Visibly pushdown transducers for approximate validation of streaming XML. In: Hartmann, S., Kern-Isberner, G. (eds.) FoIKS 2008. LNCS, vol. 4932, pp. 219–238. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-77684-0_​16 CrossRef
Metadata
Title
Minimization of Visibly Pushdown Automata Using Partial Max-SAT
Authors
Matthias Heizmann
Christian Schilling
Daniel Tischner
Copyright Year
2017
Publisher
Springer Berlin Heidelberg
Book
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 Year: 2017

DOI
https://doi.org/10.1007/978-3-662-54577-5_27

Premium Partner

    Image Credits