Abstract
Many model-finding tools, such as Alloy, charge users with providing bounds on the sizes of models. It would be preferable to automatically compute sufficient upper-bounds whenever possible. The Bernays-Schönfinkel-Ramsey fragment of first-order logic can relieve users of this burden in some cases: its sentences are satisfiable iff they are satisfied in a finite model, whose size is computable from the input problem.
Researchers have observed, however, that the class of sentences for which such a theorem holds is richer in a many-sorted framework—which Alloy inhabits—than in the one-sorted case. This paper studies this phenomenon in the general setting of order-sorted logic supporting overloading and empty sorts. We establish a syntactic condition generalizing the Bernays-Schönfinkel-Ramsey form that ensures the Finite Model Property. We give a linear-time algorithm for deciding this condition and a polynomial-time algorithm for computing the bound on model sizes. As a consequence, model-finding is a complete decision procedure for sentences in this class. Our work has been incorporated into Margrave, a tool for policy analysis, and applies in real-world situations.
This research is partially supported by the NSF.
An expanded version of this paper, with complete proofs, is available at http://tinyurl.com/osepl-tr-pdf
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
Preview
Unable to display preview. Download preview PDF.
References
Abadi, A., Rabinovich, A., Sagiv, M.: Decidable fragments of many-sorted logic. Journal of Symbolic Computation 45(2), 153–172 (2010)
Bernays, P., Schönfinkel, M.: Zum entscheidungsproblem der mathematischen Logik. Mathematische Annalen 99, 342–372 (1928)
Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer (1997)
Chang, C.C., Keisler, J.: Model Theory, 3rd edn. Studies in Logic and the Foundations of Mathematics, vol. 73. North-Holland (1990)
Claessen, K., Sorensson, N.: New techniques that improve MACE-style finite model finding. In: Proceedings of the CADE-19 Workshop on Model Computation (2003)
Fontaine, P., Gribomont, E.P.: Decidability of Invariant Validation for Paramaterized Systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 97–112. Springer, Heidelberg (2003)
Ge, Y., de Moura, L.: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009)
Goguen, J.A., Meseguer, J.: Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theor. Comput. Sci. 105(2), 217–273 (1992)
Harrison, J.: Exploiting sorts in expansion-based proof procedures (unpublished manuscript), http://www.cl.cam.ac.uk/~jrh13/papers/manysorted.pdf
Hooker, J., Rago, G., Chandru, V., Shrivastava, A.: Partial instantiation methods for inference in first-order logic. J. Automated Reasoning 28(4), 371–396 (2002)
Jereslow, R.G.: Computation-oriented reductions of predicate to propositional logic. Decision Support Systems 4, 183–197 (1988)
Krishnamurthi, S., Hopkins, P., McCarthy, J., Graunke, P., Pettyjohn, G., Felleisen, M.: Implementation and use of the PLT Scheme web server. Higher-Order and Symbolic Computation 20(4), 431–460 (2007)
Lahiri, S.K., Seshia, S.A.: The UCLID Decision Procedure. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 475–478. Springer, Heidelberg (2004)
Lewis, H.: Complexity results for classes of quantificational formulas. J. Comp. and Sys. Sci. 21(3), 317–353 (1980)
Momtahan, L.: Towards a small model theorem for data independent systems in Alloy. ENTCS 128(6), 37–52 (2005)
de Moura, L.M., Bjørner, N.: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 410–425. Springer, Heidelberg (2008)
Nelson, T., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: On the finite model property in order-sorted logic. Tech. rep., Worcester Polytechnic Institute (2010), http://tinyurl.com/osepl-tr-pdf
Oberschelp, A.: Order Sorted Predicate Logic. In: Bläsius, K.H., Rollinger, C.-R., Hedtstück, U. (eds.) Sorts and Types in Artificial Intelligence. LNCS, vol. 418, pp. 1–17. Springer, Heidelberg (1990)
Ramsey, F.P.: On a problem in formal logic. Proceedings of the London Mathematical Society 30, 264–286 (1930)
Torlak, E., Jackson, D.: Kodkod: A Relational Model Finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nelson, T., Dougherty, D.J., Fisler, K., Krishnamurthi, S. (2012). Toward a More Complete Alloy. In: Derrick, J., et al. Abstract State Machines, Alloy, B, VDM, and Z. ABZ 2012. Lecture Notes in Computer Science, vol 7316. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30885-7_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-30885-7_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30884-0
Online ISBN: 978-3-642-30885-7
eBook Packages: Computer ScienceComputer Science (R0)