Skip to main content
SpringerLink
Log in

Fully-Abstract Statecharts Semantics via Intuitionistic Kripke Models

  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1853))

Included in the following conference series:

Abstract

The semantics of Statecharts macro steps, as introduced by Pnueli and Shalev, lacks compositionality. This paper first analyzes the compositionality problem and traces it back to the invalidity of the Law of the Excluded Middle. It then characterizes the semantics via a particular class of linear, intuitionistic Kripke models, namely stabilization sequences. This yields, for the first time in the literature, a simple fully-abstract semantics which interprets Pnueli and Shalev’s concept of failure naturally. The results not only give insights into the semantic subtleties of Statecharts, but also provide a basis for developing algebraic theories for macro steps and for comparing different Statecharts variants.

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

Access this chapter

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, S. Kannan, and M. Yannakakis. Communicating hierarchical state machines. In ICALP’ 99, volume 1644 of LNCS, pages 169–178, 1999.

    Google Scholar 

  2. G. Berry. The constructive semantics of pure Esterel, 1999. Draft Version 3. Available at http://www-sop.inria.fr/meije/Personnel/Gerard.Berry.html.

  3. G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. SCP, 19(2):87–152, 1992.

    MATH  Google Scholar 

  4. M. Broy. Abstract semantics of synchronous languages: The example Esterel. Technical Report TUM-I9706, Munich Univ. of Technology, 1997.

    Google Scholar 

  5. W. Damm, B. Josko, H. Hungar, and A. Pnueli. A compositional real-time semantics of STATEMATE designs. In Compositionality: The Significant Difference, volume 1536 of LNCS, pages 186–238, 1997.

    Chapter  Google Scholar 

  6. D. Harel. Statecharts: A visual formalism for complex systems. SCP, 8:231–274, 1987.

    MATH  MathSciNet  Google Scholar 

  7. D. Harel and E. Gery. Executable object modeling with Statecharts. IEEE Computer, pages 31–42, July 1997.

    Google Scholar 

  8. D. Harel and A. Naamad. The STATEMATE semantics of Statecharts. ACM Trans. on Software Engineering, 5(4):293–333, 1996.

    Article  Google Scholar 

  9. D. Harel, A. Pnueli, J. Pruzan-Schmidt, and R. Sherman. On the formal semantics of Statecharts. In LICS’ 87, pages 54–64. IEEE Computer Society Press, 1987.

    Google Scholar 

  10. C. Huizing. Semantics of Reactive Systems: Comparison and Full Abstraction. PhD thesis, Eindhoven Univ. of Technology, 1991.

    Google Scholar 

  11. C. Huizing, R. Gerth, and W.-P. de Roever. Modeling Statecharts behavior in a fully abstract way. In CAAP’ 88, volume 299 of LNCS, pages 271–294, 1988.

    Chapter  Google Scholar 

  12. G. Lüttgen and M. Mendler. What is in a step: A fully-abstract semantics for Statecharts macro steps via intuitionistic Kripke models. Technical Report CS-00-04, Univ. of Sheffield, 2000.

    Google Scholar 

  13. G. Lüttgen, M. von der Beeck, and R. Cleaveland. Statecharts via process algebra. In CONCUR’ 99, volume 1664 of LNCS, pages 399–414, 1999.

    Google Scholar 

  14. A. Maggiolo-Schettini, A. Peron, and S. Tini. Equivalences of Statecharts. In CONCUR’ 96, volume 1119 of LNCS, pages 687–702, 1996.

    Google Scholar 

  15. F. Maraninchi. Operational and compositional semantics of synchronous automaton compositions. In CONCUR’ 92, volume 630 of LNCS, pages 550–564, 1992.

    Chapter  Google Scholar 

  16. A. Pnueli and M. Shalev. What is in a step: On the semantics of Statecharts. In TACS’ 91, volume 526 of LNCS, pages 244–264, 1991.

    Google Scholar 

  17. A.C. Uselton and S.A. Smolka. A compositional semantics for Statecharts using labeled transition systems. In CONCUR’ 94, volume 836 of LNCS, pages 2–17, 1994.

    Google Scholar 

  18. D. van Dalen. Intuitionistic logic. In Handbook of Philosophical Logic, volume III, chapter 4, pages 225–339. Reidel, 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ICASE, NASA Langley Research Center, Mail Stop 132C, Hampton, Virginia, 23681-2199, USA

    Gerald Lüttgen

  2. Department of Computer Science, Sheffield University, 211 Portobello Street, Sheffield, S1 5DP, UK

    Michael Mendler

Authors
  1. Gerald Lüttgen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Mendler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Sciences, University of Pisa, Corso Italia, 40, 56125, Pisa, Italy

    Ugo Montanari

  2. Center for Computer Sciences, University of Geneva, 24, Rue Général Dufour, 1211, Geneva 4, Switzerland

    José D. P. Rolim

  3. Department of Computer Sciences, ETH Zurich, 8092, Zurich, Switzerland

    Emo Welzl

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lüttgen, G., Mendler, M. (2000). Fully-Abstract Statecharts Semantics via Intuitionistic Kripke Models. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds) Automata, Languages and Programming. ICALP 2000. Lecture Notes in Computer Science, vol 1853. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45022-X_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-45022-X_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67715-4

  • Online ISBN: 978-3-540-45022-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation