Antichains algorithms for the inclusion problem between \(\omega\)-VPL. (English) Zbl 07777310
Sankaranarayanan, Sriram (ed.) et al., Tools and algorithms for the construction and analysis of systems. 29th international conference, TACAS 2023, held as part of the European joint conferences on theory and practice of software, ETAPS 2023, Paris, France, April 22–27, 2023. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 13993, 290-307 (2023).
Summary: We define novel algorithms for the inclusion problem between two visibly pushdown languages of infinite words, an EXPTime-complete problem. Our algorithms search for counterexamples to inclusion in the form of ultimately periodic words i.e. words of the form \(uv^{\omega}\) where \(u\) and \(v\) are finite words. They are parameterized by a pair of quasiorders telling which ultimately periodic words need not be tested as counterexamples to inclusion without compromising completeness. The pair of quasiorders enables distinct reasoning for prefixes and periods of ultimately periodic words thereby allowing to discard even more words compared to using the same quasiorder for both. We put forward two families of quasiorders: the state-based quasiorders based on automata and the syntactic quasiorders based on languages. We also implemented our algorithm and conducted an empirical evaluation on benchmarks from software verification.
For the entire collection see [Zbl 1525.68003].
For the entire collection see [Zbl 1525.68003].
MSC:
| 68Q45 | Formal languages and automata |
| 06A07 | Combinatorics of partially ordered sets |
| 68R15 | Combinatorics on words |
| 68W32 | Algorithms on strings |
References:
| [1] | Abdulla, P.A., Chen, Y.F., Clemente, L., Holík, L., Hong, C.D., Mayr, R., Vojnar, T.: Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing. In: CAV’10: Proc. 20th Int. Conf. on Computer Aided Verification. Springer (2010). doi:10.1007/978-3-642-14295-6_14 · Zbl 1343.68130 |
| [2] | Abdulla, P.A., Chen, Y.F., Clemente, L., Holík, L., Hong, C.D., Mayr, R., Vojnar, T.: Advanced Ramsey-Based Büchi Automata Inclusion Testing. In: CONCUR’11: Proc. 22nd Int. Conf. on Concurrency Theory. Springer (2011). doi:10.1007/978-3-642-23217-6_13 · Zbl 1343.68130 |
| [3] | Abdulla, P.A., Chen, Y.F., Holík, L., Mayr, R., Vojnar, T.: When Simulation Meets Antichains. In: TACAS’10: Proc. 16th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Springer (2010). doi:10.1007/978-3-642-12002-2_14 |
| [4] | Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC’04: Proc. 36th Ann. ACM Symp. on Theory of Computing. ACM (2004). doi:10.1145/1007352.1007390 |
| [5] | Bouajjani, A., Habermehl, P., Holík, L., Touili, T., Vojnar, T.: Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. In: CIAA’08: Proc. Int. Conf. on Implementation and Applications of Automata. LNCS, Springer (2008). doi:10.1007/978-3-540-70844-5_7 · Zbl 1172.68493 |
| [6] | Bruyère, V., Ducobu, M., Gauwin, O.: Visibly Pushdown Automata: Universality and Inclusion via Antichains. In: LATA’13: Proc. Int. Conf. on Language and Automata Theory and Applications. LNCS, Springer (2013). doi:10.1007/978-3-642-37064-9_18 · Zbl 1377.68104 |
| [7] | Calbrix, H., Nivat, M., Podelski, A.: Ultimately periodic words of rational \(\omega \)-languages. In: Proc. Int. Symp. on Mathematical Foundations of Programming Semantics (MFPS). LNCS, Springer (1994). doi:10.1007/3-540-58027-1_27 · Zbl 0917.20053 |
| [8] | Crespi Reghizzi, S., Mandrioli, D.: Operator precedence and the visibly pushdown property. Journal of Computer and System Sciences 78(6), 1837-1867 (2012). doi:10.1016/j.jcss.2011.12.006 · Zbl 1250.68175 |
| [9] | de Luca, A., Varricchio, S.: Well quasi-orders and regular languages. Acta Informatica 31(6), 539-557 (1994). doi:10.1007/BF01213206 · Zbl 0818.68115 |
| [10] | De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.F.: Antichains: A new algorithm for checking universality of finite automata. In: CAV’06: Proc. 16th Int. Conf. on Computer Aided Verification. Springer (2006). doi:10.1007/11817963_5 · Zbl 1188.68171 |
| [11] | Doveri, K., Ganty, P., Hadzi-Djokic, L.: omegavplinc v1.1 (Jan 2023). doi:10.5281/zenodo.7506895 |
| [12] | Doveri, K., Ganty, P., Mazzocchi, N.: FORQ-Based Language Inclusion Formal Testing. In: CAV’22: Proc. 32nd Int. Conf. on Computer Aided Verification. Springer (2022). doi:10.1007/978-3-031-13188-2_6 · Zbl 1514.68098 |
| [13] | Doveri, K., Ganty, P., Parolini, F., Ranzato, F.: Inclusion Testing of Büchi Automata Based on Well-Quasiorders. In: CONCUR’21: Proc. 32nd Int. Conf. on Concurrency Theory. LIPIcs, Schloss Dagstuhl (2021). doi:10.4230/LIPIcs.CONCUR.2021.3 · Zbl 07730605 |
| [14] | Doyen, L., Raskin, J.F.: Antichain Algorithms for Finite Automata. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS, Springer (2010) · Zbl 1284.68348 |
| [15] | Floyd, R.W.: Syntactic analysis and operator precedence. J. ACM 10(3), 316-333 (1963). doi:10.1145/321172.321179 · Zbl 0133.25504 |
| [16] | Fogarty, S., Vardi, M.Y.: Efficient Büchi Universality Checking. In: TACAS’10: Proc. 16th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, Springer (2010). doi:10.1007/978-3-642-12002-2_17 · Zbl 1258.68076 |
| [17] | Friedmann, O., Klaedtke, F., Lange, M.: Ramsey goes visibly pushdown. In: ICALP’13: Proc. 40th Int. Coll. on Automata, Languages, and Programming. LNCS, Springer (2013). doi:10.1007/978-3-642-39212-2_22 · Zbl 1334.68118 |
| [18] | Friedmann, O., Klaedtke, F., Lange, M.: Ramsey-based inclusion checking for visibly pushdown automata. ACM Transactions on Computational Logic 16(4), 1-24 (2015). doi:10.1145/2774221 · Zbl 1367.68169 |
| [19] | Ganty, P., Ranzato, F., Valero, P.: Language inclusion algorithms as complete abstract interpretations. In: Static Analysis. Springer (2019). doi:10.1007/978-3-030-32304-2_8 · Zbl 1508.68190 |
| [20] | Ganty, P., Ranzato, F., Valero, P.: Complete abstractions for checking language inclusion. ACM Trans. Comput. Logic 22(4) (2021). doi:10.1145/3462673 · Zbl 1508.68190 |
| [21] | Heizmann, M., Chen, Y., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y., Nutz, A., Musa, B., Schilling, C., Schindler, T., Podelski, A.: Ultimate automizer and the search for perfect interpolants - (competition contribution). In: TACAS’18: Proc. 24th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, Springer (2018). doi:10.1007/978-3-319-89963-3_30 |
| [22] | Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. SIGPLAN Notices 45(1), 471-482 (2010). doi:10.1145/1707801.1706353 · Zbl 1312.68059 |
| [23] | Hieronymi, P., Ma, D., Oei, R., Schaeffer, L., Schulz, C., Shallit, J.: Decidability for Sturmian Words. In: Manea, F., Simpson, A. (eds.) CSL’22: Proc. 30th EACSL Ann. Conf. on Computer Science Logic. LIPIcs, Schloss Dagstuhl (2022). doi:10.4230/LIPIcs.CSL.2022.24 · Zbl 1541.68304 |
| [24] | Meyer, R., Muskalla, S., Neumann, E.: Liveness verification and synthesis: New algorithms for recursive programs. CoRR abs/1701.02947 (2017), http://arxiv.org/abs/1701.02947 |
| [25] | Oei, R., Ma, D., Schulz, C., Hieronymi, P.: Pecan: An automated theorem prover for automatic sequences using Büchi automata (2021), https://arxiv.org/abs/2102.01727 |
| [26] | Picalausa, F., Servais, F., Zimányi, E.: Xevolve: An XML schema evolution framework. In: SAC’11: Proc. ACM Symp. on Applied Computing. p. 1645-1650. ACM (2011). doi:10.1145/1982185.1982530 |
| [27] | Rajasekaran, A., Shallit, J., Smith, T.: Additive number theory via automata theory. Theory of Computing Systems 64(3), 542-567 (2019). doi:10.1007/s00224-019-09929-9 · Zbl 1475.11040 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
