Skip to main content
SpringerLink
Log in
Book cover

International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z

ABZ 2018: Abstract State Machines, Alloy, B, TLA, VDM, and Z pp 204–218Cite as

Systematic Refinement of Abstract State Machines with Higher-Order Logic

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10817))

Abstract

Graph algorithms that involve complex conditions on subgraphs can be specified much easier, if the specification allows expressions in higher-order logic to be used. In this paper an extension of Abstract State Machines by such expressions is introduced and its usefulness is demonstrated by examples of computations on graphs, such as graph factoring and checking self-similarity. In a naïve way these high-level specifications can be refined using submachines for the evaluation of the higher-order expressions. We show that refinements can be obtained in an automatic way for well-defined fragments of higher-order logic that collapse to second-order, by means of which the naïve refinement is only necessary for second-order logic expressions.

The research reported in this paper was partially supported by the Austrian Science Fund (FWF) [I2420-N31] for the project: Higher-Order Logics and Structures.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    In the case of non-determinsm using the choice rule we actually obtain a set of update sets.

  2. 2.

    Note that even when the factoring of a graph is unique up to isomorphism, the third-order relation \(\mathcal {F}_I^{\mathcal {A}}\) provides one of the possible set of graphs which are factors of \((V_I^{\mathcal {A}}, E_I^{\mathcal {A}})\).

  3. 3.

    To make this subformula more understandable we chose to use a standard algebraic notation mixed with the syntax of third-order.

References

  1. Abrial, J.R.: The B-Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)

    MATH  Google Scholar 

  2. Abrial, J.R.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  Google Scholar 

  3. Abu-Khzam, F.N., Langston, M.A.: Graph coloring and the immersion order. In: Warnow, T., Zhu, B. (eds.) COCOON 2003. LNCS, vol. 2697, pp. 394–403. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-45071-8_40

    Chapter  MATH  Google Scholar 

  4. Beaudry, M., McKenzie, P.: Circuits, matrices, and nonassociative computation. In: Proceedings of the Seventh Annual Structure in Complexity Theory Conference, pp. 94–106 (1992)

    Google Scholar 

  5. Blass, A., Gurevich, Y.: Background of computation. Bull. EATCS 92, 82–114 (2007)

    MathSciNet  MATH  Google Scholar 

  6. Bollobás, B.: Modern Graph Theory. Graduate Texts in Mathematics, vol. 184. Springer, Heidelberg (2002). https://doi.org/10.1007/978-1-4612-0619-4

    Book  MATH  Google Scholar 

  7. Börger, E., Stärk, R.F.: Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-642-18216-7

    Book  MATH  Google Scholar 

  8. Dill, S., Kumar, R., Mccurley, K.S., Rajagopalan, S., Sivakumar, D., Tomkins, A.: Self-similarity in the web. ACM Trans. Internet Technol. 2(3), 205–223 (2002)

    Article  Google Scholar 

  9. Fagin, R.: Generalized first-order spectra and polynomial-time recognizable sets. In: Karp, R. (ed.) Complexity of Computations. SIAM-AMS Proceedings, vol. 7, pp. 27–41. American Mathematical Society (1974)

    Google Scholar 

  10. Ferrarotti, F., Schewe, K.D., Tec, L., Wang, Q.: A new thesis concerning synchronised parallel computing - simplified parallel ASM thesis. Theor. Comput. Sci. 649, 25–53 (2016)

    Article  MathSciNet  Google Scholar 

  11. Ferrarotti, F.: Expressibility of higher-order logics on relational databases: proper hierarchies. Ph.D. thesis, Massey University, Wellington, New Zealand (2008). http://hdl.handle.net/10179/799

  12. Ferrarotti, F., González, S., Turull-Torres, J.M.: On fragments of higher order logics that on finite structures collapse to second order. In: Kennedy, J., de Queiroz, R.J.G.B. (eds.) WoLLIC 2017. LNCS, vol. 10388, pp. 125–139. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-55386-2_9

    Chapter  Google Scholar 

  13. Ferrarotti, F., Ren, W., Turull Torres, J.M.: Expressing properties in second- and third-order logic: hypercube graphs and SATQBF. Logic J. IGPL 22(2), 355–386 (2014)

    Article  MathSciNet  Google Scholar 

  14. Grohe, M., Kawarabayashi, K., Marx, D., Wollan, P.: Finding topological subgraphs is fixed-parameter tractable. In: Proceedings of the 43rd Annual ACM Symposium on Theory of Computing (STOC 2011), pp. 479–488. ACM (2011)

    Google Scholar 

  15. Guimerà, R., Danon, L., Díaz-Guilera, A., Giralt, F., Arenas, A.: Self-similar community structure in a network of human interactions. Phys. Rev. E 68, 065103 (2003)

    Article  Google Scholar 

  16. Hella, L., Turull Torres, J.M.: Computing queries with higher-order logics. Theor. Comput. Sci. 355(2), 197–214 (2006)

    Article  MathSciNet  Google Scholar 

  17. Immerman, N.: Languages which capture complexity classes (preliminary report). In: Johnson, D.S., et al. (eds.) Proceedings of the 15th Annual ACM Symposium on Theory of Computing (STOC 1983), pp. 347–354. ACM (1983)

    Google Scholar 

  18. Immerman, N.: Descriptive Complexity. Graduate texts in computer science. Springer, Heidelberg (1999). https://doi.org/10.1007/978-1-4612-0539-5

    Book  MATH  Google Scholar 

  19. Lamport, L.: Specifying Systems, The TLA\(^+\) Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)

    Google Scholar 

  20. Leivant, D.: Higher order logic. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A., Siekmann, J.H. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming. Deduction Methodologies, vol. 2, pp. 229–322. Oxford University Press (1994)

    Google Scholar 

  21. Réka, A.: Scale-free networks in cell biology. J. Cell Sci. 118(21), 4947–4957 (2005)

    Article  Google Scholar 

  22. Schewe, K.D., Torres, J.M.T.: Fixed-point quantifiers in higher order logics. In: Kiyoki, Y., et al. (eds.) Information Modelling and Knowledge Bases XVII. Frontiers in Artificial Intelligence and Applications, vol. 136, pp. 237–244. IOS Press (2006)

    Google Scholar 

  23. Schewe, K.D., Wang, Q.: A customised ASM thesis for database transformations. Acta Cybernetica 19(4), 765–805 (2010)

    MathSciNet  MATH  Google Scholar 

  24. Schewe, K.D., Wang, Q.: XML database transformations. J. Univers. Comput. Sci. 16(20), 3043–3072 (2010)

    MATH  Google Scholar 

  25. Song, C., Havlin, S., Makse, H.A.: Self-similarity of complex networks. Nature 433, 392–395 (2005)

    Article  Google Scholar 

  26. Vardi, M.Y.: The complexity of relational query languages (extended abstract). In: Lewis, H.R., et al. (eds.) Proceedings of the 14th Annual ACM Symposium on Theory of Computing (STOC 2014), pp. 137–146. ACM (1982)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Competence Center Hagenberg, Hagenberg, Austria

    Flavio Ferrarotti & Senén González

  2. Christian-Doppler Laboratory for Client-Centric Cloud Computing, Linz, Austria

    Klaus-Dieter Schewe

  3. Universidad Nacional de La Matanza, Buenos Aires, Argentina

    José María Turull-Torres

Authors
  1. Flavio Ferrarotti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Senén González
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Klaus-Dieter Schewe
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. José María Turull-Torres
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Senén González .

Editor information

Editors and Affiliations

  1. University of Southampton, Southampton, United Kingdom

    Michael Butler

  2. Universität Ulm, Ulm, Germany

    Alexander Raschke

  3. University of Southampton, Southampton, United Kingdom

    Thai Son Hoang

  4. Thales Austria GmbH, Vienna, Austria

    Klaus Reichl

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ferrarotti, F., González, S., Schewe, KD., Turull-Torres, J.M. (2018). Systematic Refinement of Abstract State Machines with Higher-Order Logic. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science(), vol 10817. Springer, Cham. https://doi.org/10.1007/978-3-319-91271-4_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-91271-4_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-91270-7

  • Online ISBN: 978-3-319-91271-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation