Operational and compositional semantics of synchronous automaton compositions

  • Florence Maraninchi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


The state/transition paradigm has been used extensively for the description of event-driven, parallel systems. However, the lack for hierarchic structure in such descriptions usually prevents us from using this paradigm in a real programming language. We propose the Argos language for reactive systems. The basic components of a program are input/output-labeled transition systems verifying reactivity (a property similar to input-enabling in IO-automata). The composition operations (parallel composition and refinement, providing hierarchy) are based upon the synchronous broadcast mechanism of Esterel. We define the language formally in an algebraic framework, and give an operational semantics. The main result is the compositionality of the semantics; we prove that the bisimulation of models induces an equivalence which is a congruence for the operators we propose. An interesting point is the way we introduce hierarchy in a compositional way.


Operational Semantic Global Behaviour Parallel Composition Reachable State Label Transition System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BG88]
    G. Berry and G. Gonthier. The ESTEREL Synchronous Programming Language: Design, Semantics, Implementation. Technical Report, 842, INRIA, 1988.Google Scholar
  2. [CHPP87]
    P. Caspi, N. Halbwachs, D. Pilaud, and J. Plaice. Lustre, a declarative language for programming synchronous systems. In 14th Symposium on Principles of Programming Languages, January 1987.Google Scholar
  3. [Fer90]
    J.C. Fernandez. An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming, 13(2–3), may 1990.Google Scholar
  4. [GBBG85]
    P. Le Guernic, A. Benveniste, P. Bournai, and T. Gauthier. Signal: A Data Flow Oriented Language for Signal Processing. Technical Report, IRISA report 246, IRISA, Rennes, France, 1985.Google Scholar
  5. [Ghe92]
    G. Gherardi. Sahara: un environnement de mise au point graphique pour les programmes Esterel (in preparation). Thesis, Université de Nice, 1992.Google Scholar
  6. [Har87]
    D. Harel. Statecharts: a visual approach to complex systems. Science of Computer Programming, 8:231–275, 1987.zbMATHMathSciNetCrossRefGoogle Scholar
  7. [HGdR88]
    C. Huizing, R. Gerth, and W.P. de Roever. Modelling statecharts behaviour in a fully abstract way. In 13th CAAP, LNCS 299, Springer Verlag, April 22–24 1988.Google Scholar
  8. [HP85]
    D. Harel and A. Pnueli. On the development of reactive systems. In Logic and Models of Concurrent Systems, NATO Advanced Study Institute on Logics and Models for Verification and Specification of Concurrent Systems, NATO ASI series F, Springer Verlag, 1985.Google Scholar
  9. [Hui91]
    C. Huizing. Semantics of reactive systems: comparison and full abstraction. thesis, Eindhoven University, 1991.Google Scholar
  10. [LT89]
    N. A. Lynch and M. R. Tuttle. An Introduction to Input/Output Automata. CWI-Quaterly 3, 1989.Google Scholar
  11. [Mar89]
    F. Maraninchi. Argonaute, graphical description, semantics and verification of reactive systems by using a process algebra. In Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, Springer Verlag, June 1989.Google Scholar
  12. [Mar91a]
    F. Maraninchi. Argos: a Graphical Synchronous Language for the Description of Reactive Systems. Spectre Report C29, LGI-IMAG, Grenoble, march 1991.Google Scholar
  13. [Mar91b]
    F. Maraninchi. The argos language: graphical representation of automata and description of reactive systems. In IEEE Workshop on Visual Languages, October 1991.Google Scholar
  14. [Mil80]
    R. Milner. A calculus of communication systems. In LNCS 92, Springer Verlag, 1980.Google Scholar
  15. [NRSV90]
    X. Nicollin, J.L. Richier, J. Sifakis, and J. Voiron. ATP: an algebra for timed processes. In IFIP Working Conference on Programming Concepts and Methods, april 1990.Google Scholar
  16. [Par81]
    D. Park. Concurrency and automata on infinite sequences. In 5th GI-Conference on Theoretical Computer Science, Springer Verlag, 1981. LNCS 104.Google Scholar
  17. [PS88]
    A. Pnueli and M. Shalev. What is in a Step. Technical Report, Dept. of Applied Mathematics and Computer Science, The Weizmann Institute of Science, Israel, may 1988.Google Scholar
  18. [SYN]
    Another look at real-time programming. IEEE proceedings, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Florence Maraninchi
    • 1
  1. 1.Laboratoire de Génie InformatiqueIMAG-CampusGrenoble CedexFrance

Personalised recommendations