Abstract
Translating formulas of Linear Temporal Logic (ltl) over finite traces, or \({\textsc {ltl}}_f\), to symbolic Deterministic Finite Automata (DFA) plays an important role not only in \({\textsc {ltl}}_f\) synthesis, but also in synthesis for Safety ltl formulas. The translation is enabled by using \(\mathsf {MONA}\), a powerful tool for symbolic, BDD-based, DFA construction from logic specifications. Recent works used a first-order encoding of \({\textsc {ltl}}_f\) formulas to translate \({\textsc {ltl}}_f\) to First Order Logic (fol), which is then fed to \(\mathsf {MONA}\) to get the symbolic DFA. This encoding was shown to perform well, but other encodings have not been studied. Specifically, the natural question of whether second-order encoding, which has significantly simpler quantificational structure, can outperform first-order encoding remained open.
In this paper we address this challenge and study second-order encodings for \({\textsc {ltl}}_f\) formulas. We first introduce a specific mso encoding that captures the semantics of \({\textsc {ltl}}_f\) in a natural way and prove its correctness. We then explore is a Compact mso encoding, which benefits from automata-theoretic minimization, thus suggesting a possible practical advantage. To that end, we propose a formalization of symbolic DFA in second-order logic, thus developing a novel connection between BDDs and mso. We then show by empirical evaluations that the first-order encoding does perform better than both second-order encodings. The conclusion is that first-order encoding is a better choice than second-order encoding in \({\textsc {ltl}}_f\)-to-Automata translation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Interactive pesentation: automatic hardware synthesis from specifications: a case study. In: DATE, pp. 1188–1193 (2007)
Bohy, A., Bruyère, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652–657. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_45
Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992)
Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: \(10^{20}\) states and beyond. Inf. Comput. 98(2), 142–170 (1992)
Chandra, A., Kozen, D., Stockmeyer, L.: Alternation. J. ACM 28(1), 114–133 (1981)
De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI, pp. 854–860 (2013)
De Giacomo, G., De Masellis, R., Montali, M.: Reasoning on LTL on finite traces: insensitivity to infiniteness. In: AAAI, pp. 1027–1033 (2014)
De Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on finite traces. In: IJCAI, pp. 1558–1564 (2015)
De Giacomo, G., Vardi, M.Y.: LTL\(_f\) and LDL\(_f\) synthesis under partial observability. In: IJCAI, pp. 1044–1050 (2016)
Di Ciccio, C., Maggi, F.M., Mendling, J.: Efficient discovery of target-branched declare constraints. Inf. Syst. 56, 258–283 (2016)
Ciccio, C.D., Mecella, M.: On the discovery of declarative control flows for artful processes. ACM Trans. Manag. Inf. Syst. 5(4), 24:1–24:37 (2015)
Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 – a framework for LTL and \(\omega \)-automata manipulation. In: ATVA, pp. 122–129 (2016)
Henriksen, J.G., et al.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89–110. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60630-0_5
Akers Jr., S.B.: Binary decision diagrams. IEEE Trans. Comput. 27(6), 509–516 (1978)
Kamp, J.: Tense logic and the theory of order. Ph.D. thesis, UCLA (1968)
Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Yu, S., Păun, A. (eds.) CIAA 2000. LNCS, vol. 2088, pp. 182–194. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44674-5_15
Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS, pp. 531–540 (2005)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291–314 (2001)
Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 196–218. Springer, Heidelberg (1985). https://doi.org/10.1007/3-540-15648-8_16
Biehl, M., Klarlund, N., Rauhe, T.: Mona: decidable arithmetic in practice. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 459–462. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61648-9_56
Pan, G., Sattler, U., Vardi, M.Y.: BDD-based decision procedures for \(\cal{K}\). In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 16–30. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45620-1_2
Pan, G., Vardi, M.Y.: Optimizing a BDD-based modal solver. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 75–89. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45085-6_7
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190 (1989)
Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57 (1977)
Prescher, J., Di Ciccio, C., Mendling, J.: From declarative processes to imperative models. In: SIMPDA 2014, pp. 162–173 (2014)
Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149–167. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73370-6_11
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). https://doi.org/10.1007/978-3-642-21437-0_31
Rozier, K.Y., Vardi, M.Y.: Deterministic compilation of temporal safety properties in explicit state model checking. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 243–259. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39611-3_23
Tabakov, D., Rozier, K.Y., Vardi, M.Y.: Optimized temporal monitors for SystemC. Formal Methods Syst. Des. 41(3), 236–268 (2012)
Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A symbolic approach to safety ltl synthesis. Hardware and Software: Verification and Testing. LNCS, vol. 10629, pp. 147–162. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70389-3_10
Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: Symbolic LTL\(_f\) synthesis. In: IJCAI, pp. 1362–1369 (2017)
Acknowledgments
Work supported in part by China HGJ Project No. 2017ZX01038102-002, NSFC Projects No. 61572197, No. 61632005 and No. 61532019, NSF grants IIS-1527668, IIS-1830549, and by NSF Expeditions in Computing project “ExCAPE: Expeditions in Computer Augmented Program Engineering”. Special thanks to Jeffrey M. Dudek and Dror Fried for useful discussions.
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
Zhu, S., Pu, G., Vardi, M.Y. (2019). First-Order vs. Second-Order Encodings for \(\textsc {ltl}_f\)-to-Automata Translation. In: Gopal, T., Watada, J. (eds) Theory and Applications of Models of Computation. TAMC 2019. Lecture Notes in Computer Science(), vol 11436. Springer, Cham. https://doi.org/10.1007/978-3-030-14812-6_43
Download citation
DOI: https://doi.org/10.1007/978-3-030-14812-6_43
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-14811-9
Online ISBN: 978-3-030-14812-6
eBook Packages: Computer ScienceComputer Science (R0)