Abstract
We propose a lazy decision procedure for the logic WS\(k\)S. It builds a term-based symbolic representation of the state space of the tree automaton (TA) constructed by the classical WS\(k\)S decision procedure. The classical decision procedure transforms the symbolic representation into a TA via a bottom-up traversal and then tests its language non-emptiness, which corresponds to satisfiability of the formula. On the other hand, we start evaluating the representation from the top, construct the state space on the fly, and utilize opportunities to prune away parts of the state space irrelevant to the language emptiness test. In order to do so, we needed to extend the notion of language terms (denoting language derivatives) used in our previous procedure for the linear fragment of the logic (the so-called WS1S) into automata terms. We implemented our decision procedure and identified classes of formulae on which our prototype implementation is significantly faster than the classical procedure implemented in the Mona tool.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Intuitively, the operator can be seen as a generalization of the Kleene star to tree languages. The symbol is the Chinese character for a tree, pronounced mù, as in English moo-n, but shorter and with a falling tone, staccato-like.
- 2.
Note that our definition of projection differs from the usual one, which would in the example produce a single symbol \(\{Y \mapsto 0\}\) over a different alphabet (the alphabet of symbols over \(\{Y\}\)).
- 3.
The implementation is available at https://github.com/vhavlena/lazy-wsks.
- 4.
Building an optimised and overall competitive implementation is a subject of our further work. Our results with an implementation of a lazy decision procedure for WS1S from [29] suggest that this is possible.
References
Møller, A., Schwartzbach, M.: The pointer assertion logic engine. In: PLDI 2001. ACM Press (2001). Also in SIGPLAN Notices 36(5) (2001)
Glenn, J., Gasarch, W.: Implementing WS1S via finite automata. In: Raymond, D., Wood, D., Yu, S. (eds.) WIA 1996. LNCS, vol. 1260, pp. 50–63. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63174-7_5
Elgaard, J., Klarlund, N., Møller, A.: MONA 1.x: new techniques for WS1S and WS2S. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 516–520. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028773
Klarlund, N., Møller, A.: MONA Version 1.4 User Manual. BRICS, Department of Computer Science, Aarhus University, January 2001. Notes Series NS-01-1. http://www.brics.dk/mona/. Revision of BRICS NS-98-3
Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL 2011, pp. 611–622. ACM (2011)
Madhusudan, P., Qiu, X.: Efficient decision procedures for heaps using STRAND. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 43–59. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23702-7_8
Chin, W., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006–1036 (2012)
Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: POPL 2008, 349–361. ACM (2008)
Tateishi, T., Pistoia, M., Tripp, O.: Path- and index-sensitive string analysis based on monadic second-order logic. ACM Trans. Comput. Log. 22(4), 33 (2013)
Zhou, M., He, F., Wang, B., Gu, M., Sun, J.: Array theory of bounded elements and its applications. J. Autom. Reasoning 52(4), 379–405 (2014)
Baukus, K., Bensalem, S., Lakhnech, Y., Stahl, K.: Abstracting WS1S systems to verify parameterized networks. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 188–203. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46419-0_14
Bodeveix, J.-P., Filali, M.: FMona: a tool for expressing validation techniques over infinite state systems. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 204–219. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46419-0_15
Bozga, M., Iosif, R., Sifakis, J.: Structural invariants for parametric verification of systems with almost linear architectures. Technical report arXiv:1902.02696 (2019)
Klarlund, N., Nielsen, M., Sunesen, K.: A case study in verification based on trace abstractions. In: Broy, M., Merz, S., Spies, K. (eds.) Formal Systems Specification. LNCS, vol. 1169, pp. 341–373. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0024435
Smith, M.A., Klarlund, N.: Verification of a sliding window protocol using IOA and MONA. In: Bolognesi, T., Latella, D. (eds.) Formal Methods for Distributed System Development. ITIFIP, vol. 55, pp. 19–34. Springer, Boston, MA (2000). https://doi.org/10.1007/978-0-387-35533-7_2
Basin, D., Klarlund, N.: Automata based symbolic reasoning in hardware verification. In: CAV 1998. LNCS, pp. 349–361. Springer (1998)
Sandholm, A., Schwartzbach, M.I.: Distributed safety controllers for web services. In: Astesiano, E. (ed.) FASE 1998. LNCS, vol. 1382, pp. 270–284. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0053596
Hune, T., Sandholm, A.: A case study on using automata in control synthesis. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 349–362. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46428-X_24
Hamza, J., Jobstmann, B., Kuncak, V.: Synthesis for regular specifications over unbounded domains. In: FMCAD 2010, pp. 101–109. IEEE Computer Science (2010)
Morawietz, F., Cornell, T.: The MSO logic-automaton connection in linguistics. In: Lecomte, A., Lamarche, F., Perrier, G. (eds.) LACL 1997. LNCS (LNAI), vol. 1582, pp. 112–131. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48975-4_6
Wies, T., Muñiz, M., Kuncak, V.: An efficient decision procedure for imperative tree data structures. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 476–491. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_36
Doyen, L., Raskin, J.-F.: Antichain algorithms for finite automata. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 2–22. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_2
De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17–30. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_5
Bouajjani, A., Habermehl, P., Holík, L., Touili, T., Vojnar, T.: Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: Ibarra, O.H., Ravikumar, B. (eds.) CIAA 2008. LNCS, vol. 5148, pp. 57–67. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70844-5_7
Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When simulation meets antichains (on checking language inclusion of NFAs). In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158–174. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_14
Habermehl, P., Holík, L., Rogalewicz, A., Šimáček, J., Vojnar, T.: Forest automata for verification of heap manipulation. Formal Methods Syst. Des. 41(1), 83–106 (2012)
De Wulf, M., Doyen, L., Maquet, N., Raskin, J.-F.: Antichains: alternative algorithms for LTL satisfiability and model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 63–77. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_6
De Wulf, M., Doyen, L., Raskin, J.-F.: A lattice theory for solving games of imperfect information. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 153–168. Springer, Heidelberg (2006). https://doi.org/10.1007/11730637_14
Fiedor, T., Holík, L., Janků, P., Lengál, O., Vojnar, T.: Lazy automata techniques for WS1S. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 407–425. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_24
Havlena, V., Holík, L., Lengál, O., Vojnar, T.: Automata terms in a lazy WS\(k\)S decision procedure (technical report). Technical report arXiv:1905.08697 (2019)
Comon, H., et al.: Tree automata techniques and applications (2008)
Büchi, J.R.: On a decision method in restricted second-order arithmetic. In: International Congress on Logic, Methodology, and Philosophy of Science, pp. 1–11. Stanford University Press (1962)
Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1–35 (1969)
Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Math. Syst. Theory 2(1), 57–81 (1968)
Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time (preliminary report). In: Fifth Annual ACM Symposium on Theory of Computing, STOC 1973, pp. 1–9. ACM, New York (1973)
Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. Int. J. Found. Comput. Sci. 13(4), 571–586 (2002)
Klarlund, N.: A theory of restrictions for logics and automata. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 406–417. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48683-6_35
Topnik, C., Wilhelm, E., Margaria, T., Steffen, B.: jMosel: a stand-alone tool and jABC plugin for M2L(Str). In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 293–298. Springer, Heidelberg (2006). https://doi.org/10.1007/11691617_18
D’Antoni, L., Veanes, M.: Minimization of symbolic automata. In: POPL 2014, pp. 541–554 (2014)
Margaria, T., Steffen, B., Topnik, C.: Second-order value numbering. In: GraMoT 2010. Volume 30 of ECEASST, pp. 1–15. EASST (2010)
Fiedor, T., Holík, L., Lengál, O., Vojnar, T.: Nested antichains for WS1S. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 658–674. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_59
Traytel, D.: A coalgebraic decision procedure for WS1S. In: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Volume 41 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 487–503. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2015)
Ganzow, T., Kaiser, Ł.: New algorithm for weak monadic second-order logic on inductive structures. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 366–380. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15205-4_29
Acknowledgement
We thank the anonymous reviewers for their helpful comments on how to improve the exposition in this paper. This work was supported by the Czech Science Foundation project 17-12465S, the FIT BUT internal project FIT-S-17-4014, and The Ministry of Education, Youth and Sports from the National Programme of Sustainability (NPU II) project IT4Innovations excellence in science—LQ1602.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Havlena, V., Holík, L., Lengál, O., Vojnar, T. (2019). Automata Terms in a Lazy WSkS Decision Procedure. In: Fontaine, P. (eds) Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science(), vol 11716. Springer, Cham. https://doi.org/10.1007/978-3-030-29436-6_18
Download citation
DOI: https://doi.org/10.1007/978-3-030-29436-6_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-29435-9
Online ISBN: 978-3-030-29436-6
eBook Packages: Computer ScienceComputer Science (R0)