Structural Model Checking for Communicating Hierarchical Machines

  • Ruggero Lanotte
  • Andrea Maggiolo-Schettini
  • Adriano Peron
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3153)


In this paper we consider the problem of model checking for well structured Communicating Hierarchical Machines (CHMs), i.e. Finite State Machines with additional features of hierarchy and concurrency. For model checking we follow the automaton theoretic approach, defining an algorithm which solves the problem of model checking without flattening the structure of CHMs.


Model Check Finite State Machine Operational Semantic Parallel Component Atomic Proposition 
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. 1.
    Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. In: Proc. 6th ACM Symp. on Found of Software Engineering, pp. 175–188 (1998)Google Scholar
  2. 2.
    Alur, R., Kannan, S., Yannakakis, M.: Communicating hierarchical state machine. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 169–178. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Alur, R., Etessami, K., Yannakakis, M.: Analysis of Recursive State Machines. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 207–220. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Booch, G., Jacobson, L., Rumbaugh, J.: Unifying Modeling Language user guide. Addison-Wesley, Boston (1997)Google Scholar
  5. 5.
    Boujjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown automata: Applications to Model Checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)Google Scholar
  6. 6.
    Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. 7.
    Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8, 231–274 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Drusinsky, D., Harel, D.: On the power of bounded concurrency I: finite automata. Journal of ACM 41(3), 517–539 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Plotkin, G.: A structural approach to operational semantics, Technical report DAIMI FN-19, University of Aarhus, Denmark (1981) Google Scholar
  10. 10.
    Wolper, P.: Cstucting automata from temporal logic formulas: A tutorial. In: Lectures on formal methods and performance analysis: first EEF/Euro Summer School on Trends in Computer Science, pp. 261–277. Springer, Heidelberg (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Ruggero Lanotte
    • 1
  • Andrea Maggiolo-Schettini
    • 2
  • Adriano Peron
    • 3
  1. 1.Dipartimento di Scienze della Cultura, Politiche e dell’InformazioneUniversità dell’InsubriaComoItaly
  2. 2.Dipartimento di InformaticaUniversità di PisaPisaItaly
  3. 3.Dipartimento di Scienze FisicheUniversità di Napoli Federico IINapoliItaly

Personalised recommendations